F3: Strumienie [TODO]

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 :=
{
    hd : A;
    tl : Stream 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.

sapp

Zdefiniuj funkcję sapp, która skleja dwa strumienie. Czy taka funkcja w ogóle ma sens?
Zdefiniuj funkcję lsapp, która dokleja listę na początek strumienia.

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.


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).

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.


Hint Constructors Elem.


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).

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.


Lemma drop_tl :
  forall (A : Type) (n : nat) (s : Stream A),
    drop n (tl s) = drop (S 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.

Lemma Substream_tl :
  forall (A : Type) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (tl s1) (tl s2).

Lemma Substream_drop :
  forall (A : Type) (n : nat) (s1 s2 : Stream A),
    Substream s1 s2 -> Substream (drop n s1) (drop n s2).

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

Lemma Substream_drop_add :
  forall (A : Type) (n m : nat) (s1 s2 : Stream A),
    Substream s1 (drop n s2) -> Substream s1 (drop (n + m) s2).

Lemma Substream_trans :
  forall (A : Type) (s1 s2 s3 : Stream A),
    Substream s1 s2 -> Substream s2 s3 -> Substream s1 s3.

Lemma Substream_not_antisymm :
  exists (A : Type) (s1 s2 : Stream A),
    Substream s1 s2 /\ Substream s2 s1 /\ ~ sim s1 s2.


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 l : list A, s1 = lsapp l s2.


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),
    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ągna 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).

Strumienie za pomocą przybliżeń (TODO)


Module approx.

Print take.

Inductive Vec (A : Type) : nat -> Type :=
    | vnil : Vec A 0
    | vcons : forall n : nat, A -> Vec A n -> Vec A (S n).

Arguments vnil {A}.
Arguments vcons {A} {n}.

Definition vhd {A : Type} {n : nat} (v : Vec A (S n)) : A :=
match v with
    | vcons h _ => h
end.

Definition vtl {A : Type} {n : nat} (v : Vec A (S n)) : Vec A n :=
match v with
    | vcons _ t => t
end.

Require Import Program.Equality.

Lemma vhd_vtl :
  forall (A : Type) (n : nat) (v : Vec A (S n)),
    v = vcons (vhd v) (vtl v).

Fixpoint vtake {A : Type} (s : Stream A) (n : nat) : Vec A n :=
match n with
    | 0 => vnil
    | S n' => vcons (hd s) (vtake (tl s) n')
end.

Fixpoint vtake' {A : Type} (s : Stream A) (n : nat) : Vec A (S n) :=
match n with
    | 0 => vcons (hd s) vnil
    | S n' => vcons (hd s) (vtake' (tl s) n')
end.

CoFixpoint unvtake {A : Type} (f : forall n : nat, Vec A (S n)) : Stream A :=
{|
    hd := vhd (f 0);
    tl :=
      unvtake (fun n : nat => vtl (f (S n)))
|}.

Fixpoint vnth {A : Type} {n : nat} (v : Vec A n) (k : nat) : option A :=
match v, k with
    | vnil, _ => None
    | vcons h t, 0 => Some h
    | vcons h t, S k' => vnth t k'
end.

Ltac depdestr x :=
  let x' := fresh "x" in remember x as x'; dependent destruction x'.

Lemma unvtake_vtake' :
  forall (A : Type) (n : nat) (f : forall n : nat, Vec A (S n)),
    (forall m1 m2 k : nat, k <= m1 -> k <= m2 ->
      vnth (f m1) k = vnth (f m2) k) ->
       vtake' (unvtake f) n = f n.

Lemma vtake_unvtake :
  forall (A : Type) (s : Stream A),
    sim (unvtake (vtake' s)) s.

End approx.

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.