*To*: Makarius <makarius at sketis.net>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle2021-1-RC3. Odd sledgehammer proof reconstruction*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sun, 14 Nov 2021 00:32:31 +0100*Authentication-results*: cam.ac.uk; iprev=pass (mail-out1.in.tum.de) smtp.remote-ip=131.159.0.8; spf=pass smtp.mailfrom=in.tum.de; arc=none*In-reply-to*: <330d3f77-3d4a-fef9-7dec-1fcce14e2e03@sketis.net>*References*: <330d3f77-3d4a-fef9-7dec-1fcce14e2e03@sketis.net>*User-agent*: Evolution 3.36.5-0ubuntu1

Hi all, Isar-proof reconstruction from sledgehammer proposes a vacuous proof (that, obviously, doesn't not work). Example below. Posting it here, as this is the first time that I see such a 'proof' proposed by sledgehammer, so maybe 2021-1 regression. -- Peter sledgehammering the following goal: have H: ‹nat (bi) < LENGTH('a :: len2) ⟹ nat (uint (ai :: 'a word) * 2 ^ nat (bi)) < max_unat LENGTH('a) ⟹ nat (bintrunc (size ai) (uint ai << nat (bi))) = nat (uint ai * 2 ^ nat (bi))› for bi ai I got the following output (the last Isar 'proof', that apparently takes 0.0ms to check, is particularly interesting) Sledgehammering... Proof found... "verit": Prover error: Solver "verit" failed -- enable tracing using the "smt_trace" option for details "e": Try this: by (metis max_unat_def nat_less_numeral_power_cancel_iff push_bit_eq_mult shiftl_def uint_mult_lem uint_power_lower uint_word_arith_bintrs(3) word_size) (1.1 s) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) "cvc4": Prover error: Solver "cvc4" failed -- enable tracing using the "smt_trace" option for details "z3": Try this: by (smt (z3) max_unat_def mult.commute nat_mult_distrib nat_uint_eq push_bit_eq_mult shiftl_def size_word.rep_eq uint_power_lower uint_word_arith_bintrs(3) unat_mult_lem zero_le_power) (78 ms) "spass": Try this: by (metis max_unat_def nat_less_numeral_power_cancel_iff push_bit_eq_mult shiftl_def uint_mult_lem uint_power_lower uint_word_arith_bintrs(3) word_size) (1.2 s) "vampire": Try this: by (metis max_unat_def nat_eq_numeral_power_cancel_iff push_bit_eq_mult shiftl_def uint_mult_lem uint_power_lower uint_word_arith_bintrs(3) word_size zless_nat_conj) (> 1.0 s, timed out) Isar proof (0.0 ms): proof - assume "nat (uint ai * 2 ^ nat bi) < max_unat (len_of (TYPE('a)::'a itself))" assume "nat bi < len_of (TYPE('a)::'a itself)" qed On Fri, 2021-11-12 at 21:26 +0100, Makarius wrote: > Dear Isabelle users, > > please see https://isabelle.sketis.net/website-Isabelle2021-1-RC3 and > https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1 > for further progress on the release process. > > There is now a proper download for Linux (ARM), and the "isabelle > build_docker" tools works for it (relevant on Apple M1 hardware). > > This is also the fork-point of the isabelle-dev repository, which > continues > for the time after this release: > https://isabelle.sketis.net/repos/isabelle/rev/4f1c1c7eb95f > > > Reminder: Any feedback about release candidates should be posted with > a meaningful > Subject (not just a clone of the announcement). > > We have approx. 4 weeks left until final lift-off: afterwards there > will be no > more changes on this line. > > > Makarius >

**References**:**[isabelle] Isabelle2021-1-RC3 available for testing***From:*Makarius

- Previous by Date: Re: [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ARM64
- Next by Date: Re: [isabelle] conversions for symmetric/commutative operators
- Previous by Thread: Re: [isabelle] Isabelle2021-1-RC3: Isabelle/VSCode extension
- Next by Thread: Re: [isabelle] Isabelle2021-1-RC3: HELP! Bad context exception
- Cl-isabelle-users November 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list