Require Import List ZArith Wellfounded.
Open Scope Z_scope.

CoInductive str : Type := cs (x:Z) (t:str).
Infix "::" := cs.

CoFixpoint ones := 1::ones.

Eval compute in ones.

Definition hd (s:str) : Z := let (a, _) := s in a.

Fixpoint take (n:nat)(s:str) : list Z :=
  match s, n with
  | a::s', S p => (a::take p s')%list
  | _,_ => nil
  end.

Eval compute in take 10 ones.

CoFixpoint alt01 := 0::1::alt01.

Eval vm_compute in take 10 alt01.

CoFixpoint ftos (f : nat -> Z) (n:nat) : str :=
  f n::ftos f (n+1).

CoFixpoint map (f : Z -> Z) (s : str) : str :=
  match s with a::s' => f a::map f s' end.

CoFixpoint emap (f : Z -> Z) (s : str) : str :=
  match s with a::s' => f a::emap f s end.

Eval vm_compute in take 10 (map Zsucc alt01).

Eval vm_compute in take 10 (emap Zsucc alt01).

Fixpoint fib n : Z :=
  match n with 0%nat => 0 | 1%nat => 1 | S (S p as q) => fib p + fib q end.

Definition fibs := ftos fib 0.

Time Eval vm_compute in take 35 fibs.

Time Eval vm_compute in take 35 fibs.

Section repeatP.

Variable P : Z -> Prop.
Variable f : Z -> Z.

CoInductive alwaysfP : Z -> Prop :=
  afp : forall x, P x -> alwaysfP (f x) -> alwaysfP x.

Lemma afp2fp : forall x, alwaysfP x -> P x.
intros x [x' px' _]; assumption.
Qed.

Lemma afp2f2p : forall x, alwaysfP x -> P (f (f x)).
intros x afpx.
destruct afpx as [y py afpy].
destruct afpy as [z pz afpz].
apply afp2fp; assumption.
Qed.

Fixpoint iter (n : nat) (x : Z) :=
  match n with 0%nat  => x | S p => iter p (f x) end.

Lemma afp2fnp : forall x n, alwaysfP x -> P (iter n x).
intros x n; revert x; induction n.
 exact afp2fp.
simpl.
intros x [x' px' afpx'].
apply IHn; assumption.
Qed.

Lemma fp2afp :  (forall x, P x -> P (f x)) ->
  forall x, P x -> alwaysfP x.
intros fp.
cofix.
Check afp.
intros x hp; constructor.
  exact hp.
apply fp2afp; apply fp; assumption.
Qed.

End repeatP.

CoInductive chained (R : Z -> Z -> Prop) : str -> Prop :=
  cc : forall x y s, R x y -> chained R (y::s) ->
          chained R (x::y::s).

CoInductive streq : str -> str -> Prop :=
  csq : forall x s1 s2, streq s1 s2 -> streq (x::s1) (x::s2).

Infix "==" := streq (at level 70, no associativity).

Definition force (s:str) : str :=
  match s with a::s' => a::s' end.

Lemma force_eq : forall s, s = force s.
intros [a s']; reflexivity.
Qed.

Definition sw01 x := 1 - x.

Lemma altinv : map sw01 alt01 == 1::alt01.
cofix.
rewrite (force_eq alt01); simpl.
rewrite (force_eq (map sw01 (0::1::alt01))); simpl.
rewrite (force_eq (map sw01 (1::alt01))); simpl.
constructor.
constructor.
apply altinv.
Qed.

CoInductive ct (R : Z -> Z -> Prop) : str -> Prop :=
  Cct : forall x y s, R x y -> ct R (y::s) ->
    ct R (x::y::s).

Section filter.
Variable R : Z -> Z -> Prop.
Variable p: Z -> bool.

Hypothesis wf :
  well_founded (fun y x, R x y /\ p x = false).

Definition sr (s' s:str) : Prop :=
  R (hd s) (hd s') /\  p (hd s) = false.

Lemma swf : well_founded sr.
Proof. 
apply wf_inverse_image with (f:=@hd)(1:=wf).
Qed.

Definition sumbool_of_bool :
  forall v : bool, {v = true}+{v = false}.
intros [ | ];[left; reflexivity | right; reflexivity].
Defined.

Definition dec_ct (s : str) (h : ct R s) : 
   {x : Z & {s' | (p x = false -> sr s' s) /\ ct R s'}}.
intros [a s] h; exists a; exists s; inversion h.
split.
 intros paf; split; assumption.
assumption.
Defined.

Definition filterb :
    forall s (h : ct R s), Z * {s' | ct R s'} :=
  Fix swf (fun s => ct R s -> Z * {s' | ct R s'})
    (fun s fb h =>
     let '(existT x (exist s' (conj h1 h2))) := dec_ct s h in
    match sumbool_of_bool (p x) with
       left hp => (x, exist (fun s' => ct R s') s' h2)
     | right hp => fb s' (h1 hp) h2
     end).

CoFixpoint filter (s : str) (h : ct R s) : str :=
  let '(x, (exist s' q)) := filterb s h in 
    x::filter s' q.

End filter.

CoFixpoint zipWith f s1 s2 :=
  match s1, s2 with
    (a::s1'), (b::s2') => f a b::zipWith f s1' s2'
  end.

CoInductive ztr : Type :=
  zs (x : Z) (s : ztr) | zip (s1 s2 : ztr).

Inductive zf : ztr -> Prop :=
  ci1 : forall x s, zf (zs x s)
| ci2 : forall s1 s2, zf s1 -> zf s2 -> zf (zip s1 s2).

CoInductive zr : ztr -> Prop :=
  cc1 : forall x s, zr s -> zr (zs x s)
| cc2 : forall s1 s2, zr s1 -> zr s2 ->
   zf s1 -> zf s2 -> zr (zip s1 s2).

Lemma zf_inv1 :
  forall s, zf s -> forall s1 s2, s = zip s1 s2 -> zf s1.
intros s h; case h; [intros; discriminate | ].
intros s1 s2 h1 _ s3 s4 q; injection q; intros q2 q1;
 case q1; assumption.
Defined.

Lemma zf_inv2 :
  forall s, zf s -> forall s1 s2, s = zip s1 s2 -> zf s2.
intros s h; case h; [intros; discriminate | ].
intros s1 s2 _ h2 s3 s4 q; injection q; intros q2 q1;
 case q2; assumption.
Defined.

Lemma zr_to_zf : forall s, zr s -> zf s.
intros s h; case h; intros; constructor; assumption.
Defined.

Fixpoint extract s (h:zf s) : Z * ztr :=
  match s as x return s = x -> Z * ztr with
    zs x s' => fun _ => (x, s')
  | zip s1 s2 => fun q => 
    let (x1, s1') := extract s1 (zf_inv1 s h s1 s2 q) in
    let (x2, s2') := extract s2 (zf_inv2 s h s1 s2 q) in
    (x1 + x2, zip s1' s2')
  end (refl_equal s).

Scheme zf_ind2 := Induction for zf Sort Prop.

Lemma extract_zr : forall s h (h' : zr s), zr (snd (extract s h)).
intros s h; elim h using zf_ind2; simpl.
 intros x s' h'; inversion h'; assumption.
intros s1 s2 s1f IH1 s2f IH2 ps.
destruct (extract _ s1f) as [v1 w1].
destruct (extract _ s2f) as [v2 w2].
inversion ps; constructor; try apply zr_to_zf; auto.
Defined.

CoFixpoint iztr (s:ztr) (h:zr s) : str :=
  let h' := zr_to_zf s h in
   fst (extract s h'):: 
   iztr (snd (extract s h')) (extract_zr s h' h).

CoFixpoint zfib : ztr :=
  zs 0 (zip zfib (zs 1 zfib)).

Definition zforce (s : ztr) :=
  match s with
    zs a s' => zs a s'
  | zip s1 s2 => zip s1 s2
  end.

Lemma zforce_eq : forall s, s = zforce s.
Proof. intros [a s | s1 s2]; reflexivity. Defined.

Lemma zf_fib : zf zfib.
rewrite zforce_eq; simpl; constructor.
Defined.

Lemma zr_fib : zr zfib.
cofix.
rewrite zforce_eq; simpl.
 repeat constructor; apply zr_fib || apply zf_fib.
Defined.

Definition fib' := iztr _ zr_fib.

Eval vm_compute in take 10 fib'.

Fixpoint filtern (p : Z -> bool) (s:str) (n:nat) :=
  match s, n with
    _, 0%nat => s
  | a::tl, S n' => if p a then s else filtern p tl n'
  end.

CoFixpoint filterp (p: Z -> bool) (s:str) : str :=
  let (a, _) := s in
  let (a', s') := filtern p s (Zabs_nat a) in
   a'::filterp p s'.

Definition not_div x y :=
  negb (Zeq_bool (Zmod y x) 0).

CoFixpoint sieve (s:str) :=
  let (x,s') := s in x::sieve (filterp (not_div x) s').

CoFixpoint ns (n:Z) := n::ns (n+1).

Eval vm_compute in not_div 3 6.
Eval vm_compute in take 10 (sieve (ns 2)).

Parameter prime : Z -> Prop.

Parameter prime_exm : forall p, prime p \/ ~prime p.


Hypothesis prime_not_div : 
  forall x y, x <> 1 -> x < y -> prime y -> not_div x y = false.

Inductive insb (x : Z) : nat -> str -> Prop :=
  inf : forall s n, insb x n (x::s)
| inr : forall y n s', insb x n s' -> insb x (S n) (y::s').

Lemma Zabs_nat0 : forall x, Zabs_nat x = 0%nat -> x = 0.
intros x; case x; auto; intros p;
assert (h' := lt_O_nat_of_P p); simpl; omega.
Qed.

Lemma ns_in : forall x y, 0 <= x <= y ->
   insb y (Zabs_nat y - Zabs_nat x) (ns x).
assert (forall n x y, n = (Zabs_nat y - Zabs_nat x)%nat ->
              0 <= x <= y -> insb y n (ns x)).
  induction n.
    intros x y q int.
    rewrite <- Zabs_nat_Zminus in q;[ | assumption].
    assert (h' := Zabs_nat0 (y - x) (sym_equal q)).
    assert (h'' : x = y) by omega; rewrite h''.
  rewrite (force_eq (ns y)); simpl; apply inf.
  intros x y q int; rewrite force_eq; simpl.
  apply inr; apply IHn.
assert (h: (Zabs_nat y = Zabs_nat x + S n)%nat) by omega.
  rewrite h.
change (x+1) with (Zsucc x); rewrite Zabs_nat_Zsucc; omega.
split.
  omega.
case (Z_eq_dec x y).
  intros xy; rewrite xy, <- minus_n_n in q; discriminate.
intros; omega.
intros x y; apply H; reflexivity.
Qed.

Lemma filtern_bound :
  forall k s p x y s', insb x k s -> p x = true ->
     filtern p s k = (y::s') -> p y = true.
intros k s p x y s'; revert p y s'; induction 1 as [s n|z n s1 ix IH].
  destruct n.
    simpl; intros px q; injection q; intros q2 q1.
    rewrite <- q1; assumption.
  simpl; intros px; rewrite px; intros q; injection q; intros q2 q1.
  rewrite <- q1; assumption.
simpl; intros px; case_eq (p z); intros pz q; injection q.
  intros q2 q1; rewrite <- q1; assumption.
apply IH; assumption.
Qed.

Definition main_prop1 s :=
  exists x, insb x (Zabs_nat (hd s)) s /\ prime x.

CoInductive main_prop : str -> Prop :=
  mpc : forall a s, main_prop1 (a::s) -> main_prop s -> main_prop (a::s).

Axiom Bertrand_Chebyshev:
  forall n, 1 < n -> exists p, n <= p < 2 * n /\ prime p.

Lemma nsmp1 : forall n k, 1 < n -> Z_of_nat k <= n ->
  (forall x, n <= x < 2 * n - Z_of_nat k -> ~prime x) ->
  exists y, insb y k (ns (2*n- Z_of_nat k)) /\ prime y .
intros n; induction k as [ | k IH].
  intros ngt1 _ abs; destruct (Bertrand_Chebyshev _ ngt1) as [v [int pr]].
  case (abs v).
    simpl Z_of_nat; replace (2*n - 0) with (2*n) by ring; assumption.
  assumption.
rewrite inj_S; unfold Zsucc.

Admitted.

Lemma nsmp : forall n, main_prop (ns n).
cofix.
intros n; rewrite (force_eq (ns n)); simpl force.
constructor.