# 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,
>
> 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.