Update: With the help of Arthur Azevedo De Amorim, I finally dealt with this. The code is attached at the end of the question.
I am reading the book “Types and Programming Languages” and I am trying to prove every theorem (lemma) in this book using coq. When it came to Theorem 3.5.4, I tried and could not handle it. Here is a description of the problem.
Small language with AST:
t = :: true
:: false
:: if t then t else t
Evaluation Rules:
1. if true then t2 else t3 -> t2 (eval_if_true)
2. if false then t2 else t3 -> t3 (eval_if_false)
3. t1 -> t1'
------------------------ (eval_if)
if t1 then t2 else t3 ->
if t1' then t2 else t3
The theorem I want to prove is: for any t1 t2 t3 given t1 → t2 and t1 → t3, then t2 = t3.
And I build the type and sentence in Coq, as shown 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.
And I tried to do induction on eval_small_step t1 t2, as mentioned in the book. But I failed:
Proof.
intros t1 t2 t3.
intros H1 H2.
induction H1.
- inversion H2. reflexivity. inversion H4.
- inversion H2. reflexivity. inversion H4.
- assert (H: eval_small_step (if_stat t1 t0 t4) (if_stat t2 t0 t4)).
{
apply ev_if. apply H1.
}
Abort.
Since the inductive hypothesis is not general.
IHeval_small_step : eval_small_step t1 t3 -> t2 = t3
- ?
:
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.