F2: Strumienie [TODO]


Set Primitive Projections.
(* Set Warnings "+cannot-define-projection".
(* Set Warnings "+non-primitive-record". *) *)

W tym rozdziale będą ćwiczenia dotyczące strumieni, czyli ogólnie wesołe koinduktywne zabawy, o których jeszcze nic nie napisałem.

CoInductive Stream (A : Type) : Type := Cons
{
  hd : A;
  tl : Stream A;
}.

Arguments Cons {A}.
Arguments hd {A}.
Arguments tl {A}.

Bipodobieństwo


CoInductive sim {A : Type} (s1 s2 : Stream A) : Prop :=
{
  hds : hd s1 = hd s2;
  tls : sim (tl s1) (tl s2);
}.

Lemma sim_refl :
  forall (A : Type) (s : Stream A),
    sim s s.

Lemma sim_sym :
  forall (A : Type) (s1 s2 : Stream A),
    sim s1 s2 -> sim s2 s1.

Lemma sim_trans :
  forall (A : Type) (s1 s2 s3 : Stream A),
    sim s1 s2 -> sim s2 s3 -> sim s1 s3.

Require Import Setoid.

#[export]
Instance Equiv_sim (A : Type) : Equivalence (@sim A).

sapp

Zdefiniuj funkcję sapp, która skleja dwa strumienie. Czy taka funkcja w ogóle ma sens?

CoFixpoint sapp {A : Type} (s1 s2 : Stream A) : Stream A :=
{|
  hd := hd s1;
  tl := sapp (tl s1) s2;
|}.


Lemma sapp_pointless :
  forall (A : Type) (s1 s2 : Stream A),
    sim (sapp s1 s2) s1.

lsapp

Zdefiniuj funkcję lsapp, która dokleja listę na początek strumienia.


map

Zdefiniuj funkcję map, która aplikuje funkcję f : A -> B do każdego elementu strumienia.


Lemma map_id :
  forall (A : Type) (s : Stream A),
    sim (map (@id A) s) s.

Lemma map_map :
  forall (A B C : Type) (f : A -> B) (g : B -> C) (s : Stream A),
    sim (map g (map f s)) (map (fun x => g (f x)) s).

zipWith i unzip (TODO)

Zdefiniuj funkcję zipWith, która ze dwóch strumieni elementów A oraz B robi strumień elementów C, mając do dyspozycji funkcję f : A -> B -> C .
Następnie zdefiniuj funkcję unzip, która ze strumienia par robi parę strumieni wiadomo w jaki sposób.
Czy zipWithh pair i unzip są swoimi odwrotnościami?


Inne funkcje (TODO)

Zdefiniuj resztę przydatnych funkcji podobnych do tych, które są dostępne dla list: repeat, iterate, nth, take, drop, splitAt, insert, replace, scanl, scanr, intersperse, merge.
Zdefiniuj też funkcje, których zapomniałem (albo nie chciało mi się) wymienić.


Lemma merge_repeat :
  forall (A : Type) (x : A) (s : Stream A),
    sim (merge s (repeat x)) (intersperse x s).

(* TODO: uporządkować *)

Lemma sim_map :
  forall {A B : Type} (f : A -> B) (s1 s2 : Stream A),
    sim s1 s2 -> sim (map f s1) (map f s2).

Lemma sim_diagonal :
  forall {A : Type} (s1 s2 : Stream (Stream A)),
    sim s1 s2 -> sim (diagonal s1) (diagonal s2).

Compute take 10 (diagonal (map from (from 0))).
Compute take 10 (iterate (fun n => S (S n)) 0).

(* TODO *) Lemma diagonal_from :
  forall n : nat,
    sim
      (diagonal (map from (from n)))
      (iterate (fun n => S (S n)) n).

Lemma nth_insert :
  forall {A : Type} (n : nat) (x : A) (s : Stream A),
    nth n (insert n x s) = x.

Lemma nth_replace :
  forall {A : Type} (n : nat) (x : A) (s : Stream A),
    nth n (replace n x s) = x.

Lemma drop_map :
  forall {A B : Type} (f : A -> B) (n : nat) (s : Stream A),
    drop n (map f s) = map f (drop n s).

Lemma hd_drop :
  forall (A : Type) (n : nat) (s : Stream A),
    hd (drop n s) = nth n s.

Lemma tl_drop :
  forall (A : Type) (n : nat) (s : Stream A),
    tl (drop n s) = drop n (tl s).

Lemma nth_drop :
  forall (A : Type) (n m : nat) (s : Stream A),
    nth n (drop m s) = nth (n + m) s.

Lemma drop_drop :
  forall (A : Type) (n m : nat) (s : Stream A),
    drop m (drop n s) = drop (n + m) s.

(* TODO: take_map dla strumieni *)
(*
Lemma take_map :
  forall {A B : Type} (f : A -> B) (n : nat) (s : Stream A),
    take n (map f s) = D5.map f (take n s).
Proof.
  induction n as | n'; cbn; intros.
    reflexivity.
    rewrite IHn'. reflexivity.
Qed.
*)

Predykaty i relacje na strumieniach (TODO)

Zdefiniuj różne użyteczne predykaty i relacje podobne do tych listowych, w tym Elem, Dup, NoDup, Exists, Forall i wszystkie inne, o których zapomniałem.


#[global] Hint Constructors Elem : core.


Ltac inv H := inversion H; subst; clear H.

Require Import Arith.

Lemma Elem_nth :
  forall (A : Type) (x : A) (s : Stream A),
    Elem x s <-> exists n : nat, nth n s = x.

Lemma nth_from :
  forall n m : nat,
    nth n (from m) = n + m.

Lemma Elem_from_add :
  forall n m : nat,
    Elem n (from m) ->
      forall k : nat, Elem (k + n) (from m).

Require Import Lia.

Lemma Elem_from :
  forall n m : nat,
    Elem n (from m) <-> m <= n.

Lemma Dup_spec :
  forall (A : Type) (s : Stream A),
    Dup s <-> exists n m : nat, n <> m /\ nth n s = nth m s.

Lemma NoDup_from :
  forall n : nat,
    ~ Dup (from n).


Lemma Exists_spec :
  forall (A : Type) (P : A -> Prop) (s : Stream A),
    Exists P s <-> exists n : nat, P (nth n s).


Lemma Forall_spec :
  forall (A : Type) (s : Stream A) (P : A -> Prop),
    Forall s P <-> forall n : nat, P (nth n s).

Lemma Forall_spec' :
  forall (A : Type) (s : Stream A) (P : A -> Prop),
    Forall s P <-> forall x : A, Elem x s -> P x.

Lemma Forall_Exists :
  forall (A : Type) (P : A -> Prop) (s : Stream A),
    Forall s P -> Exists P s.

(*
(* begin hide *)
(* [projections(primitive = no)] *)
Variant SubstreamF {A : Type} (F : Stream A -> Stream A -> Prop) (s1 s2 : Stream A) : Prop :=
| MkSubstreamF :
    forall n : nat, hd s1 = nth n s2 -> F (tl s1) (drop (S n) s2) -> SubstreamF F s1 s2.
(*
{
  pos : nat;
  nth_pos_hd : hd s1 = nth pos s2;
  SubstreamT' : F (tl s1) (drop (S pos) s2);
}.
*)

CoInductive Substream {A : Type} (s1 s2 : Stream A) : Prop :=
{
  Substream_out : SubstreamT Substream s1 s2;
}.

CoInductive SubstreamT {A : Type} (s1 s2 : Stream A) : Type :=
{
  pos : nat;
  nth_pos_hd : hd s1 = nth pos s2;
  SubstreamT' : SubstreamT (tl s1) (drop (S pos) s2);
}.

Definition Substream {A : Type} (s1 s2 : Stream A) : Prop :=
  inhabited (SubstreamT s1 s2).
(* end hide *)

Lemma drop_tl :
  forall (A : Type) (n : nat) (s : Stream A),
    drop n (tl s) = drop (S n) s.
(* begin hide *)
Proof.
  reflexivity.
Qed.
(* end hide *)

Lemma Substream_tl :
  forall (A : Type) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (tl s1) (tl s2).
(* begin hide *)
Proof.
  intros A s1 s2 [n p [m q H]].
  rewrite nth_drop, <- plus_n_Sm in q.
  constructor; econstructor; now apply q |.
  now rewrite drop_drop, <- plus_n_Sm, plus_Sn_m, Nat.add_comm in H.
Qed.
(* end hide *)

Lemma Substream_tl_l :
  forall (A : Type) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (tl s1) s2.
(* begin hide *)
Proof.
  intros A s1 s2 [n p [m q H]].
  constructor; econstructor.
  - now rewrite q, nth_drop.
  - now rewrite drop_drop, Nat.add_comm, plus_Sn_m in H.
Qed.
(* end hide *)

Lemma Substream_drop :
  forall (A : Type) (n : nat) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (drop n s1) (drop n s2).
(* begin hide *)
Proof.
  induction n as | n'; cbn; intros; easy |.
  now apply IHn', Substream_tl.
Qed.
(* end hide *)

Lemma Substream_drop_l :
  forall (A : Type) (n : nat) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (drop n s1) s2.
(* begin hide *)
Proof.
  induction n as | n'; cbn; intros; easy |.
  now apply IHn', Substream_tl_l.
Qed.
(* end hide *)

Lemma Substream_refl :
  forall (A : Type) (s : Stream A),
    Substream s s.
(* begin hide *)
Proof.
  constructor; revert s.
  cofix CH.
  econstructor 1 with (pos := 0); cbn; easy |.
  now apply CH.
Qed.
(* end hide *)

Lemma Substream_trans :
  forall (A : Type) (s1 s2 s3 : Stream A),
    Substream s1 s2 -> Substream s2 s3 -> Substream s1 s3.
(* begin hide *)
Proof.
  intros A s1 s2 s3 H12 H23; constructor; revert s1 s2 s3 H12 H23.
  cofix CH.
  intros s1 s2 s3 n1 p1 H12' H23.
  destruct (Substream_drop _ n1 _ _ H23) as n2 p2 H2.
  econstructor 1 with (n := n1 + n2); cbn.
  - now rewrite Nat.add_comm, <- nth_drop, <- p2, hd_drop.
  - apply CH with (tl (drop n1 s2)).
    + now rewrite tl_drop.
    + now rewrite drop_tl, plus_n_Sm, <- drop_drop.
Qed.
(* end hide *)

Lemma Substream_not_antisymm :
  exists (A : Type) (s1 s2 : Stream A),
    Substream s1 s2 /\ Substream s2 s1 /\ ~ sim s1 s2.
(* begin hide *)
Proof.
  exists bool, (iterate negb true), (iterate negb false).
  repeat split.
  - econstructor 1 with (n := 1); cbn; easy |.
    now apply Substream_refl.
  - econstructor 1 with (n := 1); cbn; easy |.
    now apply Substream_refl.
  - intros [=] tls.
Qed.
(* end hide *)
*)


Fixpoint snoc {A : Type} (x : A) (l : list A) : list A :=
match l with
| nil => cons x nil
| cons h t => cons h (snoc x t)
end.

Lemma Suffix_spec :
  forall (A : Type) (s1 s2 : Stream A),
    Suffix s1 s2 <-> exists n : nat, s2 = drop n s1.


Lemma sim_Elem :
  forall (A : Type) (x : A) (s1 s2 : Stream A),
    sim s1 s2 -> Elem x s1 -> Elem x s2.

Lemma sim_Incl :
  forall (A : Type) (s1 s1' s2 s2' : Stream A),
    sim s1 s1' -> sim s2 s2' -> Incl s1 s2 -> Incl s1' s2'.

Lemma sim_SetEquiv :
  forall (A : Type) (s1 s1' s2 s2' : Stream A),
    sim s1 s1' -> sim s2 s2' -> SetEquiv s1 s2 -> SetEquiv s1' s2'.

Definition scons {A : Type} (x : A) (s : Stream A) : Stream A :=
{|
  hd := x;
  tl := s;
|}.

Permutacje strumieni

Zdefiniuj relację SPermutation, która jest analogiczna do relacji Permutation, którą znasz z list. Udowodnij jej specyfikację.


(* TODO *) Require Import Permutation.

Lemma lsapp_scons :
  forall (A : Type) (l : list A) (x : A) (s : Stream A),
    lsapp l (scons x s) = lsapp (snoc x l) s.

Lemma SPermutation_Permutation_lsapp :
  forall (A : Type) (l1 l2 : list A) (s1 s2 : Stream A),
    Permutation l1 l2 -> SPermutation s1 s2 ->
      SPermutation (lsapp l1 s1) (lsapp l2 s2).

Lemma take_drop :
  forall (A : Type) (n : nat) (s : Stream A),
    sim s (lsapp (take n s) (drop n s)).

Lemma take_add :
  forall (A : Type) (n m : nat) (s : Stream A),
    take (n + m) s = List.app (take n s) (take m (drop n s)).

Lemma SPermutation_spec :
  forall (A : Type) (s1 s2 : Stream A),
    SPermutation s1 s2 <->
    exists n : nat,
      Permutation (take n s1) (take n s2) /\
      drop n s1 = drop n s2.

Permutacje strumieni v2

Poprzedni podrozdział jest trochę lipny, bo tamtejsza definicja nie uchwytuje wszystkich możliwych permutacji strumieni - wymusza ona, żeby każda permutacja składa się z jedynie skończonej liczby przestawień.

CoFixpoint swap {A : Type} (s : Stream A) : Stream A :=
{|
  hd := hd (tl s);
  tl :=
  {|
    hd := hd s;
    tl := swap (tl (tl s));
  |}
|}.

Widać, że dla strumienia pokroju s = cocons 0 (cocons 1 (cocons 2 ...)) zdanie SPermutation s (swap s) nie zachodzi, bo przestawienia elementów ciągną się w nieskończoność.
Potrzebna jest nam zatem jakaś lepsza definicja permutacji.

Lemma SPermutation_not_swap :
  forall {A : Type} (s : Stream A),
    SPermutation s (swap s) -> sim s (swap s).

Pomysł dawno zapomniany: (ko)induktywne specyfikacje funkcji (TODO)


Inductive Filter {A : Type} (f : A -> bool) : Stream A -> Stream A -> Prop :=
| Filter_true :
    forall s r r' : Stream A,
      f (hd s) = true -> Filter f (tl s) r ->
        hd r' = hd s -> tl r' = r -> Filter f s r'
| Filter_false :
    forall s r : Stream A,
      f (hd s) = false -> Filter f (tl s) r -> Filter f s r.

Lemma Filter_bad :
  forall (A : Type) (f : A -> bool) (s r : Stream A),
    Filter f s r -> (forall x : A, f x = false) -> False.

CoInductive Filter' {A : Type} (f : A -> bool) (s r : Stream A) : Prop :=
{
  Filter'_true :
    f (hd s) = true -> hd s = hd r /\ Filter' f (tl s) (tl r);
  Filter'_false :
    f (hd s) = false -> Filter' f (tl s) r;
}.

Lemma Filter'_const_false :
  forall (A : Type) (s r : Stream A),
    Filter' (fun _ => false) s r.

Lemma Filter'_const_true :
  forall (A : Type) (s r : Stream A),
    Filter' (fun _ => true) s r -> sim s r.


Trochę losowości (TODO)


Require Import ZArith.

CoFixpoint rand (seed n1 n2 : Z) : Stream Z :=
{|
  hd := Zmod seed n2;
  tl := rand (Zmod seed n2 * n1) n1 n2;
|}.

CoFixpoint rand' (seed n1 n2 : Z) : Stream Z :=
{|
  hd := Zmod seed n2;
  tl := rand' (Zmod (seed * n1) n2) n1 n2;
|}.