(** Generic variable binding support *)

Require Import Arith Omega.
Require Import Max.

Set Implicit Arguments.

Definition var := nat.
Definition var_eq_dec := eq_nat_dec.

Ltac wrong := assert False; [idtac | tauto].

Section Contexts.
  Variable term : Set.

  Inductive context : Set :=
    | Empty : context
    | Bind : context -> var -> term -> context.

  Notation "G , x <: t" := (Bind G x t) (left associativity, at level 40).


  (** * Well-formedness *)

  Inductive inContext : var -> term -> context -> Prop :=
    | In_Eq : forall x t G, inContext x t (G, x <: t)
    | In_Neq : forall x t G x' t', inContext x t G
      -> inContext x t (G, x' <: t').

  Hint Constructors inContext.

  Notation "[ x <: t ] \in G" := (inContext x t G) (at level 50).

  Definition inDom x G := exists t, [x <: t] \in G.

  Notation "x \in G" := (inDom x G) (at level 50).

  Variable wfTerm : context -> term -> Prop.
  Notation "G |-- t 'ok'" := (wfTerm G t) (at level 50).

  Reserved Notation "|-- G 'ok'" (at level 50).

  Inductive wfContext : context -> Prop :=
    | WF_Empty : |-- Empty ok
    | WF_Bind : forall G x t,
      |-- G ok
      -> ~(x \in G)
      -> G |-- t ok
      -> |-- (G, x <: t) ok
  where "|-- G 'ok'" := (wfContext G).

  Hint Constructors wfContext.


  (** * Permutation and weakening *)

  Inductive insertInto : var -> term -> context -> context -> Prop :=
    | II_Head : forall x t G,
      G |-- t ok
      -> insertInto x t G (G, x <: t)
    | II_Skip : forall x t G x' t' G',
      insertInto x t G G'
      -> insertInto x t (G, x' <: t') (G', x' <: t').

  Hint Constructors insertInto.

  Inductive permute : context -> context -> Prop :=
    | PM_Empty : permute Empty Empty
    | PM_Bind : forall G x t G' G'',
      permute G G'
      -> insertInto x t G' G''
      -> permute (G, x <: t) G''.

  Hint Constructors permute.

  Lemma insertInto_inContext : forall x t G G',
    insertInto x t G G'
    -> forall x' t', [x' <: t'] \in (G, x <: t)
      -> [x' <: t'] \in G'.
    induction 1; intuition.

    inversion H0; subst; eauto.
    inversion H4; subst; eauto.
  Qed.

  Lemma permute_inContext : forall G D,
    permute G D
    -> forall x t, [x <: t] \in G
      -> [x <: t] \in D.
    induction 1; intuition.
    apply insertInto_inContext with x t G'; trivial.

    inversion H1; subst; auto.
  Qed.

  Lemma permute_inDom : forall G D,
    permute G D
    -> forall x, x \in G
      -> x \in D.
    unfold inDom.
    generalize permute_inContext.
    firstorder.
  Qed.

  Lemma permute_inDom_neg : forall G D,
    permute G D
    -> forall x, ~x \in D
      -> ~x \in G.
    generalize permute_inDom.
    firstorder.
  Qed.

  Hint Resolve permute_inContext permute_inDom permute_inDom_neg.

  Lemma insertInto_inContext' : forall x t G G',
    insertInto x t G G'
    -> forall x' t', [x' <: t'] \in G'
      -> [x' <: t'] \in (G, x <: t).
    induction 1; intuition.
    
    inversion H0; subst; eauto.
    generalize (IHinsertInto _ _ H4); intro Hin.
    inversion Hin; subst; auto.
  Qed.

  Lemma permute_inContext' : forall G D,
    permute G D
    -> forall x t, [x <: t] \in D
      -> [x <: t] \in G.
    induction 1; intuition.
    generalize (insertInto_inContext' H0 H1); intro Hin.
    
    inversion Hin; subst; auto.
  Qed.

  Lemma permute_inDom' : forall G D,
    permute G D
    -> forall x, x \in D
      -> x \in G.
    unfold inDom.
    generalize permute_inContext'.
    firstorder.
  Qed.

  Hint Resolve permute_inDom'.

  Hypothesis preweaken_wfTerm : forall G t,
    G |-- t ok
      -> forall D, (forall x, x \in G -> x \in D)
	-> D |-- t ok.

  Lemma permute_wfTy : forall G t,
    G |-- t ok
      -> forall D, permute G D
	-> D |-- t ok.
    eauto.
  Qed.

  Hint Resolve permute_wfTy.
  
  Lemma inDom_Bind : forall x t G,
    [x <: t] \in G
    -> forall x' t', [x <: t] \in G, x' <: t'.
    eauto.
  Qed.

  Lemma inContext_Bind : forall x G,
    x \in G
    -> forall x' t', x \in G, x' <: t'.
    generalize inDom_Bind.
    firstorder.
  Qed.

  Lemma inContext_Bind_neg : forall x G x' t',
    ~(x \in G, x' <: t')
    -> ~(x \in G).
    intros.
    intro.
    apply H.
    apply inContext_Bind; trivial.
  Qed.

  Hint Resolve inContext_Bind inContext_Bind_neg.

  Fixpoint weaken (G1 G2 : context) {struct G2} : context :=
    match G2 with
      | Empty => G1
      | G2', x <: t => (weaken G1 G2'), x <: t
    end.

  Infix "++" := weaken (left associativity, at level 40).

  Lemma weaken_inContext : forall G x t,
    [x <: t] \in G
    -> forall D, |-- (G ++ D) ok
      -> [x <: t] \in (G ++ D).
    induction D; simpl; auto.
    inversion 1; subst; auto.
  Qed.

  Lemma weaken_inDom : forall G x,
    x \in G
    -> forall D, |-- (G ++ D) ok
      -> x \in (G ++ D).
    generalize weaken_inContext; firstorder.
  Qed.

  Hint Resolve weaken_inContext weaken_inDom.

  Lemma permute_refl : forall G,
    |-- G ok
      -> permute G G.
    induction 1; eauto.
  Qed.

  Hint Resolve permute_refl.

  Lemma weaken_wfTy : forall G t,
    G |-- t ok
      -> forall D, |-- (G ++ D) ok
	-> G ++ D |-- t ok.
    eauto.
  Qed.

  Hint Resolve weaken_wfTy.

  Lemma insertInto_inContext2 : forall x t G G',
    insertInto x t G G'
    -> forall x' t', [x' <: t'] \in G
      -> [x' <: t'] \in G'.
    induction 1; intuition.

    inversion H0; subst; eauto.
  Qed.

  Hint Resolve insertInto_inContext2.

  Lemma insertInto_inDom : forall x t G G',
    insertInto x t G G'
    -> forall x', x' \in G
      -> x' \in G'.
    intros.
    destruct H0.
    red.
    eauto.
  Qed.

  Lemma insertInto_wfTy : forall x t G G',
    insertInto x t G G'
    -> |-- G ok
    -> forall t', G |-- t' ok
    -> G' |-- t' ok.
    eauto 6.
  Qed.

  Lemma insertInto_wfContext : forall x t G G',
    insertInto x t G G'
    -> |-- G ok
    -> ~x \in G
    -> |-- G' ok.
    induction 1; auto.
    inversion 1; subst.
    intro Hin.
    constructor; eauto.
    intro.
    destruct H1 as [t'' Ht''].
    generalize (insertInto_inContext' H Ht''); intro Hin'.
    inversion Hin'; subst.
    apply Hin; exists t'; auto.
    apply H5.
    exists t''; auto.
    
    eapply insertInto_wfTy; eauto.
  Qed.

  Hint Resolve insertInto_wfContext.

  Lemma permute_wfContext : forall G D,
    permute G D
    -> |-- G ok
    -> |-- D ok.
    induction 1; inversion 1; subst; eauto.
    eapply insertInto_wfContext; eauto.
  Qed.

  Hint Resolve permute_wfContext.

  Lemma split_inDom : forall x G y t,
    x \in G, y <: t
    -> x = y \/ (x \in G).
    intros.
    destruct H as [t' Ht'].
    inversion Ht'; subst; auto.
    right.
    exists t'; auto.
  Qed.

  Lemma head_inDom : forall x G t,
    x \in G, x <: t.
    intros.
    exists t; auto.
  Qed.

  Lemma cons_inDom : forall x G y t,
    x \in G
    -> x \in G, y <: t.
    intros.
    destruct H as [t' Ht'].
    exists t'; auto.
  Qed.

  Hint Resolve head_inDom cons_inDom.

  Lemma multiSwap : forall G x t D,
    |-- G ++ D ok
    -> ~x \in G ++ D
    -> G |-- t ok
    -> permute (G, x <: t ++ D) (G ++ D, x <: t).
    induction D; simpl; intuition.

    apply PM_Bind with (G ++ D, x <: t).
    inversion H; subst.
    apply IHD; eauto.
  
    inversion H; subst.
    eauto.
  Qed.

  Hint Resolve multiSwap.

  Lemma multiSwap' : forall G x t D,
    |-- G ++ D ok
    -> ~x \in G ++ D
    -> G |-- t ok
    -> permute (G ++ D, x <: t) (G, x <: t ++ D).
    induction D; simpl; intuition.

    apply PM_Bind with (G ++ D, v <: t0); auto.

    apply II_Skip.
    clear IHD H H0.
    induction D; simpl; intuition.
  Qed.

  Hint Resolve multiSwap'.

  Lemma move_wfContext : forall G t,
    G |-- t ok
    -> forall D, |-- G ++ D ok
    -> forall x, ~x \in G ++ D
    -> |-- G, x <: t ++ D ok.
    induction D; simpl; intuition.

    inversion H0; subst.
    constructor; eauto.
    intro.
    assert (v \in G ++ D, x <: t).
    apply permute_inDom with (G, x <: t ++ D); auto.

    destruct (split_inDom H3); subst; auto.

    apply preweaken_wfTerm with (G ++ D); intuition.
    apply permute_inDom with (G ++ D, x <: t); auto.
  Qed.

  Hint Resolve move_wfContext.

  Lemma weaken_inContext2 : forall x t G D,
    [x <: t] \in G ++ D
    -> [x <: t] \in G \/ [x <: t] \in D.
    induction D; simpl; intuition.
    inversion H; subst; eauto.
    intuition.
  Qed.

  Lemma weaken_inDom2 : forall x G D,
    x \in G ++ D
    -> x \in G \/ x \in D.
    generalize weaken_inContext2; firstorder.
  Qed.

  Lemma weaken_inContext3 : forall x t G D,
    [x <: t] \in G
    -> [x <: t] \in G ++ D.
    induction D; simpl; intuition.
  Qed.

  Lemma weaken_inDom3 : forall x G D,
    x \in G
    -> x \in G ++ D.
    generalize weaken_inContext3; firstorder.
  Qed.

  Lemma weaken_inContext4 : forall x t G D,
    [x <: t] \in D
    -> [x <: t] \in G ++ D.
    induction D; simpl; intuition.
    inversion H.
    inversion H; simpl; eauto.
  Qed.

  Lemma weaken_inDom4 : forall x G D,
    x \in D
    -> x \in G ++ D.
    generalize weaken_inContext4; firstorder.
  Qed.

  Hint Resolve weaken_inDom2 weaken_inDom3 weaken_inDom4.

  Lemma narrowing_wfTerm : forall G x t1 D t,
    G, x <: t1 ++ D |-- t ok
      -> forall t2, G, x <: t2 ++ D |-- t ok.
    intros.
    apply preweaken_wfTerm with (G, x <: t1 ++ D); intuition.
    destruct (weaken_inDom2 _ _ H0); eauto.
    destruct (split_inDom H1); subst; eauto.
  Qed.

  Hint Resolve narrowing_wfTerm.

  Lemma narrowing_inDom : forall v G x t1 D,
    v \in G, x <: t1 ++ D
    -> forall t2, v \in G, x <: t2 ++ D.
    induction D; simpl; intuition;
      destruct (split_inDom H); subst; eauto.
  Qed.

  Hint Resolve narrowing_inDom.

  Lemma narrowing_wfContext : forall G x t1 D,
    |-- G, x <: t1 ++ D ok
      -> forall t2, G |-- t2 ok
	-> |-- G, x <: t2 ++ D ok.
    intros.
    
    induction D; simpl in *; intuition.
    inversion H; subst; auto.
    
    inversion H; subst.
    constructor; eauto.
  Qed.

  Hint Resolve narrowing_wfContext.

  Lemma notBound_weaken : forall G x t D,
    |-- G, x <: t ++ D ok
      -> ~x \in G.
    induction D; simpl; intuition;
      inversion H; auto.
  Qed.

  Hint Resolve notBound_weaken.

  Lemma inContext_contra : forall x t G,
    [x <: t] \in G
    -> ~x \in G
    -> False.
    intros.
    apply H0.
    red.
    eauto.
  Qed.

  Hint Resolve inContext_contra.

  Lemma inContext_inDom : forall x t G,
    [x <: t] \in G
    -> x \in G.
    intros.
    red; eauto.
  Qed.

  Lemma wfContext_invert1 : forall G x t,
    |-- G, x <: t ok
      -> |-- G ok.
    inversion 1; trivial.
  Qed.
  
  Hint Resolve wfContext_invert1.

  Lemma squeeze_inContext : forall v G t D,
    [v <: t] \in G, v <: t ++ D.
    induction D; simpl; intuition.
  Qed.

  Lemma squeeze_inDom : forall v G t D,
    v \in G, v <: t ++ D.
    generalize squeeze_inContext; firstorder.
  Qed.

  Hint Resolve squeeze_inDom.

  Lemma narrowing_eq : forall x t D G t',
    |-- G, x <: t' ++ D ok
    -> [x <: t] \in G, x <: t' ++ D
    -> t = t'.
    induction D; simpl; intuition.
    
    inversion H0; subst; trivial.
    wrong.
    inversion H; eauto.

    inversion H0; subst; eauto.
    wrong.
    inversion H; subst.
    auto.
  Qed.

  Lemma weaken_bind_assoc : forall D G v t,
    G ++ (D, v <: t) = G ++ D, v <: t.
    induction D; simpl; intuition.
  Qed.

  Lemma wfContext_invert_weaken : forall D G,
    |-- G ++ D ok
      -> |-- G ok.
    induction D; intuition.
    rewrite weaken_bind_assoc in H.
    eauto.
  Qed.

  Hint Resolve wfContext_invert_weaken.

  Lemma narrowing_neq : forall x t G x' t' D,
    [x <: t] \in G, x' <: t' ++ D
    -> x <> x'
    -> forall t'', [x <: t] \in G, x' <: t'' ++ D.
    induction D; simpl; intuition;
      inversion H; subst; intuition.
  Qed.

  Hint Resolve narrowing_neq.

  Lemma switchBase_inDom : forall x G x' t D,
    (forall x0, x0 \in G -> x0 \in D)
    -> x \in G, x' <: t
    -> x \in D, x' <: t.
    intros.
    destruct (split_inDom H0); subst; eauto.
  Qed.

  Lemma switchTerm_inDom : forall x G x' t t',
    x \in G, x' <: t
    -> x \in G, x' <: t'.
    intros.
    destruct (split_inDom H); subst; eauto.
  Qed.

  Lemma switchWeaken_inDom' : forall D x G,
    x \in G ++ D
    -> forall G', (forall x, x \in G -> x \in G')
    -> x \in G' ++ D.
    induction D; simpl; intuition.
    destruct (split_inDom H); subst; eauto.
  Qed.

  Lemma switchWeaken_inDom : forall D x x' t G,
    x \in G, x' <: t ++ D
    -> forall t', x \in G, x' <: t' ++ D.
    intros.
    eapply switchWeaken_inDom'; eauto.
    intros.
    destruct (split_inDom H0); subst; eauto.
  Qed.
End Contexts.

Infix "++" := weaken (left associativity, at level 40).

Hint Constructors inContext wfContext insertInto permute.

Hint Resolve permute_inContext.
Hint Resolve weaken_inContext weaken_inContext2 weaken_inContext3 weaken_inContext4.

Hint Resolve permute_inDom weaken_inDom inContext_inDom.
Hint Resolve switchTerm_inDom switchBase_inDom switchWeaken_inDom.

Hint Resolve permute_wfContext move_wfContext wfContext_invert_weaken.

Hint Resolve multiSwap multiSwap'.

Hint Resolve narrowing_wfContext narrowing_neq.

Ltac narrowing_eq :=
  repeat match goal with
	   | [ H : inContext ?x0 ?u (Bind ?G ?x0 ?v ++ ?D) |- _ ] =>
	     assert (u = v);
	       [eapply narrowing_eq; eauto; fail
		 | subst; clear H]
	 end.

Ltac binding_simpl := repeat progress (simpl in *; narrowing_eq; subst; try discriminate).