The Coq mailing list

[David Van Horn <dvanhorn AT cs.uvm.edu>]

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