aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2883.v
blob: f027b5eb293e95e2e19ea31bcb406239a54fc6de (plain)
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
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 *)