(********************************************************************
* Some General Useful Tactics for COQ v8.0pl3                       *
* Arthur Charguéraud, July 2006                                     *
********************************************************************)

(********************** Immediate Extensions ***********************)

Ltac sets H E := 
  set (H := E); clearbody H.
Ltac poses H :=
  let N := fresh "HU" in sets N H.
Ltac asserts H E :=
  assert (H : E).
Ltac splits :=
  repeat split.
Ltac destructs H :=
  let H1 := fresh "H" in let H2 := fresh "H" in first 
  [ destruct H as [H1 H2]; destructs H1 ; destructs H2 | idtac ].
Ltac inversions H :=
  inversion H; subst.
Ltac injections H :=
  injection H; clear H; intros; subst.
Ltac contradictions :=
  assert False; [ idtac | contradiction ].


(************************** Added Tactics **************************)

Ltac decide_equality := 
  match goal with |- {?X = ?Y} + {?X <> ?Y} 
  => decide equality X Y end.

Ltac func_equal := match goal with
  | [ |- (?F _ = ?F _ ) ] => apply (f_equal F)
  | [ |- (?F _ _ = ?F _ _) ] => apply (f_equal2 F)
  | [ |- (?F _ _ _ = ?F _ _ _) ] => apply (f_equal3 F)
  | [ |- (?F _ _ _ _ = ?F _ _ _ _) ] => apply (f_equal4 F)
  | _ => idtac
  end.

Ltac generalize_equality expr name := let equa := fresh in
  (set (name := expr); assert (equa : name = expr); 
  [ trivial | generalize name equa; clear name equa ]).


(********************** Maths Manipulations ************************)

Require Import Omega.

Tactic Notation "change_maths" constr(H1) "with" constr(H2) :=
  replace H1 with H2; [ idtac | omega ].

Tactic Notation "absurd_maths" :=
  assert False; [ omega | contradiction ].


(********************** Aggressive Automation **********************)

Tactic Notation "auto" "*" := 
  try solve [ auto | intuition (eauto 7) | simpl; auto ]. 
Tactic Notation "auto" "**" := 
  try solve [ intuition (eauto 8) ]. 
Tactic Notation "asserts" "*" ident(H) constr(E) :=
  assert (H : E); [ auto* | idtac ].
Tactic Notation "apply" "*" constr(H) := 
  first [ apply H | eapply H ]; auto*.
Tactic Notation "splits" "*" := 
  splits; auto*.
Tactic Notation "inversion" "*" constr(H) := 
  inversion H; auto*.
Tactic Notation "induction" "*" constr(H) := 
  induction H; auto*.
Tactic Notation "inversions" "*" constr(H) := 
  inversions H; auto*.
Tactic Notation "contradictions" "*" := 
   contradictions; auto*.
Tactic Notation "rewrite" "*" constr(H) := 
  rewrite H; auto*.
Tactic Notation "rewrite" "*" "<-" constr(H) := 
  rewrite <- H; auto*.
Tactic Notation "simpl" "*" := 
  simpl; auto*.
Tactic Notation "destruct" "*" constr(H) := 
  destruct H; auto*.
Tactic Notation "func_equal" "*" := 
  func_equal; auto*.

Ltac use expr :=
  poses expr; auto*.
Ltac use2 expr1 expr2 :=
  poses expr1; use expr2.
Ltac use3 expr1 expr2 expr3 :=
  poses expr1; poses expr2; use expr3.


(********************************************************************
* Properties of Subtyping in System-F                               *
* POPLmark Challegenge: part 1A + lemma A.10                        *
* Arthur Charguéraud, July 2006, in Coq v8.0pl3                     *
********************************************************************)

Set Implicit Arguments.
Require Import List. 

(********************** Variables and Indices **********************)

(* Variables, with decidable equality and a freshname generator *)

Definition var := nat.

Lemma eq_var_dec : forall (x y : var), {x = y} + {x <> y}.
decide equality.
Qed.

Notation "X 'notin' L" := (~ (In X L)) (at level 68).

Lemma fresh_sum_plus_one : forall X L, 

  In X L -> fold_right (fun R Y => S (Y + R)) 1 L > X.
induction L; simpl; intros; destruct H.
subst. omega. poses (IHL H). omega.
Qed.

Lemma fresh_exists : forall L, exists X : var, X notin L.
intros. set (X := fold_right (fun R Y => S (Y + R)) 1 L).
exists X. intro H. sets HX (fresh_sum_plus_one X L H).
unfold X in HX. omega.
Qed.

Notation "X == Y" := (eq_var_dec X Y) (at level 67).
Notation "i === j" := (eq_nat_dec i j) (at level 67).


(****************************** Types ******************************)

Inductive typ : Set :=
  | top   : typ
  | bvar  : nat -> typ
  | fvar  : var -> typ
  | arrow : typ -> typ -> typ
  | all   : typ -> typ -> typ.

Parameter typ_dummy : typ.


(************************** Substitution ***************************)

(* Substitution for indices *)

Fixpoint substb (k : nat) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | top         => top 
  | bvar i      => if (k === i) then U else (bvar i)
  | fvar X      => fvar X 
  | arrow T1 T2 => arrow (substb k U T1) (substb k U T2)
  | all T1 T2   => all (substb k U T1) (substb (1+k) U T2)
  end.

Notation "{ k ~> U } T" := (substb k U T) (at level 67).
Notation "T ^^ U" := (substb 0 U T) (at level 67).
Notation "T ^ X" := (substb 0 (fvar X) T).

(* Substitution for names *)

Fixpoint substf (Z : var) (U : typ) (T : typ) {struct T} : typ :=
  match T with
  | top         => top 
  | bvar i      => bvar i
  | fvar X      => if (Z == X) then U else (fvar X)
  | arrow T1 T2 => arrow (substf Z U T1) (substf Z U T2)
  | all T1 T2   => all (substf Z U T1) (substf Z U T2)
  end.

Notation "[ X ~> U ] T" := (substf X U T) (at level 68).


(************************** Environments ***************************)

Inductive env : Set :=
  | env_empty : env 
  | env_push  : env -> var -> typ -> env.

Notation "¤" := (env_empty) (at level 68).
Notation "E & X <: T" := (env_push E X T) (at level 68).

Inductive env_has : env -> var -> typ -> Prop :=
  | env_has_init : forall E X T, 
      env_has (E & X <: T) X T
  | env_has_push : forall E X Y T U, 
      env_has E X T -> env_has (E & Y <: U) X T.

Notation "E 'has' X <: T" := (env_has E X T) (at level 68).

Fixpoint dom (E : env) : list var := 
  match E with
  | ¤ => nil 
  | E & X <: U => X :: (dom E)
  end.

Notation "X '#' E" := (X notin (dom E)) (at level 68).


(************************* Well-Formation **************************)

Reserved Notation "E 'wf' T" (at level 68).

Inductive wfin : env -> typ -> Prop :=
  | wfin_top : forall E, 
      E wf top
  | wfin_fvar : forall E X U, 
      E has X <: U -> E wf (fvar X) 
  | wfin_arrow : forall E T1 T2,
      E wf T1 -> E wf T2 -> E wf (arrow T1 T2)
  | wfin_all : forall L E T1 T2,      
      E wf T1 ->  
      (forall Y V, Y notin L -> (E & Y <: V) wf (T2 ^ Y)) ->
      E wf (all T1 T2)

where "E 'wf' T" := (wfin E T).

Inductive ok : env -> Prop :=
  | ok_empty : ok env_empty
  | ok_push  : forall E X T, ok E -> X # E -> E wf T -> 
               ok (E & X <: T).


(************************ Subtyping Relation ***********************)

Notation "E 'oks' S 'and' T" := 
  (ok E /\ E wf S /\ E wf T) (at level 68).

Reserved Notation "E |- S <: T" (at level 68).

Inductive sub : env -> typ -> typ -> Prop :=
  | SA_top : forall E S, 
      E oks S and top ->
      E |- S <: top 
  | SA_refl_tvar : forall E X,
      E oks (fvar X) and (fvar X) ->
      E |- (fvar X) <: (fvar X)
  | SA_trans_tvar : forall E T U X, 
      E oks (fvar X) and T ->
      E has X <: U -> E |- U <: T ->
      E |- (fvar X) <: T 
  | SA_arrow : forall E S1 S2 T1 T2, 
      E oks (arrow S1 S2) and (arrow T1 T2) ->
      E |- T1 <: S1 -> E |- S2 <: T2 ->   
      E |- (arrow S1 S2) <: (arrow T1 T2)
  | SA_all : forall L E S1 S2 T1 T2, 
      E oks (all S1 S2) and (all T1 T2) ->
      E |- T1 <: S1 -> 
      (forall X, X notin L -> (E & X <: T1) |- S2 ^ X <: T2 ^ X) ->
      E |- (all S1 S2) <: (all T1 T2)

where "E |- S <: T" := (sub E S T).


(***************************** Tactics *****************************)

Hint Constructors env_has wfin ok sub.

(* Tactic used to compare two variables *)

Ltac case_var :=
  let destr X Y := destruct (X == Y); [try subst X | idtac] in
  match goal with
  | |- context [?X == ?Y]      => destr X Y  
  | H: context [?X == ?Y] |- _ => destr X Y 
  end.

Tactic Notation "case_var" "*" := case_var; auto*.

Ltac case_nat :=
  let destr i j := destruct (i === j); simpl in *; try case_nat in
  match goal with 
  | |- context [?i === ?j]      => destr i j
  | H: context [?i === ?j] |- _ => destr i j
  end.

Tactic Notation "case_nat" "*" := case_nat; auto*.


(**************** Tactics for Picking Fresh Names ******************)

Lemma fresh_cons : forall (X:var) Y L, 

  X notin Y :: L -> X <> Y /\ X notin L.
splits; intro; apply H; simpl*.
Qed.

Lemma fresh_append : forall (X:var) K L, 

  X notin K ++ L -> X notin K /\ X notin L.
splits; use in_or_app.
Qed.

Ltac simpl_fresh H :=
  let H1 := fresh "H" in let H2 := fresh "H" in
  let recurse :=
    clear H; try (simpl_fresh H1); try (simpl_fresh H2) in
  match type of H with 
  | _ notin _ :: _ => destruct (fresh_cons H) as [H1 H2]; recurse
  | ?X notin ?K ++ ?L => 
         destruct (fresh_append X K L H) as [H1 H2]; recurse
  end.

Tactic Notation "pick" ident(X) "notin" constr(L) :=
  let H := fresh "H" in 
  (destruct (fresh_exists L) as [X H]; try simpl_fresh H).

Ltac apply_SA_all X L :=
  let Fr := fresh "Fr" in (eapply (@SA_all L); 
  [ auto* | auto* | intros X Fr; simpl_fresh Fr; auto* ]).


(************** Properties of Well-formed Environments *************)

(* if X is fresh from E, then it is not bound in E *)

Lemma has_to_not_fresh : forall E X U,

  X # E -> E has X <: U -> False.
intros. induction E. inversion H0.
simpl in H. inversions* H0. 
Qed.

(* if E is well-formed and contains two bindings
   (X<:U) and (X<:V) then it must be that U = V *)

Lemma env_functional : forall X U V E, 

  ok E -> E has X <: U -> E has X <: V -> U = V.
induction 1; intros. inversion H.
inversion H2; inversion H3; subst; try solve 
[ auto | contradictions; apply* has_to_not_fresh ].
Qed.


(******************* Well-formed Free Variables ********************)

Definition substf_id Z U T := T = [Z ~> U]T.

Lemma substf_fresh_core : forall Z U Y T k, 

  {k ~> fvar Y}T = [Z ~> U]{k ~> fvar Y}T  ->  T = [Z ~> U]T.
induction T; simpl; intros k HE; inversion HE; func_equal*.
Qed.

(* if Z is fresh from E and T is well-formed in E,
   then T = [Z~>U]T. *)

Lemma substf_fresh : forall U T Z E, 

  Z # E -> E wf T -> substf_id Z U T.
unfold substf_id. intros U T Z E FR WF.
induction WF; simpl; func_equal*.
case_var*. contradictions. apply FR.
induction* H. simpl in *. auto*.
pick Y notin (Z :: L). apply* substf_fresh_core.
apply* (@H0 Y typ_dummy). simpl*.
Qed.

(* in the proof of narrowing, we will use:  T = [Z~>Z]T  *)

Lemma substf_self : forall Z T, T = [Z ~> fvar Z]T.
induction T; simpl; func_equal*. case_var*.
Qed.


(***************** Permutation of Substitutions ********************)

Lemma substb_on_wf_core : forall U V T i j, i <> j -> 

{i ~> U}({j ~> V}T) = {j ~> V}T  ->  {i ~> U}T = T.
induction T; intros; simpl in *; inversion H0; func_equal*.
case_nat*. absurd_maths. 
Qed.

Lemma substb_on_wf : forall E T U, 

  E wf T -> forall k, {k ~> U}T = T.
intros E T u WF. induction WF; intros; simpl; func_equal*.
pick X notin L. eapply substb_on_wf_core with (j := 0). 
omega. auto*.
Qed.

Lemma subst_permutation_ind : forall E X Y U T, 

  Y <> X -> E wf U -> forall k, 

  {k ~> fvar Y} ([X ~> U]T) = [X ~> U] ({k ~> fvar Y} T).
induction T; intros; simpl; func_equal*.
case_nat*. case_var*.
case_var*. apply* substb_on_wf.
Qed.

(* Permutation of a substitution from an index to a free 
   variable and a substitution from a name to a type     *)

Lemma subst_permutation : forall E X Y U T, Y <> X -> E wf U -> 

  ([X ~> U]T) ^ Y = [X ~> U] (T ^ Y).
use subst_permutation_ind.
Qed.


(******************* Extension of Environments *********************)

Definition extends E F := 
  forall X U, E has X <: U -> F has X <: U.

Notation "E 'inc' F" := (extends E F) (at level 68).

Hint Unfold extends.

Lemma extends_push : forall E F X T, 

  E inc F -> (E & X <: T) inc (F & X <: T).
unfold extends. intros. inversion* H0.
Qed.

Hint Resolve extends_push.


(***************** Preservation of Well-formation 1 ****************)

Lemma extends_wf_induction : forall E T, 

  E wf T -> forall F, E inc F -> F wf T.
intros E T H. induction* H.
Qed.

(* Extension of environments preserves well-formation *)

Lemma extends_wf : forall E F T, 

  E inc F -> E wf T -> F wf T.
use extends_wf_induction.
Qed.

(* Types extracted from a well-formed environment are 
   well-formed in that environment *)

Lemma env_has_wf : forall E X U, 

  ok E -> E has X <: U -> E wf U.
intros E X U Eok Has. induction Has;
inversion Eok; use extends_wf.
Qed.

Hint Resolve extends_wf env_has_wf.


(****************** Substitution in Environments *******************)

Definition env_subst Z P E F :=
  forall X U, E has X <: U -> X <> Z -> F has X <: ([Z ~> P]U).

Notation "F 'ext' [ Z ~> P ] E" := (env_subst Z P E F) (at level 68).

Lemma env_subst_push : forall Z P E F X T, X <> Z -> 

  F ext [Z ~> P]E -> (F & X <: [Z~>P]T) ext [Z ~> P] (E & X <: T).
unfold env_subst. intros. inversions* H1. 
Qed.

Hint Resolve env_subst_push.

Lemma env_subst_init_narrow : forall E Z P Q, ok E -> E wf Q -> 

  Z # E -> (E & Z <: P) ext [Z ~> fvar Z](E & Z <: Q).
unfold env_subst. intros. inversions H2. contradictions*.
rewrite* <- (@substf_fresh (fvar Z) U Z E).
Qed.

Lemma env_subst_init_subst : forall E Z P Q, ok E -> 

  Z # E -> E ext [Z ~> P](E & Z <: Q).
unfold env_subst. intros. inversions H1. contradictions*.
rewrite* <- (@substf_fresh P U Z E).
Qed.


(***************** Preservation of Well-formation 2 ****************)

(* Because we defined well-formation in an enviroment and
   not in a domain, we need to hack a little *)

Definition dom_subst Z E F :=
  forall X U, E has X <: U -> X <> Z -> exists V, F has X <: V.

Lemma dom_subst_push : forall E F Z X U,

  dom_subst Z E F -> dom_subst Z (E & X <: U) (F & X <: U).
unfold dom_subst. intros.
inversions* H0. destruct* (H X0 U0 H7 H1).
Qed.

Lemma dom_subst_wf : forall E Z P T, E wf T ->

  forall F, dom_subst Z E F -> F wf P -> F wf ([Z ~> P]T).
intros E Z P T WT. induction WT; intros F SUB WP; simpl; auto*.
case_var*. destruct* (SUB X U H).
apply (@wfin_all (Z :: L)). auto*. 
intros Y V Fr. simpl_fresh Fr. 
rewrite* (@subst_permutation F).
apply* H0. apply* dom_subst_push.
Qed.

Lemma subst_env_to_dom : forall Z P E F,

  F ext [Z ~> P]E -> dom_subst Z E F.
unfold env_subst, dom_subst. auto*.
Qed.

(* Preservation of well-formation through substitution *)

Lemma subst_wf : forall T Z P E F, F wf P -> 

  F ext [Z ~> P]E -> E wf T -> F wf ([Z ~> P]T).
intros. apply* (@dom_subst_wf E). apply* subst_env_to_dom.
Qed.

Hint Resolve subst_wf.


(************************** Lemmas ****************************)

(* if subtyping holds, then all its arguments are well-formed *)

Lemma sub_to_ok : forall E S T, E |- S <: T -> ok E.
intros. inversion* H. 
Qed.

Lemma sub_to_wf1 : forall E S T, E |- S <: T -> E wf S.
intros. inversion* H. 
Qed.

Lemma sub_to_wf2 : forall E S T, E |- S <: T -> E wf T.
intros. inversion* H. 
Qed.

Hint Resolve sub_to_ok sub_to_wf1 sub_to_wf2.


(************************** Main Proofs ****************************)

Lemma sub_reflexivity : forall T E, 

  ok E -> E wf T -> E |- T <: T.
intros. induction H0; intros; auto*.
apply_SA_all X (L ++ dom E). 
Qed.

Lemma sub_extension : forall E S T,

  E |- S <: T -> forall F, E inc F -> ok F -> F |- S <: T.
intros E S T H. induction H; intros F INC OK; auto**.
apply_SA_all X (L ++ dom F). 
Qed.

Definition sub_trans_prop E Q (WQ : E wf Q) := forall F S T, 
  E inc F -> F |- S <: Q -> F |- Q <: T -> F |- S <: T.

Hint Unfold sub_trans_prop.

Lemma sub_subst : forall F0 Q (WQ : F0 wf Q) E Z P S T,

  sub_trans_prop WQ -> F0 |- P <: Q -> substf_id Z P Q -> 

  E has Z <: Q -> E |- S <: T -> 

  forall F, ok F -> F0 inc F -> F ext [Z ~> P]E ->

  F |- [Z ~> P]S <: [Z ~> P]T.
intros F0 Q WQ E Z P S T TransQ PsubQ idQ FhasZQ H.
induction H; intros F Fok EincF FrelE; simpl;
destruct H as [OK [WS WT]]; 
(assert (F0 wf P); [ auto* | idtac ]).
  (* Case SA-refl-top *)
apply* SA_top.
  (* Case SA-refl-tvar *)
inversions WS; inversions WT.
case_var; apply* sub_reflexivity.
  (* Case SA-trans-tvar *)
inversions WS. case_var.
apply* TransQ. apply* sub_extension.
rewrite idQ. rewrite* (@env_functional X Q U E). 
eapply SA_trans_tvar with (U := [Z~>P]U); auto*.
  (* Case SA-arrow *)
apply* SA_arrow.
   (* Case SA-all *)
sets WFS (@subst_wf (all S1 S2)). simpl in WFS.
sets WFT (@subst_wf (all T1 T2)). simpl in WFT.
apply_SA_all X (Z::(dom E)++(dom F)++L). 
do 2 (rewrite (@subst_permutation F); eauto). 
apply H2; eauto. 
Qed.

Lemma sub_narrowing : forall E Q (WQ : E wf Q) Z P S T, 

  sub_trans_prop WQ -> E |- P <: Q -> 

  (E & Z <: Q) |- S <: T -> (E & Z <: P) |- S <: T.
intros. rewrite (substf_self Z S). rewrite (substf_self Z T).
assert (Z # E). sets OK (sub_to_ok H1). inversions* OK. 
asserts* WQ' ((E & Z <: P) wf Q).  
apply* (sub_subst (WQ := WQ') (E := (E & Z <: Q))).
apply* SA_trans_tvar. use sub_extension.
apply* substf_fresh. 
apply* env_subst_init_narrow.
Qed.

Lemma sub_transitivity : 

  forall E Q (WQ : E wf Q), sub_trans_prop WQ.
intros. unfold sub_trans_prop. generalize_equality Q Q'.
induction WQ; intros Q' EQ F S T EincF SsubQ QsubT;
induction SsubQ; try discriminate; try injection EQ; intros;
inversion QsubT; subst; intuition eauto.
  (* Case SA-arrow *)
apply SA_arrow. auto. apply* IHWQ1. apply* IHWQ2.
  (* Case SA-all *)
apply_SA_all X ((dom E0) ++ L ++ L0 ++ L1). apply* H0. 
asserts* WQ1 (E0 wf T1). apply* (sub_narrowing (WQ := WQ1)).
Qed.


(************************* Main Results ****************************)

Lemma subtyping_reflexivity : forall T E, 

  ok E -> E wf T -> E |- T <: T.
use sub_reflexivity.
Qed.

Lemma subtyping_extension : forall E F S T,

  E |- S <: T -> E inc F -> ok F -> F |- S <: T.
use sub_extension. 
Qed.

Lemma subtyping_narrowing : forall E Q Z P S T, (E |- P <: Q) -> 

  ((E & Z <: Q) |- S <: T) -> ((E & Z <: P) |- S <: T).
intros. asserts* WQ (E wf Q). 
apply* (sub_narrowing (WQ := WQ)). 
apply* sub_transitivity.
Qed.

Lemma subtyping_transitivity : forall E S Q T,

  E |- S <: Q -> E |- Q <: T -> E |- S <: T.
intros. apply* (@sub_transitivity E Q).
Qed.

Lemma subtyping_substitution : forall E Q X P S T, 

  (E & X <: Q) |- S <: T -> E |- P <: Q -> 

  E |- [X~>P]S <: [X~>P]T.
intros. sets OK (sub_to_ok H). inversions OK. 
apply* (sub_subst (WQ := H6) (E := E & X <: Q)).
apply* sub_transitivity. 
apply* substf_fresh. 
apply* env_subst_init_subst.
Qed.