From 3be70f39bbaba7c7edb5e5f3e26d4f952c06824e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 May 2018 16:00:17 +0200 Subject: Fix #7539: Checker does not properly handle negative coinductive types. The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. --- test-suite/coqchk/bug_7539.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 test-suite/coqchk/bug_7539.v (limited to 'test-suite/coqchk') diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v new file mode 100644 index 000000000..74ebe9290 --- /dev/null +++ b/test-suite/coqchk/bug_7539.v @@ -0,0 +1,26 @@ +Set Primitive Projections. + +CoInductive Stream : Type := Cons { tl : Stream }. + +Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream := + match n with + | O => s + | S m => Str_nth_tl m (tl s) + end. + +CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_tl : EqSt (tl s1) (tl s2); +}. + +Axiom EqSt_reflex : forall (s : Stream), EqSt s s. + +CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)). + +Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)). +Proof. +induction n. ++ intros; apply EqSt_reflex. ++ cbn; intros s; apply IHn. +Qed. + +Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl. -- cgit v1.2.3