Re: [isabelle] Isabelle2021-1-RC3. Odd sledgehammer proof reconstruction



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
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.