55 lines
1.3 KiB
Coq
55 lines
1.3 KiB
Coq
Lemma step_deterministic :
|
|
deterministic step.
|
|
Proof with eauto.
|
|
unfold deterministic.
|
|
intros t t' t'' E1 E2.
|
|
generalize dependent t''.
|
|
induction E1; intros t'' E2; inversion E2; subst; clear E2...
|
|
(* ST_AppAbs *)
|
|
- inversion H3.
|
|
- exfalso; apply value__normal in H...
|
|
(* ST_App1 *)
|
|
- inversion E1.
|
|
- f_equal...
|
|
- exfalso; apply value__normal in H1...
|
|
(* ST_App2 *)
|
|
- exfalso; apply value__normal in H3...
|
|
- exfalso; apply value__normal in H...
|
|
- f_equal...
|
|
(* ST_Pair1 *)
|
|
- f_equal...
|
|
- exfalso; apply value__normal in H1...
|
|
(* ST_Pair2 *)
|
|
- exfalso; apply value__normal in H...
|
|
- f_equal...
|
|
(* ST_Fst *)
|
|
- f_equal...
|
|
- exfalso.
|
|
inversion E1; subst.
|
|
+ apply value__normal in H0...
|
|
+ apply value__normal in H1...
|
|
(* ST_FstPair *)
|
|
- exfalso.
|
|
inversion H2; subst.
|
|
+ apply value__normal in H...
|
|
+ apply value__normal in H0...
|
|
(* ST_Snd *)
|
|
- f_equal...
|
|
- exfalso.
|
|
inversion E1; subst.
|
|
+ apply value__normal in H0...
|
|
+ apply value__normal in H1...
|
|
(* ST_SndPair *)
|
|
- exfalso.
|
|
inversion H2; subst.
|
|
+ apply value__normal in H...
|
|
+ apply value__normal in H0...
|
|
- (* ST_TestTrue *)
|
|
inversion H3.
|
|
- (* ST_TestFalse *)
|
|
inversion H3.
|
|
(* ST_Test *)
|
|
- inversion E1.
|
|
- inversion E1.
|
|
- f_equal...
|
|
Qed.
|