[isabelle] stuck on proof

[Ian Lynagh]

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

[Tobias Nipkow]

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

Post by Ian Lynagh
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

[Lars Noschinski]

lemma "(principalType e = Some t) ==> (STyping e t)"
apply (induct e arbitrary: t)
apply (auto simp: STyping.intros split:option.splits SType.splits)
done

As I often forget about *.intros and similar sets: find_theorems has a
with_dups option, which shows you also these alternate names.

-- Lars

[Ian Lynagh]

Post by Ian Lynagh
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.

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):
1. !!e1 e2 e3 t aa ab.
[| !!t. TBool = t ==> STyping e1 TBool; !!t. aa = t ==> STyping e2 t;
!!t. ab = t ==> STyping e3 t; principalType e1 = Some TBool;
principalType e2 = Some aa; principalType e3 = Some ab;
(if aa = ab then Some aa else None) = Some t |]
==> STyping (EIfThenElse e1 e2 e3) t

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

[Makarius]

Post by Ian Lynagh

Post by Ian Lynagh
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.

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

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.

Post by Ian Lynagh
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

[Ian Lynagh]

Post by Makarius
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.

Fantastic, thanks! I'll have a play with it.


Thanks
Ian

[Makarius]

Post by Ian Lynagh
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".

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

[Lars Noschinski]

Post by Makarius

Post by Ian Lynagh
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".

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.

I reported it yesterday and latest tarball is already fixed.

[Ian Lynagh]

Post by Makarius

Post by Ian Lynagh
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".

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.

Done: http://proofgeneral.inf.ed.ac.uk/trac/ticket/337


Thanks
Ian