Email Gateway (Aug 18 2022 at 15:51): Email Gateway (Aug 18 2022 at 15:51):From: Ian Lynagh <igloo@earth.li>
Hi all,
I'm stuck on a proof of
lemma "(principalType e = Some t) ==> (STyping e t)"
(details in attachment). I've managed to solve the EBool case with
apply_end simp
from "STypingBool"
show "!!b. STyping (EBool b) TBool"
apply simp .
but I don't think this is a good proof: I'm sure using "apply_end simp"
is bad style, and I don't think I should be copy/pasting
"!!b. STyping (EBool b) TBool" from the proof state. Even "apply simp"
I'm not sure is good style.
I've therefore tried to write a better proof for the EInt case, but got
nowhere. The attached script shows some of my meanderings.
Has anyone got any hints, please?
I'm also not sure what's going to happen when I get to a recursive case.
I suspect "proof (cases e)" is not sufficient for the recursive case,
but "proof (induct e)" doesn't look like it's generating the right goal
for the recursive case (as t doesn't vary), and
"proof (induct rule: SExpr.induct)" has the same problem. Again, can
anyone point me in the right direction please?
Incidentally, in proof general, the "Isabelle/Show me .../Facts" menu
says "C-c C-a <h> <f>" next to it, but after typing just "ctrl-c ctrl-a h"
emacs says "C-c C-a h is undefined". Any idea what's wrong?
Thanks
Ian
q.thy
Email Gateway (Aug 18 2022 at 15:51):From: Tobias Nipkow <nipkow@in.tum.de>
lemma "(principalType e = Some t) ==> (STyping e t)"
apply (induct e arbitrary: t)
apply (auto simp: STyping.intros split:option.splits SType.splits)
done
split: ... instructs auto (or simp) to split case expressions for
certain types automatically.
Tobias
Ian Lynagh schrieb:
Email Gateway (Aug 18 2022 at 15:51):From: Makarius <makarius@sketis.net>
This looks like a problem of Proof General, and should go to
http://proofgeneral.inf.ed.ac.uk/trac/
Since David Aspinall is working on the next major release PG 4.0 right
now, it is especially important to report any remaining issues there.
Makarius
Email Gateway (Aug 18 2022 at 15:51):From: Ian Lynagh <igloo@earth.li>
Done: http://proofgeneral.inf.ed.ac.uk/trac/ticket/337
Thanks
Ian
Email Gateway (Aug 18 2022 at 15:51):From: Lars Noschinski <noschinl@in.tum.de>
I reported it yesterday and latest tarball is already fixed.
Email Gateway (Aug 18 2022 at 15:52):From: Ian Lynagh <igloo@earth.li>
Thanks, but this isn't the sort of proof I'm hoping to end up with.
My hope is to have a proof that a Haskell programmer can read,
understand and ideally even adapt; i.e. I want a machine-checked proof,
rather than a machine proof. For example, if I add an IfThenElse
construct, then the proof now leaves me with an unsolved goal:
goal (1 subgoal):
for which the solution is not clear, because the proof is opaque to
non-Isabellers.
My understanding was that Isar is more like coq's C-zar (or more
accurately, I guess, C-zar is like Isar). With C-zar I am optimistic
that readable, and not /too/ verbose, proofs would be possible.
Unfortunately, due to C-zar bugs, writing the proofs is not currently
possible, and C-zar seems to be largely dead, but the beginning of a
proof looks like this:
Lemma typingIsPrincipalType : forall (e : SExpr)
(t : SType)
(typing : STyping e t),
principalType e = Some t.
proof.
let e, t be such that typing : (STyping e t).
per induction on typing.
suppose it is (STypingBool b).
hence thesis by principalType.
suppose it is (STypingInt n).
hence thesis by principalType.
Thanks
Ian
Email Gateway (Aug 18 2022 at 15:53):From: Makarius <makarius@sketis.net>
On Thu, 19 Aug 2010, Ian Lynagh wrote:
On Tue, Aug 17, 2010 at 10:07:53AM +0200, Tobias Nipkow wrote:
lemma "(principalType e = Some t) ==> (STyping e t)"
apply (induct e arbitrary: t)
apply (auto simp: STyping.intros split:option.splits SType.splits)
donesplit: ... instructs auto (or simp) to split case expressions for
certain types automatically.Thanks, but this isn't the sort of proof I'm hoping to end up with.
My hope is to have a proof that a Haskell programmer can read,
understand and ideally even adapt; i.e. I want a machine-checked proof,
rather than a machine proof. For example, if I add an IfThenElse
construct, then the proof now leaves me with an unsolved goal:
This is exactly the purpose of structured Isar proofs: you write down the
reasoning in a way that is usable both for the machine and the user -- and
also maintainable in the end. Getting started with Isar proofs is a bit
challanging, because the interaction model of Proof General is working
against it. But once you have some proof working, it is easy to extend,
generalize, beatify etc.
Included is my result of playing a little with your theory. I have
started with the 2-liner by Tobias and tried to reconstruct the reasing
behind it. (One could rightly ask, if the system could be more helpful to
construct this reasoning in the first place).
In the attached Simple.thy there are 3 Isar proofs of increasing detail.
The smallest possible Isar proof is "by (induct ...) (auto ...)" -- this
double method invocation (initial followed by terminal one) marks the
transition from apply scripts to Isar proofs. (BTW, it is a common
mistake to put a "," for sequential method composition in between.)
lemma "principalType e = Some t ==> STyping e t"
by (induct e arbitrary: t)
(auto simp: STyping.intros split: option.splits SType.splits)
The second proof merely expands the outermost induction skeleton, and
"optimizes" the terminal justifications, to narrow down the automation by
reducing the given facts and tools in question, e.g. plain "simp" instead
of "auto" (which is relatively strong).
lemma "principalType e = Some t ==> STyping e t"
proof (induct e arbitrary: t)
case (EBool b)
then show ?case
by (simp add: STyping.intros)
next
case (EInt n)
then show ?case
by (simp add: STyping.intros)
next
case (EGreaterThan lhs rhs)
then show ?case
by (auto simp: STyping.intros split: option.splits SType.splits)
qed
The last version expands on the induction cases a little:
lemma "principalType e = Some t ==> STyping e t"
proof (induct e arbitrary: t)
case (EBool b)
then have "t = TBool" by simp
also have "STyping (EBool b) TBool" ..
finally show "STyping (EBool b) t" .
next
case (EInt n)
then have "t = TInt" by simp
also have "STyping (EInt n) TInt" ..
finally show "STyping (EInt n) t" .
next
case (EGreaterThan lhs rhs)
have *: "principalType (EGreaterThan lhs rhs) = Some t" by fact
show "STyping (EGreaterThan lhs rhs) t"
proof (cases t)
case TBool
have "STyping lhs TInt"
proof (rule EGreaterThan.hyps)
from TBool and * show "principalType lhs = Some TInt"
by (simp split: option.splits SType.splits)
qed
moreover
have "STyping rhs TInt"
proof (rule EGreaterThan.hyps)
from TBool and * show "principalType rhs = Some TInt"
by (simp split: option.splits SType.splits)
qed
ultimately have "STyping (EGreaterThan lhs rhs) TBool" ..
then show ?thesis by (simp only: TBool)
next
case TInt
with * have False by (simp split: option.splits SType.splits)
then show ?thesis ..
qed
qed
There are many possibilities here. Of course, I did not write this down
on the spot, although it is constructed in a somewhat canonical way
without two much elaboration.
To explore a certain situation with various facts being locally available,
you can either use plain rule composition, e.g.
thm r1 [OF t2]
or experiment with the effect of simplification, e.g.
from my_facts have XXX apply simp
Here the "XXX" is a literal variable, which the simplifier usually keeps
unchanged, while the concrete my_facts are normalized. This usually gives
important clues about proper concrete conclusions:
from my_facts have my_prop by simp
This forward simplification in the context of the Isar text works better
than tinkering with 'apply_end' on goal states.
My understanding was that Isar is more like coq's C-zar (or more
accurately, I guess, C-zar is like Isar). With C-zar I am optimistic
that readable, and not /too/ verbose, proofs would be possible.
Unfortunately, due to C-zar bugs, writing the proofs is not currently
possible, and C-zar seems to be largely dead, ...
In fact, C-zar is more like te "Mizar mode for HOL" by John Harrison from
1995, and it seems to share its "experimental" nature. I know myself only
too well how difficult it is to get beyond that stage.
Makarius
Simple.thy
Email Gateway (Aug 18 2022 at 15:53):From: Ian Lynagh <igloo@earth.li>
Fantastic, thanks! I'll have a play with it.
Thanks
Ian
Last updated: Apr 23 2024 at 20:15 UTC