coind.lean

import data.nat
open nat subtype function

inductive ltwo_tree_shape (X A : Type) :=
| inl {} : ltwo_tree_shape X A
| inm {} : A → X → ltwo_tree_shape X A
| inr {} : A → X → X → ltwo_tree_shape X A

local notation `shape` := ltwo_tree_shape

namespace ltwo_tree_shape
variables {A X : Type}
notation `⋆` := inl
notation `[`a`,` x `]₁` := inm a x
notation `[`a`,` x₁`,` x₂`]₂` := inr a x₁ x₂

definition is_inl : shape X A → Prop
| ⋆ := true
| _ := false

definition is_inm : shape X A → Prop
| [a, x]₁ := true
| _       := false

definition is_inr : shape X A → Prop
| [a, x₁, x₂]₂ := true
| _            := false

definition pr₁₁ [reducible] : Π {s : shape X A} (H : is_inm s), A
| ⋆             H := false.rec _ H
| [a, x]₁       H := a
| [a, x₁, x₂]₂  H := false.rec _ H

definition pr₁₂ [reducible] : Π {s : shape X A} (H : is_inm s), X
| ⋆             H := false.rec _ H
| [a, x]₁       H := x
| [a, x₁, x₂]₂  H := false.rec _ H

definition pr₂₁ [reducible] : Π {s : shape X A} (H : is_inr s), A
| ⋆             H := false.rec _ H
| [a, x]₁       H := false.rec _ H
| [a, x₁, x₂]₂  H := a

definition pr₂₂ [reducible] : Π {s : shape X A} (H : is_inr s), X
| ⋆             H := false.rec _ H
| [a, x]₁       H := false.rec _ H
| [a, x₁, x₂]₂  H := x₁

definition pr₂₃ [reducible] : Π {s : shape X A} (H : is_inr s), X
| ⋆             H := false.rec _ H
| [a, x]₁       H := false.rec _ H
| [a, x₁, x₂]₂  H := x₂
end ltwo_tree_shape
open ltwo_tree_shape

inductive l_two_tree_approx (A : Type) : ℕ → Type :=
| continue {} : l_two_tree_approx A 0
| nil {}      : Π {n : ℕ}, l_two_tree_approx A (n + 1)
| cons        : Π {n : ℕ}, A → l_two_tree_approx A n → l_two_tree_approx A (n + 1)
| cons₂       : Π {n : ℕ}, A → l_two_tree_approx A n → l_two_tree_approx A n →
                           l_two_tree_approx A (n + 1)
namespace l_two_tree_approx
variables {A B X : Type}

definition l_two_tree_approx0_eq_continue : Π (t: l_two_tree_approx A 0), t = continue
| continue := rfl

definition is_nil : Π {n : ℕ}, l_two_tree_approx A n → Prop
| is_nil nil             := true
| is_nil _               := false

definition is_cons : Π {n : ℕ}, l_two_tree_approx A n → Prop
| is_cons (cons _ _) := true
| is_cons _          := false

definition is_cons₂ : Π {n : ℕ}, l_two_tree_approx A n → Prop
| is_cons₂ (cons₂ _ _ _) := true
| is_cons₂ _             := false


/- head and tail -/

definition head [reducible] : Π {n : ℕ}, Π {t : l_two_tree_approx A (n + 1)} (H : is_cons t), A
| n nil             H := false.rec _ H
| n (cons a t)      H := a
| n (cons₂ a t₁ t₂) H := false.rec _ H

definition tail [reducible] : Π {n : ℕ}, Π {t : l_two_tree_approx A (n + 1)} (H : is_cons t), l_two_tree_approx A n
| n nil             H := false.rec _ H
| n (cons a t)      H := t
| n (cons₂ a t₁ t₂) H := false.rec _ H

definition head₂ : Π {n : ℕ}, Π {t : l_two_tree_approx A (n + 1)} (H : is_cons₂ t), A
| n nil             H := false.rec _ H
| n (cons a t)      H := false.rec _ H
| n (cons₂ a t₁ t₂) H := a

definition tail₂₁ : Π {n : ℕ}, Π {t : l_two_tree_approx A (n + 1)} (H : is_cons₂ t), l_two_tree_approx A n
| n  nil            H := false.rec _ H
| n (cons a t)      H := false.rec _ H
| n (cons₂ a t₁ t₂) H := t₁

definition tail₂₂ : Π {n : ℕ}, Π {t : l_two_tree_approx A (n + 1)} (H : is_cons₂ t), l_two_tree_approx A n
| n  nil            H := false.rec _ H
| n (cons a t)      H := false.rec _ H
| n (cons₂ a t₁ t₂) H := t₂

theorem tail1_eq_continue : Π {t : l_two_tree_approx A 1} (H : is_cons t), tail H = continue :=
begin intros, cases t, repeat (contradiction | apply l_two_tree_approx0_eq_continue) end

theorem tail₂₁1_eq_continue : Π {t : l_two_tree_approx A 1} (H : is_cons₂ t), tail₂₁ H = continue :=
begin intros, cases t, repeat (contradiction | apply l_two_tree_approx0_eq_continue) end

theorem tail₂₂1_eq_continue : Π {t : l_two_tree_approx A 1} (H : is_cons₂ t), tail₂₂ H = continue :=
begin intros, cases t, repeat (contradiction | apply l_two_tree_approx0_eq_continue) end

/- agreement -/

definition agrees : Π {n : ℕ}, l_two_tree_approx A n → l_two_tree_approx A (n + 1) → Prop
| 0 continue          _                  := true
| _ nil               nil                := true
| _ nil               _                  := false
| _ (cons a t₁)       (cons a t₂)        := agrees t₁ t₂
| _ (cons a t₁)       _                  := false
| _ (cons₂ a t₁₁ t₁₂)  (cons₂ a t₂₁ t₂₂) := agrees t₁₁ t₂₁ ∧ agrees t₁₂ t₂₂
| _ (cons₂ a₁ t₁ t₁') _                  := false

theorem is_nil_of_agrees : Π {n : ℕ}
  {t₁ : l_two_tree_approx A n} {t₂ : l_two_tree_approx A (n + 1)}
  (H : agrees t₁ t₂) (H' : is_nil t₁), is_nil t₂ :=
begin
  intros,
  repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction)
end

theorem is_cons_of_agrees : Π {n : ℕ}
  {t₁ : l_two_tree_approx A n} {t₂ : l_two_tree_approx A (n + 1)}
  (H : agrees t₁ t₂) (H' : is_cons t₁), is_cons t₂
:=
begin
  intros,
  repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction)
end

theorem is_cons₂_of_agrees : Π {n : ℕ}
  {t₁ : l_two_tree_approx A n} {t₂ : l_two_tree_approx A (n + 1)}
  (H : agrees t₁ t₂) (H' : is_cons₂ t₁), is_cons₂ t₂ :=
begin
  intros,
  repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction)
end

theorem agrees_tail : Π {n : ℕ}
  {t₁ : l_two_tree_approx A (n + 1)} {t₂ : l_two_tree_approx A (succ n + 1)}
  (H : agrees t₁ t₂) (H₁ : is_cons t₁) (H₂ : is_cons t₂), agrees (tail H₁) (tail H₂) :=
begin
  intros,
  repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction | apply H)
end

theorem agrees_tail₂₁ : Π {n : ℕ}
  {t₁ : l_two_tree_approx A (n + 1)} {t₂ : l_two_tree_approx A (succ n + 1)}
  (H : agrees t₁ t₂) (H₁ : is_cons₂ t₁) (H₂ : is_cons₂ t₂), agrees (tail₂₁ H₁) (tail₂₁ H₂) :=
begin
  intros,
  repeat (repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction);
          apply and.left H)
end

theorem agrees_tail₂₂ : Π {n : ℕ}
  {t₁ : l_two_tree_approx A (n + 1)} {t₂ : l_two_tree_approx A (succ n + 1)}
  (H : agrees t₁ t₂) (H₁ : is_cons₂ t₁) (H₂ : is_cons₂ t₂), agrees (tail₂₂ H₁) (tail₂₂ H₂) :=
begin
  intros,
  repeat (repeat (cases n | cases t₂ | apply trivial | cases t₁ | contradiction);
          apply and.right H)
end

/- map -/

definition map (f : A → B) : Π {n : ℕ}, l_two_tree_approx A n → l_two_tree_approx B n
| map continue        := continue
| map (@nil A n)      := nil
| map (cons a l)      := cons (f a) (map l)
| map (cons₂ a t₁ t₂) := cons₂ (f a) (map t₁) (map t₂)

/- corec -/

definition corec (f : X → shape X A) : Π (n : ℕ), X → l_two_tree_approx A n
| corec 0 x       := continue
| corec (n + 1) x :=
  match f x with
  | ⋆            := nil
  | [a, x₁]₁     := cons  a (corec n x₁)
  | [a, x₁, x₂]₂ := cons₂ a (corec n x₁) (corec n x₂)
  end

theorem agrees_corec {f : X → shape X A} {x : X} {n : ℕ} : agrees (corec f n x) (corec f (n + 1) x) :=
begin
  revert x,
  induction n with n IH:
  intro x,
  try trivial,
  unfold corec,
  cases (f x),
  repeat (trivial | split | apply IH)
end

theorem corec_f1x {f : X → shape X A} {x : X} : corec f 1 x =
  (ltwo_tree_shape.cases_on (f x) nil (λ a x₁, cons a continue) (λ a x₁ x₂, cons₂ a continue continue)):=
rfl

end l_two_tree_approx

definition l_two_tree (A : Type) : Type :=
{s : Π (n : ℕ), l_two_tree_approx A n | ∀ n, l_two_tree_approx.agrees (s n) (s (n + 1))}

namespace l_two_tree
variables {A B X : Type}

definition nth [reducible] (n : nat) (t : l_two_tree A) : l_two_tree_approx A n :=
elt_of t n

definition fst [reducible] (t : l_two_tree A) : l_two_tree_approx A 1 :=
nth 1 t

/- (pseudo) constructors -/

definition s_nil : ∀ n, l_two_tree_approx A n
| 0       := l_two_tree_approx.continue
| (n + 1) := @l_two_tree_approx.nil A n


theorem P_nil : ∀ n, l_two_tree_approx.agrees (@s_nil A n) (@s_nil A (n + 1)) :=
begin
  intro n,
  cases n,
  repeat trivial
end

definition nil : l_two_tree A := tag s_nil P_nil

definition s_cons (a : A) (t : l_two_tree A) : Π n, l_two_tree_approx A n
| 0       := l_two_tree_approx.continue
| (n + 1) := l_two_tree_approx.cons a (elt_of t n)

definition P_cons (a : A) (t : l_two_tree A) :
  ∀ n, l_two_tree_approx.agrees (s_cons a t n) (s_cons a t (n + 1)):=
begin
  intro n,
  cases n,
  repeat (trivial | apply has_property t)
end

definition cons : A → l_two_tree A → l_two_tree A :=
λ a t, tag (s_cons a t) (P_cons a t)

definition s_cons₂ (a : A) (t₁ t₂ : l_two_tree A) : Π n, l_two_tree_approx A n
| 0       := l_two_tree_approx.continue
| (n + 1) := l_two_tree_approx.cons₂ a (elt_of t₁ n) (elt_of t₂ n)

definition P_cons₂ (a : A) (t₁ t₂ : l_two_tree A) :
  ∀ n, l_two_tree_approx.agrees (s_cons₂ a t₁ t₂ n) (s_cons₂ a t₁ t₂ (n + 1)):=
begin
  intro n,
  cases n,
  repeat (trivial | apply has_property t₁ | apply has_property t₂ | split)
end

definition cons₂ : A → l_two_tree A → l_two_tree A → l_two_tree A :=
λ a t₁ t₂, tag (s_cons₂ a t₁ t₂) (P_cons₂ a t₁ t₂)

definition is_nil : l_two_tree A → Prop :=
λ t, l_two_tree_approx.is_nil (fst t)

theorem is_nil_of_forall (t : l_two_tree A)
  (H : ∀ n, l_two_tree_approx.is_nil (elt_of t (n + 1))) : is_nil t := H 0

theorem forall_is_nil {t : l_two_tree A} (H : is_nil t) (n : ℕ) :
  l_two_tree_approx.is_nil(elt_of t (n + 1)) :=
begin
  induction n with n IH:
  (exact H | exact l_two_tree_approx.is_nil_of_agrees (has_property t (n + 1)) IH)
end

definition is_cons : l_two_tree A → Prop :=
λ t, l_two_tree_approx.is_cons (fst t)

theorem is_cons_of_forall (t : l_two_tree A)
  (H : ∀ n, l_two_tree_approx.is_cons (elt_of t (n + 1))) : is_cons t := H 0

theorem forall_is_cons {t : l_two_tree A} (H : is_cons t) :
  ∀ n, l_two_tree_approx.is_cons (elt_of t (n + 1)) :=
begin
  intro n,
  induction n with n IH:
  (exact H | exact l_two_tree_approx.is_cons_of_agrees (has_property t (n + 1)) IH)
end

definition is_cons₂ : l_two_tree A → Prop :=
λ t, l_two_tree_approx.is_cons₂ (fst t)

theorem is_cons₂_of_forall (t : l_two_tree A)
  (H : ∀ n, l_two_tree_approx.is_cons₂ (elt_of t (n + 1))) : is_cons₂ t := H 0

theorem forall_is_cons₂ {t : l_two_tree A} (H : is_cons₂ t) :
  ∀ n, l_two_tree_approx.is_cons₂ (elt_of t (n + 1)) :=
begin
  intro n,
  induction n with n IH:
  (exact H | exact l_two_tree_approx.is_cons₂_of_agrees (has_property t (n + 1)) IH)
end

theorem is_nil_or_is_cons_or_is_cons₂ {t : l_two_tree A} : is_nil t ∨ is_cons t ∨ is_cons₂ t :=
begin
  cases t with elt prop,
  rewrite ↑[is_nil, is_cons, is_cons₂, fst, nth],
  cases (elt 1),
  repeat (append left (append right trivial)) ; now
end

/- head and tail -/

definition head {t : l_two_tree A} (H : is_cons t) : A :=
l_two_tree_approx.head H

definition s_tail {t : l_two_tree A} (H : is_cons t) : Π n, l_two_tree_approx A n :=
λ n, l_two_tree_approx.tail (forall_is_cons H _)

definition P_tail {t : l_two_tree A} (H : is_cons t) :
  ∀ n, l_two_tree_approx.agrees (s_tail H n) (s_tail H (n + 1)) :=
begin
  intro n,
  cases n with n : rewrite ↑s_tail,
  rewrite l_two_tree_approx.tail1_eq_continue, trivial,
  apply l_two_tree_approx.agrees_tail (has_property t (succ n + 1)) (forall_is_cons H (succ n)) (forall_is_cons H (succ (succ n)))
end

definition tail {t : l_two_tree A} (H : is_cons t) : l_two_tree A :=
tag (s_tail H) (P_tail H)

definition head₂ {t : l_two_tree A} (H : is_cons₂ t) : A :=
l_two_tree_approx.head₂ H

definition s_tail₂₁ {t : l_two_tree A} (H : is_cons₂ t) : Π n, l_two_tree_approx A n :=
λ n, l_two_tree_approx.tail₂₁ (forall_is_cons₂ H _)

definition P_tail₂₁ {t : l_two_tree A} (H : is_cons₂ t) :
  ∀ n, l_two_tree_approx.agrees (s_tail₂₁ H n) (s_tail₂₁ H (n + 1)) :=
begin
  intro n,
  cases n with n:
  rewrite ↑s_tail₂₁,
    {rewrite l_two_tree_approx.tail₂₁1_eq_continue,
      trivial},
    apply l_two_tree_approx.agrees_tail₂₁ (has_property t (succ n + 1)) (forall_is_cons₂ H (succ n)) (forall_is_cons₂ H (succ (succ n)))
end

definition tail₂₁ {t : l_two_tree A} (H : is_cons₂ t) : l_two_tree A :=
tag (s_tail₂₁ H) (P_tail₂₁ H)

definition s_tail₂₂ {t : l_two_tree A} (H : is_cons₂ t) : Π n, l_two_tree_approx A n :=
λ n, l_two_tree_approx.tail₂₂ (forall_is_cons₂ H _)

definition P_tail₂₂ {t : l_two_tree A} (H : is_cons₂ t) :
  ∀ n, l_two_tree_approx.agrees (s_tail₂₂ H n) (s_tail₂₂ H (n + 1)) :=
begin
  intro n,
  cases n with n:
  rewrite ↑s_tail₂₂,
    {rewrite l_two_tree_approx.tail₂₂1_eq_continue, trivial},
    apply l_two_tree_approx.agrees_tail₂₂ (has_property t (succ n + 1)) (forall_is_cons₂ H (succ n)) (forall_is_cons₂ H (succ (succ n)))
end

definition tail₂₂ {t : l_two_tree A} (H : is_cons₂ t) : l_two_tree A :=
tag (s_tail₂₂ H) (P_tail₂₂ H)

theorem head_cons (a : A) (t : l_two_tree A) : @head A (cons a t) trivial = a :=
by esimp

theorem tail_cons (a : A) (t : l_two_tree A) : @tail A (cons a t) trivial = t :=
by cases t; esimp

theorem s_eta₁ {t : l_two_tree A} (H : is_cons t) : s_cons (head H) (tail H) = elt_of t :=
funext (λ i,
  begin
    rewrite ↑s_cons,
    cases i with i:
    esimp,
      {symmetry; apply l_two_tree_approx.l_two_tree_approx0_eq_continue},
      rewrite ↑[head, tail, s_tail],
      rewrite ↑[is_cons, nth, fst] at H,
      exact sorry     -- TODO needs a simple lemma, eta rule for l_two_tree_approx
end)

theorem eta₁ {t : l_two_tree A} (H : is_cons t) : cons (head H) (tail H) = t :=
sorry -- TODO

theorem head₂_cons₂ (a : A) (t₁ t₂ : l_two_tree A) :
  @head₂ A (cons₂ a t₁ t₂) trivial = a :=
by rewrite ↑head₂

theorem tail₂₁_cons₂ (a : A) (t₁ t₂ : l_two_tree A) : @tail₂₁ A (cons₂ a t₁ t₂) trivial = t₁ :=
by cases t₁; cases t₂; esimp

theorem tail₂₂_cons₂ (a : A) (t₁ t₂ : l_two_tree A) : @tail₂₂ A (cons₂ a t₁ t₂) trivial = t₂ :=
by cases t₁; cases t₂; esimp

/- map -/
definition s_map (f : A → B) (t : l_two_tree A) : Π n, l_two_tree_approx B n :=
λ n, l_two_tree_approx.map f (elt_of t n)

definition P_map (f : A → B) (t : l_two_tree A) :
  ∀ n, l_two_tree_approx.agrees (s_map f t n) (s_map f t (n + 1)):=
sorry -- TODO

definition map : (A → B) → l_two_tree A → l_two_tree B :=
λ f t, tag (s_map f t) (P_map f t)

/- corec -/

definition s_corec (f : X → shape X A) (x : X) : ∀ n, l_two_tree_approx A n :=
λ n, l_two_tree_approx.corec f n x

definition P_corec (f : X → shape X A) (x : X) :
  ∀ n, l_two_tree_approx.agrees (s_corec f x n) (s_corec f x (n + 1)) :=
by intro n; apply l_two_tree_approx.agrees_corec

definition corec (f : X → shape X A) (x : X) : l_two_tree A :=
tag (s_corec f x) (P_corec f x)

definition unfolds (f : X → shape X A) (x : X) : l_two_tree A :=
corec f x


-- TODO prove the opposite direction for the theorems below

theorem is_inl_of_is_nil_corec {f : X → shape X A} {x : X} (H : is_nil (corec f x)) : is_inl (f x) :=
begin
  rewrite ↑[is_nil, fst, nth, corec, s_corec] at H,
  rewrite l_two_tree_approx.corec_f1x at H,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

theorem is_nil_corec_of_is_inm {f : X → shape X A} {x : X} (H : is_inl (f x)) : is_nil (corec f x) :=
begin
  rewrite ↑[is_nil, corec, fst, nth, s_corec],
  rewrite l_two_tree_approx.corec_f1x,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

theorem is_inm_of_is_cons_corec {f : X → shape X A} {x : X} (H : is_cons (corec f x)) : is_inm (f x) :=
begin
  unfold [is_cons, fst, nth, corec, s_corec] at H,
  rewrite l_two_tree_approx.corec_f1x at H,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

theorem is_cons_corec_of_is_inm {f : X → shape X A} {x : X} (H : is_inm (f x)) : is_cons (corec f x) :=
begin
  rewrite ↑[is_cons, corec, fst, nth, s_corec],
  rewrite l_two_tree_approx.corec_f1x,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

theorem is_inr_of_is_cons₂_corec {f : X → shape X A} {x : X} (H : is_cons₂ (corec f x)) : is_inr (f x) :=
begin
  rewrite ↑[is_cons₂, nth, fst, corec, s_corec] at H,
  rewrite l_two_tree_approx.corec_f1x at H,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

theorem is_cons₂_corec_of_is_inr {f : X → shape X A} {x : X} (H : is_inr (f x)) : is_cons₂ (corec f x) :=
begin
  rewrite ↑[is_cons₂, corec, fst, nth, s_corec],
  rewrite l_two_tree_approx.corec_f1x,
  revert H,
  cases (f x),
  repeat (intros ; (trivial | contradiction))
end

-- TODO shorten this proof (too many generalize)

theorem head_corec {f : X → shape X A} {x : X} (H : is_cons (corec f x)) : head H = pr₁₁ (is_inm_of_is_cons_corec H) :=
begin
  generalize is_inm_of_is_cons_corec H;
  revert H,
  unfold [head, pr₁₁, is_cons, fst, nth, corec, s_corec],
  rewrite l_two_tree_approx.corec_f1x,
  cases (f x),
  repeat (intros; reflexivity)
end
end l_two_tree