From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/2883.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 test-suite/bugs/closed/2883.v (limited to 'test-suite/bugs/closed/2883.v') diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v new file mode 100644 index 00000000..5a5d90a4 --- /dev/null +++ b/test-suite/bugs/closed/2883.v @@ -0,0 +1,34 @@ +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 *) -- cgit v1.2.3