Email Gateway (Aug 18 2022 at 15:22): Email Gateway (Aug 18 2022 at 15:22):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I have to prove the following lemma:
lemma "[| a <= sup b c; e <= sup d a |] ==> e <= sup (sup d b)
(c::'a::upper_semilattice)"
auto, force,blast,fast, etc cannot prove this automatically.
Is there any way to prove this automatically, or to feed the right
lemmas to auto?
Best,
Peter
Email Gateway (Aug 18 2022 at 15:22):From: Tobias Nipkow <nipkow@in.tum.de>
This is what sledgehammer (with the help of Spass and minimization)
gives me quite quickly:
by (metis le_sup_iff order_trans_rules(23) sup_ge1 sup_ge2).
Tobias
Peter Lammich wrote:
Email Gateway (Aug 18 2022 at 15:22):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi
Tobias Nipkow schrieb:
This is what sledgehammer (with the help of Spass and minimization)
gives me quite quickly:by (metis le_sup_iff order_trans_rules(23) sup_ge1 sup_ge2).
I also got something similar by sledge-hammering and minimization using
Spass.
However, I interrupted the metis-prover after approx 3 minutes, b/c it
did not terminate. (I'm using Isabelle2009-1)
For your proposal, metis also did not yet terminate within 5 minutes ...
Best and thanks,
Peter
Tobias
Peter Lammich wrote:
Hi all,
I have to prove the following lemma:
lemma "[| a <= sup b c; e <= sup d a |] ==> e <= sup (sup d b)
(c::'a::upper_semilattice)"auto, force,blast,fast, etc cannot prove this automatically.
Is there any way to prove this automatically, or to feed the right
lemmas to auto?Best,
Peter
Email Gateway (Aug 18 2022 at 15:22):From: Tobias Nipkow <nipkow@in.tum.de>
Unfortunately you are right. I thought I had tried the metis call, but
had not. :-(
Tobias
Peter Lammich wrote:
Email Gateway (Aug 18 2022 at 15:22):From: Lawrence Paulson <lp15@cam.ac.uk>
apply (metis ge_sup_conv le_iff_sup sup_absorb1 sup_assoc sup_commute sup_ge1)
Larry
Email Gateway (Aug 18 2022 at 15:23):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Peter,
Using the lattest repository version of Isabelle, I invoked Sledgehammer with the "[isar_proof, isar_shrink_factor = 2]" options and got the following structured proof, which is quite fast to process:
proof -
assume A1: "a \<le> sup b c"
assume "e \<le> sup d a"
hence F1: "\<forall>u\<ge>sup d a. e \<le> u" by (metis xtrans(6))
have F2: "\<forall>u. a \<le> sup (sup b c) u" by (metis A1 sup_ge1 xtrans(6))
have "\<forall>u. a \<le> u \<and> d \<le> u \<longrightarrow> e \<le> u" by (metis F1 le_supI semilattice_sup_class.sup.commute)
hence "e \<le> sup b (sup c d)" by (metis F2 le_supE semilattice_sup_class.sup.assoc sup_ge2)
hence "e \<le> sup c (sup b d)" by (metis semilattice_sup_class.sup.left_commute)
thus "e \<le> sup (sup d b) c" by (metis semilattice_sup_class.sup.commute)
qed
The names of some of the theorems have changed in the meantime. Some of the steps could be simplified.
Jasmin
P.S. Tobias: On my machine "isar_proof" works perfectly well. I'll try to reproduce your problems on a Linux machine.
Email Gateway (Aug 18 2022 at 15:23):From: Brian Huffman <brianh@cs.pdx.edu>
Here's a proof using "fast" that works quickly:
by (fast elim: order_trans intro: le_supI1 le_supI2 sup_least)
By the way, what is up with sledgehammer returning theorem names like
"order_trans_rules(23)"? Shouldn't it prefer names of individual
theorems like "order_trans" instead?
Last updated: Apr 26 2024 at 20:16 UTC