Add a test-suite file ensuring coinductives with primitive projections

do not enjoy eta-conversion and do not allow the usual failure of
subject reduction in presence of dependent pattern-matching.

1 files changed, 52 insertions, 0 deletions

diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
new file mode 100644
index 000000000..4e0b7bf5c
--- /dev/null
+++ b/test-suite/success/coindprim.v
@@ -0,0 +1,52 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks : stream unit :=
+  {| hd := tt; tl := ticks |}.
+
+Arguments hd [ A ] s.
+Arguments tl [ A ] s.
+
+CoInductive bisim {A} : stream A -> stream A -> Prop :=
+  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.
+
+Lemma bisim_refl {A} (s : stream A) : bisim s s.
+Proof.
+  revert s.
+  cofix aux. intros. constructor. reflexivity. apply aux.
+Defined.
+
+Lemma constr : forall (A : Type) (s : stream A),
+    bisim s (Build_stream _ s.(hd) s.(tl)).
+Proof.
+  intros. constructor. reflexivity. simpl. apply bisim_refl.
+Defined.
+
+Lemma constr' : forall (A : Type) (s : stream A),
+  s = Build_stream _ s.(hd) s.(tl).
+Proof.
+  intros. 
+  Fail destruct s. 
+Abort.
+
+Eval compute in constr _ ticks.
+
+Notation convertible x y := (eq_refl x : x = y).
+
+Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.
+
+CoInductive U := inU
+ { outU : U }.
+
+CoFixpoint u : U :=
+  inU u.
+
+CoFixpoint force (u : U) : U :=
+  inU (outU u).
+
+Lemma eq (x : U) : x = force x.
+Proof.
+  Fail destruct x.
+Abort.
+  (* Impossible *)
\ No newline at end of file