From Tealeaves.Backends.Common Require Import
  Names AtomSet.
From Tealeaves Require Import
  Misc.NaturalNumbers
  Functors.Option
  Classes.Kleisli.DecoratedTraversableMonad.
From Tealeaves.Theory Require Import
  TraversableFunctor
  DecoratedTraversableMonad.

#[local] Generalizable Variable T.

Import DecoratedTraversableMonad.Notations.
Import DecoratedContainerFunctor.Notations.
Import AtomSet.Notations.
Open Scope tealeaves_scope.
Open Scope set_scope.

Import DecoratedTraversableMonad.UsefulInstances.

(** * Locally nameless leaves *)
(**********************************************************************)
Inductive leaf :=
| Fr: atom -> leaf
| Bd: nat -> nat -> leaf.
(* Bd group index, individual index *)

Theorem eq_dec_leaf: forall l1 l2: leaf, {l1 = l2} + {l1 <> l2}.
forall l1 l2 : leaf, {l1 = l2} + {l1 <> l2}
Proof.
forall l1 l2 : leaf, {l1 = l2} + {l1 <> l2}
  decide equality.
l1, l2: leaf
n, n0: atom
{n = n0} + {n <> n0}
l1, l2: leaf
n, n0, n1, n2: nat
a: n = n1
{n0 = n2} + {n0 <> n2}
l1, l2: leaf
n, n0, n1, n2: nat
{n = n1} + {n <> n1}
  -
l1, l2: leaf
n, n0: atom
{n = n0} + {n <> n0} compare values n and n0; auto.
  -
l1, l2: leaf
n, n0, n1, n2: nat
a: n = n1
{n0 = n2} + {n0 <> n2} compare values n and n0; auto.
l1, l2: leaf
n0, n2: nat
DESTR_EQs: n0 = n0
{n0 = n2} + {n0 <> n2}
l1, l2: leaf
n0, n1, n2: nat
DESTR_NEQs: n0 <> n1
DESTR_NEQ: n1 <> n0
{n0 = n2} + {n0 <> n2}
    compare values n0 and n2; auto.
l1, l2: leaf
n0, n1, n2: nat
DESTR_NEQs: n0 <> n1
DESTR_NEQ: n1 <> n0
{n0 = n2} + {n0 <> n2}
    compare values n0 and n2; auto.
  -
l1, l2: leaf
n, n0, n1, n2: nat
{n = n1} + {n <> n1} compare values n and n1; auto.
Qed.

#[export] Instance EqDec_leaf: EquivDec.EqDec leaf eq := eq_dec_leaf.

Fixpoint nth {A} (n: nat) (l: list A): option A :=
  match n, l with
  | O, x :: l' => Some x
  | O, other => None
  | S m, nil => None
  | S m, x :: t => nth m t
  end.

Lemma nth1: forall (A: Type) (n: nat), nth n (@nil A) = None.
forall (A : Type) (n : nat), nth n nil = None
Proof.
forall (A : Type) (n : nat), nth n nil = None
  intros.
A: Type
n: nat
nth n nil = None now induction n.
Qed.

Lemma nth2: forall (A: Type) (n: nat) (w: list A),
    Nat.compare n (length w) = Gt -> nth n w = None.
forall (A : Type) (n : nat) (w : list A),
Nat.compare n (length w) = Gt -> nth n w = None
Proof.
forall (A : Type) (n : nat) (w : list A),
Nat.compare n (length w) = Gt -> nth n w = None
  intros.
A: Type
n: nat
w: list A
H: Nat.compare n (length w) = Gt
nth n w = None generalize dependent n.
A: Type
w: list A
forall n : nat,
Nat.compare n (length w) = Gt -> nth n w = None induction w.
A: Type
forall n : nat,
Nat.compare n (length nil) = Gt -> nth n nil = None
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
forall n : nat,
Nat.compare n (length (a :: w)) = Gt ->
nth n (a :: w) = None
  -
A: Type
forall n : nat,
Nat.compare n (length nil) = Gt -> nth n nil = None intros.
A: Type
n: nat
H: Nat.compare n (length nil) = Gt
nth n nil = None now rewrite nth1.
  -
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
forall n : nat,
Nat.compare n (length (a :: w)) = Gt ->
nth n (a :: w) = None intros.
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
n: nat
H: Nat.compare n (length (a :: w)) = Gt
nth n (a :: w) = None destruct n.
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
H: Nat.compare 0 (length (a :: w)) = Gt
nth 0 (a :: w) = None
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
n: nat
H: Nat.compare (S n) (length (a :: w)) = Gt
nth (S n) (a :: w) = None
    +
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
H: Nat.compare 0 (length (a :: w)) = Gt
nth 0 (a :: w) = None cbv in H.
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
H: Lt = Gt
nth 0 (a :: w) = None inversion H.
    +
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
n: nat
H: Nat.compare (S n) (length (a :: w)) = Gt
nth (S n) (a :: w) = None cbn in *.
A: Type
a: A
w: list A
IHw: forall n : nat, Nat.compare n (length w) = Gt -> nth n w = None
n: nat
H: Nat.compare n (length w) = Gt
nth n w = None auto.
Qed.

Lemma nth3: forall (A: Type) (w: list A),
    nth (length w) w = None.
forall (A : Type) (w : list A),
nth (length w) w = None
Proof.
forall (A : Type) (w : list A),
nth (length w) w = None
  intros.
A: Type
w: list A
nth (length w) w = None induction w.
A: Type
nth (length nil) nil = None
A: Type
a: A
w: list A
IHw: nth (length w) w = None
nth (length (a :: w)) (a :: w) = None
  -
A: Type
nth (length nil) nil = None cbn.
A: Type
None = None reflexivity.
  -
A: Type
a: A
w: list A
IHw: nth (length w) w = None
nth (length (a :: w)) (a :: w) = None cbn.
A: Type
a: A
w: list A
IHw: nth (length w) w = None
nth (length w) w = None auto.
Qed.

(** * Operations for locally nameless *)
(**********************************************************************)

(** ** Local operations *)
(**********************************************************************)
Section local_operations.

  Context
    `{Return T}.

  Implicit Types (x: atom).

  Definition free_loc: leaf -> list atom :=
    fun l => match l with
             | Fr x => cons x List.nil
             | _ => List.nil
             end.

  Definition subst_loc x (u: T leaf): leaf -> T leaf :=
    fun l => match l with
             | Fr y => if x == y then u else ret (T := T) (Fr y)
             | Bd grp ix => ret (T := T) (Bd grp ix)
             end.

  Definition open_loc (binders: list (T leaf)): list nat * leaf -> option (T leaf) :=
    fun p => match p with
             | (w, l) =>
                 match l with
                 | Fr x => Some (ret (T := T) (Fr x))
                 | Bd grp ix =>
                     match Nat.compare grp (length w) with
                     | Lt => Some (ret (T := T) (Bd grp ix))
                     | Eq => nth ix binders
                     | Gt => Some (ret (T := T) (Bd (grp - 1) ix))
                     end
                 end
             end.

  Definition is_bound_or_free: list nat * leaf -> Prop :=
    fun p => match p with
             | (w, l) =>
                 match l with
                 | Fr x => True
                 | Bd grp ix =>
                     match nth grp w with
                     | Some size => ix < size
                     | None => False
                     end
                 end
             end.

End local_operations.

(** ** Lifted operations *)
(**********************************************************************)
Section LocallyNamelessOperations.

  Context
    (T: Type -> Type)
    `{DecoratedTraversableMonad (list nat)
    (op := @List.app nat) (unit := nil) T}.

  Definition open (binders: list (T leaf)): T leaf -> option (T leaf) :=
    binddt (T := T) (open_loc binders).


  Definition locally_closed: T leaf -> Prop :=
    fun t => forall w l, (w, l) ∈d t -> is_bound_or_free (w, l).

  Corollary open_respectful_id (us: list (T leaf)): forall (t: T leaf),
      (forall w a,
          (w, a) ∈d t -> open_loc us (w, a) = Some (ret (T := T) a)) ->
      binddt (open_loc us) t = pure t.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
us: list (T leaf)
forall t : T leaf,
(forall (w : list nat) (a : leaf),
 (w, a) ∈d t -> open_loc us (w, a) = Some (ret a)) ->
binddt (open_loc us) t = pure t
  Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
us: list (T leaf)
forall t : T leaf,
(forall (w : list nat) (a : leaf),
 (w, a) ∈d t -> open_loc us (w, a) = Some (ret a)) ->
binddt (open_loc us) t = pure t
    intros.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
us: list (T leaf)
t: T leaf
H0: forall (w : list nat) (a : leaf),
(w, a) ∈d t -> open_loc us (w, a) = Some (ret a)
binddt (open_loc us) t = pure t
    now apply (binddt_respectful_pure).
  Qed.

  Theorem correct: forall (t: T leaf) (us: list (T leaf)),
      locally_closed t -> open us t = Some t.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
forall (t : T leaf) (us : list (T leaf)),
locally_closed t -> open us t = Some t
  Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
forall (t : T leaf) (us : list (T leaf)),
locally_closed t -> open us t = Some t
    introv LC.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
LC: locally_closed t
open us t = Some t unfold locally_closed in LC.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
LC: forall (w : list nat) (l : leaf),
(w, l) ∈d t -> is_bound_or_free (w, l)
open us t = Some t
    apply open_respectful_id.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
LC: forall (w : list nat) (l : leaf),
(w, l) ∈d t -> is_bound_or_free (w, l)
forall (w : list nat) (a : leaf),
(w, a) ∈d t -> open_loc us (w, a) = Some (ret a)
    intros w l Hin.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
LC: forall (w : list nat) (l : leaf),
(w, l) ∈d t -> is_bound_or_free (w, l)
w: list nat
l: leaf
Hin: (w, l) ∈d t
open_loc us (w, l) = Some (ret l) specialize (LC w l Hin).
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
l: leaf
LC: is_bound_or_free (w, l)
Hin: (w, l) ∈d t
open_loc us (w, l) = Some (ret l)
    destruct l; cbn in LC.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n: atom
LC: True
Hin: (w, Fr n) ∈d t
open_loc us (w, Fr n) = Some (ret (Fr n))
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
open_loc us (w, Bd n n0) = Some (ret (Bd n n0))
    -
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n: atom
LC: True
Hin: (w, Fr n) ∈d t
open_loc us (w, Fr n) = Some (ret (Fr n)) reflexivity.
    -
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
open_loc us (w, Bd n n0) = Some (ret (Bd n n0)) cbn.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
match Nat.compare n (length w) with
| Eq => nth n0 us
| Lt => Some (ret (Bd n n0))
| Gt => Some (ret (Bd (n - 1) n0))
end = Some (ret (Bd n n0)) compare naturals n and (length w).
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n0: nat
ineqrw: PeanoNat.Nat.compare (length w) (length w) =
Eq
Hin: (w, Bd (length w) n0) ∈d t
LC: match nth (length w) w with
| Some size => n0 < size
| None => False
end
nth n0 us = Some (ret (Bd (length w) n0))
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
ineqrw: PeanoNat.Nat.compare n (length w) = Gt
ineqp: n > length w
n - 1 = n
      +
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n0: nat
ineqrw: PeanoNat.Nat.compare (length w) (length w) =
Eq
Hin: (w, Bd (length w) n0) ∈d t
LC: match nth (length w) w with
| Some size => n0 < size
| None => False
end
nth n0 us = Some (ret (Bd (length w) n0)) rewrite nth3 in LC.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n0: nat
ineqrw: PeanoNat.Nat.compare (length w) (length w) =
Eq
Hin: (w, Bd (length w) n0) ∈d t
LC: False
nth n0 us = Some (ret (Bd (length w) n0)) inversion LC.
      +
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
ineqrw: PeanoNat.Nat.compare n (length w) = Gt
ineqp: n > length w
n - 1 = n assert (lemma: nth n w = None) by auto using nth2.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: match nth n w with
| Some size => n0 < size
| None => False
end
Hin: (w, Bd n n0) ∈d t
ineqrw: PeanoNat.Nat.compare n (length w) = Gt
ineqp: n > length w
lemma: nth n w = None
n - 1 = n
        rewrite lemma in LC.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt (list nat) T T
H: DecoratedTraversableMonad (list nat) T
t: T leaf
us: list (T leaf)
w: list nat
n, n0: nat
LC: False
Hin: (w, Bd n n0) ∈d t
ineqrw: PeanoNat.Nat.compare n (length w) = Gt
ineqp: n > length w
lemma: nth n w = None
n - 1 = n inversion LC.
  Qed.

End LocallyNamelessOperations.