The Coq mailing list

[Robert Pierson <fried_flagrum AT yahoo.com>]

Hello, I am a new user to Coq and I am having trouble
with the simplest proofs.  I have the following
defintions:

Section Boolean_Expressions.
(* Fig 3.1 in Pierce's TAPL. *)

Inductive term : Set :=
  | true : term
  | false : term
  | If : term -> term -> term -> term.

Inductive red1 : term -> term -> Prop :=
  | E_IfTrue : 
    forall t2 t3 : term, (red1 (If true t2 t3) t2)
  | E_IfFalse : 
    forall t2 t3 : term, (red1 (If false 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))).


I would like to prove

Theorem determinacy : 
  forall t t' t'', 
    (red1 t t') /\ (red1 t t'') -> t'=t''.

But I haven't been able to.  Could someone provide
help.  

Thanks,
Robert

__________________________________
Do you Yahoo!?
Get better spam protection with Yahoo! Mail.
http://antispam.yahoo.com/tools