Require Import terms_debruijn.
Require Import Atom.
Require Import Metatheory.
Require Import FSetNotin.

(*
 * Substitution has no effect if the variable is not free
 *)
Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
  x `notin` (type_fv τ) ->
  ([ x ~> σ ] τ) = τ
.
Proof.
  intros.
  induction τ.

  - reflexivity.

  - unfold type_fv in H.
    apply AtomSetNotin.elim_notin_singleton in H.
    simpl.
    case_eq (x == a).
    congruence.
    reflexivity.

  - reflexivity.

  - simpl. rewrite IHτ.
    reflexivity.
    apply H.

  - simpl; rewrite IHτ1, IHτ2.
    reflexivity.
    simpl type_fv in H; fsetdec.
    simpl type_fv in H; fsetdec.

  - simpl. rewrite IHτ1, IHτ2.
    reflexivity.
    simpl type_fv in H; fsetdec.
    simpl type_fv in H; fsetdec.

  - simpl. rewrite IHτ1, IHτ2.
    reflexivity.
    simpl type_fv in H; fsetdec.
    simpl type_fv in H; fsetdec.

  - simpl. rewrite IHτ1, IHτ2.
    reflexivity.
    simpl type_fv in H; fsetdec.
    simpl type_fv in H; fsetdec.
Qed.



Lemma open_rec_lc_core : forall τ i σ1 j σ2,
  i <> j ->
  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
  ({j ~> σ2} τ) = τ.

Proof with eauto*.
  induction τ;
  intros i σ1 j σ2 Neq H.

  (* id *)
  - reflexivity.
  
  (* free var *)
  - reflexivity.
  
  (* bound var *)
  - simpl in *.
    destruct (j === n).
    destruct (i === n).
    3:reflexivity.

    rewrite e,e0 in Neq.
    contradiction Neq.
    reflexivity.

    rewrite H,e.
    simpl.
    destruct (n===n).
    reflexivity.
    contradict n1.
    reflexivity.

  (* univ *)
  - simpl in *.
    inversion H.
    f_equal.
    apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
    auto.
    apply H1.

  (* spec *)
  - simpl in *.
    inversion H.
    f_equal.
    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H1.
    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H2.

  (* func *)
  - simpl in *.
    inversion H.
    f_equal.
    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H1.
    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H2.


  (* morph *)
  - simpl in *.
    inversion H.
    f_equal.
    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H1.
    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H2.

  (* ladder *)
  - simpl in *.
    inversion H.
    f_equal.
    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H1.
    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
      auto.
      apply H2.

Qed.


Lemma type_open_rec_lc : forall k σ τ,
  type_lc τ ->
  ({ k ~> σ } τ) = τ
.
Proof.
  intros.
  generalize dependent k.
  induction H.

  (* id *)
  - auto.

  (* free var *)
  - auto.

  (* univ *)
  - simpl.
    intro k.
    f_equal.
    unfold type_open in *.
    pick fresh x for L.
    apply open_rec_lc_core with
      (i := 0) (σ1 := (ty_fvar x))
      (j := S k) (σ2 := σ).
    trivial.
    apply eq_sym, H0, Fr.

  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
Qed.

Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
  type_lc σ2 ->

  [x ~> σ2] ({k ~> σ1} τ)
  =
  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
Proof.
  induction τ;
  intros; simpl; f_equal; auto.

  (* free var *)
  - destruct (x == a).
    subst.
    apply eq_sym, type_open_rec_lc.
    assumption.
    trivial.

  (* bound var *)
  - destruct (k === n).
    reflexivity.
    trivial.
Qed.