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.