Email Gateway (Aug 22 2022 at 13:03): Email Gateway (Aug 22 2022 at 13:03):From: michel levy <michel.levy@imag.fr>
I tried the example (suggested in the User's Guide to Sledgehammer)
theory Scratch
imports Main
begin
lemma "[a] = [b] ⟶ a = b"
I apply sledgehammer (with the button sledgehammer clicked) with
provers cvc4 remote_vampire z3 spass e
and the button Isar proofs clicked
I have in the output window
"cvc4": Try this: by (metis list.inject ) (28 ms ms) .
Warning : Isar proof construction failed.
"z3" : Try this: by auto (0.0 ms).
(No Isar proof available.)
"spass" : Try this : by (metis list.inject) (16 ms)
(No Isar proof available.)
"remote_vampire : Try this : by (metis list.inject) (8 ms)
(No Isar proof available.)
"e" : Try this: by (metis the_elem_set) (12 ms).
(No Isar proof available.)
What that means ? Is the lemma proved ?
Why there is no Isar proof available ?
-- email : michel.levy@imag.fr
http://membres-liglab.imag.fr/michel.levy
Email Gateway (Aug 22 2022 at 13:03):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Michel,
I apply sledgehammer (with the button sledgehammer clicked) with
provers cvc4 remote_vampire z3 spass e
and the button Isar proofs clickedI have in the output window
"cvc4": Try this: by (metis list.inject ) (28 ms ms) .
Warning : Isar proof construction failed.
"z3" : Try this: by auto (0.0 ms).
(No Isar proof available.)
"spass" : Try this : by (metis list.inject) (16 ms)
(No Isar proof available.)
"remote_vampire : Try this : by (metis list.inject) (8 ms)
(No Isar proof available.)
"e" : Try this: by (metis the_elem_set) (12 ms).
(No Isar proof available.)What that means ? Is the lemma proved ?
The calls such as "by (metis list.inject)" are snippets you can click on and insert in your theory.
Why there is no Isar proof available ?
Multi-line Isar proofs are generated only if the provers provide a multi-line proof in the first place. Here, the property is so simple that there is no such proof, only a one-line proof.
Cheers,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC