F4: Kolisty [TODO]


Set Primitive Projections.

Set Warnings "+cannot-define-projection".
Set Warnings "+non-primitive-record".

Kolisty nie znaczy okrągły


From Typonomikon 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.

Inductive CoListF (A : Type) (F : Type -> Type) : Type :=
| NilF : CoListF A F
| ConsF : forall (h : A) (t : F A), CoListF A F.

Arguments NilF {A F}.
Arguments ConsF {A F} _ _.

CoInductive CoList (A : Type) : Type :=
{
  uncons : CoListF A CoList
}.

Arguments uncons {A}.

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.

#[export]
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 = NilF -> uncons l2 <> NilF -> CoList_neq l1 l2
| CoList_neq_cn :
    forall l1 l2 : CoList A,
      uncons l1 <> NilF -> uncons l2 = NilF -> CoList_neq l1 l2
| CoList_neq_cc_here :
    forall (h1 h2 : A) (t1 t2 l1 l2 : CoList A),
      uncons l1 = ConsF h1 t1 ->
      uncons l2 = ConsF h2 t2 ->
        h1 <> h2 -> CoList_neq l1 l2
| CoList_neq_cc_there :
    forall (h1 h2 : A) (t1 t2 l1 l2 : CoList A),
      uncons l1 = ConsF h1 t1 ->
      uncons l2 = ConsF 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.

#[global] 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ść będą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.

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

(* [global] Hint Constructors lsimF : core. *)

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.
Uwaga: nazywamy tę funkcję lmap zamiast po prostu map, żeby uniknąć konfliktu nazw - nazwa map jest już zajętą przez analogiczną funkcję dla list.


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

Lemma scan_lmap :
  forall (A B C : Type) (f : B -> C -> B) (g : A -> C) (l : CoList A) (b : B),
    lsim (scan (lmap g l) f b) (scan l (fun b a => f b (g a)) b).

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 len_intersperse :
  forall (A : Type) (x : A) (l : CoList A),
    len l <> zero -> len l <> succ zero ->
      sim (len (intersperse x l)) ((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).

#[global] Hint Constructors Finite : core.

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 = ConsF h t -> P h -> Exists P l
| Exists_tl :
    forall (l : CoList A) (h : A) (t : CoList A),
      uncons l = ConsF h t -> Exists P t -> Exists P l.

CoInductive All {A : Type} (P : A -> Prop) (l : CoList A) : Prop :=
{
  All' :
    uncons l = NilF \/
    exists (h : A) (t : CoList A),
      uncons l = ConsF 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.

*)

(*



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 : Type} (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.
Admitted.
(*
  cofix CH.
  intros A l1 l2 Hinf.
  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.
Admitted.
(*
  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
}.

[global] Hint Constructors bisim2 : core. Lemma bisim2_refl : forall (A : Type) (l : coList A), bisim2 l l. Proof. Admitted. (* 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.
Admitted.
(*
  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 H0 in p. inversion p.
    econstructor.
      exact p2.
      rewrite p1 in p. inversion p; subst. eapply CH; eauto.
Qed.
*)

(*


(* begin hide *)
(** TODO: końcówka kolistowego burdla *)

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

(*
CoInductive Rev {A : Type} (l r : CoList A) : Prop :=
{
  Rev' :
    (uncons l = None /\ uncons r = None)
    \/
    exists (h : A) (tl tr : CoList A),
      uncons l = Some (h, tl) /\ r = snoc tr h /\ Rev tl tr
}.

Lemma Rev_wut :
  forall (A : Type) (l r : CoList A),
    Infinite l -> Infinite r -> Rev l r.
(* begin hide *)
Proof.
  cofix CH.
  constructor. right. destruct H, H0.
  exists h, t, r. split.
    assumption.
    split.
      apply eq_lsim. apply lsim_symm. apply Infinite_snoc. econstructor; eauto.
      apply CH; auto; econstructor; eauto.
Qed.
(* end hide *)

Lemma Rev_Finite :
  forall (A : Type) (l r : CoList A),
    Rev l r -> Finite r -> Finite l.
(* begin hide *)
Proof.
  intros A l r HRev H. revert l HRev.
  induction H as r H | h t r' H IH; intros.
    destruct HRev as [[H1 H2] | (h & tl & tr & H1 & H2 & H3)].
      left. assumption.
      subst. cbn in H. destruct (uncons tr) as []|; inv H.
    destruct HRev as [[H1 H2] | (h' & tl & tr & H1 & H2 & H3)].
      congruence.
      subst.
Abort.
(* end hide *)

Lemma Rev_Finite :
  forall (A : Type) (l r : CoList A),
    Rev l r -> Finite l -> Finite r.
(* begin hide *)
Proof.
  intros A l r HRev H. revert r HRev.
  induction H; intros.
    destruct HRev as [[H1 H2] | (h & tl & tr & H1 & H2 & H3)].
      left. assumption.
      subst. congruence.
    destruct HRev as [[H1 H2] | (h' & tl & tr & H1 & H2 & H3)].
      congruence.
      subst. rewrite H1 in H. inv H. apply Finite_snoc, IHFinite.
        assumption.
Qed.
(* end hide *)

Lemma Infinite_Rev :
  forall (A : Type) (l r : CoList A),
    Rev l r -> Infinite l -> Infinite r.
(* begin hide *)
Proof.
  cofix CH.
  destruct 1. (* decompose ex or and Revc0; clear Revc0.
    destruct 1. congruence.
    intro. subst. destruct x1 as [[h t] |]; cbn.
      econstructor.
        cbn. reflexivity.
        apply (CH _ (cocons x t)).
          constructor. cbn. right. exists x, t, t. auto.
      congruence.
      subst. cbn in *. inversion p; subst. *)
Abort.
(* end hide *)

Lemma Finite_cocons :
  forall (A : Type) (x : A) (l : CoList A),
    Finite l -> Finite (cocons x l).
(* begin hide *)
Proof.
  intros. apply (Finite_Some x l); auto.
Qed.
(* end hide *)

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.
(* begin hide *)
Proof.
  induction l1 as | h1 t1; destruct l2 as | h2 t2; cbn; inversion 1.
    reflexivity.
    f_equal. apply IHt1. assumption.
Defined.
*)
(* end hide *)
*)