diff options
Diffstat (limited to 'test-suite/coqchk/bug_7539.v')
-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 00000000..74ebe929 --- /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. |