diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:08:04 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:08:04 +0200 |
commit | 1757f89b6c61024bbe3aebd6b43c56df0d92f5eb (patch) | |
tree | 3a04f1f948df72be5d58ae992508e303128db23d /test-suite/coqchk | |
parent | 10e323fe4cebd1addfe1af32407f1277214d2c7b (diff) | |
parent | 3be70f39bbaba7c7edb5e5f3e26d4f952c06824e (diff) |
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinductive types.
Diffstat (limited to 'test-suite/coqchk')
-rw-r--r-- | test-suite/coqchk/bug_7539.v | 26 |
1 files changed, 26 insertions, 0 deletions
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. |