Email Gateway (Aug 18 2022 at 17:18): Email Gateway (Aug 18 2022 at 17:18):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
How about
lemma cata_uniq:
assumes "cata c f b"
shows "c as = catafunc f b as"
proof (induct as)
case (Singleton a)
from assms show ?case
by (simp add: catafunc_def cata_def)
next
case (Snoc as a)
from assms show ?case
by (simp only: Snoc cata_def cons_rewrite) simp
qed
The fact that I need to split the final step into 2 parts (one only
using cons_rewrite cata_def and the induction hypothesis, and the other
using all the simplification rules that are around) indicates that some
of your equations may be oriented in the wrong direction (without the
split, the simplifier loops). But I didn't have closer look. Another
thing that I find strange in your original proof is the use of
catafunc_def which was defined via "fun" an hence provides
simplification rules catafunc.simps.
A few words on the above proof: Fixing local variables and stating
assumptions (e.g., the IH) is done automatically when using "case", e.g.,
case (Snoc as a)
is a kind of abbreviation for
fix as a
assume "c as = catafunc f b as"
I hope this helps.
cheers
chris
Email Gateway (Aug 18 2022 at 17:18):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Donnerstag, den 31.03.2011, 13:29 +0200 schrieb Søren Haagerup:
Hello,
I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
http://gawis.dk/misc/apply_sample.thyIn the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thy
Do not add catafunc_def, this is the wrong simp rule. The rules
catafunc.simps are automatically added to the simpset by primrec.
This also adds the rules for "app" to the simp set, which is the
inverse of cata_rewrite, and hence when you add cata_rewrite without
removing app.simps, like "simp add: cata_rewrite" the simplifier does
not terminate. Instead use "simp add: cata_rewrite del: app.simps"
You cata_helper lemma is always a good idea to add. Probably named
added to the simplifier. However adding rules to the automatization
needs some experience, but you should try to play with it. (they also
look like nice dest rules)
The "case" command lets you specify the fixed variables no need to
add "fix" and "assume".
If you use "case" with the method "induct" the thesis is not
named ?thesis but ?case, the facts are named after the case name (look
at Isabelle / Show me / Facts) :
proof (induct c)
case (Cons1 a b c) then show ?case ...
next
case (Cons2 a b c) then show ?case ...
qed
In your structured cata_uniq you do not need the additional
show "" proof - ... qed
command.
My solution would be:
lemma cata_uniq:
"cata c f b ==> c as = catafunc f b as"
proof (induct as)
case (Snoc as a)
then have "c (app as (Singleton a)) = b (catafunc f b as) (f a)"
by (simp_all add: cata_def del: app.simps)
then show ?case
by simp
qed (simp add: cata_def)
(** the method supplied to "qed" is applied to the remaining goals.
Here it is the Singleton case. **)
Another possible solution would be:
lemma cata_uniq:
"cata c f b ==> c as = catafunc f b as"
proof (induct as)
case (Snoc as a) then show ?case
by (simp add: cata_def cons_rewrite del: app.simps) simp
qed (simp add: cata_def)
This is shorted but probably not as readable and stable as the previous
proof.
The lines
by (simp add: cata_def cons_rewrite del: app.simps)
simp
are the same as
proof (simp add: cata_def cons_rewrite del: app.simps)
qed simp
Hope this helps,
Johannes
Is there a way to make a concise structured proof of this fact?
Best regards,
Søren
Email Gateway (Aug 18 2022 at 17:18):From: Christian Urban <urbanc@in.tum.de>
Quoting Søren Haagerup <shaagerup@gmail.com>:
Hello,
I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
http://gawis.dk/misc/apply_sample.thyIn the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thyIs there a way to make a concise structured proof of this fact?
Well, you have to keep in mind that a 'good' Isar proof conveys more
information than an apply-script. In a 'good' Isar proof you should
be able to easily read off the proof idea. This means in practice
that an Isar proof is sometimes a bit more verbose.
However looking at your proof, I would formulate it as follows.
lemma cata_uniq :
assumes a: "cata c f b"
shows "c as = catafunc f b as"
proof (induct as)
case (Singleton a)
show "c (Singleton a) = catafunc f b (Singleton a)"
using a by (simp add: catafunc_def cata_def)
next
case (Snoc as a)
have hyp: "c as = catafunc f b as" by fact
have "c (Snoc as a) = c (app as (Singleton a))" by (simp only:
cons_rewrite)
also have "... = b (c as) (f a)"
using cata_helper(3)[OF a, of as "Singleton a"]
cata_helper(2)[OF a, of a] by auto
also have "... = b (catafunc f b as) (f a)" using hyp by auto
finally show "c (Snoc as a) = catafunc f b (Snoc as a)"
by simp
qed
1.) As suggested before, I fix the variables at the case-level. This
gets rid of the explicit fix lines.
2.) Also often I start with a proof like yours (which contains forward
and backward reasoning steps). If possible, I then reformulate these
proofs to
be completely forward proofs, which tend to be slightly shorter (you
can save the lines about opening and closing subproofs).
3.) If you think that the Singleton-case is too trivial and should not
be shown
explicitly, you can 'hide' it by discharging it at the qed-statement,
like this:
lemma cata_uniq :
assumes a: "cata c f b"
shows "c as = catafunc f b as"
proof (induct as)
case (Snoc as a)
have hyp: "c as = catafunc f b as" by fact
have "c (Snoc as a) = c (app as (Singleton a))" by (simp only: cons_rewrite)
also have "... = b (c as) (f a)"
using cata_helper(3)[OF a, of as "Singleton a"] cata_helper(2)[OF
a, of a] by auto
also have "... = b (catafunc f b as) (f a)" using hyp by auto
finally show "c (Snoc as a) = catafunc f b (Snoc as a)"
by simp
qed (simp add: a[unfolded cata_def])
OK, this is not as short as your apply-script and the two solutions,
but as said above the purpose of an Isar proof is not to be as concise as
an apply-script, but to easily read off the proof idea (your calculation).
This might mean in this case that the proof is a bit more verbose (but this
is not always the case).
I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.
My experience is also that going from an apply script to an Isar proof
is not that easy. Fiddling with an apply script usually completely buries
the proof idea. Constructing then the corresponding Isar proof means that
one has to think again about what are the important steps in the proof are.
That can sometimes be non-obvious.
Hope this helps,
Christian
Email Gateway (Aug 18 2022 at 17:18):From: Søren Haagerup <shaagerup@gmail.com>
This really made my day -- I have been craving for such a feature for
very long :-)
Thank you for all your suggestions and solutions - it sped up my
learning process a lot!
Best,
Søren
Email Gateway (Aug 18 2022 at 17:29):From: Søren Haagerup <shaagerup@gmail.com>
Hello,
I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.
In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
http://gawis.dk/misc/apply_sample.thy
In the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thy
Is there a way to make a concise structured proof of this fact?
Best regards,
Søren
Email Gateway (Aug 18 2022 at 17:29):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi,
While drinking tea, I took a quick stab at it too, here's what I ended
up with:
lemma cata_uniq2: "cata c f b ==> c as = catafunc f b as"
unfolding cata_def
proof (induct as)
case (Singleton a) thus ?case by simp
next
case (Snoc as a)
thus ?case
by (subst catafunc.simps)
(simp add: cons_rewrite del: app.simps)
qed
The "cons_rewrite" lemma is in direct conflict with app.simps, so they
can't both be in the simpset at the same time.
If you repeatedly run into this type of conflict, you might want to
remove the function equations from the simpset using:
declare app.simps[simp del]
Then you can always add them back in to the simplifier when needed.
By now, you should have a nice collection of various people's proving
styles in Isar :)
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 17:34):From: Tjark Weber <webertj@in.tum.de>
I've found metis quite handy in similar situations. metis knows about
symmetry, so (unlike simp) it may still succeed when equalities are
oriented the wrong way.
Kind regards,
Tjark
Last updated: Nov 21 2024 at 12:39 UTC