(* This module defines an equivalence relation
 * on type-terms.
 *
 * In general, we want distributivity of ladders
 * over all other type constructors, e.g. type-
 * specializations or function-types.
 *
 * Formally, we define two rewrite rules that
 * shall define how we are able to rewrite type-terms
 * such that they remain equivalent.
 *
 * (1) `-->distribute-ladder` which distributes
 *    ladder types over other type constructors, e.g.
 *    <S T~U>  -->distribute-ladder   <S T> ~ <S U>.
 *
 * (2) `-->condense-ladder` which does the
 *    inverse operation, e.g.
 *    <S T> ~ <S U>  -->condense-ladder  <S T~U>
 *
 * When applied exhaustively, each rewrite rule yields
 * a normal form, namely *Ladder Normal Form (LNF)*, which
 * is reached by exhaustive application of `-->distribute-ladder`,
 * and *Parameter Normal Form (PNF)*, which is reached by exhaustive
 * application of `-->condense-ladder`.
 *
 * The equivalence relation `===` over type-terms is then defined
 * as the reflexive and transitive hull over `-->distribute-ladder`
 * and `-->condense-ladder`. Since the latter two are the inverse
 * rewrite-step of each other, `===` is symmetric and thus `===`
 * satisfies all properties required of an equivalence relation.
 *)

Require Import terms.
Require Import subst.
From Coq Require Import Strings.String.

(** Alpha conversion in types *)

Reserved Notation "S '--->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop :=
  | TAlpha_Rename : forall x y t,
  (type_univ x t) --->α (type_univ y (type_subst x (type_var y) t))

  | TAlpha_SubUniv : forall x τ τ',
    (τ --->α τ') ->
    [< ∀x,τ >] --->α [< ∀x,τ' >]

  | TAlpha_SubSpec1 : forall τ1 τ1' τ2,
    (τ1 --->α τ1') ->
    [< <τ1 τ2> >] --->α [< <τ1' τ2> >]

  | TAlpha_SubSpec2 : forall τ1 τ2 τ2',
    (τ2 --->α τ2') ->
    [< <τ1 τ2> >] --->α [< <τ1 τ2'> >]

  | TAlpha_SubFun1 : forall τ1 τ1' τ2,
    (τ1 --->α τ1') ->
    [< τ1 -> τ2 >] --->α [< τ1' -> τ2 >]

  | TAlpha_SubFun2 : forall τ1 τ2 τ2',
    (τ2 --->α τ2') ->
    [< τ1 -> τ2 >] --->α [< τ1 -> τ2' >]

  | TAlpha_SubMorph1 : forall τ1 τ1' τ2,
    (τ1 --->α τ1') ->
    [< τ1 ->morph τ2 >] --->α [< τ1' ->morph τ2 >]

  | TAlpha_SubMorph2 : forall τ1 τ2 τ2',
    (τ2 --->α τ2') ->
    [< τ1 ->morph τ2 >] --->α [< τ1 ->morph τ2' >]

  | TAlpha_SubLadder1 : forall τ1 τ1' τ2,
    (τ1 --->α τ1') ->
    [< τ1 ~ τ2 >] --->α [< τ1' ~ τ2 >]

  | TAlpha_SubLadder2 : forall τ1 τ2 τ2',
    (τ2 --->α τ2') ->
    [< τ1 ~ τ2 >] --->α [< τ1 ~ τ2' >]

where "S '--->α' T" := (type_conv_alpha S T).

(** Alpha conversion is symmetric *)
Lemma type_alpha_symm :
  forall σ τ,
  (σ --->α τ) -> (τ --->α σ).
Proof.
  intros.
  induction H.
  - admit.
  - auto using TAlpha_Rename,type_subst,type_subst_symm, TAlpha_SubUniv.
  - auto using TAlpha_SubSpec1.
  - auto using TAlpha_SubSpec2.
  - auto using TAlpha_SubFun1.
  - auto using TAlpha_SubFun2.
  - auto using TAlpha_SubMorph1.
  - auto using TAlpha_SubMorph2.
  - auto using TAlpha_SubLadder1.
  - auto using TAlpha_SubLadder2.
Admitted.

(** Define all rewrite steps $\label{coq:type-dist}$ *)

Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_term -> type_term -> 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',
    (type_morph x (type_ladder y y'))
    -->distribute-ladder
    (type_ladder (type_morph x y) (type_morph x 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_term -> type_term -> 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).


(** 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.
  apply L_CondenseOverSpec1.
  apply L_CondenseOverSpec2.
  apply L_CondenseOverFun1.
  apply L_CondenseOverFun2.
  apply L_CondenseOverMorph1.
  apply L_CondenseOverMorph2.
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.
  apply L_DistributeOverSpec1.
  apply L_DistributeOverSpec2.
  apply L_DistributeOverFun1.
  apply L_DistributeOverFun2.
  apply L_DistributeOverMorph1.
  apply L_DistributeOverMorph2.
Qed.


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

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

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

  | 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_Alpha : forall x y,
    x --->α y ->
    x === y

  | 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_LadderAssocRL.
  apply TEq_LadderAssocLR.

  apply type_alpha_symm in H.
  apply TEq_Alpha.
  apply H.

  apply TEq_Condense.
  apply distribute_inverse.
  apply H.

  apply TEq_Distribute.
  apply condense_inverse.
  apply H.
Qed.

(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
  | FlatVar : forall x, (type_is_flat (type_var x))
  | FlatId : forall x, (type_is_flat (type_id x))
  | FlatApp : forall x y,
    (type_is_flat x) ->
    (type_is_flat y) ->
    (type_is_flat (type_spec x y))

  | FlatFun : forall x y,
    (type_is_flat x) ->
    (type_is_flat y) ->
    (type_is_flat (type_fun x y))

  | FlatSub : forall x v,
    (type_is_flat x) ->
    (type_is_flat (type_univ v x))
.

(** Ladder Normal Form:
    exhaustive application of -->distribute-ladder
 *)
Inductive type_is_lnf : type_term -> Prop :=
  | LNF : forall x : type_term,
  (not (exists y:type_term, x -->distribute-ladder y))
  -> (type_is_lnf x)
.

(** Parameter Normal Form:
    exhaustive application of -->condense-ladder
*)
Inductive type_is_pnf : type_term -> Prop :=
  | PNF : forall x : type_term,
  (not (exists y:type_term, x -->condense-ladder y))
  -> (type_is_pnf x)
.

(** Any term in LNF either is flat, or is a ladder T1~T2 where T1 is flat and T2 is in LNF *)
Lemma lnf_shape :
  forall τ:type_term,
  (type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_ladder τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2)))
.
Proof.
  intros τ H.
  induction τ.

  left.
  apply FlatId.
  
  left.
  apply FlatVar.
(*
  left.
  apply IHτ1 in H.
  apply FlatFun.
  apply H.
  destruct H.
  destruct H.
  
  apply IHτ1.
*)
  admit.
  admit.
  admit.
  admit.
Admitted.

(** every type has an equivalent LNF *)
Lemma lnf_normalizing :
  forall t, exists t', (t === t') /\ (type_is_lnf t').
Proof.
  intros.
  destruct t.

  exists (type_id s).
  split. apply TEq_Refl.
  apply LNF.
  admit.
  admit.
  admit.
  
  exists (type_univ s t).
  split.
  apply TEq_Refl.
  apply LNF.
  
Admitted.

(** every type has an equivalent PNF *)
Lemma pnf_normalizing :
  forall t, exists t', (t === t') /\ (type_is_pnf t').
Proof.
Admitted.

Lemma lnf_uniqueness :
  forall t t' t'',
  (t === t') /\ (type_is_lnf t') /\ (t === t'') /\ (type_is_lnf t'')
  -> t = t'.
Proof.
Admitted.





(**
 *  Examples
 *)

Example example_flat_type :
    type_is_flat [< <$"PosInt"$ $"10"$> >].
Proof.
    apply FlatApp.
    apply FlatId.
    apply FlatId.
Qed.

Example example_lnf_type :
    type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >].
Proof.
Admitted.

Example example_type_eq :
    [< [$"Char"$ ~ $"Byte"$] >]
    ===
    [< [$"Char"$] ~ [$"Byte"$] >]
.
Proof.
  apply TEq_Distribute.
  apply L_DistributeOverSpec2.
Qed.