import implementation of Fsub from the Coq tutorial of UPenn

taken from 'https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/index.html'

coq-Fsub/AdditionalTactics.v

@@ -0,0 +1,109 @@
+(** A library of additional tactics. *)
+
+Require Export String.
+Open Scope string_scope.
+
+
+(* *********************************************************************** *)
+(** * Extensions of the standard library *)
+
+(** "[remember c as x in |-]" replaces the term [c] by the identifier
+    [x] in the conclusion of the current goal and introduces the
+    hypothesis [x=c] into the context.  This tactic differs from a
+    similar one in the standard library in that the replacmement is
+    made only in the conclusion of the goal; the context is left
+    unchanged. *)
+
+Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=
+  let x := fresh x in
+  let H := fresh "Heq" x in
+  (set (x := c); assert (H : x = c) by reflexivity; clearbody x).
+
+(** "[unsimpl E]" replaces all occurence of [X] by [E], where [X] is
+    the result that tactic [simpl] would give when used to evaluate
+    [E]. *)
+
+Tactic Notation "unsimpl" constr(E) :=
+  let F := (eval simpl in E) in change F with E.
+
+(** The following tactic calls the [apply] tactic with the first
+    hypothesis that succeeds, "first" meaning the hypothesis that
+    comes earlist in the context (i.e., higher up in the list). *)
+
+Ltac apply_first_hyp :=
+  match reverse goal with
+    | H : _ |- _ => apply H
+  end.
+
+
+(* *********************************************************************** *)
+(** * Variations on [auto] *)
+
+(** The [auto*] and [eauto*] tactics are intended to be "stronger"
+    versions of the [auto] and [eauto] tactics.  Similar to [auto] and
+    [eauto], they each take an optional "depth" argument.  Note that
+    if we declare these tactics using a single string, e.g., "auto*",
+    then the resulting tactics are unusable since they fail to
+    parse. *)
+
+Tactic Notation "auto" "*" :=
+  try solve [ congruence | auto | intuition auto ].
+
+Tactic Notation "auto" "*" integer(n) :=
+  try solve [ congruence | auto n | intuition (auto n) ].
+
+Tactic Notation "eauto" "*" :=
+  try solve [ congruence | eauto | intuition eauto ].
+
+Tactic Notation "eauto" "*" integer(n) :=
+  try solve [ congruence | eauto n | intuition (eauto n) ].
+
+
+(* *********************************************************************** *)
+(** * Delineating cases in proofs *)
+
+(** This section was taken from the POPLmark Wiki
+    ( http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/ ). *)
+
+(** ** Tactic definitions *)
+
+Ltac move_to_top x :=
+  match reverse goal with
+  | H : _ |- _ => try move x after H
+  end.
+
+Tactic Notation "assert_eq" ident(x) constr(v) :=
+  let H := fresh in
+  assert (x = v) as H by reflexivity;
+  clear H.
+
+Tactic Notation "Case_aux" ident(x) constr(name) :=
+  first [
+    set (x := name); move_to_top x
+  | assert_eq x name
+  | fail 1 "because we are working on a different case." ].
+
+Ltac Case name := Case_aux case name.
+Ltac SCase name := Case_aux subcase name.
+Ltac SSCase name := Case_aux subsubcase name.
+
+(** ** Example
+
+    One mode of use for the above tactics is to wrap Coq's [induction]
+    tactic such that automatically inserts "case" markers into each
+    branch of the proof.  For example:
+
+<<
+ Tactic Notation "induction" "nat" ident(n) :=
+   induction n; [ Case "O" | Case "S" ].
+ Tactic Notation "sub" "induction" "nat" ident(n) :=
+   induction n; [ SCase "O" | SCase "S" ].
+ Tactic Notation "sub" "sub" "induction" "nat" ident(n) :=
+   induction n; [ SSCase "O" | SSCase "S" ].
+>>
+
+    If you use such customized versions of the induction tactics, then
+    the [Case] tactic will verify that you are working on the case
+    that you think you are.  You may also use the [Case] tactic with
+    the standard version of [induction], in which case no verification
+    is done. *)

coq-Fsub/Atom.v

@@ -0,0 +1,262 @@
+(** Support for atoms, i.e., objects with decidable equality.  We
+    provide here the ability to generate an atom fresh for any finite
+    collection, e.g., the lemma [atom_fresh_for_set], and a tactic to
+    pick an atom fresh for the current proof context.
+
+    Authors: Arthur Charguéraud and Brian Aydemir.
+
+    Implementation note: In older versions of Coq, [OrderedTypeEx]
+    redefines decimal constants to be integers and not natural
+    numbers.  The following scope declaration is intended to address
+    this issue.  In newer versions of Coq, the declaration should be
+    benign. *)
+
+Require Import List.
+Require Import Max.
+Require Import OrderedType.
+Require Import OrderedTypeEx.
+Open Scope nat_scope.
+
+Require Import FiniteSets.
+Require Import FSetDecide.
+Require Import FSetNotin.
+Require Import ListFacts.
+
+
+(* ********************************************************************** *)
+(** * Definition *)
+
+(** Atoms are structureless objects such that we can always generate
+    one fresh from a finite collection.  Equality on atoms is [eq] and
+    decidable.  We use Coq's module system to make abstract the
+    implementation of atoms.  The [Export AtomImpl] line below allows
+    us to refer to the type [atom] and its properties without having
+    to qualify everything with "[AtomImpl.]". *)
+
+Module Type ATOM.
+
+  Parameter atom : Set.
+
+  Parameter atom_fresh_for_list :
+    forall (xs : list atom), {x : atom | ~ List.In x xs}.
+
+  Declare Module Atom_as_OT : UsualOrderedType with Definition t := atom.
+
+  Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}.
+
+End ATOM.
+
+(** The implementation of the above interface is hidden for
+    documentation purposes. *)
+
+Module AtomImpl : ATOM.
+
+  (* begin hide *)
+
+  Definition atom := nat.
+
+  Lemma max_lt_r : forall x y z,
+    x <= z -> x <= max y z.
+  Proof.
+    induction x. auto with arith.
+    induction y; auto with arith.
+      simpl. induction z. omega. auto with arith.
+  Qed.
+
+  Lemma nat_list_max : forall (xs : list nat),
+    { n : nat | forall x, In x xs -> x <= n }.
+  Proof.
+    induction xs as [ | x xs [y H] ].
+    (* case: nil *)
+    exists 0. inversion 1.
+    (* case: cons x xs *)
+    exists (max x y). intros z J. simpl in J. destruct J as [K | K].
+      subst. auto with arith.
+      auto using max_lt_r.
+  Qed.
+
+  Lemma atom_fresh_for_list :
+    forall (xs : list nat), { n : nat | ~ List.In n xs }.
+  Proof.
+    intros xs. destruct (nat_list_max xs) as [x H].
+    exists (S x). intros J. lapply (H (S x)). omega. trivial.
+  Qed.
+
+  Module Atom_as_OT := Nat_as_OT.
+  Module Facts := OrderedTypeFacts Atom_as_OT.
+
+  Definition eq_atom_dec : forall x y : atom, {x = y} + {x <> y} :=
+    Facts.eq_dec.
+
+  (* end hide *)
+
+End AtomImpl.
+
+Export AtomImpl.
+
+
+(* ********************************************************************** *)
+(** * Finite sets of atoms *)
+
+
+(* ********************************************************************** *)
+(** ** Definitions *)
+
+Module AtomSet : FiniteSets.S with Module E := Atom_as_OT :=
+  FiniteSets.Make Atom_as_OT.
+
+(** The type [atoms] is the type of finite sets of [atom]s. *)
+
+Notation atoms := AtomSet.F.t.
+
+(** Basic operations on finite sets of atoms are available, in the
+    remainder of this file, without qualification.  We use [Import]
+    instead of [Export] in order to avoid unnecessary namespace
+    pollution. *)
+
+Import AtomSet.F.
+
+(** We instantiate two modules which provide useful lemmas and tactics
+    work working with finite sets of atoms. *)
+
+Module AtomSetDecide := FSetDecide.Decide AtomSet.F.
+Module AtomSetNotin  := FSetNotin.Notin   AtomSet.F.
+
+
+(* *********************************************************************** *)
+(** ** Tactics for working with finite sets of atoms *)
+
+(** The tactic [fsetdec] is a general purpose decision procedure
+    for solving facts about finite sets of atoms. *)
+
+Ltac fsetdec := try apply AtomSet.eq_if_Equal; AtomSetDecide.fsetdec.
+
+(** The tactic [notin_simpl] simplifies all hypotheses of the form [(~
+    In x F)], where [F] is constructed from the empty set, singleton
+    sets, and unions. *)
+
+Ltac notin_simpl := AtomSetNotin.notin_simpl_hyps.
+
+(** The tactic [notin_solve], solves goals of the form [(~ In x F)],
+    where [F] is constructed from the empty set, singleton sets, and
+    unions.  The goal must be provable from hypothesis of the form
+    simplified by [notin_simpl]. *)
+
+Ltac notin_solve := AtomSetNotin.notin_solve.
+
+
+(* *********************************************************************** *)
+(** ** Lemmas for working with finite sets of atoms *)
+
+(** We make some lemmas about finite sets of atoms available without
+    qualification by using abbreviations. *)
+
+Notation eq_if_Equal        := AtomSet.eq_if_Equal.
+Notation notin_empty        := AtomSetNotin.notin_empty.
+Notation notin_singleton    := AtomSetNotin.notin_singleton.
+Notation notin_singleton_rw := AtomSetNotin.notin_singleton_rw.
+Notation notin_union        := AtomSetNotin.notin_union.
+
+
+(* ********************************************************************** *)
+(** * Additional properties *)
+
+(** One can generate an atom fresh for a given finite set of atoms. *)
+
+Lemma atom_fresh_for_set : forall L : atoms, { x : atom | ~ In x L }.
+Proof.
+  intros L. destruct (atom_fresh_for_list (elements L)) as [a H].
+  exists a. intros J. contradiction H.
+  rewrite <- InA_iff_In. auto using elements_1.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * Additional tactics *)
+
+
+(* ********************************************************************** *)
+(** ** #<a name="pick_fresh"></a># Picking a fresh atom *)
+
+(** We define three tactics which, when combined, provide a simple
+    mechanism for picking a fresh atom.  We demonstrate their use
+    below with an example, the [example_pick_fresh] tactic.
+
+   [(gather_atoms_with F)] returns the union of [(F x)], where [x]
+   ranges over all objects in the context such that [(F x)] is
+   well typed.  The return type of [F] should be [atoms].  The
+   complexity of this tactic is due to the fact that there is no
+   support in [Ltac] for folding a function over the context. *)
+
+Ltac gather_atoms_with F :=
+  let rec gather V :=
+    match goal with
+    | H: ?S |- _ =>
+      let FH := constr:(F H) in
+      match V with
+      | empty => gather FH
+      | context [FH] => fail 1
+      | _ => gather (union FH V)
+      end
+    | _ => V
+    end in
+  let L := gather empty in eval simpl in L.
+
+(** [(beautify_fset V)] takes a set [V] built as a union of finite
+    sets and returns the same set with empty sets removed and union
+    operations associated to the right.  Duplicate sets are also
+    removed from the union. *)
+
+Ltac beautify_fset V :=
+  let rec go Acc E :=
+     match E with
+     | union ?E1 ?E2 => let Acc1 := go Acc E2 in go Acc1 E1
+     | empty => Acc
+     | ?E1 => match Acc with
+              | empty => E1
+              | context [E1] => Acc
+              | _ => constr:(union E1 Acc)
+              end
+     end
+  in go empty V.
+
+(** The tactic [(pick fresh Y for L)] takes a finite set of atoms [L]
+    and a fresh name [Y], and adds to the context an atom with name
+    [Y] and a proof that [(~ In Y L)], i.e., that [Y] is fresh for
+    [L].  The tactic will fail if [Y] is already declared in the
+    context. *)
+
+Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
+  let Fr := fresh "Fr" in
+  let L := beautify_fset L in
+  (destruct (atom_fresh_for_set L) as [Y Fr]).
+
+
+(* ********************************************************************** *)
+(** ** Demonstration *)
+
+(** The [example_pick_fresh] tactic below illustrates the general
+    pattern for using the above three tactics to define a tactic which
+    picks a fresh atom.  The pattern is as follows:
+      - Repeatedly invoke [gather_atoms_with], using functions with
+        different argument types each time.
+      - Union together the result of the calls, and invoke
+        [(pick fresh ... for ...)] with that union of sets. *)
+
+Ltac example_pick_fresh Y :=
+  let A := gather_atoms_with (fun x : atoms => x) in
+  let B := gather_atoms_with (fun x : atom => singleton x) in
+  pick fresh Y for (union A B).
+
+Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3: atoms), True.
+(* begin show *)
+Proof.
+  intros x y z L1 L2 L3. example_pick_fresh k.
+
+  (** At this point in the proof, we have a new atom [k] and a
+      hypothesis [Fr : ~ In k (union L1 (union L2 (union L3 (union
+      (singleton x) (union (singleton y) (singleton z))))))]. *)
+
+  trivial.
+Qed.
+(* end show *)

coq-Fsub/Environment.v

@@ -0,0 +1,658 @@
+(** Operations, lemmas, and tactics for working with environments,
+    association lists whose keys are atoms.  Unless stated otherwise,
+    implicit arguments will not be declared by default.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios
+    Vytiniotis, Stephanie Weirich, and Steve Zdancewic.
+
+    Table of contents:
+      - #<a href="##overview">Overview</a>#
+      - #<a href="##functions">Functions on environments</a>#
+      - #<a href="##env_rel">Relations on environments</a>#
+      - #<a href="##op_prop">Properties of operations</a>#
+      - #<a href="##auto1">Automation and tactics (I)</a>#
+      - #<a href="##props">Properties of well-formedness and freshness</a>#
+      - #<a href="##binds_prop">Properties of binds</a>#
+      - #<a href="##auto2">Automation and tactics (II)</a>#
+      - #<a href="##binds_prop2">Additional properties of binds</a>#
+      - #<a href="##auto3">Automation and tactics (III)</a># *)
+
+Require Export List.
+Require Export ListFacts.
+Require Import Atom.
+
+Import AtomSet.F.
+Hint Local Unfold E.eq.
+
+
+(* ********************************************************************** *)
+(** * #<a name="overview"></a># Overview *)
+
+(** An environment is a list of pairs, where the first component of
+    each pair is an [atom].  We view the second component of each pair
+    as being bound to the first component.  In a well-formed
+    environment, there is at most one binding for any given atom.
+    Bindings at the head of the list are "more recent" than bindings
+    toward the tail of the list, and we view an environment as growing
+    on the left, i.e., at its head.
+
+    We normally work only with environments built up from the
+    following: the empty list, one element lists, and concatenations
+    of two lists.  This seems to be more convenient in practice.  For
+    example, we don't need to distinguish between consing on a binding
+    and concatenating a binding, a difference that Coq's tactics can
+    be sensitive to.
+
+    However, basic definitions are by induction on the usual structure
+    of lists ([nil] and [cons]).
+
+    To make it convenient to write one element lists, we define a
+    special notation.  Note that this notation is local to this
+    particular library, to allow users to use alternate notations if
+    they desire. *)
+
+Notation Local "[ x ]" := (cons x nil).
+
+(** In the remainder of this library, we define a number of
+    operations, lemmas, and tactics that simplify working with
+    environments. *)
+
+
+(* ********************************************************************** *)
+(** * #<a name="functions"></a># Functions on environments *)
+
+(** Implicit arguments will be declared by default for the definitions
+    in this section. *)
+
+Set Implicit Arguments.
+
+Section Definitions.
+
+Variables A B : Type.
+
+(** The domain of an environment is the set of atoms that it maps. *)
+
+Fixpoint dom (E : list (atom * A)) : atoms :=
+  match E with
+  | nil => empty
+  | (x, _) :: E' => union (singleton x) (dom E')
+  end.
+
+(** [map] applies a function to all bindings in the environment. *)
+
+Fixpoint map (f : A -> B) (E : list (atom * A)) : list (atom * B) :=
+  match E with
+  | nil => nil
+  | (x, V) :: E' => (x, f V) :: map f E'
+  end.
+
+(** [get] returns the value bound to the given atom in an environment
+    or [None] if the given atom is not bound.  If the atom has
+    multiple bindings, the one nearest to the head of the environment
+    is returned. *)
+
+Fixpoint get (x : atom) (E : list (atom * A)) : option A :=
+  match E with
+  | nil => None
+  | (y,a) :: E' => if eq_atom_dec x y then Some a else get x E'
+  end.
+
+End Definitions.
+
+Unset Implicit Arguments.
+
+
+(* ********************************************************************** *)
+(** * #<a name="env_rel"></a># Relations on environments *)
+
+(** Implicit arguments will be declared by default for the definitions
+    in this section. *)
+
+Set Implicit Arguments.
+
+Section Relations.
+
+Variable A : Type.
+
+(** An environment is well-formed if and only if each atom is bound at
+    most once. *)
+
+Inductive ok : list (atom * A) -> Prop :=
+  | ok_nil :
+      ok nil
+  | ok_cons : forall (E : list (atom * A)) (x : atom) (a : A),
+      ok E -> ~ In x (dom E) -> ok ((x, a) :: E).
+
+(** #<a name="binds_doc"></a># An environment [E] contains a binding
+    from [x] to [b], denoted [(binds x b E)], if and only if the most
+    recent binding for [x] is mapped to [b]. *)
+
+Definition binds x b (E : list (atom * A)) :=
+  get x E = Some b.
+
+End Relations.
+
+Unset Implicit Arguments.
+
+
+(* ********************************************************************** *)
+(** * #<a name="op_prop"></a># Properties of operations *)
+
+Section OpProperties.
+Variable A B : Type.
+Implicit Types E F : list (atom * A).
+Implicit Types a b : A.
+
+(** ** Facts about concatenation *)
+
+Lemma concat_nil : forall E,
+  E ++ nil = E.
+Proof.
+  auto using List.app_nil_end.
+Qed.
+
+Lemma nil_concat : forall E,
+  nil ++ E = E.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma concat_assoc : forall E F G,
+  (G ++ F) ++ E = G ++ (F ++ E).
+Proof.
+  auto using List.app_ass.
+Qed.
+
+(** ** [map] commutes with environment-building operations *)
+
+Lemma map_nil : forall (f : A -> B),
+  map f nil = nil.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map_single : forall (f : A -> B) y b,
+  map f [(y,b)] = [(y, f b)].
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map_push : forall (f : A -> B) y b E,
+  map f ([(y,b)] ++ E) = [(y, f b)] ++ map f E.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map_concat : forall (f : A -> B) E F,
+  map f (F ++ E) = (map f F) ++ (map f E).
+Proof.
+  induction F as [|(x,a)]; simpl; congruence.
+Qed.
+
+(** ** Facts about the domain of an environment *)
+
+Lemma dom_nil :
+  @dom A nil = empty.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma dom_single : forall x a,
+  dom [(x,a)] = singleton x.
+Proof.
+  simpl. intros. fsetdec.
+Qed.
+
+Lemma dom_push : forall x a E,
+  dom ([(x,a)] ++ E) = union (singleton x) (dom E).
+Proof.
+  simpl. intros. reflexivity.
+Qed.
+
+Lemma dom_concat : forall E F,
+  dom (F ++ E) = union (dom F) (dom E).
+Proof.
+  induction F as [|(x,a) F IH]; simpl.
+  fsetdec.
+  rewrite IH. fsetdec.
+Qed.
+
+Lemma dom_map : forall (f : A -> B) E,
+  dom (map f E) = dom E.
+Proof.
+  induction E as [|(x,a)]; simpl; congruence.
+Qed.
+
+(** ** Other trivial rewrites *)
+
+Lemma cons_concat_assoc : forall x a E F,
+   ((x, a) :: E) ++ F = (x, a) :: (E ++ F).
+Proof.
+  reflexivity.
+Qed.
+
+End OpProperties.
+
+
+(* ********************************************************************** *)
+(** * #<a name="auto1"></a># Automation and tactics (I) *)
+
+(** ** [simpl_env] *)
+
+(** The [simpl_env] tactic can be used to put environments in the
+    standardized form described above, with the additional properties
+    that concatenation is associated to the right and empty
+    environments are removed.  Similar to the [simpl] tactic, we
+    define "[in *]" and "[in H]" variants of [simpl_env]. *)
+
+Definition singleton_list (A : Type) (x : atom * A) := x :: nil.
+Implicit Arguments singleton_list [A].
+
+Lemma cons_concat : forall (A : Type) (E : list (atom * A)) x a,
+  (x, a) :: E = singleton_list (x, a) ++ E.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map_singleton_list : forall (A B : Type) (f : A -> B) y b,
+  map f (singleton_list (y,b)) = [(y, f b)].
+Proof.
+  reflexivity.
+Qed.
+
+Lemma dom_singleton_list : forall (A : Type) (x : atom) (a : A),
+  dom (singleton_list (x,a)) = singleton x.
+Proof.
+  simpl. intros. fsetdec.
+Qed.
+
+Hint Rewrite
+  cons_concat map_singleton_list dom_singleton_list
+  concat_nil nil_concat concat_assoc
+  map_nil map_single map_push map_concat
+  dom_nil dom_single dom_push dom_concat dom_map : rew_env.
+
+Ltac simpl_env_change_aux :=
+  match goal with
+    | H : context[?x :: nil] |- _ =>
+      progress (change (x :: nil) with (singleton_list x) in H);
+      simpl_env_change_aux
+    | |- context[?x :: nil] =>
+      progress (change (x :: nil) with (singleton_list x));
+      simpl_env_change_aux
+    | _ =>
+      idtac
+  end.
+
+Ltac simpl_env :=
+  simpl_env_change_aux;
+  autorewrite with rew_env;
+  unfold singleton_list in *.
+
+Tactic Notation "simpl_env" "in" hyp(H) :=
+  simpl_env_change_aux;
+  autorewrite with rew_env in H;
+  unfold singleton_list in *.
+
+Tactic Notation "simpl_env" "in" "*" :=
+  simpl_env_change_aux;
+  autorewrite with rew_env in *;
+  unfold singleton_list in *.
+
+(** ** [rewrite_env] *)
+
+(** The tactic [(rewrite_env E)] replaces an environment in the
+    conclusion of the goal with [E].  Suitability for replacement is
+    determined by whether [simpl_env] can put [E] and the chosen
+    environment in the same normal form, up to convertability in Coq.
+    We also define a "[in H]" variant that performs the replacement in
+    a hypothesis [H]. *)
+
+Tactic Notation "rewrite_env" constr(E) :=
+  match goal with
+    | |- context[?x] =>
+      change x with E
+    | |- context[?x] =>
+      replace x with E; [ | try reflexivity; simpl_env; reflexivity ]
+  end.
+
+Tactic Notation "rewrite_env" constr(E) "in" hyp(H) :=
+  match type of H with
+    | context[?x] =>
+      change x with E in H
+    | context[?x] =>
+      replace x with E in H; [ | try reflexivity; simpl_env; reflexivity ]
+  end.
+
+(** ** Hints *)
+
+Hint Constructors ok.
+
+Hint Local Extern 1 (~ In _ _) => simpl_env in *; fsetdec.
+
+
+(* ********************************************************************** *)
+(** * #<a name="props"></a># Properties of well-formedness and freshness *)
+
+Section OkProperties.
+Variable A B : Type.
+Implicit Types E F : list (atom * A).
+Implicit Types a b : A.
+
+(** Facts about when an environment is well-formed. *)
+
+Lemma ok_push :  forall (E : list (atom * A)) (x : atom) (a : A),
+      ok E -> ~ In x (dom E) -> ok ([(x, a)] ++ E).
+Proof.
+  exact (@ok_cons A).
+Qed.
+
+Lemma ok_singleton : forall x a,
+  ok [(x,a)].
+Proof.
+  auto.
+Qed.
+
+Lemma ok_remove_mid : forall F E G,
+  ok (G ++ F ++ E) -> ok (G ++ E).
+Proof with auto.
+  induction G as [|(y,a)]; intros Ok.
+    induction F as [|(y,a)]; simpl... inversion Ok...
+    inversion Ok. simpl...
+Qed.
+
+Lemma ok_remove_mid_cons : forall x a E G,
+  ok (G ++ (x, a) :: E) ->
+  ok (G ++ E).
+Proof.
+  intros. simpl_env in *. eauto using ok_remove_mid.
+Qed.
+
+Lemma ok_map : forall E (f : A -> B),
+  ok E -> ok (map f E).
+Proof with auto.
+  intros.
+  induction E as [ | (y,b) E ] ; simpl...
+  inversion H...
+Qed.
+
+Lemma ok_map_app_l : forall E F (f : A -> A),
+  ok (F ++ E) -> ok (map f F ++ E).
+Proof with auto.
+  intros. induction F as [|(y,a)]; simpl...
+  inversion H...
+Qed.
+
+(** A binding in the middle of an environment has an atom fresh from
+    all bindings before and after it. *)
+
+Lemma fresh_mid_tail : forall E F x a,
+  ok (F ++ [(x,a)] ++ E) -> ~ In x (dom E).
+Proof with auto.
+  induction F as [|(y,b)]; intros x c Ok; simpl_env in *.
+    inversion Ok...
+    inversion Ok; subst. simpl_env in *. apply (IHF _ _ H1).
+Qed.
+
+Lemma fresh_mid_head : forall E F x a,
+  ok (F ++ [(x,a)] ++ E) -> ~ In x (dom F).
+Proof with auto.
+  induction F as [|(y,b)]; intros x c Ok; simpl_env in *.
+    inversion Ok...
+    inversion Ok; subst. simpl_env in *. pose proof (IHF _ _ H1)...
+Qed.
+
+End OkProperties.
+
+
+(* ********************************************************************** *)
+(** * #<a name="binds_prop"></a># Properties of [binds] *)
+
+Section BindsProperties.
+Variable A B : Type.
+Implicit Types E F : list (atom * A).
+Implicit Types a b : A.
+
+(** ** Introduction forms for [binds] *)
+
+(** The following properties allow one to view [binds] as an
+    inductively defined predicate.  This is the preferred way of
+    working with the relation. *)
+
+Lemma binds_singleton : forall x a,
+  binds x a [(x,a)].
+Proof.
+  intros x a. unfold binds. simpl. destruct (eq_atom_dec x x); intuition.
+Qed.
+
+Lemma binds_tail : forall x a E F,
+  binds x a E -> ~ In x (dom F) -> binds x a (F ++ E).
+Proof with auto.
+  unfold binds. induction F as [|(y,b)]; simpl...
+  destruct (eq_atom_dec x y)... intros _ J. destruct J. fsetdec.
+Qed.
+
+Lemma binds_head : forall x a E F,
+  binds x a F -> binds x a (F ++ E).
+Proof.
+  unfold binds. induction F as [|(y,b)]; simpl; intros H.
+  discriminate.
+  destruct (eq_atom_dec x y); intuition.
+Qed.
+
+(** ** Case analysis on [binds] *)
+
+Lemma binds_concat_inv : forall x a E F,
+  binds x a (F ++ E) -> (~ In x (dom F) /\ binds x a E) \/ (binds x a F).
+Proof with auto.
+  unfold binds. induction F as [|(y,b)]; simpl; intros H...
+  destruct (eq_atom_dec x y).
+    right...
+    destruct (IHF H) as [[? ?] | ?]. left... right...
+Qed.
+
+Lemma binds_singleton_inv : forall x y a b,
+  binds x a [(y,b)] -> x = y /\ a = b.
+Proof.
+  unfold binds. simpl. intros. destruct (eq_atom_dec x y).
+    split; congruence.
+    discriminate.
+Qed.
+
+(** ** Retrieving bindings from an environment *)
+
+Lemma binds_mid : forall x a E F,
+  ok (F ++ [(x,a)] ++ E) -> binds x a (F ++ [(x,a)] ++ E).
+Proof with auto.
+  unfold binds. induction F as [|(z,b)]; simpl; intros Ok.
+  destruct (eq_atom_dec x x); intuition.
+  inversion Ok; subst. destruct (eq_atom_dec x z)...
+    destruct H3. simpl_env. fsetdec.
+Qed.
+
+Lemma binds_mid_eq : forall z a b E F,
+  binds z a (F ++ [(z,b)] ++ E) -> ok (F ++ [(z,b)] ++ E) -> a = b.
+Proof with auto.
+  unfold binds. induction F as [|(x,c)]; simpl; intros H Ok.
+  destruct (eq_atom_dec z z). congruence. intuition.
+  inversion Ok; subst. destruct (eq_atom_dec z x)...
+    destruct H4. simpl_env. fsetdec.
+Qed.
+
+Lemma binds_mid_eq_cons : forall x a b E F,
+  binds x a (F ++ (x,b) :: E) ->
+  ok (F ++ (x,b) :: E) ->
+  a = b.
+Proof.
+  intros. simpl_env in *. eauto using binds_mid_eq.
+Qed.
+
+End BindsProperties.
+
+
+(* ********************************************************************** *)
+(** * #<a name="auto2"></a># Automation and tactics (II) *)
+
+(** ** Hints *)
+
+Hint Immediate ok_remove_mid ok_remove_mid_cons.
+
+Hint Resolve
+  ok_push ok_singleton ok_map ok_map_app_l
+  binds_singleton binds_head binds_tail.
+
+(** ** [binds_get] *)
+
+(** The tactic [(binds_get H)] takes a hypothesis [H] of the form
+    [(binds x a (F ++ [(x,b)] ++ E))] and introduces the equality
+    [a=b] into the context.  Then, the tactic checks if the equality
+    is discriminable and otherwise tries substituting [b] for [a].
+    The [auto] tactic is used to show that [(ok (F ++ [(x,b)] ++ E))],
+    which is needed to prove the equality [a=b] from [H]. *)
+
+Ltac binds_get H :=
+  match type of H with
+    | binds ?z ?a (?F ++ [(?z,?b)] ++ ?E) =>
+        let K := fresh in
+          assert (K : ok (F ++ [(z,b)] ++ E));
+          [ auto
+          | let J := fresh in
+              assert (J := @binds_mid_eq _ _ _ _ _ _ H K);
+              clear K;
+              try discriminate;
+              try match type of J with
+                    | ?a = ?b => subst a
+                  end
+          ]
+  end.
+
+(** ** [binds_cases] *)
+
+(** The tactic [(binds_case H)] performs a case analysis on an
+    hypothesis [H] of the form [(binds x a E)].  There will be one
+    subgoal for each component of [E] that [x] could be bound in, and
+    each subgoal will have appropriate freshness conditions on [x].
+    Some attempts are made to automatically discharge contradictory
+    cases. *)
+
+Ltac binds_cases H :=
+  let Fr := fresh "Fr" in
+  let J1 := fresh in
+  let J2 := fresh in
+    match type of H with
+      | binds _ _ nil =>
+          inversion H
+      | binds ?x ?a [(?y,?b)] =>
+          destruct (@binds_singleton_inv _ _ _ _ _ H);
+          clear H;
+          try discriminate;
+          try subst y;
+          try match goal with
+                | _ : ?z <> ?z |- _ => intuition
+              end
+      | binds ?x ?a (?F ++ ?E) =>
+          destruct (@binds_concat_inv _ _ _ _ _ H) as [[Fr J1] | J2];
+          clear H;
+          [ binds_cases J1 | binds_cases J2 ]
+      | _ => idtac
+  end.
+
+
+(* *********************************************************************** *)
+(** * #<a name="binds_prop2"></a># Additional properties of [binds] *)
+
+(** The following lemmas are proven in manner that should be
+    independent of the concrete definition of [binds]. *)
+
+Section AdditionalBindsProperties.
+Variable A B : Type.
+Implicit Types E F : list (atom * A).
+Implicit Types a b : A.
+
+(** Lemmas about the relationship between [binds] and the domain of an
+    environment. *)
+
+Lemma binds_In : forall a x E,
+  binds x a E -> In x (dom E).
+Proof.
+  induction E as [|(y,b)]; simpl_env; intros H.
+  binds_cases H.
+  binds_cases H; subst. auto using union_3. fsetdec.
+Qed.
+
+Lemma binds_fresh : forall x a E,
+  ~ In x (dom E) -> ~ binds x a E.
+Proof.
+  induction E as [|(y,b)]; simpl_env; intros Fresh H.
+  binds_cases H.
+  binds_cases H. intuition. fsetdec.
+Qed.
+
+(** Additional lemmas for showing that a binding is in an
+    environment. *)
+
+Lemma binds_map : forall x a (f : A -> B) E,
+  binds x a E -> binds x (f a) (map f E).
+Proof.
+  induction E as [|(y,b)]; simpl_env; intros H.
+  binds_cases H.
+  binds_cases H; auto. subst; auto.
+Qed.
+
+Lemma binds_concat_ok : forall x a E F,
+  binds x a E -> ok (F ++ E) -> binds x a (F ++ E).
+Proof.
+  induction F as [|(y,b)]; simpl_env; intros H Ok.
+  auto.
+  inversion Ok; subst. destruct (eq_atom_dec x y); subst; auto.
+    assert (In y (dom (F ++ E))) by eauto using binds_In.
+    intuition.
+Qed.
+
+Lemma binds_weaken : forall x a E F G,
+  binds x a (G ++ E) ->
+  ok (G ++ F ++ E) ->
+  binds x a (G ++ F ++ E).
+Proof.
+  induction G as [|(y,b)]; simpl_env; intros H Ok.
+  auto using binds_concat_ok.
+  inversion Ok; subst. binds_cases H; subst; auto.
+Qed.
+
+Lemma binds_weaken_at_head : forall x a F G,
+  binds x a G ->
+  ok (F ++ G) ->
+  binds x a (F ++ G).
+Proof.
+  intros x a F G H J.
+  rewrite_env (nil ++ F ++ G).
+  apply binds_weaken; simpl_env; trivial.
+Qed.
+
+Lemma binds_remove_mid : forall x y a b F G,
+  binds x a (F ++ [(y,b)] ++ G) ->
+  x <> y ->
+  binds x a (F ++ G).
+Proof.
+  intros x y a b F G H J.
+  binds_cases H; auto.
+Qed.
+
+Lemma binds_remove_mid_cons : forall x y a b E G,
+  binds x a (G ++ (y, b) :: E) ->
+  x <> y ->
+  binds x a (G ++ E).
+Proof.
+  intros. simpl_env in *. eauto using binds_remove_mid.
+Qed.
+
+End AdditionalBindsProperties.
+
+
+(* *********************************************************************** *)
+(** * #<a name="auto3"></a># Automation and tactics (III) *)
+
+Hint Resolve binds_map binds_concat_ok binds_weaken binds_weaken_at_head.
+
+Hint Immediate binds_remove_mid binds_remove_mid_cons.

coq-Fsub/FSetNotin.v

@@ -0,0 +1,164 @@
+(** Lemmas and tactics for working with and solving goals related to
+    non-membership in finite sets.  The main tactic of interest here
+    is [notin_solve].
+
+    Authors: Arthur Charguéraud and Brian Aydemir. *)
+
+Set Implicit Arguments.
+Require Import FSetInterface.
+
+
+(* *********************************************************************** *)
+(** * Implementation *)
+
+Module Notin (X : FSetInterface.S).
+
+Import X.
+
+
+(* *********************************************************************** *)
+(** ** Facts about set (non-)membership *)
+
+Lemma in_singleton : forall x,
+  In x (singleton x).
+Proof.
+  auto using singleton_2.
+Qed.
+
+Lemma notin_empty : forall x,
+  ~ In x empty.
+Proof.
+  auto using empty_1.
+Qed.
+
+Lemma notin_union : forall x E F,
+  ~ In x E -> ~ In x F -> ~ In x (union E F).
+Proof.
+  intros x E F H J K.
+  destruct (union_1 K); intuition.
+Qed.
+
+Lemma elim_notin_union : forall x E F,
+  ~ In x (union E F) -> (~ In x E) /\ (~ In x F).
+Proof.
+  intros x E F H. split; intros J; contradiction H.
+  auto using union_2.
+  auto using union_3.
+Qed.
+
+Lemma notin_singleton : forall x y,
+  ~ E.eq x y -> ~ In x (singleton y).
+Proof.
+  intros x y H J. assert (K := singleton_1 J). intuition.
+Qed.
+
+Lemma elim_notin_singleton : forall x y,
+  ~ In x (singleton y) -> ~ E.eq x y.
+Proof.
+  intros x y H J. contradiction H. auto using singleton_2.
+Qed.
+
+Lemma elim_notin_singleton' : forall x y,
+  ~ In x (singleton y) -> x <> y.
+Proof.
+  intros. assert (~ E.eq x y). auto using singleton_2.
+  intros J. subst. intuition.
+Qed.
+
+Lemma notin_singleton_swap : forall x y,
+  ~ In x (singleton y) -> ~ In y (singleton x).
+Proof.
+  intros.
+  assert (Q := elim_notin_singleton H).
+  auto using singleton_1.
+Qed.
+
+
+(* *********************************************************************** *)
+(** ** Rewriting non-membership facts *)
+
+Lemma notin_singleton_rw : forall x y,
+  ~ In x (singleton y) <-> ~ E.eq x y.
+Proof.
+  intros. split.
+    auto using elim_notin_singleton.
+    auto using notin_singleton.
+Qed.
+
+
+(* *********************************************************************** *)
+(** ** Tactics *)
+
+(** The tactic [notin_simpl_hyps] destructs all hypotheses of the form
+    [(~ In x E)], where [E] is built using only [empty], [union], and
+    [singleton]. *)
+
+Ltac notin_simpl_hyps :=
+  try match goal with
+        | H: In ?x ?E -> False |- _ =>
+          change (~ In x E) in H;
+          notin_simpl_hyps
+        | H: ~ In _ empty |- _ =>
+          clear H;
+          notin_simpl_hyps
+        | H: ~ In ?x (singleton ?y) |- _ =>
+          let F1 := fresh in
+          let F2 := fresh in
+          assert (F1 := @elim_notin_singleton x y H);
+          assert (F2 := @elim_notin_singleton' x y H);
+          clear H;
+          notin_simpl_hyps
+        | H: ~ In ?x (union ?E ?F) |- _ =>
+          destruct (@elim_notin_union x E F H);
+          clear H;
+          notin_simpl_hyps
+      end.
+
+(** The tactic [notin_solve] solves goals of them form [(x <> y)] and
+    [(~ In x E)] that are provable from hypotheses of the form
+    destructed by [notin_simpl_hyps]. *)
+
+Ltac notin_solve :=
+  notin_simpl_hyps;
+  repeat (progress (  apply notin_empty
+                   || apply notin_union
+                   || apply notin_singleton));
+  solve [ trivial | congruence | intuition auto ].
+
+
+(* *********************************************************************** *)
+(** ** Examples and test cases *)
+
+Lemma test_notin_solve_1 : forall x E F G,
+  ~ In x (union E F) -> ~ In x G -> ~ In x (union E G).
+Proof.
+  intros. notin_solve.
+Qed.
+
+Lemma test_notin_solve_2 : forall x y E F G,
+  ~ In x (union E (union (singleton y) F)) -> ~ In x G ->
+  ~ In x (singleton y) /\ ~ In y (singleton x).
+Proof.
+  intros. split. notin_solve. notin_solve.
+Qed.
+
+Lemma test_notin_solve_3 : forall x y,
+  ~ E.eq x y -> ~ In x (singleton y) /\ ~ In y (singleton x).
+Proof.
+  intros. split. notin_solve. notin_solve.
+Qed.
+
+Lemma test_notin_solve_4 : forall x y E F G,
+  ~ In x (union E (union (singleton x) F)) -> ~ In y G.
+Proof.
+  intros. notin_solve.
+Qed.
+
+Lemma test_notin_solve_5 : forall x y E F,
+  ~ In x (union E (union (singleton y) F)) -> ~ In y E ->
+  ~ E.eq y x /\ ~ E.eq x y.
+Proof.
+  intros. split. notin_solve. notin_solve.
+Qed.
+
+End Notin.

coq-Fsub/FiniteSets.v

@@ -0,0 +1,61 @@
+(** A library for finite sets with extensional equality.
+
+    Author: Brian Aydemir. *)
+
+Require Import FSets.
+Require Import ListFacts.
+
+
+(* *********************************************************************** *)
+(** * Interface *)
+
+(** The following interface wraps the standard library's finite set
+    interface with an additional property: extensional equality. *)
+
+Module Type S.
+
+  Declare Module E : UsualOrderedType.
+  Declare Module F : FSetInterface.S with Module E := E.
+
+  Parameter eq_if_Equal :
+    forall s s' : F.t, F.Equal s s' -> s = s'.
+
+End S.
+
+
+(* *********************************************************************** *)
+(** * Implementation *)
+
+(** For documentation purposes, we hide the implementation of a
+    functor implementing the above interface.  We note only that the
+    implementation here assumes (as an axiom) that proof irrelevance
+    holds. *)
+
+Module Make (X : UsualOrderedType) <: S with Module E := X.
+
+  (* begin hide *)
+
+  Module E := X.
+  Module F := FSetList.Make E.
+  Module OFacts := OrderedType.OrderedTypeFacts E.
+
+  Axiom sort_F_E_lt_proof_irrel : forall xs (p q : sort F.E.lt xs), p = q.
+
+  Lemma eq_if_Equal :
+    forall s s' : F.t, F.Equal s s' -> s = s'.
+  Proof.
+    intros [s1 pf1] [s2 pf2] Eq.
+    assert (s1 = s2).
+      unfold F.Raw.t in *.
+      eapply Sort_InA_eq_ext; eauto.
+      intros; eapply E.lt_trans; eauto.
+      intros; eapply OFacts.lt_eq; eauto.
+      intros; eapply OFacts.eq_lt; eauto.
+    subst s1.
+    rewrite (sort_F_E_lt_proof_irrel _ pf1 pf2).
+    reflexivity.
+  Qed.
+
+  (* end hide *)
+
+End Make.

coq-Fsub/Fsub_Definitions.v

@@ -0,0 +1,493 @@
+(** Definition of Fsub (System F with subtyping).
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
+
+    Table of contents:
+      - #<a href="##syntax">Syntax (pre-terms)</a>#
+      - #<a href="##open">Opening</a>#
+      - #<a href="##lc">Local closure</a>#
+      - #<a href="##env">Environments</a>#
+      - #<a href="##wf">Well-formedness</a>#
+      - #<a href="##sub">Subtyping</a>#
+      - #<a href="##typing_doc">Typing</a>#
+      - #<a href="##values">Values</a>#
+      - #<a href="##reduction">Reduction</a>#
+      - #<a href="##auto">Automation</a>#
+*)
+
+Require Export Metatheory.
+
+
+(* ********************************************************************** *)
+(** * #<a name="syntax"></a># Syntax (pre-terms) *)
+
+(** We use a locally nameless representation for Fsub, where bound
+    variables are represented as natural numbers (de Bruijn indices)
+    and free variables are represented as [atom]s.  The type [atom],
+    defined in the [Atom] library, represents names: there are
+    infinitely many atoms, equality is decidable on atoms, and it is
+    possible to generate an atom fresh for any given finite set of
+    atoms.
+
+    We say that the definitions below define pre-types ([typ]) and
+    pre-expressions ([exp]), collectively pre-terms, since the
+    datatypes admit terms, such as [(typ_all typ_top (typ_bvar 3))],
+    where indices are unbound.  A term is locally closed when it
+    contains no unbound indices.
+
+    Note that indices for bound type variables are distinct from
+    indices for bound expression variables.  We make this explicit in
+    the definitions below of the opening operations. *)
+
+Inductive typ : Set :=
+  | typ_top : typ
+  | typ_bvar : nat -> typ
+  | typ_fvar : atom -> typ
+  | typ_arrow : typ -> typ -> typ
+  | typ_all : typ -> typ -> typ
+.
+
+Inductive exp : Set :=
+  | exp_bvar : nat -> exp
+  | exp_fvar : atom -> exp
+  | exp_abs : typ -> exp -> exp
+  | exp_app : exp -> exp -> exp
+  | exp_tabs : typ -> exp -> exp
+  | exp_tapp : exp -> typ -> exp
+.
+
+(** We declare the constructors for indices and variables to be
+    coercions.  For example, if Coq sees a [nat] where it expects an
+    [exp], it will implicitly insert an application of [exp_bvar];
+    similar behavior happens for [atom]s.  Thus, we may write
+    [(exp_abs typ_top (exp_app 0 x))] instead of [(exp_abs typ_top
+    (exp_app (exp_bvar 0) (exp_fvar x)))]. *)
+
+Coercion typ_bvar : nat >-> typ.
+Coercion typ_fvar : atom >-> typ.
+Coercion exp_bvar : nat >-> exp.
+Coercion exp_fvar : atom >-> exp.
+
+
+(* ********************************************************************** *)
+(** * #<a name="open"></a># Opening terms *)
+
+(** Opening replaces an index with a term.  This operation is required
+    if we wish to work only with locally closed terms when going under
+    binders (e.g., the typing rule for [exp_abs]).  It also
+    corresponds to informal substitution for a bound variable, which
+    occurs in the rule for beta reduction.
+
+    We need to define three functions for opening due the syntax of
+    Fsub, and we name them according to the following convention.
+      - [tt]: Denotes an operation involving types appearing in types.
+      - [te]: Denotes an operation involving types appearing in
+        expressions.
+      - [ee]: Denotes an operation involving expressions appearing in
+        expressions.
+
+    The notation used below for decidable equality on atoms and
+    natural numbers (e.g., [K === J]) is defined in the [Metatheory]
+    library.  The order of arguments to each "open" function is the
+    same.  For example, [(open_tt_rec K U T)] can be read as
+    "substitute [U] for index [K] in [T]."
+
+    Note that we assume that [U] is locally closed (and similarly for
+    the other opening functions).  This assumption simplifies the
+    implementations of opening by letting us avoid shifting.  Since
+    bound variables are indices, there is no need to rename variables
+    to avoid capture.  Finally, we assume that these functions are
+    initially called with index zero and that zero is the only unbound
+    index in the term.  This eliminates the need to possibly subtract
+    one in the case of indices. *)
+
+Fixpoint open_tt_rec (K : nat) (U : typ) (T : typ)  {struct T} : typ :=
+  match T with
+  | typ_top => typ_top
+  | typ_bvar J => if K === J then U else (typ_bvar J)
+  | typ_fvar X => typ_fvar X
+  | typ_arrow T1 T2 => typ_arrow (open_tt_rec K U T1) (open_tt_rec K U T2)
+  | typ_all T1 T2 => typ_all (open_tt_rec K U T1) (open_tt_rec (S K) U T2)
+  end.
+
+Fixpoint open_te_rec (K : nat) (U : typ) (e : exp) {struct e} : exp :=
+  match e with
+  | exp_bvar i => exp_bvar i
+  | exp_fvar x => exp_fvar x
+  | exp_abs V e1 => exp_abs  (open_tt_rec K U V)  (open_te_rec K U e1)
+  | exp_app e1 e2 => exp_app  (open_te_rec K U e1) (open_te_rec K U e2)
+  | exp_tabs V e1 => exp_tabs (open_tt_rec K U V)  (open_te_rec (S K) U e1)
+  | exp_tapp e1 V => exp_tapp (open_te_rec K U e1) (open_tt_rec K U V)
+  end.
+
+Fixpoint open_ee_rec (k : nat) (f : exp) (e : exp)  {struct e} : exp :=
+  match e with
+  | exp_bvar i => if k === i then f else (exp_bvar i)
+  | exp_fvar x => exp_fvar x
+  | exp_abs V e1 => exp_abs V (open_ee_rec (S k) f e1)
+  | exp_app e1 e2 => exp_app (open_ee_rec k f e1) (open_ee_rec k f e2)
+  | exp_tabs V e1 => exp_tabs V (open_ee_rec k f e1)
+  | exp_tapp e1 V => exp_tapp (open_ee_rec k f e1) V
+  end.
+
+(** Many common applications of opening replace index zero with an
+    expression or variable.  The following definitions provide
+    convenient shorthands for such uses.  Note that the order of
+    arguments is switched relative to the definitions above.  For
+    example, [(open_tt T X)] can be read as "substitute the variable
+    [X] for index [0] in [T]" and "open [T] with the variable [X]."
+    Recall that the coercions above let us write [X] in place of
+    [(typ_fvar X)], assuming that [X] is an [atom]. *)
+
+Definition open_tt T U := open_tt_rec 0 U T.
+Definition open_te e U := open_te_rec 0 U e.
+Definition open_ee e1 e2 := open_ee_rec 0 e2 e1.
+
+
+(* ********************************************************************** *)
+(** * #<a name="lc"></a># Local closure *)
+
+(** Recall that [typ] and [exp] define pre-terms; these datatypes
+    admit terms that contain unbound indices.  A term is locally
+    closed, or syntactically well-formed, when no indices appearing in
+    it are unbound.  The proposition [(type T)] holds when a type [T]
+    is locally closed, and [(expr e)] holds when an expression [e] is
+    locally closed.
+
+    The inductive definitions below formalize local closure such that
+    the resulting induction principles serve as structural induction
+    principles over (locally closed) types and (locally closed)
+    expressions.  In particular, unlike the situation with pre-terms,
+    there are no cases for indices.  Thus, these induction principles
+    correspond more closely to informal practice than the ones arising
+    from the definitions of pre-terms.
+
+    The interesting cases in the inductive definitions below are those
+    that involve binding constructs, e.g., [typ_all].  Intuitively, to
+    check if the pre-term [(typ_all T1 T2)] is locally closed we much
+    check that [T1] is locally closed, and that [T2] is locally closed
+    when opened with a variable.  However, there is a choice as to how
+    many variables to quantify over.  One possibility is to quantify
+    over only one variable ("existential" quantification), as in
+<<
+  type_all : forall X T1 T2,
+      type T1 ->
+      type (open_tt T2 X) ->
+      type (typ_all T1 T2)
+>>  or we could quantify over as many variables as possible ("universal"
+    quantification), as in
+<<
+  type_all : forall T1 T2,
+      type T1 ->
+      (forall X : atom, type (open_tt T2 X)) ->
+      type (typ_all T1 T2)
+>>  It is possible to show that the resulting relations are equivalent.
+    The former makes it easy to build derivations, while the latter
+    provides a strong induction principle.  McKinna and Pollack used
+    both forms of this relation in their work on formalizing Pure Type
+    Systems.
+
+    We take a different approach here and use "cofinite
+    quantification": we quantify over all but finitely many variables.
+    This approach provides a convenient middle ground: we can build
+    derivations reasonably easily and get reasonably strong induction
+    principles.  With some work, one can show that the definitions
+    below are equivalent to ones that use existential, and hence also
+    universal, quantification. *)
+
+Inductive type : typ -> Prop :=
+  | type_top :
+      type typ_top
+  | type_var : forall X,
+      type (typ_fvar X)
+  | type_arrow : forall T1 T2,
+      type T1 ->
+      type T2 ->
+      type (typ_arrow T1 T2)
+  | type_all : forall L T1 T2,
+      type T1 ->
+      (forall X : atom, X `notin` L -> type (open_tt T2 X)) ->
+      type (typ_all T1 T2)
+.
+
+Inductive expr : exp -> Prop :=
+  | expr_var : forall x,
+      expr (exp_fvar x)
+  | expr_abs : forall L T e1,
+      type T ->
+      (forall x : atom, x `notin` L -> expr (open_ee e1 x)) ->
+      expr (exp_abs T e1)
+  | expr_app : forall e1 e2,
+      expr e1 ->
+      expr e2 ->
+      expr (exp_app e1 e2)
+  | expr_tabs : forall L T e1,
+      type T ->
+      (forall X : atom, X `notin` L -> expr (open_te e1 X)) ->
+      expr (exp_tabs T e1)
+  | expr_tapp : forall e1 V,
+      expr e1 ->
+      type V ->
+      expr (exp_tapp e1 V)
+.
+
+
+
+(* ********************************************************************** *)
+(** * #<a name="env"></a># Environments *)
+
+(** In our presentation of System F with subtyping, we use a single
+    environment for both typing and subtyping assumptions.  We
+    formalize environments by representing them as association lists
+    (lists of pairs of keys and values) whose keys are atoms.
+
+    The [Metatheory] and [Environment] libraries provide functions,
+    predicates, tactics, notations and lemmas that simplify working
+    with environments.  The [Environment] library treats environments
+    as lists of type [list (atom * A)].
+
+    Since environments map [atom]s, the type [A] should encode whether
+    a particular binding is a typing or subtyping assumption.  Thus,
+    we instantiate [A] with the type [binding], defined below. *)
+
+Inductive binding : Set :=
+  | bind_sub : typ -> binding
+  | bind_typ : typ -> binding.
+
+(** A binding [(X, bind_sub T)] records that a type variable [X] is a
+    subtype of [T], and a binding [(x, bind_typ U)] records that an
+    expression variable [x] has type [U].
+
+    We define an abbreviation [env] for the type of environments, and
+    an abbreviation [empty] for the empty environment.
+
+    Note: Each instance of [Notation] below defines an abbreviation
+    since the left-hand side consists of a single identifier that is
+    not in quotes.  These abbreviations are used for both parsing (the
+    left-hand side is equivalent to the right-hand side in all
+    contexts) and printing (the right-hand side is pretty-printed as
+    the left-hand side).  Since [nil] is normally a polymorphic
+    constructor whose type argument is implicit, we prefix the name
+    with "[@]" to signal to Coq that we are going to supply arguments
+    to [nil] explicitly. *)
+
+Notation env := (list (atom * binding)).
+Notation empty := (@nil (atom * binding)).
+
+(** We also define a notation that makes it convenient to write one
+    element lists.  This notation is useful because of our convention
+    for building environments; see the examples below. *)
+
+Notation "[ x ]" := (x :: nil).
+
+(** #<b>#Examples:#</b># We use a convention where environments are
+    never built using a cons operation [((x, a) :: E)] where [E] is
+    non-[nil].  This makes the shape of environments more uniform and
+    saves us from excessive fiddling with the shapes of environments.
+    For example, Coq's tactics sometimes distinguish between consing
+    on a new binding and prepending a one element list, even though
+    the two operations are convertible with each other.
+
+    Consider the following environments written in informal notation.
+<<
+  1. (empty environment)
+  2. x : T
+  3. x : T, Y <: S
+  4. E, x : T, F
+>>  In the third example, we have an environment that binds an
+    expression variable [x] to [T] and a type variable [Y] to [S].
+    In Coq, we would write these environments as follows.
+<<
+  1. empty
+  2. [(x, bind_typ T)]
+  3. [(Y, bind_sub S)] ++ [(x, bind_typ T)]
+  4. F ++ [(x, bind_typ T)] ++ E
+>> The symbol "[++]" denotes list concatenation and associates to the
+    right.  (That notation is defined in Coq's [List] library.)  Note
+    that in Coq, environments grow on the left, since that is where
+    the head of a list is. *)
+
+
+(* ********************************************************************** *)
+(** * #<a name="wf"></a># Well-formedness *)
+
+(** A type [T] is well-formed with respect to an environment [E],
+    denoted [(wf_typ E T)], when [T] is locally-closed and its free
+    variables are bound in [E].  We need this relation in order to
+    restrict the subtyping and typing relations, defined below, to
+    contain only well-formed types.  (This relation is missing in the
+    original statement of the POPLmark Challenge.)
+
+    Note: It is tempting to define the premise of [wf_typ_var] as [(X
+    `in` dom E)], since that makes the rule easier to apply (no need
+    to guess an instantiation for [U]).  Unfortunately, this is
+    incorrect.  We need to check that [X] is bound as a type-variable,
+    not an expression-variable; [(dom E)] does not distinguish between
+    the two kinds of bindings. *)
+
+Inductive wf_typ : env -> typ -> Prop :=
+  | wf_typ_top : forall E,
+      wf_typ E typ_top
+  | wf_typ_var : forall U E (X : atom),
+      binds X (bind_sub U) E ->
+      wf_typ E (typ_fvar X)
+  | wf_typ_arrow : forall E T1 T2,
+      wf_typ E T1 ->
+      wf_typ E T2 ->
+      wf_typ E (typ_arrow T1 T2)
+  | wf_typ_all : forall L E T1 T2,
+      wf_typ E T1 ->
+      (forall X : atom, X `notin` L ->
+        wf_typ ([(X, bind_sub T1)] ++ E) (open_tt T2 X)) ->
+      wf_typ E (typ_all T1 T2)
+.
+
+(** An environment E is well-formed, denoted [(wf_env E)], if each
+    atom is bound at most at once and if each binding is to a
+    well-formed type.  This is a stronger relation than the [ok]
+    relation defined in the [Environment] library.  We need this
+    relation in order to restrict the subtyping and typing relations,
+    defined below, to contain only well-formed environments.  (This
+    relation is missing in the original statement of the POPLmark
+    Challenge.)  *)
+
+Inductive wf_env : env -> Prop :=
+  | wf_env_empty :
+      wf_env empty
+  | wf_env_sub : forall (E : env) (X : atom) (T : typ),
+      wf_env E ->
+      wf_typ E T ->
+      X `notin` dom E ->
+      wf_env ([(X, bind_sub T)] ++ E)
+  | wf_env_typ : forall (E : env) (x : atom) (T : typ),
+      wf_env E ->
+      wf_typ E T ->
+      x `notin` dom E ->
+      wf_env ([(x, bind_typ T)] ++ E).
+
+
+(* ********************************************************************** *)
+(** * #<a name="sub"></a># Subtyping *)
+
+(** The definition of subtyping is straightforward.  It uses the
+    [binds] relation from the [Environment] library (in the
+    [sub_trans_tvar] case) and cofinite quantification (in the
+    [sub_all] case). *)
+
+Inductive sub : env -> typ -> typ -> Prop :=
+  | sub_top : forall E S,
+      wf_env E ->
+      wf_typ E S ->
+      sub E S typ_top
+  | sub_refl_tvar : forall E X,
+      wf_env E ->
+      wf_typ E (typ_fvar X) ->
+      sub E (typ_fvar X) (typ_fvar X)
+  | sub_trans_tvar : forall U E T X,
+      binds X (bind_sub U) E ->
+      sub E U T ->
+      sub E (typ_fvar X) T
+  | sub_arrow : forall E S1 S2 T1 T2,
+      sub E T1 S1 ->
+      sub E S2 T2 ->
+      sub E (typ_arrow S1 S2) (typ_arrow T1 T2)
+  | sub_all : forall L E S1 S2 T1 T2,
+      sub E T1 S1 ->
+      (forall X : atom, X `notin` L ->
+          sub ([(X, bind_sub T1)] ++ E) (open_tt S2 X) (open_tt T2 X)) ->
+      sub E (typ_all S1 S2) (typ_all T1 T2)
+.
+
+
+(* ********************************************************************** *)
+(** * #<a name="typing_doc"></a># Typing *)
+
+(** The definition of typing is straightforward.  It uses the [binds]
+    relation from the [Environment] library (in the [typing_var] case)
+    and cofinite quantification in the cases involving binders (e.g.,
+    [typing_abs] and [typing_tabs]). *)
+
+Inductive typing : env -> exp -> typ -> Prop :=
+  | typing_var : forall E x T,
+      wf_env E ->
+      binds x (bind_typ T) E ->
+      typing E (exp_fvar x) T
+  | typing_abs : forall L E V e1 T1,
+      (forall x : atom, x `notin` L ->
+        typing ([(x, bind_typ V)] ++ E) (open_ee e1 x) T1) ->
+      typing E (exp_abs V e1) (typ_arrow V T1)
+  | typing_app : forall T1 E e1 e2 T2,
+      typing E e1 (typ_arrow T1 T2) ->
+      typing E e2 T1 ->
+      typing E (exp_app e1 e2) T2
+  | typing_tabs : forall L E V e1 T1,
+      (forall X : atom, X `notin` L ->
+        typing ([(X, bind_sub V)] ++ E) (open_te e1 X) (open_tt T1 X)) ->
+      typing E (exp_tabs V e1) (typ_all V T1)
+  | typing_tapp : forall T1 E e1 T T2,
+      typing E e1 (typ_all T1 T2) ->
+      sub E T T1 ->
+      typing E (exp_tapp e1 T) (open_tt T2 T)
+  | typing_sub : forall S E e T,
+      typing E e S ->
+      sub E S T ->
+      typing E e T
+.
+
+
+(* ********************************************************************** *)
+(** * #<a name="values"></a># Values *)
+
+Inductive value : exp -> Prop :=
+  | value_abs : forall T e1,
+      expr (exp_abs T e1) ->
+      value (exp_abs T e1)
+  | value_tabs : forall T e1,
+      expr (exp_tabs T e1) ->
+      value (exp_tabs T e1)
+.
+
+
+(* ********************************************************************** *)
+(** * #<a name="reduction"></a># Reduction *)
+
+Inductive red : exp -> exp -> Prop :=
+  | red_app_1 : forall e1 e1' e2,
+      expr e2 ->
+      red e1 e1' ->
+      red (exp_app e1 e2) (exp_app e1' e2)
+  | red_app_2 : forall e1 e2 e2',
+      value e1 ->
+      red e2 e2' ->
+      red (exp_app e1 e2) (exp_app e1 e2')
+  | red_tapp : forall e1 e1' V,
+      type V ->
+      red e1 e1' ->
+      red (exp_tapp e1 V) (exp_tapp e1' V)
+  | red_abs : forall T e1 v2,
+      expr (exp_abs T e1) ->
+      value v2 ->
+      red (exp_app (exp_abs T e1) v2) (open_ee e1 v2)
+  | red_tabs : forall T1 e1 T2,
+      expr (exp_tabs T1 e1) ->
+      type T2 ->
+      red (exp_tapp (exp_tabs T1 e1) T2) (open_te e1 T2)
+.
+
+
+(* ********************************************************************** *)
+(** * #<a name="auto"></a># Automation *)
+
+(** We declare most constructors as [Hint]s to be used by the [auto]
+    and [eauto] tactics.  We exclude constructors from the subtyping
+    and typing relations that use cofinite quantification.  It is
+    unlikely that [eauto] will find an instantiation for the finite
+    set [L], and in those cases, [eauto] can take some time to fail.
+    (A priori, this is not obvious.  In practice, one adds as hints
+    all constructors and then later removes some constructors when
+    they cause proof search to take too long.) *)
+
+Hint Constructors type expr wf_typ wf_env value red.
+Hint Resolve sub_top sub_refl_tvar sub_arrow.
+Hint Resolve typing_var typing_app typing_tapp typing_sub.

coq-Fsub/Fsub_Infrastructure.v

@@ -0,0 +1,665 @@
+(** Infrastructure lemmas and tactic definitions for Fsub.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
+
+    This file contains a number of definitions, tactics, and lemmas
+    that are based only on the syntax of the language at hand.  While
+    the exact statements of everything here would change for a
+    different language, the general structure of this file (i.e., the
+    sequence of definitions, tactics, and lemmas) would remain the
+    same.
+
+    Table of contents:
+      - #<a href="##fv">Free variables</a>#
+      - #<a href="##subst">Substitution</a>#
+      - #<a href="##pick_fresh">The "pick fresh" tactic</a>#
+      - #<a href="##apply_fresh">The "pick fresh and apply" tactic</a>#
+      - #<a href="##properties">Properties of opening and substitution</a>#
+      - #<a href="##lc">Local closure is preserved under substitution</a>#
+      - #<a href="##auto">Automation</a># *)
+
+
+Require Export Fsub_Definitions.
+
+
+(* ********************************************************************** *)
+(** * #<a name="fv"></a># Free variables *)
+
+(** In this section, we define free variable functions.  The functions
+    [fv_tt] and [fv_te] calculate the set of atoms used as free type
+    variables in a type or expression, respectively.  The function
+    [fv_ee] calculates the set of atoms used as free expression
+    variables in an expression.  Cases involving binders are
+    straightforward since bound variables are indices, not names, in
+    locally nameless representation. *)
+
+Fixpoint fv_tt (T : typ) {struct T} : atoms :=
+  match T with
+  | typ_top => {}
+  | typ_bvar J => {}
+  | typ_fvar X => singleton X
+  | typ_arrow T1 T2 => (fv_tt T1) `union` (fv_tt T2)
+  | typ_all T1 T2 => (fv_tt T1) `union` (fv_tt T2)
+  end.
+
+Fixpoint fv_te (e : exp) {struct e} : atoms :=
+  match e with
+  | exp_bvar i => {}
+  | exp_fvar x => {}
+  | exp_abs V e1  => (fv_tt V) `union` (fv_te e1)
+  | exp_app e1 e2 => (fv_te e1) `union` (fv_te e2)
+  | exp_tabs V e1 => (fv_tt V) `union` (fv_te e1)
+  | exp_tapp e1 V => (fv_tt V) `union` (fv_te e1)
+  end.
+
+Fixpoint fv_ee (e : exp) {struct e} : atoms :=
+  match e with
+  | exp_bvar i => {}
+  | exp_fvar x => singleton x
+  | exp_abs V e1 => (fv_ee e1)
+  | exp_app e1 e2 => (fv_ee e1) `union` (fv_ee e2)
+  | exp_tabs V e1 => (fv_ee e1)
+  | exp_tapp e1 V => (fv_ee e1)
+  end.
+
+
+(* ********************************************************************** *)
+(** * #<a name="subst"></a># Substitution *)
+
+(** In this section, we define substitution for expression and type
+    variables appearing in types, expressions, and environments.
+    Substitution differs from opening because opening replaces indices
+    whereas substitution replaces free variables.  The definitions
+    below are relatively simple for two reasons.
+      - We are using locally nameless representation, where bound
+        variables are represented using indices.  Thus, there is no
+        need to rename variables to avoid capture.
+      - The definitions below assume that the term being substituted
+        in, i.e., the second argument to each function, is locally
+        closed.  Thus, there is no need to shift indices when passing
+        under a binder. *)
+
+Fixpoint subst_tt (Z : atom) (U : typ) (T : typ) {struct T} : typ :=
+  match T with
+  | typ_top => typ_top
+  | typ_bvar J => typ_bvar J
+  | typ_fvar X => if X == Z then U else T
+  | typ_arrow T1 T2 => typ_arrow (subst_tt Z U T1) (subst_tt Z U T2)
+  | typ_all T1 T2 => typ_all (subst_tt Z U T1) (subst_tt Z U T2)
+  end.
+
+Fixpoint subst_te (Z : atom) (U : typ) (e : exp) {struct e} : exp :=
+  match e with
+  | exp_bvar i => exp_bvar i
+  | exp_fvar x => exp_fvar x
+  | exp_abs V e1 => exp_abs  (subst_tt Z U V)  (subst_te Z U e1)
+  | exp_app e1 e2 => exp_app  (subst_te Z U e1) (subst_te Z U e2)
+  | exp_tabs V e1 => exp_tabs (subst_tt Z U V)  (subst_te Z U e1)
+  | exp_tapp e1 V => exp_tapp (subst_te Z U e1) (subst_tt Z U V)
+  end.
+
+Fixpoint subst_ee (z : atom) (u : exp) (e : exp) {struct e} : exp :=
+  match e with
+  | exp_bvar i => exp_bvar i
+  | exp_fvar x => if x == z then u else e
+  | exp_abs V e1 => exp_abs V (subst_ee z u e1)
+  | exp_app e1 e2 => exp_app (subst_ee z u e1) (subst_ee z u e2)
+  | exp_tabs V e1 => exp_tabs V (subst_ee z u e1)
+  | exp_tapp e1 V => exp_tapp (subst_ee z u e1) V
+  end.
+
+Definition subst_tb (Z : atom) (P : typ) (b : binding) : binding :=
+  match b with
+  | bind_sub T => bind_sub (subst_tt Z P T)
+  | bind_typ T => bind_typ (subst_tt Z P T)
+  end.
+
+
+(* ********************************************************************** *)
+(** * #<a name="pick_fresh"></a># The "[pick fresh]" tactic *)
+
+(** The "[pick fresh]" tactic introduces a fresh atom into the context.
+    We define it in two steps.
+
+    The first step is to define an auxiliary tactic [gather_atoms],
+    meant to be used in the definition of other tactics, which returns
+    a set of atoms in the current context.  The definition of
+    [gather_atoms] follows a pattern based on repeated calls to
+    [gather_atoms_with].  The one argument to this tactic is a
+    function that takes an object of some particular type and returns
+    a set of atoms that appear in that argument.  It is not necessary
+    to understand exactly how [gather_atoms_with] works.  If we add a
+    new inductive datatype, say for kinds, to our language, then we
+    would need to modify [gather_atoms].  On the other hand, if we
+    merely add a new type, say products, then there is no need to
+    modify [gather_atoms]; the required changes would be made in
+    [fv_tt]. *)
+
+Ltac gather_atoms :=
+  let A := gather_atoms_with (fun x : atoms => x) in
+  let B := gather_atoms_with (fun x : atom => singleton x) in
+  let C := gather_atoms_with (fun x : exp => fv_te x) in
+  let D := gather_atoms_with (fun x : exp => fv_ee x) in
+  let E := gather_atoms_with (fun x : typ => fv_tt x) in
+  let F := gather_atoms_with (fun x : env => dom x) in
+  constr:(A `union` B `union` C `union` D `union` E `union` F).
+
+(** The second step in defining "[pick fresh]" is to define the tactic
+    itself.  It is based on the [(pick fresh ... for ...)] tactic
+    defined in the [Atom] library.  Here, we use [gather_atoms] to
+    construct the set [L] rather than leaving it to the user to
+    provide.  Thus, invoking [(pick fresh x)] introduces a new atom
+    [x] into the current context that is fresh for "everything" in the
+    context. *)
+
+Tactic Notation "pick" "fresh" ident(x) :=
+  let L := gather_atoms in (pick fresh x for L).
+
+
+(* *********************************************************************** *)
+(** * #<a name="apply_fresh"></a># The "[pick fresh and apply]" tactic *)
+
+(** This tactic is implementation specific only because of its
+    reliance on [gather_atoms], which is itself implementation
+    specific.  The definition below may be copied between developments
+    without any changes, assuming that the other other developments
+    define an appropriate [gather_atoms] tactic.  For documentation on
+    the tactic on which the one below is based, see the
+    [Metatheory] library. *)
+
+Tactic Notation
+      "pick" "fresh" ident(atom_name) "and" "apply" constr(lemma) :=
+  let L := gather_atoms in
+  pick fresh atom_name excluding L and apply lemma.
+
+
+(* ********************************************************************** *)
+(** * #<a name="properties"></a># Properties of opening and substitution *)
+
+(** The following lemmas provide useful structural properties of
+    substitution and opening.  While the exact statements are language
+    specific, we have found that similar properties are needed in a
+    wide range of languages.
+
+    Below, we indicate which lemmas depend on which other lemmas.
+    Since [te] functions depend on their [tt] counterparts, a similar
+    dependency can be found in the lemmas.
+
+    The lemmas are split into three sections, one each for the [tt],
+    [te], and [ee] functions.  The most important lemmas are the
+    following:
+      - Substitution and opening commute with each other, e.g.,
+        [subst_tt_open_tt_var].
+      - Opening a term is equivalent to opening the term with a fresh
+        name and then substituting for that name, e.g.,
+        [subst_tt_intro].
+
+    We keep the sections as uniform in structure as possible.  In
+    particular, we state explicitly strengthened induction hypotheses
+    even when there are more concise ways of proving the lemmas of
+    interest. *)
+
+
+(* ********************************************************************** *)
+(** ** Properties of type substitution in types *)
+
+(** The next lemma is the strengthened induction hypothesis for the
+    lemma that follows, which states that opening a locally closed
+    term is the identity.  This lemma is not otherwise independently
+    useful. *)
+
+Lemma open_tt_rec_type_aux : forall T j V i U,
+  i <> j ->
+  open_tt_rec j V T = open_tt_rec i U (open_tt_rec j V T) ->
+  T = open_tt_rec i U T.
+Proof with eauto*.
+  induction T; intros j V i U Neq H; simpl in *; inversion H; f_equal...
+  Case "typ_bvar".
+    destruct (j === n)... destruct (i === n)...
+Qed.
+
+(** Opening a locally closed term is the identity.  This lemma depends
+    on the immediately preceding lemma. *)
+
+Lemma open_tt_rec_type : forall T U k,
+  type T ->
+  T = open_tt_rec k U T.
+Proof with auto*.
+  intros T U k Htyp. revert k.
+  induction Htyp; intros k; simpl; f_equal...
+  Case "typ_all".
+    unfold open_tt in *.
+    pick fresh X.
+    apply (open_tt_rec_type_aux T2 0 (typ_fvar X))...
+Qed.
+
+(** If a name is fresh for a term, then substituting for it is the
+    identity. *)
+
+Lemma subst_tt_fresh : forall Z U T,
+   Z `notin` fv_tt T ->
+   T = subst_tt Z U T.
+Proof with auto*.
+  induction T; simpl; intro H; f_equal...
+  Case "typ_fvar".
+    destruct (a == Z)...
+    absurd_hyp H; fsetdec.
+Qed.
+
+(** Substitution commutes with opening under certain conditions.  This
+    lemma depends on the fact that opening a locally closed term is
+    the identity. *)
+
+Lemma subst_tt_open_tt_rec : forall T1 T2 X P k,
+  type P ->
+  subst_tt X P (open_tt_rec k T2 T1) =
+    open_tt_rec k (subst_tt X P T2) (subst_tt X P T1).
+Proof with auto*.
+  intros T1 T2 X P k WP. revert k.
+  induction T1; intros k; simpl; f_equal...
+  Case "typ_bvar".
+    destruct (k === n); subst...
+  Case "typ_fvar".
+    destruct (a == X); subst... apply open_tt_rec_type...
+Qed.
+
+(** The next lemma is a direct corollary of the immediately preceding
+    lemma---the index is specialized to zero. *)
+
+Lemma subst_tt_open_tt : forall T1 T2 (X:atom) P,
+  type P ->
+  subst_tt X P (open_tt T1 T2) = open_tt (subst_tt X P T1) (subst_tt X P T2).
+Proof with auto*.
+  intros.
+  unfold open_tt.
+  apply subst_tt_open_tt_rec...
+Qed.
+
+(** The next lemma is a direct corollary of the immediately preceding
+    lemma---here, we're opening the term with a variable.  In
+    practice, this lemma seems to be needed as a left-to-right rewrite
+    rule, when stated in its current form. *)
+
+Lemma subst_tt_open_tt_var : forall (X Y:atom) P T,
+  Y <> X ->
+  type P ->
+  open_tt (subst_tt X P T) Y = subst_tt X P (open_tt T Y).
+Proof with auto*.
+  intros X Y P T Neq Wu.
+  unfold open_tt.
+  rewrite subst_tt_open_tt_rec...
+  simpl.
+  destruct (Y == X)...
+Qed.
+
+(** The next lemma states that opening a term is equivalent to first
+    opening the term with a fresh name and then substituting for the
+    name.  This is actually the strengthened induction hypothesis for
+    the version we use in practice. *)
+
+Lemma subst_tt_intro_rec : forall X T2 U k,
+  X `notin` fv_tt T2 ->
+  open_tt_rec k U T2 = subst_tt X U (open_tt_rec k (typ_fvar X) T2).
+Proof with auto*.
+  induction T2; intros U k Fr; simpl in *; f_equal...
+  Case "typ_bvar".
+    destruct (k === n)... simpl. destruct (X == X)...
+  Case "typ_fvar".
+    destruct (a == X)... absurd_hyp Fr; fsetdec.
+Qed.
+
+(** The next lemma is a direct corollary of the immediately preceding
+    lemma---the index is specialized to zero.  *)
+
+Lemma subst_tt_intro : forall X T2 U,
+  X `notin` fv_tt T2 ->
+  open_tt T2 U = subst_tt X U (open_tt T2 X).
+Proof with auto*.
+  intros.
+  unfold open_tt.
+  apply subst_tt_intro_rec...
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Properties of type substitution in expressions *)
+
+(** This section follows the structure of the previous section.  The
+    one notable difference is that we require two auxiliary lemmas to
+    show that substituting a type in a locally-closed expression is
+    the identity. *)
+
+Lemma open_te_rec_expr_aux : forall e j u i P ,
+  open_ee_rec j u e = open_te_rec i P (open_ee_rec j u e) ->
+  e = open_te_rec i P e.
+Proof with eauto*.
+  induction e; intros j u i P H; simpl in *; inversion H; f_equal...
+Qed.
+
+Lemma open_te_rec_type_aux : forall e j Q i P,
+  i <> j ->
+  open_te_rec j Q e = open_te_rec i P (open_te_rec j Q e) ->
+  e = open_te_rec i P e.
+Proof.
+  induction e; intros j Q i P Neq Heq; simpl in *; inversion Heq;
+    f_equal; eauto using open_tt_rec_type_aux.
+Qed.
+
+Lemma open_te_rec_expr : forall e U k,
+  expr e ->
+  e = open_te_rec k U e.
+Proof with auto*.
+  intros e U k WF. revert k.
+  induction WF; intros k; simpl; f_equal; auto using open_tt_rec_type;
+  try solve [
+    unfold open_ee in *;
+    pick fresh x;
+    eapply open_te_rec_expr_aux with (j := 0) (u := exp_fvar x);
+    auto*
+  | unfold open_te in *;
+    pick fresh X;
+    eapply open_te_rec_type_aux with (j := 0) (Q := typ_fvar X);
+    auto*
+  ].
+Qed.
+
+Lemma subst_te_fresh : forall X U e,
+  X `notin` fv_te e ->
+  e = subst_te X U e.
+Proof.
+  induction e; simpl; intros; f_equal; auto using subst_tt_fresh.
+Qed.
+
+Lemma subst_te_open_te_rec : forall e T X U k,
+  type U ->
+  subst_te X U (open_te_rec k T e) =
+    open_te_rec k (subst_tt X U T) (subst_te X U e).
+Proof.
+  intros e T X U k WU. revert k.
+  induction e; intros k; simpl; f_equal; auto using subst_tt_open_tt_rec.
+Qed.
+
+Lemma subst_te_open_te : forall e T X U,
+  type U ->
+  subst_te X U (open_te e T) = open_te (subst_te X U e) (subst_tt X U T).
+Proof with auto*.
+  intros.
+  unfold open_te.
+  apply subst_te_open_te_rec...
+Qed.
+
+Lemma subst_te_open_te_var : forall (X Y:atom) U e,
+  Y <> X ->
+  type U ->
+  open_te (subst_te X U e) Y = subst_te X U (open_te e Y).
+Proof with auto*.
+  intros X Y U e Neq WU.
+  unfold open_te.
+  rewrite subst_te_open_te_rec...
+  simpl.
+  destruct (Y == X)...
+Qed.
+
+Lemma subst_te_intro_rec : forall X e U k,
+  X `notin` fv_te e ->
+  open_te_rec k U e = subst_te X U (open_te_rec k (typ_fvar X) e).
+Proof.
+  induction e; intros U k Fr; simpl in *; f_equal;
+    auto using subst_tt_intro_rec.
+Qed.
+
+Lemma subst_te_intro : forall X e U,
+  X `notin` fv_te e ->
+  open_te e U = subst_te X U (open_te e X).
+Proof with auto*.
+  intros.
+  unfold open_te.
+  apply subst_te_intro_rec...
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Properties of expression substitution in expressions *)
+
+(** This section follows the structure of the previous two sections. *)
+
+Lemma open_ee_rec_expr_aux : forall e j v u i,
+  i <> j ->
+  open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) ->
+  e = open_ee_rec i u e.
+Proof with eauto*.
+  induction e; intros j v u i Neq H; simpl in *; inversion H; f_equal...
+  Case "exp_bvar".
+    destruct (j===n)... destruct (i===n)...
+Qed.
+
+Lemma open_ee_rec_type_aux : forall e j V u i,
+  open_te_rec j V e = open_ee_rec i u (open_te_rec j V e) ->
+  e = open_ee_rec i u e.
+Proof.
+  induction e; intros j V u i H; simpl; inversion H; f_equal; eauto.
+Qed.
+
+Lemma open_ee_rec_expr : forall u e k,
+  expr e ->
+  e = open_ee_rec k u e.
+Proof with auto*.
+  intros u e k Hexpr. revert k.
+  induction Hexpr; intro k; simpl; f_equal; auto*;
+  try solve [
+    unfold open_ee in *;
+    pick fresh x;
+    eapply open_ee_rec_expr_aux with (j := 0) (v := exp_fvar x);
+    auto*
+  | unfold open_te in *;
+    pick fresh X;
+    eapply open_ee_rec_type_aux with (j := 0) (V := typ_fvar X);
+    auto*
+  ].
+Qed.
+
+Lemma subst_ee_fresh : forall (x: atom) u e,
+  x `notin` fv_ee e ->
+  e = subst_ee x u e.
+Proof with auto*.
+  intros x u e; induction e; simpl; intro H; f_equal...
+  Case "exp_fvar".
+    destruct (a==x)...
+    absurd_hyp H; fsetdec.
+Qed.
+
+Lemma subst_ee_open_ee_rec : forall e1 e2 x u k,
+  expr u ->
+  subst_ee x u (open_ee_rec k e2 e1) =
+    open_ee_rec k (subst_ee x u e2) (subst_ee x u e1).
+Proof with auto*.
+  intros e1 e2 x u k WP. revert k.
+  induction e1; intros k; simpl; f_equal...
+  Case "exp_bvar".
+    destruct (k === n); subst...
+  Case "exp_fvar".
+    destruct (a == x); subst... apply open_ee_rec_expr...
+Qed.
+
+Lemma subst_ee_open_ee : forall e1 e2 x u,
+  expr u ->
+  subst_ee x u (open_ee e1 e2) =
+    open_ee (subst_ee x u e1) (subst_ee x u e2).
+Proof with auto*.
+  intros.
+  unfold open_ee.
+  apply subst_ee_open_ee_rec...
+Qed.
+
+Lemma subst_ee_open_ee_var : forall (x y:atom) u e,
+  y <> x ->
+  expr u ->
+  open_ee (subst_ee x u e) y = subst_ee x u (open_ee e y).
+Proof with auto*.
+  intros x y u e Neq Wu.
+  unfold open_ee.
+  rewrite subst_ee_open_ee_rec...
+  simpl.
+  destruct (y == x)...
+Qed.
+
+Lemma subst_te_open_ee_rec : forall e1 e2 Z P k,
+  subst_te Z P (open_ee_rec k e2 e1) =
+    open_ee_rec k (subst_te Z P e2) (subst_te Z P e1).
+Proof with auto*.
+  induction e1; intros e2 Z P k; simpl; f_equal...
+  Case "exp_bvar".
+    destruct (k === n)...
+Qed.
+
+Lemma subst_te_open_ee : forall e1 e2 Z P,
+  subst_te Z P (open_ee e1 e2) = open_ee (subst_te Z P e1) (subst_te Z P e2).
+Proof with auto*.
+  intros.
+  unfold open_ee.
+  apply subst_te_open_ee_rec...
+Qed.
+
+Lemma subst_te_open_ee_var : forall Z (x:atom) P e,
+  open_ee (subst_te Z P e) x = subst_te Z P (open_ee e x).
+Proof with auto*.
+  intros.
+  rewrite subst_te_open_ee...
+Qed.
+
+Lemma subst_ee_open_te_rec : forall e P z u k,
+  expr u ->
+  subst_ee z u (open_te_rec k P e) = open_te_rec k P (subst_ee z u e).
+Proof with auto*.
+  induction e; intros P z u k H; simpl; f_equal...
+  Case "exp_fvar".
+    destruct (a == z)... apply open_te_rec_expr...
+Qed.
+
+Lemma subst_ee_open_te : forall e P z u,
+  expr u ->
+  subst_ee z u (open_te e P) = open_te (subst_ee z u e) P.
+Proof with auto*.
+  intros.
+  unfold open_te.
+  apply subst_ee_open_te_rec...
+Qed.
+
+Lemma subst_ee_open_te_var : forall z (X:atom) u e,
+  expr u ->
+  open_te (subst_ee z u e) X = subst_ee z u (open_te e X).
+Proof with auto*.
+  intros z X u e H.
+  rewrite subst_ee_open_te...
+Qed.
+
+Lemma subst_ee_intro_rec : forall x e u k,
+  x `notin` fv_ee e ->
+  open_ee_rec k u e = subst_ee x u (open_ee_rec k (exp_fvar x) e).
+Proof with auto*.
+  induction e; intros u k Fr; simpl in *; f_equal...
+  Case "exp_bvar".
+    destruct (k === n)... simpl. destruct (x == x)...
+  Case "exp_fvar".
+    destruct (a == x)... absurd_hyp Fr; fsetdec.
+Qed.
+
+Lemma subst_ee_intro : forall x e u,
+  x `notin` fv_ee e ->
+  open_ee e u = subst_ee x u (open_ee e x).
+Proof with auto*.
+  intros.
+  unfold open_ee.
+  apply subst_ee_intro_rec...
+Qed.
+
+
+(* *********************************************************************** *)
+(** * #<a name="lc"></a># Local closure is preserved under substitution *)
+
+(** While these lemmas may be considered properties of substitution, we
+    separate them out due to the lemmas that they depend on. *)
+
+(** The following lemma depends on [subst_tt_open_tt_var]. *)
+
+Lemma subst_tt_type : forall Z P T,
+  type T ->
+  type P ->
+  type (subst_tt Z P T).
+Proof with auto.
+  intros Z P T HT HP.
+  induction HT; simpl...
+  Case "type_fvar".
+    destruct (X == Z)...
+  Case "type_all".
+    pick fresh Y and apply type_all...
+    rewrite subst_tt_open_tt_var...
+Qed.
+
+(** The following lemma depends on [subst_tt_type] and
+    [subst_te_open_ee_var]. *)
+
+Lemma subst_te_expr : forall Z P e,
+  expr e ->
+  type P ->
+  expr (subst_te Z P e).
+Proof with eauto using subst_tt_type.
+  intros Z P e He Hp.
+  induction He; simpl; auto using subst_tt_type;
+  try solve [
+    econstructor;
+    try instantiate (1 := L `union` singleton Z);
+    intros;
+    try rewrite subst_te_open_ee_var;
+    try rewrite subst_te_open_te_var;
+    eauto using subst_tt_type
+  ].
+Qed.
+
+(** The following lemma depends on [subst_ee_open_ee_var] and
+    [subst_ee_open_te_var]. *)
+
+Lemma subst_ee_expr : forall z e1 e2,
+  expr e1 ->
+  expr e2 ->
+  expr (subst_ee z e2 e1).
+Proof with auto.
+  intros z e1 e2 He1 He2.
+  induction He1; simpl; auto;
+  try solve [
+    econstructor;
+    try instantiate (1 := L `union` singleton z);
+    intros;
+    try rewrite subst_ee_open_ee_var;
+    try rewrite subst_ee_open_te_var;
+    auto
+  ].
+  Case "expr_var".
+    destruct (x == z)...
+Qed.
+
+
+
+
+
+
+
+(* *********************************************************************** *)
+(** * #<a name="auto"></a># Automation *)
+
+(** We add as hints the fact that local closure is preserved under
+    substitution.  This is part of our strategy for automatically
+    discharging local-closure proof obligations. *)
+
+Hint Resolve subst_tt_type subst_te_expr subst_ee_expr.
+
+
+
+(** When reasoning about the [binds] relation and [map], we
+    occasionally encounter situations where the binding is
+    over-simplified.  The following hint undoes that simplification,
+    thus enabling [Hint]s from the [Environment] library. *)
+
+Hint Extern 1 (binds _ (?F (subst_tt ?X ?U ?T)) _) =>
+  unsimpl (subst_tb X U (F T)).

coq-Fsub/Fsub_Lemmas.v

@@ -0,0 +1,399 @@
+(** Administrative lemmas for Fsub.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
+
+    This file contains a number of administrative lemmas that we
+    require for proving type-safety.  The lemmas mainly concern the
+    relations [wf_typ] and [wf_env].
+
+    This file also contains regularity lemmas, which show that various
+    relations hold only for locally closed terms.  In addition to
+    being necessary to complete the proof of type-safety, these lemmas
+    help demonstrate that our definitions are correct; they would be
+    worth proving even if they are unneeded for any "real" proofs.
+
+    Table of contents:
+      - #<a href="##wft">Properties of wf_typ</a>#
+      - #<a href="##oktwft">Properties of wf_env and wf_typ</a>#
+      - #<a href="##okt">Properties of wf_env</a>#
+      - #<a href="##subst">Properties of substitution</a>#
+      - #<a href="##regularity">Regularity lemmas</a>#
+      - #<a href="##auto">Automation</a># *)
+
+Require Export Fsub_Infrastructure.
+
+
+(* ********************************************************************** *)
+(** * #<a name="wft"></a># Properties of [wf_typ] *)
+
+(** If a type is well-formed in an environment, then it is locally
+    closed. *)
+
+Lemma type_from_wf_typ : forall E T,
+  wf_typ E T -> type T.
+Proof.
+  intros E T H; induction H; eauto.
+Qed.
+
+(** The remaining properties are analogous to the properties that we
+    need to show for the subtyping and typing relations. *)
+
+Lemma wf_typ_weakening : forall T E F G,
+  wf_typ (G ++ E) T ->
+  ok (G ++ F ++ E) ->
+  wf_typ (G ++ F ++ E) T.
+Proof with simpl_env; eauto.
+  intros T E F G Hwf_typ Hk.
+  remember (G ++ E) as F.
+  generalize dependent G.
+  induction Hwf_typ; intros G Hok Heq; subst...
+  Case "type_all".
+    pick fresh Y and apply wf_typ_all...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+Lemma wf_typ_weaken_head : forall T E F,
+  wf_typ E T ->
+  ok (F ++ E) ->
+  wf_typ (F ++ E) T.
+Proof.
+  intros.
+  rewrite_env (empty ++ F++ E).
+  auto using wf_typ_weakening.
+Qed.
+
+Lemma wf_typ_narrowing : forall V U T E F X,
+  wf_typ (F ++ [(X, bind_sub V)] ++ E) T ->
+  ok (F ++ [(X, bind_sub U)] ++ E) ->
+  wf_typ (F ++ [(X, bind_sub U)] ++ E) T.
+Proof with simpl_env; eauto.
+  intros V U T E F X Hwf_typ Hok.
+  remember (F ++ [(X, bind_sub V)] ++ E) as G.
+  generalize dependent F.
+  induction Hwf_typ; intros F Hok Heq; subst...
+  Case "wf_typ_var".
+    binds_cases H...
+  Case "typ_all".
+    pick fresh Y and apply wf_typ_all...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+Lemma wf_typ_strengthening : forall E F x U T,
+ wf_typ (F ++ [(x, bind_typ U)] ++ E) T ->
+ wf_typ (F ++ E) T.
+Proof with simpl_env; eauto.
+  intros E F x U T H.
+  remember (F ++ [(x, bind_typ U)] ++ E) as G.
+  generalize dependent F.
+  induction H; intros F Heq; subst...
+  Case "wf_typ_var".
+    binds_cases H...
+  Case "wf_typ_all".
+    pick fresh Y and apply wf_typ_all...
+    rewrite <- concat_assoc.
+    apply H1...
+Qed.
+
+Lemma wf_typ_subst_tb : forall F Q E Z P T,
+  wf_typ (F ++ [(Z, bind_sub Q)] ++ E) T ->
+  wf_typ E P ->
+  ok (map (subst_tb Z P) F ++ E) ->
+  wf_typ (map (subst_tb Z P) F ++ E) (subst_tt Z P T).
+Proof with simpl_env; eauto using wf_typ_weaken_head, type_from_wf_typ.
+  intros F Q E Z P T WT WP.
+  remember (F ++ [(Z, bind_sub Q)] ++ E) as G.
+  generalize dependent F.
+  induction WT; intros F EQ Ok; subst; simpl subst_tt...
+  Case "wf_typ_var".
+    destruct (X == Z); subst...
+    SCase "X <> Z".
+      binds_cases H...
+      apply (wf_typ_var (subst_tt Z P U))...
+  Case "wf_typ_all".
+    pick fresh Y and apply wf_typ_all...
+    rewrite subst_tt_open_tt_var...
+    rewrite_env (map (subst_tb Z P) ([(Y, bind_sub T1)] ++ F) ++ E).
+    apply H0...
+Qed.
+
+Lemma wf_typ_open : forall E U T1 T2,
+  ok E ->
+  wf_typ E (typ_all T1 T2) ->
+  wf_typ E U ->
+  wf_typ E (open_tt T2 U).
+Proof with simpl_env; eauto.
+  intros E U T1 T2 Ok WA WU.
+  inversion WA; subst.
+  pick fresh X.
+  rewrite (subst_tt_intro X)...
+  rewrite_env (map (subst_tb X U) empty ++ E).
+  eapply wf_typ_subst_tb...
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="oktwft"></a># Properties of [wf_env] and [wf_typ] *)
+
+Lemma ok_from_wf_env : forall E,
+  wf_env E ->
+  ok E.
+Proof.
+  intros E H; induction H; auto.
+Qed.
+
+(** We add [ok_from_wf_env] as a hint here since it helps blur the
+    distinction between [wf_env] and [ok] in proofs.  The lemmas in
+    the [Environment] library use [ok], whereas here we naturally have
+    (or can easily show) the stronger [wf_env].  Thus,
+    [ok_from_wf_env] serves as a bridge that allows us to use the
+    environments library. *)
+
+Hint Resolve ok_from_wf_env.
+
+Lemma wf_typ_from_binds_typ : forall x U E,
+  wf_env E ->
+  binds x (bind_typ U) E ->
+  wf_typ E U.
+Proof with auto using wf_typ_weaken_head.
+  induction 1; intros J; binds_cases J...
+  inversion H4; subst...
+Qed.
+
+Lemma wf_typ_from_wf_env_typ : forall x T E,
+  wf_env ([(x, bind_typ T)] ++ E) ->
+  wf_typ E T.
+Proof.
+  intros x T E H. inversion H; auto.
+Qed.
+
+Lemma wf_typ_from_wf_env_sub : forall x T E,
+  wf_env ([(x, bind_sub T)] ++ E) ->
+  wf_typ E T.
+Proof.
+  intros x T E H. inversion H; auto.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="okt"></a># Properties of [wf_env] *)
+
+(** These properties are analogous to the properties that we need to
+    show for the subtyping and typing relations. *)
+
+Lemma wf_env_narrowing : forall V E F U X,
+  wf_env (F ++ [(X, bind_sub V)] ++ E) ->
+  wf_typ E U ->
+  wf_env (F ++ [(X, bind_sub U)] ++ E).
+Proof with eauto 6 using wf_typ_narrowing.
+  induction F; intros U X Wf_env Wf;
+    inversion Wf_env; subst; simpl_env in *...
+Qed.
+
+Lemma wf_env_strengthening : forall x T E F,
+  wf_env (F ++ [(x, bind_typ T)] ++ E) ->
+  wf_env (F ++ E).
+Proof with eauto using wf_typ_strengthening.
+  induction F; intros Wf_env; inversion Wf_env; subst; simpl_env in *...
+Qed.
+
+Lemma wf_env_subst_tb : forall Q Z P E F,
+  wf_env (F ++ [(Z, bind_sub Q)] ++ E) ->
+  wf_typ E P ->
+  wf_env (map (subst_tb Z P) F ++ E).
+Proof with eauto 6 using wf_typ_subst_tb.
+  induction F; intros Wf_env WP; simpl_env;
+    inversion Wf_env; simpl_env in *; simpl subst_tb...
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="subst"></a># Environment is unchanged by substitution for a fresh name *)
+
+Lemma notin_fv_tt_open : forall (Y X : atom) T,
+  X `notin` fv_tt (open_tt T Y) ->
+  X `notin` fv_tt T.
+Proof.
+ intros Y X T. unfold open_tt.
+ generalize 0.
+ induction T; simpl; intros k Fr; notin_simpl; try apply notin_union; eauto.
+Qed.
+
+Lemma notin_fv_wf : forall E (X : atom) T,
+  wf_typ E T ->
+  X `notin` dom E ->
+  X `notin` fv_tt T.
+Proof with auto.
+  intros E X T Wf_typ.
+  induction Wf_typ; intros Fr; simpl...
+  Case "wf_typ_var".
+    assert (X0 `in` (dom E))...
+    eapply binds_In; eauto.
+  Case "wf_typ_all".
+    apply notin_union...
+    pick fresh Y.
+    apply (notin_fv_tt_open Y)...
+Qed.
+
+Lemma map_subst_tb_id : forall G Z P,
+  wf_env G ->
+  Z `notin` dom G ->
+  G = map (subst_tb Z P) G.
+Proof with auto.
+  intros G Z P H.
+  induction H; simpl; intros Fr; simpl_env...
+  rewrite <- IHwf_env...
+    rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto.
+  rewrite <- IHwf_env...
+    rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="regularity"></a># Regularity of relations *)
+
+Lemma sub_regular : forall E S T,
+  sub E S T ->
+  wf_env E /\ wf_typ E S /\ wf_typ E T.
+Proof with simpl_env; auto*.
+  intros E S T H.
+  induction H...
+  Case "sub_trans_tvar".
+    eauto*.
+  Case "sub_all".
+    repeat split...
+    SCase "Second of original three conjuncts".
+      pick fresh Y and apply wf_typ_all...
+      destruct (H1 Y)...
+      rewrite_env (empty ++ [(Y, bind_sub S1)] ++ E).
+      apply (wf_typ_narrowing T1)...
+    SCase "Third of original three conjuncts".
+      pick fresh Y and apply wf_typ_all...
+      destruct (H1 Y)...
+Qed.
+
+Lemma typing_regular : forall E e T,
+  typing E e T ->
+  wf_env E /\ expr e /\ wf_typ E T.
+Proof with simpl_env; auto*.
+  intros E e T H; induction H...
+  Case "typing_var".
+    repeat split...
+    eauto using wf_typ_from_binds_typ.
+  Case "typing_abs".
+    pick fresh y.
+    destruct (H0 y) as [Hok [J K]]...
+    repeat split. inversion Hok...
+    SCase "Second of original three conjuncts".
+      pick fresh x and apply expr_abs.
+        eauto using type_from_wf_typ, wf_typ_from_wf_env_typ.
+        destruct (H0 x)...
+    SCase "Third of original three conjuncts".
+      apply wf_typ_arrow; eauto using wf_typ_from_wf_env_typ.
+      rewrite_env (empty ++ E).
+      eapply wf_typ_strengthening; simpl_env; eauto.
+  Case "typing_app".
+    repeat split...
+    destruct IHtyping1 as [_ [_ K]].
+    inversion K...
+  Case "typing_tabs".
+    pick fresh Y.
+    destruct (H0 Y) as [Hok [J K]]...
+    inversion Hok; subst.
+    repeat split...
+    SCase "Second of original three conjuncts".
+      pick fresh X and apply expr_tabs.
+        eauto using type_from_wf_typ, wf_typ_from_wf_env_sub...
+        destruct (H0 X)...
+    SCase "Third of original three conjuncts".
+      pick fresh Z and apply wf_typ_all...
+      destruct (H0 Z)...
+  Case "typing_tapp".
+    destruct (sub_regular _ _ _ H0) as [R1 [R2 R3]].
+    repeat split...
+    SCase "Second of original three conjuncts".
+      apply expr_tapp...
+      eauto using type_from_wf_typ.
+    SCase "Third of original three conjuncts".
+      destruct IHtyping as [R1' [R2' R3']].
+      eapply wf_typ_open; eauto.
+  Case "typing_sub".
+    repeat split...
+    destruct (sub_regular _ _ _ H0)...
+Qed.
+
+Lemma value_regular : forall e,
+  value e ->
+  expr e.
+Proof.
+  intros e H. induction H; auto.
+Qed.
+
+Lemma red_regular : forall e e',
+  red e e' ->
+  expr e /\ expr e'.
+Proof with auto*.
+  intros e e' H.
+  induction H; assert(J := value_regular); split...
+  Case "red_abs".
+    inversion H. pick fresh y. rewrite (subst_ee_intro y)...
+  Case "red_tabs".
+    inversion H. pick fresh Y. rewrite (subst_te_intro Y)...
+Qed.
+
+
+(* *********************************************************************** *)
+(** * #<a name="auto"></a># Automation *)
+
+(** The lemma [ok_from_wf_env] was already added above as a hint since it
+    helps blur the distinction between [wf_env] and [ok] in proofs.
+
+    As currently stated, the regularity lemmas are ill-suited to be
+    used with [auto] and [eauto] since they end in conjunctions.  Even
+    if we were, for example, to split [sub_regularity] into three
+    separate lemmas, the resulting lemmas would be usable only by
+    [eauto] and there is no guarantee that [eauto] would be able to
+    find proofs effectively.  Thus, the hints below apply the
+    regularity lemmas and [type_from_wf_typ] to discharge goals about
+    local closure and well-formedness, but in such a way as to
+    minimize proof search.
+
+    The first hint introduces an [wf_env] fact into the context.  It
+    works well when combined with the lemmas relating [wf_env] and
+    [wf_typ].  We choose to use those lemmas explicitly via [(auto
+    using ...)] tactics rather than add them as hints.  When used this
+    way, the explicitness makes the proof more informative rather than
+    more cluttered (with useless details).
+
+    The other three hints try outright to solve their respective
+    goals. *)
+
+Hint Extern 1 (wf_env ?E) =>
+  match goal with
+  | H: sub _ _ _ |- _ => apply (proj1 (sub_regular _ _ _ H))
+  | H: typing _ _ _ |- _ => apply (proj1 (typing_regular _ _ _ H))
+  end.
+
+Hint Extern 1 (wf_typ ?E ?T) =>
+  match goal with
+  | H: typing E _ T |- _ => apply (proj2 (proj2 (typing_regular _ _ _ H)))
+  | H: sub E T _ |- _ => apply (proj1 (proj2 (sub_regular _ _ _ H)))
+  | H: sub E _ T |- _ => apply (proj2 (proj2 (sub_regular _ _ _ H)))
+  end.
+
+Hint Extern 1 (type ?T) =>
+  let go E := apply (type_from_wf_typ E); auto in
+  match goal with
+  | H: typing ?E _ T |- _ => go E
+  | H: sub ?E T _ |- _ => go E
+  | H: sub ?E _ T |- _ => go E
+  end.
+
+Hint Extern 1 (expr ?e) =>
+  match goal with
+  | H: typing _ ?e _ |- _ => apply (proj1 (proj2 (typing_regular _ _ _ H)))
+  | H: red ?e _ |- _ => apply (proj1 (red_regular _ _ H))
+  | H: red _ ?e |- _ => apply (proj2 (red_regular _ _ H))
+  end.

coq-Fsub/Fsub_Soundness.v

@@ -0,0 +1,593 @@
+(** Type-safety proofs for Fsub.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis.
+
+    In parentheses are given the label of the corresponding lemma in
+    the appendix (informal proofs) of the POPLmark Challenge.
+
+    Table of contents:
+      - #<a href="##subtyping">Properties of subtyping</a>#
+      - #<a href="##typing">Properties of typing</a>#
+      - #<a href="##preservation">Preservation</a>#
+      - #<a href="##progress">Progress</a># *)
+
+Require Export Fsub_Lemmas.
+
+
+(* ********************************************************************** *)
+(** * #<a name="subtyping"></a># Properties of subtyping *)
+
+
+(* ********************************************************************** *)
+(** ** Reflexivity (1) *)
+
+Lemma sub_reflexivity : forall E T,
+  wf_env E ->
+  wf_typ E T ->
+  sub E T T.
+Proof with eauto.
+  intros E T Ok Wf.
+  induction Wf...
+  pick fresh Y and apply sub_all...
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Weakening (2) *)
+
+Lemma sub_weakening : forall E F G S T,
+  sub (G ++ E) S T ->
+  wf_env (G ++ F ++ E) ->
+  sub (G ++ F ++ E) S T.
+Proof with simpl_env; auto using wf_typ_weakening.
+  intros E F G S T Sub Ok.
+  remember (G ++ E) as H.
+  generalize dependent G.
+  induction Sub; intros G Ok EQ; subst...
+  Case "sub_trans_tvar".
+    apply (sub_trans_tvar U)...
+  Case "sub_all".
+    pick fresh Y and apply sub_all...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Narrowing and transitivity (3) *)
+
+Definition transitivity_on Q := forall E S T,
+  sub E S Q -> sub E Q T -> sub E S T.
+
+Lemma sub_narrowing_aux : forall Q F E Z P S T,
+  transitivity_on Q ->
+  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
+  sub E P Q ->
+  sub (F ++ [(Z, bind_sub P)] ++ E) S T.
+Proof with simpl_env; eauto using wf_typ_narrowing, wf_env_narrowing.
+  intros Q F E Z P S T TransQ SsubT PsubQ.
+  remember (F ++ [(Z, bind_sub Q)] ++ E) as G. generalize dependent F.
+  induction SsubT; intros F EQ; subst...
+  Case "sub_top".
+    apply sub_top...
+  Case "sub_refl_tvar".
+    apply sub_refl_tvar...
+  Case "sub_trans_tvar".
+    destruct (X == Z); subst.
+    SCase "X = Z".
+      apply (sub_trans_tvar P); [ eauto using fresh_mid_head | ].
+      apply TransQ.
+      SSCase "P <: Q".
+        rewrite_env (empty ++ (F ++ [(Z, bind_sub P)]) ++ E).
+        apply sub_weakening...
+      SSCase "Q <: T".
+        binds_get H.
+        inversion H1; subst...
+    SCase "X <> Z".
+      apply (sub_trans_tvar U)...
+      binds_cases H...
+  Case "sub_all".
+    pick fresh Y and apply sub_all...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+Lemma sub_transitivity : forall Q,
+  transitivity_on Q.
+Proof with simpl_env; auto.
+  unfold transitivity_on.
+  intros Q E S T SsubQ QsubT.
+  assert (W : type Q) by auto.
+  generalize dependent T.
+  generalize dependent S.
+  generalize dependent E.
+  remember Q as Q' in |-.
+  generalize dependent Q'.
+  induction W;
+    intros Q' EQ E S SsubQ;
+    induction SsubQ; try discriminate; inversion EQ; subst;
+    intros T' QsubT;
+    inversion QsubT; subst; eauto 4 using sub_trans_tvar.
+  Case "sub_all / sub_top".
+    assert (sub E (typ_all S1 S2) (typ_all T1 T2)).
+      SCase "proof of assertion".
+      pick fresh y and apply sub_all...
+    auto.
+  Case "sub_all / sub_all".
+    pick fresh Y and apply sub_all.
+    SCase "bounds".
+      eauto.
+    SCase "bodies".
+      lapply (H0 Y); [ intros K | auto ].
+      apply (K (open_tt T2 Y))...
+      rewrite_env (empty ++ [(Y, bind_sub T0)] ++ E).
+      apply (sub_narrowing_aux T1)...
+      unfold transitivity_on.
+      auto using (IHW T1).
+Qed.
+
+Lemma sub_narrowing : forall Q E F Z P S T,
+  sub E P Q ->
+  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
+  sub (F ++ [(Z, bind_sub P)] ++ E) S T.
+Proof.
+  intros.
+  eapply sub_narrowing_aux; eauto.
+  apply sub_transitivity.
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Type substitution preserves subtyping (10) *)
+
+Lemma sub_through_subst_tt : forall Q E F Z S T P,
+  sub (F ++ [(Z, bind_sub Q)] ++ E) S T ->
+  sub E P Q ->
+  sub (map (subst_tb Z P) F ++ E) (subst_tt Z P S) (subst_tt Z P T).
+Proof with
+      simpl_env;
+      eauto 4 using wf_typ_subst_tb, wf_env_subst_tb, wf_typ_weaken_head.
+  intros Q E F Z S T P SsubT PsubQ.
+  remember (F ++ [(Z, bind_sub Q)] ++ E) as G.
+  generalize dependent F.
+  induction SsubT; intros G EQ; subst; simpl subst_tt...
+  Case "sub_top".
+    apply sub_top...
+  Case "sub_refl_tvar".
+    destruct (X == Z); subst.
+    SCase "X = Z".
+      apply sub_reflexivity...
+    SCase "X <> Z".
+      apply sub_reflexivity...
+      inversion H0; subst.
+      binds_cases H3...
+      apply (wf_typ_var (subst_tt Z P U))...
+  Case "sub_trans_tvar".
+    destruct (X == Z); subst.
+    SCase "X = Z".
+      apply (sub_transitivity Q).
+      SSCase "left branch".
+        rewrite_env (empty ++ map (subst_tb Z P) G ++ E).
+        apply sub_weakening...
+      SSCase "right branch".
+        rewrite (subst_tt_fresh Z P Q).
+          binds_get H.
+            inversion H1; subst...
+          apply (notin_fv_wf E); eauto using fresh_mid_tail.
+    SCase "X <> Z".
+      apply (sub_trans_tvar (subst_tt Z P U))...
+      rewrite (map_subst_tb_id E Z P);
+        [ | auto | eapply fresh_mid_tail; eauto ].
+      binds_cases H...
+  Case "sub_all".
+    pick fresh X and apply sub_all...
+    rewrite subst_tt_open_tt_var...
+    rewrite subst_tt_open_tt_var...
+    rewrite_env (map (subst_tb Z P) ([(X, bind_sub T1)] ++ G) ++ E).
+    apply H0...
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="typing"></a># Properties of typing *)
+
+
+(* ********************************************************************** *)
+(** ** Weakening (5) *)
+
+Lemma typing_weakening : forall E F G e T,
+  typing (G ++ E) e T ->
+  wf_env (G ++ F ++ E) ->
+  typing (G ++ F ++ E) e T.
+Proof with simpl_env;
+           eauto using wf_typ_weakening,
+                       wf_typ_from_wf_env_typ,
+                       wf_typ_from_wf_env_sub,
+                       sub_weakening.
+  intros E F G e T Typ.
+  remember (G ++ E) as H.
+  generalize dependent G.
+  induction Typ; intros G EQ Ok; subst...
+  Case "typing_abs".
+    pick fresh x and apply typing_abs.
+    lapply (H x); [intros K | auto].
+    rewrite <- concat_assoc.
+    apply (H0 x)...
+  Case "typing_tabs".
+    pick fresh X and apply typing_tabs.
+    lapply (H X); [intros K | auto].
+    rewrite <- concat_assoc.
+    apply (H0 X)...
+Qed.
+
+
+(* ********************************************************************** *)
+(** ** Strengthening (6) *)
+
+Lemma sub_strengthening : forall x U E F S T,
+  sub (F ++ [(x, bind_typ U)] ++ E) S T ->
+  sub (F ++ E) S T.
+Proof with eauto using wf_typ_strengthening, wf_env_strengthening.
+  intros x U E F S T SsubT.
+  remember (F ++ [(x, bind_typ U)] ++ E) as E'.
+  generalize dependent F.
+  induction SsubT; intros F EQ; subst...
+  Case "sub_trans_tvar".
+    apply (sub_trans_tvar U0)...
+    binds_cases H...
+  Case "sub_all".
+    pick fresh X and apply sub_all...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+
+(************************************************************************ *)
+(** ** Narrowing for typing (7) *)
+
+Lemma typing_narrowing : forall Q E F X P e T,
+  sub E P Q ->
+  typing (F ++ [(X, bind_sub Q)] ++ E) e T ->
+  typing (F ++ [(X, bind_sub P)] ++ E) e T.
+Proof with eauto 6 using wf_env_narrowing, wf_typ_narrowing, sub_narrowing.
+  intros Q E F X P e T PsubQ Typ.
+  remember (F ++ [(X, bind_sub Q)] ++ E) as E'.
+  generalize dependent F.
+  induction Typ; intros F EQ; subst...
+  Case "typing_var".
+    binds_cases H0...
+  Case "typing_abs".
+    pick fresh y and apply typing_abs.
+    rewrite <- concat_assoc.
+    apply H0...
+  Case "typing_tabs".
+    pick fresh Y and apply typing_tabs.
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+
+
+(************************************************************************ *)
+(** ** Substitution preserves typing (8) *)
+
+Lemma typing_through_subst_ee : forall U E F x T e u,
+  typing (F ++ [(x, bind_typ U)] ++ E) e T ->
+  typing E u U ->
+  typing (F ++ E) (subst_ee x u e) T.
+(* begin show *)
+
+(** We provide detailed comments for the following proof, mainly to
+    point out several useful tactics and proof techniques.
+
+    Starting a proof with "Proof with <some tactic>" allows us to
+    specify a default tactic that should be used to solve goals.  To
+    invoke this default tactic at the end of a proof step, we signal
+    the end of the step with three periods instead of a single one,
+    e.g., "apply typing_weakening...". *)
+
+Proof with simpl_env;
+           eauto 4 using wf_typ_strengthening,
+                         wf_env_strengthening,
+                         sub_strengthening.
+
+  (** The proof proceeds by induction on the given typing derivation
+      for e.  We use the remember tactic, along with generalize
+      dependent, to ensure that the goal is properly strengthened
+      before we use induction. *)
+
+  intros U E F x T e u TypT TypU.
+  remember (F ++ [(x, bind_typ U)] ++ E) as E'.
+  generalize dependent F.
+  induction TypT; intros F EQ; subst; simpl subst_ee...
+
+  (** The typing_var case involves a case analysis on whether the
+      variable is the same as the one being substituted for. *)
+
+  Case "typing_var".
+    destruct (x0 == x); subst.
+
+    (** In the case where x0=x, we first observe that hypothesis H0
+        implies that T=U, since x can only be bound once in the
+        environment.  The conclusion then follows from hypothesis TypU
+        and weakening.  We can use the binds_get tactic, described in
+        the Environment library, with H0 to obtain the fact that
+        T=U. *)
+
+    SCase "x0 = x".
+      binds_get H0.
+        inversion H2; subst.
+
+        (** In order to apply typing_weakening, we need to rewrite the
+            environment so that it has the right shape.  (We could
+            also prove a corollary of typing_weakening.)  The
+            rewrite_env tactic, described in the Environment library,
+            is one way to perform this rewriting. *)
+
+        rewrite_env (empty ++ F ++ E).
+        apply typing_weakening...
+
+    (** In the case where x0<>x, the result follows by an exhaustive
+        case analysis on exactly where x0 is bound in the environment.
+        We perform this case analysis by using the binds_cases tactic,
+        described in the Environment library. *)
+
+    SCase "x0 <> x".
+      binds_cases H0.
+        eauto using wf_env_strengthening.
+        eauto using wf_env_strengthening.
+
+  (** Informally, the typing_abs case is a straightforward application
+      of the induction hypothesis, which is called H0 here. *)
+
+  Case "typing_abs".
+
+    (** We use the "pick fresh and apply" tactic to apply the rule
+        typing_abs without having to calculate the appropriate finite
+        set of atoms. *)
+
+    pick fresh y and apply typing_abs.
+
+    (** We cannot apply H0 directly here.  The first problem is that
+        the induction hypothesis has (subst_ee open_ee), whereas in
+        the goal we have (open_ee subst_ee).  The lemma
+        subst_ee_open_ee_var lets us swap the order of these two
+        operations. *)
+
+    rewrite subst_ee_open_ee_var...
+
+    (** The second problem is how the concatenations are associated in
+        the environments.  In the goal, we currently have
+
+<<       ([(y, bind_typ V)] ++ F ++ E),
+>>
+        where concatenation associates to the right.  In order to
+        apply the induction hypothesis, we need
+
+<<        (([(y, bind_typ V)] ++ F) ++ E).
+>>
+        We can use the rewrite_env tactic to perform this rewriting,
+        or we can rewrite directly with an appropriate lemma from the
+        Environment library. *)
+
+    rewrite <- concat_assoc.
+
+    (** Now we can apply the induction hypothesis. *)
+
+    apply H0...
+
+  (** The remaining cases in this proof are straightforward, given
+      everything that we have pointed out above. *)
+
+  Case "typing_tabs".
+    pick fresh Y and apply typing_tabs.
+    rewrite subst_ee_open_te_var...
+    rewrite <- concat_assoc.
+    apply H0...
+Qed.
+(* end show *)
+
+
+(************************************************************************ *)
+(** ** Type substitution preserves typing (11) *)
+
+Lemma typing_through_subst_te : forall Q E F Z e T P,
+  typing (F ++ [(Z, bind_sub Q)] ++ E) e T ->
+  sub E P Q ->
+  typing (map (subst_tb Z P) F ++ E) (subst_te Z P e) (subst_tt Z P T).
+Proof with simpl_env;
+           eauto 6 using wf_env_subst_tb,
+                         wf_typ_subst_tb,
+                         sub_through_subst_tt.
+  intros Q E F Z e T P Typ PsubQ.
+  remember (F ++ [(Z, bind_sub Q)] ++ E) as G.
+  generalize dependent F.
+  induction Typ; intros F EQ; subst;
+    simpl subst_te in *; simpl subst_tt in *...
+  Case "typing_var".
+    apply typing_var...
+      rewrite (map_subst_tb_id E Z P);
+        [ | auto | eapply fresh_mid_tail; eauto ].
+      binds_cases H0...
+  Case "typing_abs".
+    pick fresh y and apply typing_abs.
+    rewrite subst_te_open_ee_var...
+    rewrite_env (map (subst_tb Z P) ([(y, bind_typ V)] ++ F) ++ E).
+    apply H0...
+  Case "typing_tabs".
+    pick fresh Y and apply typing_tabs.
+    rewrite subst_te_open_te_var...
+    rewrite subst_tt_open_tt_var...
+    rewrite_env (map (subst_tb Z P) ([(Y, bind_sub V)] ++ F) ++ E).
+    apply H0...
+  Case "typing_tapp".
+    rewrite subst_tt_open_tt...
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="preservation"></a># Preservation *)
+
+
+(* ********************************************************************** *)
+(** ** Inversion of typing (13) *)
+
+Lemma typing_inv_abs : forall E S1 e1 T,
+  typing E (exp_abs S1 e1) T ->
+  forall U1 U2, sub E T (typ_arrow U1 U2) ->
+     sub E U1 S1
+  /\ exists S2, exists L, forall x, x `notin` L ->
+     typing ([(x, bind_typ S1)] ++ E) (open_ee e1 x) S2 /\ sub E S2 U2.
+Proof with auto.
+  intros E S1 e1 T Typ.
+  remember (exp_abs S1 e1) as e.
+  generalize dependent e1.
+  generalize dependent S1.
+  induction Typ; intros S1 b1 EQ U1 U2 Sub; inversion EQ; subst.
+  Case "typing_abs".
+    inversion Sub; subst.
+    split...
+    exists T1. exists L...
+  Case "typing_sub".
+    auto using (sub_transitivity T).
+Qed.
+
+Lemma typing_inv_tabs : forall E S1 e1 T,
+  typing E (exp_tabs S1 e1) T ->
+  forall U1 U2, sub E T (typ_all U1 U2) ->
+     sub E U1 S1
+  /\ exists S2, exists L, forall X, X `notin` L ->
+     typing ([(X, bind_sub U1)] ++ E) (open_te e1 X) (open_tt S2 X)
+     /\ sub ([(X, bind_sub U1)] ++ E) (open_tt S2 X) (open_tt U2 X).
+Proof with simpl_env; auto.
+  intros E S1 e1 T Typ.
+  remember (exp_tabs S1 e1) as e.
+  generalize dependent e1.
+  generalize dependent S1.
+  induction Typ; intros S1 e0 EQ U1 U2 Sub; inversion EQ; subst.
+  Case "typing_tabs".
+    inversion Sub; subst.
+    split...
+    exists T1.
+    exists (L0 `union` L).
+    intros Y Fr.
+    split...
+    rewrite_env (empty ++ [(Y, bind_sub U1)] ++ E).
+    apply (typing_narrowing S1)...
+  Case "typing_sub".
+    auto using (sub_transitivity T).
+Qed.
+
+
+
+(* ********************************************************************** *)
+(** ** Preservation (20) *)
+
+Lemma preservation : forall E e e' T,
+  typing E e T ->
+  red e e' ->
+  typing E e' T.
+Proof with simpl_env; eauto.
+  intros E e e' T Typ. generalize dependent e'.
+  induction Typ; intros e' Red; try solve [ inversion Red; subst; eauto ].
+  Case "typing_app".
+    inversion Red; subst...
+    SCase "red_abs".
+      destruct (typing_inv_abs _ _ _ _ Typ1 T1 T2) as [P1 [S2 [L P2]]].
+        apply sub_reflexivity...
+      pick fresh x.
+      destruct (P2 x) as [? ?]...
+      rewrite (subst_ee_intro x)...
+      rewrite_env (empty ++ E).
+      apply (typing_through_subst_ee T).
+        apply (typing_sub S2)...
+          rewrite_env (empty ++ [(x, bind_typ T)] ++ E).
+          apply sub_weakening...
+        eauto.
+  Case "typing_tapp".
+    inversion Red; subst...
+    SCase "red_tabs".
+      destruct (typing_inv_tabs _ _ _ _ Typ T1 T2) as [P1 [S2 [L P2]]].
+        apply sub_reflexivity...
+      pick fresh X.
+      destruct (P2 X) as [? ?]...
+      rewrite (subst_te_intro X)...
+      rewrite (subst_tt_intro X)...
+      rewrite_env (map (subst_tb X T) empty ++ E).
+      apply (typing_through_subst_te T1)...
+Qed.
+
+
+(* ********************************************************************** *)
+(** * #<a name="progress"></a># Progress *)
+
+
+(* ********************************************************************** *)
+(** ** Canonical forms (14) *)
+
+Lemma canonical_form_abs : forall e U1 U2,
+  value e ->
+  typing empty e (typ_arrow U1 U2) ->
+  exists V, exists e1, e = exp_abs V e1.
+Proof.
+  intros e U1 U2 Val Typ.
+  remember empty as E.
+  remember (typ_arrow U1 U2) as T.
+  revert U1 U2 HeqT HeqE.
+  induction Typ; intros U1 U2 EQT EQE; subst;
+    try solve [ inversion Val | inversion EQT | eauto ].
+  Case "typing_sub".
+    inversion H; subst; eauto.
+    inversion H0.
+Qed.
+
+Lemma canonical_form_tabs : forall e U1 U2,
+  value e ->
+  typing empty e (typ_all U1 U2) ->
+  exists V, exists e1, e = exp_tabs V e1.
+Proof.
+  intros e U1 U2 Val Typ.
+  remember empty as E.
+  remember (typ_all U1 U2) as T.
+  revert U1 U2 HeqT HeqT.
+  induction Typ; intros U1 U2 EQT EQE; subst;
+    try solve [ inversion Val | inversion EQT | eauto ].
+  Case "typing_sub".
+    inversion H; subst; eauto.
+    inversion H0.
+Qed.
+
+
+
+(* ********************************************************************** *)
+(** ** Progress (16) *)
+
+Lemma progress : forall e T,
+  typing empty e T ->
+  value e \/ exists e', red e e'.
+Proof with eauto.
+  intros e T Typ.
+  remember empty as E. generalize dependent HeqE.
+  assert (Typ' : typing E e T)...
+  induction Typ; intros EQ; subst...
+  Case "typing_var".
+    inversion H0.
+  Case "typing_app".
+    right.
+    destruct IHTyp1 as [Val1 | [e1' Rede1']]...
+    SCase "Val1".
+      destruct IHTyp2 as [Val2 | [e2' Rede2']]...
+      SSCase "Val2".
+        destruct (canonical_form_abs _ _ _ Val1 Typ1) as [S [e3 EQ]].
+        subst.
+        exists (open_ee e3 e2)...
+  Case "typing_tapp".
+    right.
+    destruct IHTyp as [Val1 | [e1' Rede1']]...
+    SCase "Val1".
+      destruct (canonical_form_tabs _ _ _ Val1 Typ) as [S [e3 EQ]].
+      subst.
+      exists (open_te e3 T)...
+    SCase "e1' Rede1'".
+      exists (exp_tapp e1' T)...
+Qed.

coq-Fsub/ListFacts.v

@@ -0,0 +1,283 @@
+(** Assorted facts about lists.
+
+    Author: Brian Aydemir.
+
+    Implicit arguments are declared by default in this library. *)
+
+Set Implicit Arguments.
+
+Require Import Eqdep_dec.
+Require Import List.
+Require Import SetoidList.
+Require Import Sorting.
+Require Import Relations.
+
+
+(* ********************************************************************** *)
+(** * List membership *)
+
+Lemma not_in_cons :
+  forall (A : Type) (ys : list A) x y,
+  x <> y -> ~ In x ys -> ~ In x (y :: ys).
+Proof.
+  induction ys; simpl; intuition.
+Qed.
+
+Lemma not_In_app :
+  forall (A : Type) (xs ys : list A) x,
+  ~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys).
+Proof.
+  intros A xs ys x H J K.
+  destruct (in_app_or _ _ _ K); auto.
+Qed.
+
+Lemma elim_not_In_cons :
+  forall (A : Type) (y : A) (ys : list A) (x : A),
+  ~ In x (y :: ys) -> x <> y /\ ~ In x ys.
+Proof.
+  intros. simpl in *. auto.
+Qed.
+
+Lemma elim_not_In_app :
+  forall (A : Type) (xs ys : list A) (x : A),
+  ~ In x (xs ++ ys) -> ~ In x xs /\ ~ In x ys.
+Proof.
+  split; auto using in_or_app.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * List inclusion *)
+
+Lemma incl_nil :
+  forall (A : Type) (xs : list A), incl nil xs.
+Proof.
+  unfold incl.
+  intros A xs a H; inversion H.
+Qed.
+
+Lemma incl_trans :
+  forall (A : Type) (xs ys zs : list A),
+  incl xs ys -> incl ys zs -> incl xs zs.
+Proof.
+  unfold incl; firstorder.
+Qed.
+
+Lemma In_incl :
+  forall (A : Type) (x : A) (ys zs : list A),
+  In x ys -> incl ys zs -> In x zs.
+Proof.
+  unfold incl; auto.
+Qed.
+
+Lemma elim_incl_cons :
+  forall (A : Type) (x : A) (xs zs : list A),
+  incl (x :: xs) zs -> In x zs /\ incl xs zs.
+Proof.
+  unfold incl. auto with datatypes.
+Qed.
+
+Lemma elim_incl_app :
+  forall (A : Type) (xs ys zs : list A),
+  incl (xs ++ ys) zs -> incl xs zs /\ incl ys zs.
+Proof.
+  unfold incl. auto with datatypes.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * Setoid facts *)
+
+Lemma InA_iff_In :
+  forall (A : Set) x xs, InA (@eq A) x xs <-> In x xs.
+Proof.
+  split. 2:auto using In_InA.
+  induction xs as [ | y ys IH ].
+    intros H. inversion H.
+    intros H. inversion H; subst; auto with datatypes.
+Qed.
+
+
+(* ********************************************************************* *)
+(** * Equality proofs for lists *)
+
+Section EqRectList.
+
+Variable A : Type.
+Variable eq_A_dec : forall (x y : A), {x = y} + {x <> y}.
+
+Lemma eq_rect_eq_list :
+  forall (p : list A) (Q : list A -> Type) (x : Q p) (h : p = p),
+  eq_rect p Q x p h = x.
+Proof with auto.
+  intros.
+  apply K_dec with (p := h)...
+  decide equality. destruct (eq_A_dec a a0)...
+Qed.
+
+End EqRectList.
+
+
+(* ********************************************************************** *)
+(** * Decidable sorting and uniqueness of proofs *)
+
+Section DecidableSorting.
+
+Variable A : Set.
+Variable leA : relation A.
+Hypothesis leA_dec : forall x y, {leA x y} + {~ leA x y}.
+
+Theorem lelistA_dec :
+  forall a xs, {lelistA leA a xs} + {~ lelistA leA a xs}.
+Proof.
+  induction xs as [ | x xs IH ]; auto with datatypes.
+  destruct (leA_dec a x); auto with datatypes.
+  right. intros J. inversion J. auto.
+Qed.
+
+Theorem sort_dec :
+  forall xs, {sort leA xs} + {~ sort leA xs}.
+Proof.
+  induction xs as [ | x xs IH ]; auto with datatypes.
+  destruct IH; destruct (lelistA_dec x xs); auto with datatypes.
+  right. intros K. inversion K. auto.
+  right. intros K. inversion K. auto.
+  right. intros K. inversion K. auto.
+Qed.
+
+Section UniqueSortingProofs.
+
+  Hypothesis eq_A_dec : forall (x y : A), {x = y} + {x <> y}.
+  Hypothesis leA_unique : forall (x y : A) (p q : leA x y), p = q.
+
+  Scheme lelistA_ind' := Induction for lelistA Sort Prop.
+  Scheme sort_ind' := Induction for sort Sort Prop.
+
+  Theorem lelistA_unique :
+    forall (x : A) (xs : list A) (p q : lelistA leA x xs), p = q.
+  Proof with auto.
+    induction p using lelistA_ind'; intros q.
+    (* case: nil_leA *)
+    replace (nil_leA leA x) with (eq_rect _ (fun xs => lelistA leA x xs)
+      (nil_leA leA x) _ (refl_equal (@nil A)))...
+    generalize (refl_equal (@nil A)).
+    pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ].
+    intros. rewrite eq_rect_eq_list...
+    (* case: cons_sort *)
+    replace (cons_leA leA x b l l0) with (eq_rect _ (fun xs => lelistA leA x xs)
+      (cons_leA leA x b l l0) _ (refl_equal (b :: l)))...
+    generalize (refl_equal (b :: l)).
+    pattern (b :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ].
+    intros. inversion e; subst.
+    rewrite eq_rect_eq_list...
+    rewrite (leA_unique l0 l2)...
+  Qed.
+
+  Theorem sort_unique :
+    forall (xs : list A) (p q : sort leA xs), p = q.
+  Proof with auto.
+    induction p using sort_ind'; intros q.
+    (* case: nil_sort *)
+    replace (nil_sort leA) with (eq_rect _ (fun xs => sort leA xs)
+      (nil_sort leA) _ (refl_equal (@nil A)))...
+    generalize (refl_equal (@nil A)).
+    pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ].
+    intros. rewrite eq_rect_eq_list...
+    (* case: cons_sort *)
+    replace (cons_sort p l0) with (eq_rect _ (fun xs => sort leA xs)
+      (cons_sort p l0) _ (refl_equal (a :: l)))...
+    generalize (refl_equal (a :: l)).
+    pattern (a :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ].
+    intros. inversion e; subst.
+    rewrite eq_rect_eq_list...
+    rewrite (lelistA_unique l0 l2).
+    rewrite (IHp s)...
+  Qed.
+
+End UniqueSortingProofs.
+End DecidableSorting.
+
+
+(* ********************************************************************** *)
+(** * Equality on sorted lists *)
+
+Section Equality_ext.
+
+Variable A : Set.
+Variable ltA : relation A.
+Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
+Hypothesis ltA_not_eqA : forall x y, ltA x y -> x <> y.
+Hypothesis ltA_eqA : forall x y z, ltA x y -> y = z -> ltA x z.
+Hypothesis eqA_ltA : forall x y z, x = y -> ltA y z -> ltA x z.
+
+Hint Resolve ltA_trans.
+Hint Immediate ltA_eqA eqA_ltA.
+
+Notation Inf := (lelistA ltA).
+Notation Sort := (sort ltA).
+
+Lemma not_InA_if_Sort_Inf :
+  forall xs a, Sort xs -> Inf a xs -> ~ InA (@eq A) a xs.
+Proof.
+  induction xs as [ | x xs IH ]; intros a Hsort Hinf H.
+  inversion H.
+  inversion H; subst.
+    inversion Hinf; subst.
+      assert (x <> x) by auto; intuition.
+    inversion Hsort; inversion Hinf; subst.
+      assert (Inf a xs) by eauto using InfA_ltA.
+      assert (~ InA (@eq A) a xs) by auto.
+      intuition.
+Qed.
+
+Lemma Sort_eq_head :
+  forall x xs y ys,
+  Sort (x :: xs) ->
+  Sort (y :: ys) ->
+  (forall a, InA (@eq A) a (x :: xs) <-> InA (@eq A) a (y :: ys)) ->
+  x = y.
+Proof.
+  intros x xs y ys SortXS SortYS H.
+  inversion SortXS; inversion SortYS; subst.
+  assert (Q3 : InA (@eq A) x (y :: ys)) by firstorder.
+  assert (Q4 : InA (@eq A) y (x :: xs)) by firstorder.
+  inversion Q3; subst; auto.
+  inversion Q4; subst; auto.
+  assert (ltA y x) by (refine (SortA_InfA_InA _ _ _ _ _ H6 H7 H1); auto).
+  assert (ltA x y) by (refine (SortA_InfA_InA _ _ _ _ _ H2 H3 H4); auto).
+  assert (y <> y) by eauto.
+  intuition.
+Qed.
+
+Lemma Sort_InA_eq_ext :
+  forall xs ys,
+  Sort xs ->
+  Sort ys ->
+  (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys) ->
+  xs = ys.
+Proof.
+  induction xs as [ | x xs IHxs ]; induction ys as [ | y ys IHys ];
+      intros SortXS SortYS H; auto.
+  (* xs -> nil, ys -> y :: ys *)
+  assert (Q : InA (@eq A) y nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> nil *)
+  assert (Q : InA (@eq A) x nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> y :: ys *)
+  inversion SortXS; inversion SortYS; subst.
+  assert (x = y) by eauto using Sort_eq_head.
+  cut (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys).
+  intros. assert (xs = ys) by auto. subst. auto.
+  intros a; split; intros L.
+    assert (Q2 : InA (@eq A) a (y :: ys)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y xs) by auto using not_InA_if_Sort_Inf.
+      intuition.
+    assert (Q2 : InA (@eq A) a (x :: xs)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y ys) by auto using not_InA_if_Sort_Inf.
+      intuition.
+Qed.
+
+End Equality_ext.

coq-Fsub/Metatheory.v

@@ -0,0 +1,95 @@
+(** Library for programming languages metatheory.
+
+    Authors: Brian Aydemir and Arthur Charguéraud, with help from
+    Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios
+    Vytiniotis, Stephanie Weirich, and Steve Zdancewic. *)
+
+Require Export AdditionalTactics.
+Require Export Atom.
+Require Export Environment.
+
+
+(* ********************************************************************** *)
+(** * Notations *)
+
+(** Decidable equality on atoms and natural numbers may be written
+    using natural notation. *)
+
+Notation "x == y" :=
+  (eq_atom_dec x y) (at level 67) : metatheory_scope.
+Notation "i === j" :=
+  (Peano_dec.eq_nat_dec i j) (at level 67) : metatheory_scope.
+
+(** Common set operations may be written using infix notation. *)
+
+Notation "E `union` F" :=
+  (AtomSet.F.union E F)
+  (at level 69, right associativity, format "E  `union`  '/' F")
+  : set_scope.
+Notation "x `in` E" :=
+  (AtomSet.F.In x E) (at level 69) : set_scope.
+Notation "x `notin` E" :=
+  (~ AtomSet.F.In x E) (at level 69) : set_scope.
+
+(** The empty set may be written similarly to informal practice. *)
+
+Notation "{}" :=
+  (AtomSet.F.empty) : metatheory_scope.
+
+(** It is useful to have an abbreviation for constructing singleton
+    sets. *)
+
+Notation singleton := (AtomSet.F.singleton).
+
+(** Open the notation scopes declared above. *)
+
+Open Scope metatheory_scope.
+Open Scope set_scope.
+
+
+(* ********************************************************************** *)
+(** * Tactic for working with cofinite quantification *)
+
+(** Consider a rule [H] (equivalently, hypothesis, constructor, lemma,
+    etc.) of the form [(forall L ..., ... -> (forall y, y `notin` L ->
+    P) -> ... -> Q)], where [Q]'s outermost constructor is not a
+    [forall].  There may be multiple hypotheses of with the indicated
+    form in [H].
+
+    The tactic [(pick fresh x and apply H)] applies [H] to the current
+    goal, instantiating [H]'s first argument (i.e., [L]) with the
+    finite set of atoms [L'].  In each new subgoal arising from a
+    hypothesis of the form [(forall y, y `notin` L -> P)], the atom
+    [y] is introduced as [x], and [(y `notin` L)] is introduced using
+    a generated name.
+
+    If we view [H] as a rule that uses cofinite quantification, the
+    tactic can be read as picking a sufficiently fresh atom to open a
+    term with.  *)
+
+Tactic Notation
+      "pick" "fresh" ident(atom_name)
+      "excluding" constr(L)
+      "and" "apply" constr(H) :=
+  let L := beautify_fset L in
+    first [apply (@H L) | eapply (@H L)];
+    match goal with
+      | |- forall _, _ `notin` _ -> _ =>
+            let Fr := fresh "Fr" in intros atom_name Fr
+      | |- forall _, _ `notin` _ -> _ =>
+            fail 1 "because" atom_name "is already defined"
+      | _ =>
+            idtac
+    end.
+
+
+(* ********************************************************************** *)
+(** * Automation *)
+
+(** These hints should discharge many of the freshness and inequality
+    goals that arise in programming language metatheory proofs, in
+    particular those arising from cofinite quantification. *)
+
+Hint Resolve notin_empty notin_singleton notin_union.
+Hint Extern 4 (_ `notin` _) => simpl_env; notin_solve.
+Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve.

coq-Fsub/_CoqProject

@@ -0,0 +1,13 @@
+-R . Fsub
+AdditionalTactics.v
+FSetDecide.v
+FSetNotin.v
+ListFacts.v
+FiniteSets.v
+Atom.v
+Metatheory.v
+Fsub_Definitions.v
+Fsub_Infrastructure.v
+Fsub_Lemmas.v
+Fsub_Soundness.v
+