Tutorial outdated at 4.1

[Hibou57]

The tutorial says DEVIDES_ADD and DEVIDES_SUB can be proved by Metis, but it stops after timeout (I waited long). I guess it was OK before but not anymore (proof assistants automation is a lot sensible to updates, I noticed).

This, instead, works fine to prove both lemmas:

g `!d a b. d divides a /\ d divides b ==> d divides (a+b)`;
e (rw[divides_def]);
e (qexists_tac `q + q'`);
e (rw[]);
val DIVIDES_ADD = top_thm();
drop();

g `!d a b. d divides a /\ d divides b ==> d divides (a-b)`;
e (rw[divides_def]);
e (qexists_tac `q - q'`);
e (rw[]);
val DIVIDES_SUB = top_thm();
drop();

(P.S. hope this time I will really have enough time to learn HOL :-p )

[mn200]

Your proofs are fine, but I can't reproduce the failure in the metis_tac versions that you're seeing. I've just added further checks to make sure that the proofs do work. Note you also can try

   bin/hol < examples/euclid.sml

(in the root HOL directory) to also check that the script from the Tutorial is working.

[mn200]

In fact, the current repository version of HOL already checks these proofs when it builds the Tutorial, so I don't have a commit to add to what's already there.

[Hibou57]

@mn200 , the version just says “HOL-4 [Kananaskis 12 (stdknl, built Sat Mar 30 18:58:17 2019)]”. It was built from the ZIP archive.

[mn200]

Thanks for the report, but I will close this without further work as the issue isn't apparent on master and that will soon (!) turn into a K-13 release.