aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqchk/bug_7539.v
blob: 74ebe9290de58e4123427c3a616579b66bb745c0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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.