Set Primitive Projections.

(* Set Warnings "+cannot-define-projection".
(* Set Warnings "+non-primitive-record". *)
 *)
Require Import List.
Import ListNotations.

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

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

Module Record.

#[projections(primitive)]
Record product (A B : Type) : Type := Pair
{
  outl : A;
  outr : B;
}.

Arguments outl {A B} _.
Arguments outr {A B} _.

Lemma eq_product :
  forall {A B : Type} (p1 p2 : product A B),
    outl p1 = outl p2 -> outr p1 = outr p2 -> p1 = p2.
Proof.
  intros A B [a1 b1] [a2 b2]; cbn.
  now intros -> ->.
Qed.

End Record.

Module Inductive.

#[projections(primitive)]
Inductive product (A B : Type) : Type := Pair
{
  outl : A;
  outr : B;
}.

Arguments outl {A B} _.
Arguments outr {A B} _.

Lemma eq_product :
  forall {A B : Type} (p1 p2 : product A B),
    outl p1 = outl p2 -> outr p1 = outr p2 -> p1 = p2.
Proof.
  Fail intros A B [a1 b1] [a2 b2]; cbn.
Abort.

End Inductive.

Module CoInductive.

#[projections(primitive)]
CoInductive product (A B : Type) : Type := Pair
{
  outl : A;
  outr : B;
}.

Arguments outl {A B} _.
Arguments outr {A B} _.

Lemma eq_product :
  forall {A B : Type} (p1 p2 : product A B),
    outl p1 = outl p2 -> outr p1 = outr p2 -> p1 = p2.
Proof.
  Fail intros A B [a1 b1] [a2 b2]; cbn.
Abort.

End CoInductive.

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.
Admitted.
(*
  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.
*)

From Typonomikon Require Import F4.