The Coq mailing list

[Dimitri Hendriks <hendriks AT cs.kun.nl>]

Hi Robert,

Here is a proof. You need to load your induction a little.

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

Theorem determinacy :
  forall t t',
  (red1 t t') ->
  forall t'', (red1 t t'') -> t'=t''.
induction 1; intros.
inversion_clear H.
reflexivity.
inversion H0.
inversion_clear H.
reflexivity.
inversion H0.
generalize H; clear H.
inversion_clear H0; intro H0.
inversion H0.
inversion H0.
rewrite <- IHred1 with (1:=H).
reflexivity.
Qed.

On Mar 1, 2004, at 05:12, Robert Pierson wrote:

> 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''.