# Re: [isabelle] stuck on proof

```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)
> 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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.