F1: Koindukcja i korekursja [TODO]



Require Import List.
Import ListNotations.

Require Import FunctionalExtensionality.
Require Import Setoid.
Require Import FinFun.

Require Import NArith.
Require Import Div2.
Require Import ZArith.

W tym rozdziale zgromadziłem sporo kodu dotyczącego koindukcji, ale nie zdążyłem jeszcze nic na jej temat napisać. Jeśli nie masz nic lepszego do roboty, to możesz samodzielnie wykminić, o co z nią chodzi, po prostu przyglądając się temu kodowi.

Koindukcja (TODO)

Strumienie (TODO)


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

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

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

Lemma bisim_refl :
  forall (A : Type) (s : Stream A), bisim s s.
Proof.
  cofix CH. constructor; auto.
Qed.

Lemma bisim_sym :
  forall (A : Type) (s1 s2 : Stream A),
    bisim s1 s2 -> bisim s2 s1.
Proof.
  cofix CH.
  destruct 1 as [hds tls]. constructor; auto.
Qed.

Lemma bisim_trans :
  forall (A : Type) (s1 s2 s3 : Stream A),
    bisim s1 s2 -> bisim s2 s3 -> bisim s1 s3.
Proof.
  cofix CH.
  destruct 1 as [hds1 tls1], 1 as [hds2 tls2].
  constructor; eauto. rewrite hds1. assumption.
Qed.

Jakieś pierdoły (TODO)


CoFixpoint from' (n : nat) : Stream nat :=
{|
    hd := n;
    tl := from' (S n);
|}.

CoFixpoint facts' (r n : nat) : Stream nat :=
{|
    hd := r;
    tl := facts' (r * S n) (S n);
|}.

Definition facts : Stream nat := facts' 1 0.

(*Compute stake 9 facts.*)

Przykład z manuala Agdy (TODO)

hd (evens s) := hd s; tl (evens s) := evens (tl (tl s));

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

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

Definition split {A : Type} (s : Stream A) : Stream A * Stream A :=
  (evens s, odds s).

CoFixpoint merge {A : Type} (ss : Stream A * Stream A) : Stream A :=
{|
    hd := hd (fst ss);
    tl := merge (snd ss, tl (fst ss));
|}.

Lemma merge_split :
  forall (A : Type) (s : Stream A),
    bisim (merge (split s)) s.
Proof.
  cofix CH.
  intros. constructor.
    cbn. reflexivity.
    cbn. constructor.
      cbn. reflexivity.
      cbn. apply CH.
Qed.

Bijekcja między Stream unit i unit (TODO)


Instance Equiv_bisim (A : Type) : Equivalence (@bisim A).

CoFixpoint theChosenOne : Stream unit :=
{|
    hd := tt;
    tl := theChosenOne;
|}.

Lemma all_chosen_unit_aux :
  forall s : Stream unit, bisim s theChosenOne.

Lemma all_chosen_unit :
  forall x y : Stream unit, bisim x y.

Axiom bisim_eq :
  forall (A : Type) (x y : Stream A), bisim x y -> x = y.

Theorem all_eq :
  forall x y : Stream unit, x = y.

Definition unit_to_stream (u : unit) : Stream unit := theChosenOne.
Definition stream_to_unit (s : Stream unit) : unit := tt.

Lemma unit_is_Stream_unit :
  Bijective unit_to_stream.

Trochę losowości (TODO)


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;
|}.

Fixpoint stake {A : Type} (n : nat) (s : Stream A) : list A :=
match n with
    | 0 => []
    | S n' => hd s :: stake n' (tl s)
end.

Compute stake 10 (rand 1 123456789 987654321).
Compute stake 10 (rand' 1235 234567890 6652).

Kolisty (TODO)


CoInductive Conat : Type :=
{
    pred : option Conat;
}.

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

Arguments uncons {A}.

Fixpoint tocoList {A : Type} (l : list A) : coList A :=
{|
    uncons :=
    match l with
        | [] => None
        | h :: t => Some (h, tocoList t)
    end
|}.

Lemma tocoList_inj :
  forall {A : Set} (l1 l2 : list A),
    tocoList l1 = tocoList l2 -> l1 = l2.
Proof.
  induction l1 as [| h1 t1]; destruct l2 as [| h2 t2]; cbn; inversion 1.
    reflexivity.
    f_equal. apply IHt1. assumption.
Defined.

CoFixpoint from (n : nat) : coList nat :=
{|
    uncons := Some (n, from (S n));
|}.

Definition lhead {A : Type} (l : coList A) : option A :=
match uncons l with
    | Some (a, _) => Some a
    | _ => None
end.

Definition ltail {A : Type} (l : coList A) : option (coList A) :=
match uncons l with
    | Some (_, t) => Some t
    | _ => None
end.

Fixpoint lnth {A : Type} (n : nat) (l : coList A) : option A :=
match n, uncons l with
    | _, None => None
    | 0, Some (x, _) => Some x
    | S n', Some (_, l') => lnth n' l'
end.

Eval compute in lnth 511 (from 0).

Definition nats := from 0.

CoFixpoint repeat {A : Type} (x : A) : coList A :=
{|
    uncons := Some (x, repeat x);
|}.

Eval cbn in lnth 123 (repeat 5).

CoFixpoint lapp {A : Type} (l1 l2 : coList A) : coList A :=
match uncons l1 with
    | None => l2
    | Some (h, t) => {| uncons := Some (h, lapp t l2) |}
end.

CoFixpoint lmap {A B : Type} (f : A -> B) (l : coList A) : coList B :=
{|
    uncons :=
    match uncons l with
        | None => None
        | Some (h, t) => Some (f h, lmap f t)
    end
|}.

Inductive Finite {A : Type} : coList A -> Prop :=
    | Finite_nil : Finite {| uncons := None |}
    | Finite_cons :
        forall (h : A) (t : coList A),
          Finite t -> Finite {| uncons := Some (h, t) |}.

CoInductive Infinite {A : Type} (l : coList A) : Prop :=
{
    h : A;
    t : coList A;
    p : uncons l = Some (h, t);
    inf' : Infinite t;
}.

Lemma empty_not_Infinite :
  forall A : Type, ~ Infinite {| uncons := @None (A * coList A) |}.
Proof.
  intros A []. cbn in p. inversion p.
Qed.

Lemma lmap_Infinite :
  forall (A B : Type) (f : A -> B) (l : coList A),
    Infinite l -> Infinite (lmap f l).
Proof.
  cofix CH.
  destruct 1. econstructor.
    cbn. rewrite p. reflexivity.
    apply CH. assumption.
Qed.

Lemma lapp_Infinite_l :
  forall (A : Type) (l1 l2 : coList A),
    Infinite l1 -> Infinite (lapp l1 l2).
Proof.
  cofix CH.
  destruct 1. econstructor.
    destruct l1; cbn in *; inversion p; cbn. reflexivity.
    apply CH. assumption.
Qed.

Lemma lapp_Infinite_r :
  forall (A : Type) (l1 l2 : coList A),
    Infinite l2 -> Infinite (lapp l1 l2).
Proof.
  cofix CH.
  destruct l1 as [[[h t] |]]; intros.
    econstructor.
      cbn. reflexivity.
      apply CH. assumption.
    destruct H. econstructor.
      lazy. destruct l2; cbn in *. rewrite p. reflexivity.
      assumption.
Qed.

Lemma Finite_not_Infinite :
  forall (A : Type) (l : coList A),
    Finite l -> ~ Infinite l.
Proof.
  induction 1; intro.
    inversion H. cbn in p. inversion p.
    apply IHFinite. inversion H0; inversion p; subst. assumption.
Qed.

CoInductive bisim2 {A : Type} (l1 l2 : coList A) : Prop :=
{
    bisim2' :
      uncons l1 = None /\ uncons l2 = None \/
      exists (h1 : A) (t1 : coList A) (h2 : A) (t2 : coList A),
        uncons l1 = Some (h1, t1) /\
        uncons l2 = Some (h2, t2) /\
          h1 = h2 /\ bisim2 t1 t2
}.

Hint Constructors bisim2.

Lemma bisim2_refl :
  forall (A : Type) (l : coList A), bisim2 l l.
Proof.
  cofix CH.
  destruct l as [[[h t]|]].
    constructor. right. exists h, t, h, t; auto.
    constructor. left. cbn. split; reflexivity.
Qed.

Lemma bisim2_symm :
  forall (A : Type) (l1 l2 : coList A),
    bisim2 l1 l2 -> bisim2 l2 l1.
Proof.
  cofix CH.
  destruct 1 as [[[] | (h1 & t1 & h2 & t2 & p1 & p2 & p3 & H)]].
    constructor. left. split; assumption.
    constructor. right. exists h2, t2, h1, t1. auto.
Qed.

Lemma bisim2_trans :
  forall (A : Type) (l1 l2 l3 : coList A),
    bisim2 l1 l2 -> bisim2 l2 l3 -> bisim2 l1 l3.
Proof.
  cofix CH.
  destruct 1 as [[[] | (h11 & t11 & h12 & t12 & p11 & p12 & p13 & H1)]],
           1 as [[[] | (h21 & t21 & h22 & t22 & p21 & p22 & p23 & H2)]];
  subst.
    auto.
    rewrite H0 in p21. inversion p21.
    rewrite H in p12. inversion p12.
    rewrite p12 in p21; inversion p21; subst.
      econstructor. right. exists h22, t11, h22, t22.
        do 3 try split; auto. eapply CH; eauto.
Qed.

Lemma lmap_compose :
  forall (A B C : Type) (f : A -> B) (g : B -> C) (l : coList A),
    bisim2 (lmap g (lmap f l)) (lmap (fun x => g (f x)) l).
Proof.
  cofix CH.
  constructor. destruct l as [[[h t]|]]; [right | left]; cbn.
    exists (g (f h)), (lmap g (lmap f t)),
           (g (f h)), (lmap (fun x => g (f x)) t).
      repeat (split; [reflexivity | idtac]). apply CH.
    do 2 split.
Qed.

Lemma bisim2_Infinite :
  forall (A : Type) (l1 l2 : coList A),
    bisim2 l1 l2 -> Infinite l1 -> Infinite l2.
Proof.
  cofix CH.
  destruct 1 as [[[] | (h1 & t1 & h2 & t2 & p1 & p2 & p3 & H)]], 1.
    rewrite H in p. inversion p.
    econstructor.
      exact p2.
      rewrite p1 in p. inversion p; subst. eapply CH; eauto.
Qed.

Drzewka (TODO)


CoInductive coBTree (A : Type) : Type :=
{
    root : option (coBTree A * A * coBTree A)
}.

Arguments root {A} _.

CoFixpoint fmap {A B : Type} (f : A -> B) (t : coBTree A) : coBTree B :=
{|
    root :=
    match root t with
        | None => None
        | Some (l, v, r) => Some (fmap f l, f v, fmap f r)
    end
|}.

CoFixpoint ns (n : nat) : coBTree nat :=
{|
    root := Some (ns (1 + 2 * n), n, ns (2 + 2 * n))
|}.

Inductive BTree (A : Type) : Type :=
    | Empty : BTree A
    | Node : A -> BTree A -> BTree A -> BTree A.

Arguments Empty {A}.
Arguments Node {A} _ _ _.

Fixpoint ttake (n : nat) {A : Type} (t : coBTree A) : BTree A :=
match n with
    | 0 => Empty
    | S n' =>
        match root t with
            | None => Empty
            | Some (l, v, r) => Node v (ttake n' l) (ttake n' r)
        end
end.

Compute ttake 5 (ns 0).

CoInductive tsim {A : Type} (t1 t2 : coBTree A) : Prop :=
{
    tsim' :
      root t1 = None /\ root t2 = None \/
      exists (v1 v2 : A) (l1 l2 r1 r2 : coBTree A),
        root t1 = Some (l1, v1, r1) /\
        root t2 = Some (l2, v2, r2) /\
          tsim l1 l2 /\ tsim r1 r2
}.

CoFixpoint mirror {A : Type} (t : coBTree A) : coBTree A :=
{|
    root :=
      match root t with
          | None => None
          | Some (l, v, r) => Some (mirror r, v, mirror l)
      end
|}.

Lemma tsim_mirror_inv :
  forall (A : Type) (t : coBTree A),
    tsim (mirror (mirror t)) t.
Proof.
  cofix CH.
  destruct t as [[[[l v] r]|]]; constructor; [right | left]. cbn.
    exists v, v, (mirror (mirror l)), l, (mirror (mirror r)), r. auto.
    auto.
Qed.

Rekursja ogólna (TODO)




Lemma Rev_Finite :
  forall (A : Type) (l r : coList A),
    Rev l r -> Finite r -> Finite l.

Lemma Rev_Finite :
  forall (A : Type) (l r : coList A),
    Rev l r -> Finite l -> Finite r.

Lemma Infinite_Rev :
  forall (A : Type) (l r : coList A),
    Rev l r -> Infinite l -> Infinite r.

Lemma Finite_cocons :
  forall (A : Type) (x : A) (l : coList A),
    Finite l -> Finite (cocons x l).

Fixpoint fromList {A : Type} (l : list A) : coList A :=
{|
    uncons :=
    match l with
        | [] => None
        | h :: t => Some (h, fromList t)
    end
|}.

Lemma fromList_inj :
  forall {A : Set} (l1 l2 : list A),
    fromList l1 = fromList l2 -> l1 = l2.

Ćwiczenia (TODO)

Ćwiczenie

Zdefiniuj typ potencjalnie nieskończonych drzew binarnych trzymających wartości typu A w węzłach, jego relację bipodobieństwa, predykaty "skończony" i "nieskończony" oraz funkcję mirror, która zwraca lustrzane odbicie drzewa. Udowodnij, że bipodobieństwo jest relacją równoważności i że funkcja mirror jest inwolucją (tzn. mirror (mirror t) jest bipodobne do t), która zachowuje właściwości bycia drzewem skończonym/nieskończonym. Pokaż, że drzewo nie może być jednocześnie skończone i nieskończone.


Ćwiczenie

Znajdź taką rodzinę typów koinduktywnych C, że dla dowolnego typu A, C A jest w bijekcji z typem funkcji nat -> A. Przez bijekcję będziemy tu rozumieć funkcję, która ma odwrotność, z którą w obie strony składa się do identyczności.
Uwaga: nie da się tego udowodnić bez użycia dodatkowych aksjomatów, które na szczęście są bardzo oczywiste i same się narzucają.


Ćwiczenie

Zdefiniuj pojęcie "nieskończonego łańcucha malejącego" (oczywiście za pomocą koindukcji) i udowodnij, że jeżeli relacja jest dobrze ufundowana, to nie ma nieskończonych łańcuchów malejących.