Require Import terms_debruijn.

Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.

Reserved Notation "S '-->distribute-ladder' T" (at level 40).

Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
  | L_DistributeOverSpec1 : forall x x' y,
    [<  <x~x' y>  >]
    -->distribute-ladder
    [<  <x y>~<x' y>  >]

  | L_DistributeOverSpec2 : forall x y y',
    [<  <x y~y'>  >]
    -->distribute-ladder
    [<  <x y>~<x y'>  >]

  | L_DistributeOverFun1 : forall x x' y,
    [<  (x~x' -> y)  >]
    -->distribute-ladder
    [<  (x -> y) ~ (x' -> y)  >]

  | L_DistributeOverFun2 : forall x y y',
    [<  (x -> y~y')  >]
    -->distribute-ladder
    [<  (x -> y) ~ (x -> y')  >]

  | L_DistributeOverMorph1 : forall x x' y,
    [<  (x~x' ->morph y)  >]
    -->distribute-ladder
    [<  (x ->morph y) ~ (x' ->morph y)  >]

  | L_DistributeOverMorph2 : forall x y y',
    [<  x ->morph y~y'  >]
    -->distribute-ladder
    [<  (x ->morph y) ~ (x ->morph y')  >]

where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).


Reserved Notation "S '-->condense-ladder' T" (at level 40).
Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
  | L_CondenseOverSpec1 : forall x x' y,
    [< <x y>~<x' y> >]
    -->condense-ladder
    [< <x~x' y> >]

  | L_CondenseOverSpec2 : forall x y y',
    [< <x y>~<x y'> >]
    -->condense-ladder
    [< <x y~y'> >]

  | L_CondenseOverFun1 : forall x x' y,
    [< (x -> y) ~ (x' -> y) >]
    -->condense-ladder
    [< (x~x') -> y >]

  | L_CondenseOverFun2 : forall x y y',
    [< (x -> y) ~ (x -> y') >]
    -->condense-ladder
    [< (x -> y~y') >]

  | L_CondenseOverMorph1 : forall x x' y,
    [< (x ->morph y) ~ (x' ->morph y) >]
    -->condense-ladder
    [< (x~x' ->morph y) >]

  | L_CondenseOverMorph2 : forall x y y',
    [< (x ->morph y) ~ (x ->morph y') >]
    -->condense-ladder
    [< (x ->morph y~y') >]

where "S '-->condense-ladder' T" := (type_condense_ladder S T).

Create HintDb type_eq_hints.

Hint Constructors type_distribute_ladder : type_eq_hints.
Hint Constructors type_condense_ladder : type_eq_hints.

(** Inversion Lemma:
   `-->distribute-ladder` is the inverse of `-->condense-ladder
*)
Lemma distribute_inverse :
  forall x y,
  x -->distribute-ladder y ->
  y -->condense-ladder x.
Proof.
  intros.
  destruct H.
  all: auto with type_eq_hints.
Qed.

(** Inversion Lemma:
    `-->condense-ladder`  is the inverse of  `-->distribute-ladder`
*)
Lemma condense_inverse :
  forall x y,
  x -->condense-ladder y ->
  y -->distribute-ladder x.
Proof.
  intros.
  destruct H.
  all: auto with type_eq_hints.
Qed.


(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)

Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop :=
  | TEq_Refl : forall x,
    x === x

  | TEq_Trans : forall x y z,
    x === y ->
    y === z ->
    x === z

  | TEq_SubFun : forall x x' y y',
    x === x' ->
    y === y' ->
    [< x -> y >] === [< x' -> y' >]

  | TEq_SubMorph : forall x x' y y',
    x === x' ->
    y === y' ->
    [< x ->morph y >] === [< x' ->morph y' >]

  | TEq_LadderAssocLR : forall x y z,
    [< (x~y)~z >]
    ===
    [< x~(y~z) >]

  | TEq_LadderAssocRL : forall x y z,
    [< x~(y~z) >]
    ===
    [< (x~y)~z >]

  | TEq_Distribute : forall x y,
    x -->distribute-ladder y ->
    x === y

  | TEq_Condense : forall x y,
    x -->condense-ladder y ->
    x === y

where "S '===' T" := (type_eq S T).



(** Symmetry of === *)
Lemma TEq_Symm :
  forall x y,
  (x === y) -> (y === x).
Proof.
  intros.
  induction H.

  apply TEq_Refl.

  apply TEq_Trans with (y:=y).
  apply IHtype_eq2.
  apply IHtype_eq1.

  apply TEq_SubFun.
  auto. auto.
  apply TEq_SubMorph.
  auto. auto.
  apply TEq_LadderAssocRL.
  apply TEq_LadderAssocLR.

  apply TEq_Condense.
  apply distribute_inverse.
  apply H.

  apply TEq_Distribute.
  apply condense_inverse.
  apply H.
Qed.