Univs: test-suite file for bug #2016

1 files changed, 62 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
new file mode 100644
index 000000000..13ec5bea9
--- /dev/null
+++ b/test-suite/bugs/closed/2016.v
@@ -0,0 +1,62 @@
+(* Coq 8.2beta4 *)
+Require Import Classical_Prop. 
+
+Record coreSemantics : Type := CoreSemantics {
+  core: Type;
+  corestep: core ->  core -> Prop;
+  corestep_fun: forall q q1 q2, corestep q q1 -> corestep q q2 -> q1 = q2
+}.
+
+Definition state : Type := {sem: coreSemantics & sem.(core)}.
+
+Inductive step: state -> state -> Prop :=
+  | step_core: forall sem st st'
+             (Hcs: sem.(corestep) st st'),
+             step (existT _ sem st) (existT _ sem st').
+
+Lemma step_fun: forall st1 st2 st2', step st1 st2 -> step st1 st2' -> st2 = st2'.
+Proof.
+intros.
+inversion H; clear H; subst. inversion H0; clear H0; subst; auto.
+generalize (inj_pairT2 _ _ _ _ _ H2); clear H2; intro; subst.
+rewrite (corestep_fun _ _ _ _ Hcs Hcs0); auto.
+Qed.
+
+Record oe_core := oe_Core {
+    in_core: Type;
+    in_corestep: in_core -> in_core -> Prop;
+    in_corestep_fun: forall q  q1 q2,  in_corestep q q1 -> in_corestep q q2 -> q1 = q2;
+   in_q: in_core
+}.
+
+Definition oe2coreSem (oec : oe_core) : coreSemantics :=
+  CoreSemantics oec.(in_core) oec.(in_corestep)  oec.(in_corestep_fun).
+
+Definition oe_corestep (q q': oe_core) :=
+    step (existT _ (oe2coreSem q) q.(in_q)) (existT _ (oe2coreSem q') q'.(in_q)).
+
+Lemma inj_pairT1: forall (U: Type) (P: U -> Type) (p1 p2: U) x y,
+      existT P p1 x = existT P p2 y -> p1=p2.
+Proof. intros; injection H; auto.
+Qed.
+
+Definition f := CoreSemantics oe_core.
+
+Lemma oe_corestep_fun: forall q q1 q2, 
+       oe_corestep q q1 -> oe_corestep q q2 -> q1 = q2.
+Proof.
+unfold oe_corestep; intros.
+assert (HH:= step_fun _ _ _ H H0); clear H H0.
+destruct q1; destruct q2; unfold oe2coreSem; simpl in *.
+generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros.
+injection H; clear H; intros.
+revert in_q1  in_corestep1 in_corestep_fun1
+          H.
+pattern in_core1.
+apply eq_ind_r with (x := in_core0).
+admit.
+apply sym_eq.
+(** good to here **)
+Show Universes.
+Print Universes.
+Fail apply H0.
\ No newline at end of file