Email Gateway (Aug 22 2022 at 18:23): Email Gateway (Aug 22 2022 at 18:23):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Is there a one-line proof of the equation? The following is the shortest
one I can find. I am surprised that arith does not solve it directly.
More generally, how do I tell Isabelle just keep normalizing and then apply
reflexivity, like how refl works in Coq?
Thanks!
lemma test: "foo 2 = foo (Suc (Suc 0))"
proof -
have "2 = Suc (Suc 0)" by arith
then show ?thesis by arith
qed
Email Gateway (Aug 22 2022 at 18:24):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
One-line proof:
lemma test: "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat by (rule refl)
Regards, Jørgen
Email Gateway (Aug 22 2022 at 18:24):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Thanks!
How about "foo (Suc (Suc n)) = foo (n + 2)"?
Email Gateway (Aug 22 2022 at 18:24):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
I am no expert on the matter but here is a suggestion:
lemma "foo (Suc (Suc n)) = foo (n + 2)"
by (simp add: eval_nat_numeral)
Regards, Jørgen
PS - Shorter proofs of your first lemma:
lemma "foo 2 = foo (Suc (Suc 0))"
using numeral_nat by metis
lemma "foo 2 = foo (Suc (Suc 0))"
using numeral_2_eq_2 by argo
lemma "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat using refl .
Email Gateway (Aug 22 2022 at 18:24):From: Jørgen Villadsen <jovi@dtu.dk>
Actually just "by simp" but "by (simp add: eval_nat_numeral)" works on you first lemma too... :-)
Jørgen
Email Gateway (Aug 22 2022 at 18:24):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Thanks!
Where are these tricks documented?
Email Gateway (Aug 22 2022 at 18:24):From: Tobias Nipkow <nipkow@in.tum.de>
On 04/09/2018 01:00, Jørgen Villadsen wrote:
Actually just "by simp" but "by (simp add: eval_nat_numeral)" works on you first lemma too... :-)
That is what I do. There is also numeral_eq_Suc, which may be a bit easier to
remember than eval_nat_numeral. In fact, the latter one may disappear at some point.
Tobias
Jørgen
From: Jørgen Villadsen
Sent: 4. september 2018 00:55
To: 'Ching-Tsun Chou'; cl-isabelle-users@lists.cam.ac.uk
Subject: RE: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?Hi,
I am no expert on the matter but here is a suggestion:
lemma "foo (Suc (Suc n)) = foo (n + 2)"
by (simp add: eval_nat_numeral)Regards, Jørgen
PS - Shorter proofs of your first lemma:
lemma "foo 2 = foo (Suc (Suc 0))"
using numeral_nat by metislemma "foo 2 = foo (Suc (Suc 0))"
using numeral_2_eq_2 by argolemma "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat using refl .From: Ching-Tsun Chou [mailto:chingtsun.chou@gmail.com]
Sent: 4. september 2018 00:45
To: Jørgen Villadsen
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?Thanks!
How about "foo (Suc (Suc n)) = foo (n + 2)"?
- Ching Tsun
On Mon, Sep 3, 2018 at 3:08 PM Jørgen Villadsen <jovi@dtu.dk<mailto:jovi@dtu.dk>> wrote:
Hi,One-line proof:
lemma test: "foo 2 = foo (Suc (Suc 0))"
unfolding numeral_nat by (rule refl)Regards, Jørgen
-----Original Message-----
From: cl-isabelle-users-bounces@lists.cam.ac.uk<mailto:cl-isabelle-users-bounces@lists.cam.ac.uk> [mailto:cl-isabelle-users-bounces@lists.cam.ac.uk<mailto:cl-isabelle-users-bounces@lists.cam.ac.uk>] On Behalf Of Ching-Tsun Chou
Sent: 3. september 2018 23:34
To: cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] How do I prove "foo 2 = foo (Suc (Suc 0))"?Is there a one-line proof of the equation? The following is the shortest
one I can find. I am surprised that arith does not solve it directly.More generally, how do I tell Isabelle just keep normalizing and then apply
reflexivity, like how refl works in Coq?Thanks!
- Ching Tsunlemma test: "foo 2 = foo (Suc (Suc 0))"
proof -
have "2 = Suc (Suc 0)" by arith
then show ?thesis by arith
qed
Last updated: Apr 26 2024 at 20:16 UTC