F4: Kolisty [TODO]

Kolisty nie znaczy okrągły

Require Import D5.

Ten rozdział będzie o kolistach, czyli koinduktywnych odpowiednikach list różniących się od nich tym, że mogą być potencjalnie nieskończone.

CoInductive coList (A : Type) : Type :=
{
uncons : option (A * coList A);
}.

Arguments uncons {A}.

Przydatny będzie następujący, dość oczywisty fakt dotyczący równości kolist.

Lemma eq_uncons :
forall (A : Type) (l1 l2 : coList A),
uncons l1 = uncons l2 -> l1 = l2.

Bipodobieństwo

Zdefiniuj relację bipodobieństwa dla kolist. Udowodnij, że jest ona relacją równoważności. Z powodu konfliktu nazw bipodobieństwo póki co nazywać się będzie lsim.

Lemma lsim_refl :
  forall (A : Type) (l : coList A), lsim l l.

Lemma lsim_symm :
  forall (A : Type) (l1 l2 : coList A),
    lsim l1 l2 -> lsim l2 l1.

Lemma lsim_trans :
  forall (A : Type) (l1 l2 l3 : coList A),
    lsim l1 l2 -> lsim l2 l3 -> lsim l1 l3.

Przyda się też instancja klasy Equivalence, żebyśmy przy dowodzeniu o lsim mogli używać taktyk reflexivity, symmetry oraz rewrite.

Instance Equivalence_lsim (A : Type) : Equivalence (@lsim A).
Proof.
  esplit; red.
    apply lsim_refl.
    apply lsim_symm.
    apply lsim_trans.
Defined.

Różność

Przyda się też induktywna wersja relacji <>. Zdefiniuj ją i pokaż, że induktywna wersja implikuje zwykłą. Czy implikacja w drugą stronę zachodzi?

Inductive coList_neq
  {A : Type} : coList A -> coList A -> Prop :=
    | coList_neq_nc :
        forall l1 l2 : coList A,
          uncons l1 = None -> uncons l2 <> None -> coList_neq l1 l2
    | coList_neq_cn :
        forall l1 l2 : coList A,
          uncons l1 <> None -> uncons l2 = None -> coList_neq l1 l2
    | coList_neq_cc_here :
        forall (h1 h2 : A) (t1 t2 l1 l2 : coList A),
          uncons l1 = Some (h1, t1) ->
          uncons l2 = Some (h2, t2) ->
            h1 <> h2 -> coList_neq l1 l2
    | coList_neq_cc_there :
        forall (h1 h2 : A) (t1 t2 l1 l2 : coList A),
          uncons l1 = Some (h1, t1) ->
          uncons l2 = Some (h2, t2) ->
            coList_neq t1 t2 -> coList_neq l1 l2.

Lemma coList_neq_not_lsim :
  forall {A : Type} {l1 l2 : coList A},
    coList_neq l1 l2 -> ~ lsim l1 l2.

Lemma nlsim_neq :
  forall {A : Type} {l1 l2 : coList A},
    ~ lsim l1 l2 -> l1 <> l2.

Lemma coList_neq_antirefl :
  forall {A : Type} (l : coList A),
    ~ coList_neq l l.

Hint Constructors coList_neq : core.

Lemma coList_neq_sym :
  forall {A : Type} {l1 l2 : coList A},
    coList_neq l1 l2 -> coList_neq l2 l1.

conil i cocons

Zdefiniuj conil, czyli kolistę pustą, oraz cocons, czyli funkcję, która dokleja do kolisty nową głowę. Udowodnij, że cocons zachowuje i odbija bipodobieństwo.

Lemma lsim_cocons :
  forall (A : Type) (x y : A) (l1 l2 : coList A),
    x = y -> lsim l1 l2 -> lsim (cocons x l1) (cocons y l2).

Lemma lsim_cocons_inv :
  forall (A : Type) (x y : A) (l1 l2 : coList A),
    lsim (cocons x l1) (cocons y l2) -> x = y /\ lsim l1 l2.

len

Przygodę z funkcjami na kolistach zaczniemy od długości. Tak jak zwykła, induktywna lista ma długość wyrażającą się liczbą naturalną, tak też i długość kolisty można wyrazić za pomocą liczby konaturalnej.

Napisz funkcję len, która oblicza długość kolisty. Pokaż, że bipodobne kolisty mają tę samą długość. Długość kolisty pustej oraz coconsa powinny być oczywiste.

Require Import F2.

Lemma sim_len :
  forall (A : Type) (l1 l2 : coList A),
    lsim l1 l2 -> sim (len l1) (len l2).

Lemma len_conil :
  forall A : Type,
    len (@conil A) = zero.

Lemma len_cocons :
  forall (A : Type) (x : A) (l : coList A),
    len (cocons x l) = succ (len l).

snoc

Zdefiniuj funkcję snoc, która dostawia element na koniec kolisty.

Lemma snoc_cocons :
  forall (A : Type) (l : coList A) (x y : A),
    lsim (snoc (cocons x l) y) (cocons x (snoc l y)).

Lemma len_snoc :
  forall (A : Type) (l : coList A) (x : A),
    sim (len (snoc l x)) (succ (len l)).

app

Zdefiniuj funkcję app, która skleja dwie kolisty. Czy jest to w ogóle możliwe? Czy taka funkcja ma sens? Porównaj z przypadkiem sklejania strumieni.

Lemma app_conil_l :
  forall (A : Type) (l : coList A),
    app conil l = l.

Lemma app_conil_r :
  forall (A : Type) (l : coList A),
    lsim (app l conil) l.

Lemma app_cocons_l :
  forall (A : Type) (x : A) (l1 l2 : coList A),
    lsim (app (cocons x l1) l2) (cocons x (app l1 l2)).

Lemma len_app :
  forall (A : Type) (l1 l2 : coList A),
    sim (len (app l1 l2)) (add (len l1) (len l2)).

Lemma snoc_app :
  forall (A : Type) (l1 l2 : coList A) (x : A),
    lsim (snoc (app l1 l2) x) (app l1 (snoc l2 x)).

Lemma app_snoc_l :
  forall (A : Type) (l1 l2 : coList A) (x : A),
    lsim (app (snoc l1 x) l2) (app l1 (cocons x l2)).

Lemma app_assoc :
  forall (A : Type) (l1 l2 l3 : coList A),
    lsim (app (app l1 l2) l3) (app l1 (app l2 l3)).

lmap

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

TODO: wyklarować, dlaczego niektóre rzeczy mają "l" na początku nazwy

Lemma lmap_conil :
  forall (A B : Type) (f : A -> B),
    lmap f conil = conil.

Lemma lmap_cocons :
  forall (A B : Type) (f : A -> B) (x : A) (l : coList A),
    lsim (lmap f (cocons x l)) (cocons (f x) (lmap f l)).

Lemma len_lmap :
  forall (A B : Type) (f : A -> B) (l : coList A),
    sim (len (lmap f l)) (len l).

Lemma lmap_snoc :
  forall (A B : Type) (f : A -> B) (l : coList A) (x : A),
    lsim (lmap f (snoc l x)) (snoc (lmap f l) (f x)).

Lemma lmap_app :
  forall (A B : Type) (f : A -> B) (l1 l2 : coList A),
    lsim (lmap f (app l1 l2)) (app (lmap f l1) (lmap f l2)).

Lemma lmap_id :
  forall (A : Type) (l : coList A),
    lsim (lmap id l) l.

Lemma lmap_comp :
  forall (A B C : Type) (f : A -> B) (g : B -> C) (l : coList A),
    lsim (lmap g (lmap f l)) (lmap (fun x => g (f x)) l).

Lemma lmap_ext :
  forall (A B : Type) (f g : A -> B) (l : coList A),
    (forall x : A, f x = g x) -> lsim (lmap f l) (lmap g l).

iterate

Zdefiniuj funkcję iterate, która tworzy nieskończoną kolistę przez iterowanie funkcji f poczynając od pewnego ustalonego elementu.

Lemma len_iterate :
forall (A : Type) (f : A -> A) (x : A),
sim (len (iterate f x)) omega.

piterate

Zdefiniuj funkcję piterate, która tworzy kolistę przez iterowanie funkcji częściowej f : A -> option B poczynając od pewnego ustalonego elementu.

zipW

Zdefiniuj funkcję zipW, która bierze funkcję f : A -> B -> C oraz dwie kolisty l1 i l2 i zwraca kolistę, której elementy powstają z połączenia odpowiadających sobie elementów l1 i l2 za pomocą funkcji f.

Lemma zipW_conil_l :
  forall (A B C : Type) (f : A -> B -> C) (l : coList B),
    lsim (zipW f conil l) conil.

Lemma zipW_conil_r :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    sim (len (zipW f l1 l2)) (min (len l1) (len l2)).

Lemma len_zipW :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    sim (len (zipW f l1 l2)) (min (len l1) (len l2)).

scan

Napisz funkcję scan, która przekształca l : coList A w kolistę sum częściowych działania f : B -> A -> B.

Lemma scan_conil :
  forall (A B : Type) (f : B -> A -> B) (b : B),
    lsim (scan conil f b) conil.

Lemma scan_cocons :
  forall (A B : Type) (x : A) (l : coList A) (f : B -> A -> B) (b : B),
    lsim (scan (cocons x l) f b) (cocons b (scan l f (f b x))).

Lemma len_scan :
  forall (A B : Type) (l : coList A) (f : B -> A -> B) (b : B),
    sim (len (scan l f b)) (len l).

intersperse

Napisz funkcję intersperse, która działa analogicznie jak dla list.

Lemma intersperse_conil :
forall (A : Type) (x : A),
lsim (intersperse x conil) conil.

Pułapka: czy poniższe twierdzenie jest prawdziwe?

Lemma add_succ :
  forall n m : conat,
    sim (add (succ n) m) (succ (add n m)).
Proof.
  constructor. cbn.
  right. do 2 eexists. intuition.
Qed.

Lemma len_intersperse :
  forall (A : Type) (x : A) (l : coList A),
    sim (len (intersperse x l)) (succ (add (len l) (len l))).

splitAt

Napisz rekurencyjną funkcję splitAt. splitAt l n zwraca Some (begin, x, rest), gdzie begin jest listą reprezentującą początkowy fragment kolisty l o długości n, x to element l znajdujący się na pozycji n, zaś rest to kolista będącą tym, co z kolisty l pozostanie po zabraniu z niej l oraz x. Jeżeli l nie ma fragmentu początkowego o długości n, funkcja splitAt zwraca None.

Funkcji splitAt można użyć do zdefiniowania całej gamy funkcji działających na kolistach - rozbierających ją na kawałki, wstawiających, zamieniających i usuwających elementy, etc.

Definition nth {A : Type} (l : coList A) (n : nat) : option A :=
match splitAt l n with
    | None => None
    | Some (_, x, _) => Some x
end.

Definition take {A : Type} (l : coList A) (n : nat) : option (list A) :=
match splitAt l n with
    | None => None
    | Some (l, _, _) => Some l
end.

Definition drop {A : Type} (l : coList A) (n : nat) : option (coList A) :=
match splitAt l n with
    | None => None
    | Some (_, _, l) => Some l
end.

Fixpoint fromList {A : Type} (l : list A) : coList A :=
match l with
    | [] => conil
    | h :: t => cocons h (fromList t)
end.

Definition insert {A : Type} (l : coList A) (n : nat) (x : A)
  : option (coList A) :=
match splitAt l n with
    | None => None
    | Some (start, mid, rest) =>
        Some (app (fromList start) (cocons x (cocons mid rest)))
end.

Definition remove {A : Type} (l : coList A) (n : nat)
  : option (coList A) :=
match splitAt l n with
    | None => None
    | Some (start, _, rest) => Some (app (fromList start) rest)
end.

Finite i Infinite

Zdefiniuj predykaty Finite oraz Infinite, które są spełnione, odpowiednio, przez skończone i nieskończone kolisty. Zastanów się dobrze, czy definicje powinny być induktywne, czy koinduktywne.

Udowodnij, że niezaprzeczalnie każda kolista jest skończona lub nieskończona oraz że żadna kolista nie jest jednocześnia skończona i nieskończona.

Następnie udowodnij własności tych predykatów oraz sprawdź, które kolisty i operacje je spełniają.

Lemma Finite_or_Infinite_irrefutable :
  forall {A : Type} (l : coList A),
    ~ ~ (Finite l \/ Infinite l).

Lemma Finite_not_Infinite :
  forall (A : Type) (l : coList A),
    Finite l -> Infinite l -> False.

Lemma sim_Infinite :
  forall (A : Type) (l1 l2 : coList A),
    lsim l1 l2 -> Infinite l1 -> Infinite l2.

Lemma len_Finite :
  forall (A : Type) (l : coList A),
    Finite l -> len l <> omega.

Lemma len_Infinite :
  forall (A : Type) (l : coList A),
    len l = omega -> Infinite l.

Lemma len_Infinite_conv :
  forall (A : Type) (l : coList A),
    Infinite l -> sim (len l) omega.

Lemma Finite_snoc :
  forall (A : Type) (l : coList A) (x : A),
    Finite l -> Finite (snoc l x).

Lemma Infinite_snoc :
  forall (A : Type) (l : coList A) (x : A),
    Infinite l -> lsim (snoc l x) l.

Lemma Infinite_app_l :
  forall (A : Type) (l1 l2 : coList A),
    Infinite l1 -> Infinite (app l1 l2).

Lemma Infinite_app_r :
  forall (A : Type) (l1 l2 : coList A),
    Infinite l2 -> Infinite (app l1 l2).

Lemma Infinite_app :
  forall (A : Type) (l1 l2 : coList A),
    Infinite l1 \/ Infinite l2 -> Infinite (app l1 l2).

Lemma Finite_app :
  forall (A : Type) (l1 l2 : coList A),
    Finite l1 -> Finite l2 -> Finite (app l1 l2).

Hint Constructors Finite.

Lemma Finite_app_conv :
  forall (A : Type) (l1 l2 : coList A),
    Finite (app l1 l2) -> Finite l1 /\ Finite l2.

Lemma Finite_lmap :
  forall (A B : Type) (f : A -> B) (l : coList A),
    Finite l -> Finite (lmap f l).

Lemma Infinite_lmap :
  forall (A B : Type) (f : A -> B) (l : coList A),
    Infinite l -> Infinite (lmap f l).

Lemma Infinite_iterate :
  forall (A : Type) (f : A -> A) (x : A),
    Infinite (iterate f x).

Lemma piterate_Finite :
  forall (A : Type) (f : A -> option A) (x : A),
    Finite (piterate f x) -> exists x : A, f x = None.

Lemma Finite_zipW_l :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    Finite l1 -> Finite (zipW f l1 l2).

Lemma Finite_zipW_r :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    Finite l2 -> Finite (zipW f l1 l2).

Lemma Infinite_zipW_l :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    Infinite (zipW f l1 l2) -> Infinite l1.

Lemma Infinite_zipW_r :
  forall (A B C : Type) (f : A -> B -> C) (l1 : coList A) (l2 : coList B),
    Infinite (zipW f l1 l2) -> Infinite l1.

Lemma Infinite_splitAt :
  forall (A : Type) (n : nat) (l : coList A),
    Infinite l ->
      exists (start : list A) (x : A) (rest : coList A),
        splitAt l n = Some (start, x, rest).

Exists i Forall

Zdefiniuj predykaty Exists P oraz Forall P, które są spełnione przez kolisty, których odpowiednio jakiś/wszystkie elementy spełniają predykat P. Zastanów się dobrze, czy definicje powinny być induktywne, czy koinduktywne.

Sprawdź, które z praw de Morgana zachodzą.

Inductive Exists {A : Type} (P : A -> Prop) : coList A -> Prop :=
    | Exists_hd :
        forall (l : coList A) (h : A) (t : coList A),
          uncons l = Some (h, t) -> P h -> Exists P l
    | Exists_tl :
        forall (l : coList A) (h : A) (t : coList A),
          uncons l = Some (h, t) -> Exists P t -> Exists P l.

CoInductive All {A : Type} (P : A -> Prop) (l : coList A) : Prop :=
{
    All' :
      uncons l = None \/
      exists (h : A) (t : coList A),
        uncons l = Some (h, t) /\ P h /\ All P t;
}.

Lemma Exists_not_All :
  forall (A : Type) (P : A -> Prop) (l : coList A),
    Exists P l -> ~ All (fun x : A => ~ P x) l.

Lemma All_Exists :
  forall (A : Type) (P : A -> Prop) (l : coList A),
    All P l -> l = conil \/ Exists P l.