Create a gist now

Instantly share code, notes, and snippets.

@mzp /Zakky.v
Created Aug 2, 2014

What would you like to do?
Inductive Term : Set :=
| T
| F
| TIf (_ : Term) (_ : Term) (_ : Term).
Inductive Step : Term -> Term -> Prop :=
| EIfTrue : forall (t1 t2 : Term), Step (TIf T t1 t2) t1
| EIfFalse : forall (t1 t2 : Term), Step (TIf F t1 t2) t2
| EIf : forall (t1 t1' t2 t3 : Term), Step t1 t1' -> Step (TIf t1 t2 t3) (TIf t1' t2 t3).
Lemma dec: forall (t t' t'' : Term),
Step t t' -> Step t t'' -> t' = t''.
Proof.
Check Step_ind.
intros t t' t'' Q.
generalize t''.
apply Step_ind with (t:=t) (t0:=t'); intros; auto.
inversion H; auto.
inversion H4.
inversion H; auto.
inversion H4.
destruct t1.
inversion H.
inversion H.
inversion H1.
apply H0 in H6.
rewrite H6.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment