Email Gateway (Aug 19 2022 at 13:21): Email Gateway (Aug 19 2022 at 13:21):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I have the following two lemmas:
lemma "(2 + (Suc n)) = (3 + n)"
by simp
lemma "f (2 + (Suc n)) = f (3 + n)"
by simp
The first one is proved by simp, but the proof on the
second lemma fails. How can I simplify numerical
constants in context?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 13:21):From: Johannes Hölzl <hoelzl@in.tum.de>
You can use numeral_eq_Suc to rewrite numerals into "Suc"s,
e.g. 3 into Suc (Suc (Suc 0)).
Email Gateway (Aug 19 2022 at 13:22):From: Christian Sternagel <c.sternagel@gmail.com>
I would have suggested
lemma "f (2 + (Suc n)) = f (3 + n)"
by (rule arg_cong) simp
which works (thanks to backtracking?). Unfortunately, if you write the
same as
lemma "f (2 + (Suc n)) = f (3 + n)"
apply (rule arg_cong)
apply (simp)
done
in order to see the intermediate results, the prove fails, since "apply
(rule arg_cong)" does not change the goal. Is this intended? Is "rule"
allowed to leave a goal unchanged? (Btw: a little instantiation helps,
e.g., "apply (rule arg_cong [of _ _ f])").
cheers
chris
Email Gateway (Aug 19 2022 at 13:22):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Chris,
My context is more complicated than f … = f …
I need to instantiate an assumption (forall n . …) with n, 1+n, 2+n, …, 10+n
and among other things I get
f (y (1 + n)) = 1 + f (y n) + 1
f (y (2 + n)) = 1 + f (y (1 + n)) + 1
…
I need to get all these simplified to
f (y (10 + n)) = f (y n) + 10 and ultimately prove f (y (10 + n)) >= 10 knowing
that f (y n) >= 0.
The problem occurred when using 3 + n which was not simplified anymore
to Suc … . At first it seemed impossible to go forward, but then I remembered
sledgehammer, and I used it. It suggested the lemma Suc3_eq_add_3.
Using this lemma at the step (3+n), I could go forward. There were still
some problems because I mixed (… + n) and (n + …), but then they
were solved when changing everything to (… + n).
Best regards,
Viorel
Email Gateway (Aug 19 2022 at 13:22):From: Christian Sternagel <c.sternagel@gmail.com>
On 01/28/2014 10:45 AM, Viorel Preoteasa wrote:
Hi Chris,
My context is more complicated than f … = f …
I need to instantiate an assumption (forall n . …) with n, 1+n, 2+n, …, 10+n
and among other things I get
f (y (1 + n)) = 1 + f (y n) + 1
f (y (2 + n)) = 1 + f (y (1 + n)) + 1
…
I need to get all these simplified to
f (y (10 + n)) = f (y n) + 10 and ultimately prove f (y (10 + n)) >= 10 knowing
that f (y n) >= 0.
I see.
The problem occurred when using 3 + n which was not simplified anymore
to Suc … . At first it seemed impossible to go forward, but then I remembered
sledgehammer, and I used it. It suggested the lemma Suc3_eq_add_3.
Using this lemma at the step (3+n), I could go forward. There were still
some problems because I mixed (… + n) and (n + …), but then they
were solved when changing everything to (… + n).
For this case (i.e., commutativity) it might help to add "ac_simps" to
the "simp" or "auto".
cheers
chris
Best regards,
Viorel
On 28 Jan 2014, at 11:28, Christian Sternagel <c.sternagel@gmail.com> wrote:
I would have suggested
lemma "f (2 + (Suc n)) = f (3 + n)"
by (rule arg_cong) simpwhich works (thanks to backtracking?). Unfortunately, if you write the same as
lemma "f (2 + (Suc n)) = f (3 + n)"
apply (rule arg_cong)
apply (simp)
donein order to see the intermediate results, the prove fails, since "apply (rule arg_cong)" does not change the goal. Is this intended? Is "rule" allowed to leave a goal unchanged? (Btw: a little instantiation helps, e.g., "apply (rule arg_cong [of _ _ f])").
cheers
chris
On 01/27/2014 03:56 PM, Viorel Preoteasa wrote:
I have the following two lemmas:
lemma "(2 + (Suc n)) = (3 + n)"
by simplemma "f (2 + (Suc n)) = f (3 + n)"
by simpThe first one is proved by simp, but the proof on the
second lemma fails. How can I simplify numerical
constants in context?Best regards,
Viorel Preoteasa
Last updated: Apr 20 2024 at 08:16 UTC