From Coq Require Import Lists.List.
Import ListNotations.
Require Import Atom.
Require Import Metatheory.
Require Import FSetNotin.
Require Import debruijn.

(*
 * 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 ~tt~> σ ] τ) = τ
.
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.

(*
 * Substitution has no effect if the variable is not free
 *)
Lemma expr_subst_fresh : forall (x : atom) (t:expr_DeBruijn) (e:expr_DeBruijn),
  x `notin` (expr_fv e) ->
  ([ x ~ee~> t ] e) = e
.
Proof.
  intros.
  induction e.

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

  - reflexivity.

  - simpl. rewrite IHe.
    all: auto.

  - simpl; rewrite IHe.
    auto. auto.
  - simpl; rewrite IHe.
    auto. auto.
  - simpl; rewrite IHe.
    auto. auto.

  - simpl. rewrite IHe1, IHe2.
    reflexivity.
    simpl expr_fv in H; fsetdec.
    simpl expr_fv in H; fsetdec.

  - simpl. rewrite IHe1, IHe2.
    reflexivity.
    simpl expr_fv in H; fsetdec.
    simpl expr_fv in H; fsetdec.

  - simpl; rewrite IHe.
    auto. auto.
  - simpl; rewrite IHe.
    auto. auto.
Qed.


Lemma type_open_lc_core : forall (τ:type_DeBruijn) i (σ1:type_DeBruijn) j (σ2:type_DeBruijn),
  i <> j ->
  {i ~tt~> σ1} τ = {j ~tt~> σ2} ({i ~tt~> σ1} τ) ->
  ({j ~tt~> σ2} τ) = τ
.
Proof.
  induction τ;
  intros i σ1 j σ2 Neq H;
  simpl in *;
  inversion H;
  f_equal; eauto.

  (* 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.
Qed.


(*
 * opening is idempotent on locally closed types
 *)
Lemma type_open_lc : forall k σ τ,
  type_lc τ ->
  ({ k ~tt~> σ } τ) = τ
.
Proof.
  intros.
  generalize dependent k.
  induction H; eauto; simpl in *; intro k.

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

  (* rest *)
  all: rewrite IHtype_lc1; rewrite IHtype_lc2; reflexivity.
Qed.


(*
 * type substitution distributes over opening
 *)
Lemma type_subst_open : forall τ σ1 σ2 x k,
  type_lc σ2 ->

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

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

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








Lemma expr_open_lc_core : forall (t:expr_DeBruijn) i (s1:expr_DeBruijn) j (s2:expr_DeBruijn),
  i <> j ->
  {i ~ee~> s1} t = {j ~ee~> s2} ({i ~ee~> s1} t) ->
  ({j ~ee~> s2} t) = t
.
Proof.
  induction t;
  intros i s1 j s2 Neq H;
  simpl in *;
  inversion H;
  f_equal; eauto.

  (* 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.
Qed.


(*
 * opening is idempotent on locally closed expressions
 *)
Lemma expr_open_lc : forall k s t,
  expr_lc t ->
  ({ k ~ee~> s } t) = t
.
Proof.
  intros.
  generalize dependent k.
  induction H; eauto; simpl in *; intro k; f_equal; eauto.

  - unfold expr_open in *.
    pick fresh x for L.
    apply expr_open_lc_core with (i:=0) (s1:=(ex_fvar x)) (j:=S k) (s2:=s).
    discriminate.
    apply eq_sym, H1.
    assumption.

  - unfold expr_open in *.
    pick fresh x for L.
    apply expr_open_lc_core with (i:=0) (s1:=(ex_fvar x)) (j:=S k) (s2:=s).
    discriminate.
    apply eq_sym, H1.
    assumption.
Qed.

(*
 * type substitution distributes over opening
 *)
Lemma expr_subst_open : forall t s1 s2 x k,
  expr_lc s2 ->

  [x ~ee~> s2] ({k ~ee~> s1} t)
  =
  {k ~ee~> [x ~ee~> s2] s1} ([x ~ee~> s2] t).
Proof.
  induction t;
  intros; simpl; f_equal; auto.

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

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