Recently I started reading the book ** Types and Programming Languages. **And I found it interesting to proof the lemmas in the book using Coq.

My first attempt is to proof lemma **3_5_4 **in the book. This language is quite simple and its statics and dynamics are shown in the following picture:

The lemma I am going to prove here is:

Lemma: [Determinacy of one-step evaluation]: If t → t1 and t → t2, then t1 = t2 .

We use coq to model the language inductively as below:

```
Inductive t : Type :=
| zhen (* represent true *)
| jia (* represent false *)
| if_stat : t -> t -> t -> t.
Inductive eval_small_step : t -> t -> Prop :=
| ev_if_true : forall (t2 t3 : t),
eval_small_step (if_stat zhen t2 t3) t2
| ev_if_false : forall (t2 t3 : t),
eval_small_step (if_stat jia t2 t3) t3
| ev_if : forall (t1 t2 t3 t4 : t),
eval_small_step t1 t2 ->
eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4).
```

Then the proof is sort of straightforward. But at first I encountered a problem which can be viewed here: https://stackoverflow.com/questions/44490405/how-to-prove-theorem-3-5-4-in-types-and-programming-languages-using-coq. Finally I manage it, the full code is as below:

```
Inductive t : Type :=
| zhen (* represent true *)
| jia (* represent false *)
| if_stat : t -> t -> t -> t.
Inductive eval_small_step : t -> t -> Prop :=
| ev_if_true : forall (t2 t3 : t),
eval_small_step (if_stat zhen t2 t3) t2
| ev_if_false : forall (t2 t3 : t),
eval_small_step (if_stat jia t2 t3) t3
| ev_if : forall (t1 t2 t3 t4 : t),
eval_small_step t1 t2 ->
eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4).
Theorem determinacy : forall (t1 t2 t3 : t),
eval_small_step t1 t2 -> eval_small_step t1 t3 -> t2 = t3.
Proof.
intros t1 t2 t3.
intros H1.
revert t3.
induction H1.
- intros t0. intros H.
inversion H.
+ reflexivity.
+ inversion H4.
- intros t0. intros H.
inversion H.
+ reflexivity.
+ inversion H4.
- intros t0.
intros H.
assert(H': eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4)).
{
apply ev_if. apply H1.
}
inversion H.
+ rewrite <- H2 in H1. inversion H1.
+ rewrite <- H2 in H1. inversion H1.
+ assert(H'': t2 = t6).
{
apply IHeval_small_step.
apply H5.
}
rewrite H''. reflexivity.
Qed.
```

It is always good to make puzzles for yourself and try hard to solve them when you are learning something.