Email Gateway (Aug 22 2022 at 12:45): Email Gateway (Aug 22 2022 at 12:45):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
following
http://stackoverflow.com/questions/35156803/sledgehammer-gives-insufficient-proof-tactic
I created
theory Even
imports Main
begin
inductive
structural_even :: "nat ⇒ bool"
where
"structural_even 0"
| "structural_even n ⟹ structural_even (Suc(Suc n))"
fun
computational_even :: "nat ⇒ bool"
where
"computational_even 0 = True"
| "computational_even (Suc 0) = False"
| "computational_even (Suc(Suc n)) = computational_even n"
lemma "computational_even n ⟹ structural_even n"
proof (induct n rule: computational_even.induct)
show "computational_even 0 ⟹ structural_even 0"
by (metis structural_even.intros(1))
next
show "computational_even (Suc 0) ⟹ structural_even (Suc 0)"
by (metis computational_even.simps(2))
next
show "⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))"
proof
fix n
assume "computational_even n ⟹ structural_even n"
from this show "computational_even (Suc (Suc n)) ⟹ structural_even n"
by (simp only: computational_even.simps(3))
qed
qed
end
Email Gateway (Aug 22 2022 at 12:45):From: Lars Hupel <hupel@in.tum.de>
Hi Gergely,
Is it standard practice not to bother these but postpone solving them via the final qed?
I'd say it's not standard practice. Most Isabelle users prefer not using
meta-implications and meta-quantification in Isar proofs if it can be
avoided. See Lars Noschinski's answer here for a case where it actually
doesn't work if you use meta-implication:
<https://stackoverflow.com/a/25442787/4776939>
Isabelle2016 has changed some things with that respect. For example, you
can now write
fix P
assume "P x" for x
instead of
fix P
assume "⋀x. P x"
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:46):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Lars,
Thanks. Re-formulating my goal I wrote
lemma
fixes n :: "nat"
assumes "computational_even n"
shows "structural_even n"
proof (induct n rule:computational_even.induct)
which results in
goal (3 subgoals):
where the 2nd subgoal is simply not true.
What is wrong with that lemma expression?
Email Gateway (Aug 22 2022 at 12:46):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Mittwoch, den 03.02.2016, 11:50 +0100 schrieb Buday Gergely:
Hi Lars,
Is it standard practice not to bother these but postpone solving
them via
the final qed?I'd say it's not standard practice. Most Isabelle users prefer not
using meta-
implications and meta-quantification in Isar proofs if it can be
avoided. See
Lars Noschinski's answer here for a case where it actually doesn't
work if you
use meta-implication:Thanks. Re-formulating my goal I wrote
lemma
fixes n :: "nat"
assumes "computational_even n"
shows "structural_even n"
proof (induct n rule:computational_even.induct)
You need to add the assumption with "using":
assumes "computational_even n"
shows "structural_even n"
using assms
proof (induct n rule:computational_even.induct)
Then your 2. goal should state:
computational_even (Suc 0) ==> structural_even (Suc 0)
Which is true as "computational_even (Suc 0) = False"
which results in
goal (3 subgoals):
1. structural_even 0
2. structural_even (Suc 0)
3. ⋀n. structural_even n ⟹ structural_even (Suc (Suc n))where the 2nd subgoal is simply not true.
What is wrong with that lemma expression?
- Gergely
Email Gateway (Aug 22 2022 at 12:46):From: Manuel Eberl <eberlm@in.tum.de>
You are not using your assumption at all, so effectively, you're trying
to show that /every/ number n is structurally even, which is, of course,
false.
Chain in the assumption by putting a "using assms" in front of your
"proof". Then you will have the additional assumption
"computational_even (Suc 0)" in the second case, and that should be
false, which means the second case is trivially provable.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:46):From: Tobias Nipkow <nipkow@in.tum.de>
You need not modify the lemma statement and "proof" line at all. Induction is
very happy with implicational goals.
Tobias
smime.p7s
Last updated: Apr 19 2024 at 12:27 UTC