Re: [isabelle] stuck on proof



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

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
(* :encoding=utf-8: *)

theory Simple
imports Main
begin

datatype SExpr =
    EBool bool
  | EInt int
  | EGreaterThan SExpr SExpr

datatype SType = TBool | TInt

inductive STyping :: "SExpr => SType => bool"
  where
    STypingBool: "STyping (EBool b) TBool"
  | STypingInt: "STyping (EInt n) TInt"
  | STypingGreaterThan:
      "STyping lhs TInt \<Longrightarrow> STyping rhs TInt \<Longrightarrow>
        STyping (EGreaterThan lhs rhs) TBool"

fun principalType :: "SExpr => SType option"
  where
    "principalType (EBool b) = Some TBool"
  | "principalType (EInt n) = Some TInt"
  | "principalType (EGreaterThan lhs rhs) =
      (case (principalType lhs, principalType rhs) of
        (Some TInt, Some TInt) => Some TBool
      | _ => None)"

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

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

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

end


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