The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon David Van Horn 
<dvanhorn AT cs.uvm.edu>:


Dear David,

 Your theorem can be proven with a little lemma telling that any
conditional expression can be rewritten. This lemma is proven by
induction on the first term of the consitional. Then your theorem
follows by a reductio ad absurdum.

Pierre

> Hello,
>
> I'm working my way through Coq'Art and applying the concepts to prove simple
> results from the text Types and Programming Languages.  I am stuck trying to
> prove the following trivial result about boolean programs: a term in normal
> form implies the term is a value.  Here is the development:
>
> Inductive term : Set :=
>    | ETrue  : term
>    | EFalse : term
>    | If  : term -> term -> term -> term.
>
> (* The single step reduction relation, --> *)
> Inductive red1 : term -> term -> Prop :=
>     | E_IfTrue  : forall t2 t3 : term, (red1 (If ETrue  t2 t3) t2)
>     | E_IfFalse : forall t2 t3 : term, (red1 (If EFalse t2 t3) t3)
>     | E_If      : forall t1 t1': term, (red1 t1 t1') ->
>                     (forall t2 t3 : term, (red1 (If t1 t2 t3) (If t1' t2
> t3))).
>
> Definition normal_form (t : term) := ~(ex term (fun t':term => red1 t t')).
>
> Definition value (t : term) := t=ETrue \/ t=EFalse.
>
> Theorem normal_implies_value : forall t, (normal_form t) -> (value t).
>
>
> The proof should go by case analysis on t, and it easy to show that when t 
> is
> ETrue or EFalse that the result holds:
>
>    unfold value, normal_form, not.
>    intro t.
>    case t.
>      intro H; left;  reflexivity.
>      intro H; right; reflexivity.
>
> However I can't seem to show the remaining case.  Could someone comment on
> how
> to obtain this result?  Also, is there an alternative formulation of
> normal_form, mine strikes me as awkward?  Finally, is there a more
> appropriate
> forum for asking these sorts of beginner questions?
>
> Thanks,
> David
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Attachment: coqclub.v
Description: Binary data