Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Converting apply-style induction to Structured...


view this post on Zulip 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

view this post on Zulip 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.thy

In the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thy

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

view this post on Zulip 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.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?

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC