1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
Require Import TestSuite.admit.
Require Import List.
Require Import Coq.Program.Equality.
Inductive star {genv state : Type}
(step : genv -> state -> state -> Prop)
(ge : genv) : state -> state -> Prop :=
| star_refl : forall s : state, star step ge s s
| star_step :
forall (s1 : state) (s2 : state)
(s3 : state),
step ge s1 s2 ->
star step ge s2 s3 ->
star step ge s1 s3.
Parameter genv expr env mem : Type.
Definition genv' := genv.
Inductive state : Type :=
| State : expr -> env -> mem -> state.
Parameter step : genv' -> state -> state -> Prop.
Section Test.
Variable ge : genv'.
Lemma compat_eval_steps:
forall a b e a' b',
star step ge (State a e b) (State a' e b') ->
True.
Proof.
intros. dependent induction H.
trivial.
eapply IHstar; eauto.
replace s2 with (State a' e b') by admit. eauto.
Qed. (* Oups *)
End Test.
|
