diff --git a/coq-Fsub/AdditionalTactics.v b/coq-Fsub/AdditionalTactics.v
new file mode 100644
index 0000000..ff2d7cf
--- /dev/null
+++ b/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. *)
diff --git a/coq-Fsub/Atom.v b/coq-Fsub/Atom.v
new file mode 100644
index 0000000..255296c
--- /dev/null
+++ b/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 *)
+
+
+(* ********************************************************************** *)
+(** ** ## 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 *)
diff --git a/coq-Fsub/Environment.v b/coq-Fsub/Environment.v
new file mode 100644
index 0000000..f17ea3f
--- /dev/null
+++ b/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:
+ - #Overview#
+ - #Functions on environments#
+ - #Relations on environments#
+ - #Properties of operations#
+ - #Automation and tactics (I)#
+ - #Properties of well-formedness and freshness#
+ - #Properties of binds#
+ - #Automation and tactics (II)#
+ - #Additional properties of binds#
+ - #Automation and tactics (III)# *)
+
+Require Export List.
+Require Export ListFacts.
+Require Import Atom.
+
+Import AtomSet.F.
+Hint Local Unfold E.eq.
+
+
+(* ********************************************************************** *)
+(** * ## 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. *)
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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).
+
+(** ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* *********************************************************************** *)
+(** * ## 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.
+
+
+(* *********************************************************************** *)
+(** * ## 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.
diff --git a/coq-Fsub/FSetDecide.v b/coq-Fsub/FSetDecide.v
new file mode 100644
index 0000000..e946620
--- /dev/null
+++ b/coq-Fsub/FSetDecide.v
@@ -0,0 +1,1052 @@
+(**************************************************************)
+(* FSetDecide.v *)
+(* *)
+(* Author: Aaron Bohannon *)
+(**************************************************************)
+
+(** This file implements a decision procedure for a certain
+ class of propositions involving finite sets. *)
+
+Require Import FSets.
+
+Module Decide (Import M : S).
+
+(** * Overview
+ This functor defines the tactic [fsetdec], which will
+ solve any valid goal of the form
+<<
+ forall s1 ... sn,
+ forall x1 ... xm,
+ P1 -> ... -> Pk -> P
+>>
+ where [P]'s are defined by the grammar:
+<<
+
+P ::=
+| Q
+| Empty F
+| Subset F F'
+| Equal F F'
+
+Q ::=
+| E.eq X X'
+| In X F
+| Q /\ Q'
+| Q \/ Q'
+| Q -> Q'
+| Q <-> Q'
+| ~ Q
+| True
+| False
+
+F ::=
+| S
+| empty
+| singleton X
+| add X F
+| remove X F
+| union F F'
+| inter F F'
+| diff F F'
+
+X ::= x1 | ... | xm
+S ::= s1 | ... | sn
+
+>>
+
+The tactic will also work on some goals that vary slightly from
+the above form:
+- The variables and hypotheses may be mixed in any order and may
+ have already been introduced into the context. Moreover,
+ there may be additional, unrelated hypotheses mixed in (these
+ will be ignored).
+- A conjunction of hypotheses will be handled as easily as
+ separate hypotheses, i.e., [P1 /\ P2 -> P] can be solved iff
+ [P1 -> P2 -> P] can be solved.
+- [fsetdec] should solve any goal if the FSet-related hypotheses
+ are contradictory.
+- [fsetdec] will first perform any necessary zeta and beta
+ reductions and will invoke [subst] to eliminate any Coq
+ equalities between finite sets or their elements.
+- If [E.eq] is convertible with Coq's equality, it will not
+ matter which one is used in the hypotheses or conclusion.
+- The tactic can solve goals where the finite sets or set
+ elements are expressed by Coq terms that are more complicated
+ than variables. However, non-local definitions are not
+ expanded, and Coq equalities between non-variable terms are
+ not used. For example, this goal will be solved:
+<<
+ forall (f : t -> t),
+ forall (g : elt -> elt),
+ forall (s1 s2 : t),
+ forall (x1 x2 : elt),
+ Equal s1 (f s2) ->
+ E.eq x1 (g (g x2)) ->
+ In x1 s1 ->
+ In (g (g x2)) (f s2)
+>>
+ This one will not be solved:
+<<
+ forall (f : t -> t),
+ forall (g : elt -> elt),
+ forall (s1 s2 : t),
+ forall (x1 x2 : elt),
+ Equal s1 (f s2) ->
+ E.eq x1 (g x2) ->
+ In x1 s1 ->
+ g x2 = g (g x2) ->
+ In (g (g x2)) (f s2)
+>>
+*)
+
+ (** * Facts and Tactics for Propositional Logic
+ These lemmas and tactics are in a module so that they do
+ not affect the namespace if you import the enclosing
+ module [Decide]. *)
+ Module FSetLogicalFacts.
+ Require Export Decidable.
+ Require Export Setoid.
+
+ (** ** Lemmas and Tactics About Decidable Propositions
+ XXX: The lemma [dec_iff] should have been included in
+ [Decidable.v]. Some form of the [solve_decidable]
+ tactics below would also make sense in [Decidable.v].
+ *)
+
+ Lemma dec_iff : forall P Q : Prop,
+ decidable P ->
+ decidable Q ->
+ decidable (P <-> Q).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ (** With this hint database, we can leverage [auto] to check
+ decidability of propositions. *)
+ Hint Resolve
+ dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
+ : decidable_prop.
+
+ (** [solve_decidable using lib] will solve goals about the
+ decidability of a proposition, assisted by an auxiliary
+ database of lemmas. The database is intended to contain
+ lemmas stating the decidability of base propositions,
+ (e.g., the decidability of equality on a particular
+ inductive type). *)
+ Tactic Notation "solve_decidable" "using" ident(db) :=
+ match goal with
+ | |- decidable ?P =>
+ solve [ auto 100 with decidable_prop db ]
+ end.
+
+ Tactic Notation "solve_decidable" :=
+ solve_decidable using core.
+
+ (** ** Propositional Equivalences Involving Negation
+ These are all written with the unfolded form of
+ negation, since I am not sure if setoid rewriting will
+ always perform conversion. *)
+
+ (** *** Eliminating Negations
+ We begin with lemmas that, when read from left to right,
+ can be understood as ways to eliminate uses of [not]. *)
+
+ Lemma not_true_iff :
+ (True -> False) <-> False.
+ Proof.
+ tauto.
+ Qed.
+
+ Lemma not_false_iff :
+ (False -> False) <-> True.
+ Proof.
+ tauto.
+ Qed.
+
+ Lemma not_not_iff : forall P : Prop,
+ decidable P ->
+ (((P -> False) -> False) <-> P).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma contrapositive : forall P Q : Prop,
+ decidable P ->
+ (((P -> False) -> (Q -> False)) <-> (Q -> P)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma or_not_l_iff_1 : forall P Q : Prop,
+ decidable P ->
+ ((P -> False) \/ Q <-> (P -> Q)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma or_not_l_iff_2 : forall P Q : Prop,
+ decidable Q ->
+ ((P -> False) \/ Q <-> (P -> Q)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma or_not_r_iff_1 : forall P Q : Prop,
+ decidable P ->
+ (P \/ (Q -> False) <-> (Q -> P)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma or_not_r_iff_2 : forall P Q : Prop,
+ decidable Q ->
+ (P \/ (Q -> False) <-> (Q -> P)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma imp_not_l : forall P Q : Prop,
+ decidable P ->
+ (((P -> False) -> Q) <-> (P \/ Q)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ (** *** Moving Negations Around
+ We have four lemmas that, when read from left to right,
+ describe how to push negations toward the leaves of a
+ proposition and, when read from right to left, describe
+ how to pull negations toward the top of a proposition. *)
+
+ Lemma not_or_iff : forall P Q : Prop,
+ (P \/ Q -> False) <-> (P -> False) /\ (Q -> False).
+ Proof.
+ tauto.
+ Qed.
+
+ Lemma not_and_iff : forall P Q : Prop,
+ (P /\ Q -> False) <-> (P -> Q -> False).
+ Proof.
+ tauto.
+ Qed.
+
+ Lemma not_imp_iff : forall P Q : Prop,
+ decidable P ->
+ (((P -> Q) -> False) <-> P /\ (Q -> False)).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ Lemma not_imp_rev_iff : forall P Q : Prop,
+ decidable P ->
+ (((P -> Q) -> False) <-> (Q -> False) /\ P).
+ Proof.
+ unfold decidable in *. tauto.
+ Qed.
+
+ (** ** Tactics for Negations *)
+
+ Tactic Notation "fold" "any" "not" :=
+ repeat (
+ match goal with
+ | H: context [?P -> False] |- _ =>
+ fold (~ P) in H
+ | |- context [?P -> False] =>
+ fold (~ P)
+ end).
+
+ (** [push not using db] will pushes all negations to the
+ leaves of propositions in the goal, using the lemmas in
+ [db] to assist in checking the decidability of the
+ propositions involved. If [using db] is omitted, then
+ [core] will be used. Additional versions are provided
+ to manipulate the hypotheses or the hypotheses and goal
+ together.
+
+ XXX: This tactic and the similar subsequent ones should
+ have been defined using [autorewrite]. However, there
+ is a bug in the order that Coq generates subgoals when
+ rewriting using a setoid. In order to work around this
+ bug, these tactics had to be written out in an explicit
+ way. When the bug is fixed these tactics will break!!
+ *)
+
+ Tactic Notation "push" "not" "using" ident(db) :=
+ unfold not, iff;
+ repeat (
+ match goal with
+ (** simplification by not_true_iff *)
+ | |- context [True -> False] =>
+ rewrite not_true_iff
+ (** simplification by not_false_iff *)
+ | |- context [False -> False] =>
+ rewrite not_false_iff
+ (** simplification by not_not_iff *)
+ | |- context [(?P -> False) -> False] =>
+ rewrite (not_not_iff P);
+ [ solve_decidable using db | ]
+ (** simplification by contrapositive *)
+ | |- context [(?P -> False) -> (?Q -> False)] =>
+ rewrite (contrapositive P Q);
+ [ solve_decidable using db | ]
+ (** simplification by or_not_l_iff_1/_2 *)
+ | |- context [(?P -> False) \/ ?Q] =>
+ (rewrite (or_not_l_iff_1 P Q);
+ [ solve_decidable using db | ]) ||
+ (rewrite (or_not_l_iff_2 P Q);
+ [ solve_decidable using db | ])
+ (** simplification by or_not_r_iff_1/_2 *)
+ | |- context [?P \/ (?Q -> False)] =>
+ (rewrite (or_not_r_iff_1 P Q);
+ [ solve_decidable using db | ]) ||
+ (rewrite (or_not_r_iff_2 P Q);
+ [ solve_decidable using db | ])
+ (** simplification by imp_not_l *)
+ | |- context [(?P -> False) -> ?Q] =>
+ rewrite (imp_not_l P Q);
+ [ solve_decidable using db | ]
+ (** rewriting by not_or_iff *)
+ | |- context [?P \/ ?Q -> False] =>
+ rewrite (not_or_iff P Q)
+ (** rewriting by not_and_iff *)
+ | |- context [?P /\ ?Q -> False] =>
+ rewrite (not_and_iff P Q)
+ (** rewriting by not_imp_iff *)
+ | |- context [(?P -> ?Q) -> False] =>
+ rewrite (not_imp_iff P Q);
+ [ solve_decidable using db | ]
+ end);
+ fold any not.
+
+ Tactic Notation "push" "not" :=
+ push not using core.
+
+ Tactic Notation
+ "push" "not" "in" "*" "|-" "using" ident(db) :=
+ unfold not, iff in * |-;
+ repeat (
+ match goal with
+ (** simplification by not_true_iff *)
+ | H: context [True -> False] |- _ =>
+ rewrite not_true_iff in H
+ (** simplification by not_false_iff *)
+ | H: context [False -> False] |- _ =>
+ rewrite not_false_iff in H
+ (** simplification by not_not_iff *)
+ | H: context [(?P -> False) -> False] |- _ =>
+ rewrite (not_not_iff P) in H;
+ [ | solve_decidable using db ]
+ (** simplification by contrapositive *)
+ | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
+ rewrite (contrapositive P Q) in H;
+ [ | solve_decidable using db ]
+ (** simplification by or_not_l_iff_1/_2 *)
+ | H: context [(?P -> False) \/ ?Q] |- _ =>
+ (rewrite (or_not_l_iff_1 P Q) in H;
+ [ | solve_decidable using db ]) ||
+ (rewrite (or_not_l_iff_2 P Q) in H;
+ [ | solve_decidable using db ])
+ (** simplification by or_not_r_iff_1/_2 *)
+ | H: context [?P \/ (?Q -> False)] |- _ =>
+ (rewrite (or_not_r_iff_1 P Q) in H;
+ [ | solve_decidable using db ]) ||
+ (rewrite (or_not_r_iff_2 P Q) in H;
+ [ | solve_decidable using db ])
+ (** simplification by imp_not_l *)
+ | H: context [(?P -> False) -> ?Q] |- _ =>
+ rewrite (imp_not_l P Q) in H;
+ [ | solve_decidable using db ]
+ (** rewriting by not_or_iff *)
+ | H: context [?P \/ ?Q -> False] |- _ =>
+ rewrite (not_or_iff P Q) in H
+ (** rewriting by not_and_iff *)
+ | H: context [?P /\ ?Q -> False] |- _ =>
+ rewrite (not_and_iff P Q) in H
+ (** rewriting by not_imp_iff *)
+ | H: context [(?P -> ?Q) -> False] |- _ =>
+ rewrite (not_imp_iff P Q) in H;
+ [ | solve_decidable using db ]
+ end);
+ fold any not.
+
+ Tactic Notation "push" "not" "in" "*" "|-" :=
+ push not in * |- using core.
+
+ Tactic Notation "push" "not" "in" "*" "using" ident(db) :=
+ push not using db; push not in * |- using db.
+ Tactic Notation "push" "not" "in" "*" :=
+ push not in * using core.
+
+ (** A simple test case to see how this works. *)
+ Lemma test_push : forall P Q R : Prop,
+ decidable P ->
+ decidable Q ->
+ (~ True) ->
+ (~ False) ->
+ (~ ~ P) ->
+ (~ (P /\ Q) -> ~ R) ->
+ ((P /\ Q) \/ ~ R) ->
+ (~ (P /\ Q) \/ R) ->
+ (R \/ ~ (P /\ Q)) ->
+ (~ R \/ (P /\ Q)) ->
+ (~ P -> R) ->
+ (~ ((R -> P) \/ (R -> Q))) ->
+ (~ (P /\ R)) ->
+ (~ (P -> R)) ->
+ True.
+ Proof.
+ intros. push not in *. tauto.
+ Qed.
+
+ (** [pull not using db] will pull as many negations as
+ possible toward the top of the propositions in the goal,
+ using the lemmas in [db] to assist in checking the
+ decidability of the propositions involved. If [using
+ db] is omitted, then [core] will be used. Additional
+ versions are provided to manipulate the hypotheses or
+ the hypotheses and goal together. *)
+
+ Tactic Notation "pull" "not" "using" ident(db) :=
+ unfold not, iff;
+ repeat (
+ match goal with
+ (** simplification by not_true_iff *)
+ | |- context [True -> False] =>
+ rewrite not_true_iff
+ (** simplification by not_false_iff *)
+ | |- context [False -> False] =>
+ rewrite not_false_iff
+ (** simplification by not_not_iff *)
+ | |- context [(?P -> False) -> False] =>
+ rewrite (not_not_iff P);
+ [ solve_decidable using db | ]
+ (** simplification by contrapositive *)
+ | |- context [(?P -> False) -> (?Q -> False)] =>
+ rewrite (contrapositive P Q);
+ [ solve_decidable using db | ]
+ (** simplification by or_not_l_iff_1/_2 *)
+ | |- context [(?P -> False) \/ ?Q] =>
+ (rewrite (or_not_l_iff_1 P Q);
+ [ solve_decidable using db | ]) ||
+ (rewrite (or_not_l_iff_2 P Q);
+ [ solve_decidable using db | ])
+ (** simplification by or_not_r_iff_1/_2 *)
+ | |- context [?P \/ (?Q -> False)] =>
+ (rewrite (or_not_r_iff_1 P Q);
+ [ solve_decidable using db | ]) ||
+ (rewrite (or_not_r_iff_2 P Q);
+ [ solve_decidable using db | ])
+ (** simplification by imp_not_l *)
+ | |- context [(?P -> False) -> ?Q] =>
+ rewrite (imp_not_l P Q);
+ [ solve_decidable using db | ]
+ (** rewriting by not_or_iff *)
+ | |- context [(?P -> False) /\ (?Q -> False)] =>
+ rewrite <- (not_or_iff P Q)
+ (** rewriting by not_and_iff *)
+ | |- context [?P -> ?Q -> False] =>
+ rewrite <- (not_and_iff P Q)
+ (** rewriting by not_imp_iff *)
+ | |- context [?P /\ (?Q -> False)] =>
+ rewrite <- (not_imp_iff P Q);
+ [ solve_decidable using db | ]
+ (** rewriting by not_imp_rev_iff *)
+ | |- context [(?Q -> False) /\ ?P] =>
+ rewrite <- (not_imp_rev_iff P Q);
+ [ solve_decidable using db | ]
+ end);
+ fold any not.
+
+ Tactic Notation "pull" "not" :=
+ pull not using core.
+
+ Tactic Notation
+ "pull" "not" "in" "*" "|-" "using" ident(db) :=
+ unfold not, iff in * |-;
+ repeat (
+ match goal with
+ (** simplification by not_true_iff *)
+ | H: context [True -> False] |- _ =>
+ rewrite not_true_iff in H
+ (** simplification by not_false_iff *)
+ | H: context [False -> False] |- _ =>
+ rewrite not_false_iff in H
+ (** simplification by not_not_iff *)
+ | H: context [(?P -> False) -> False] |- _ =>
+ rewrite (not_not_iff P) in H;
+ [ | solve_decidable using db ]
+ (** simplification by contrapositive *)
+ | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
+ rewrite (contrapositive P Q) in H;
+ [ | solve_decidable using db ]
+ (** simplification by or_not_l_iff_1/_2 *)
+ | H: context [(?P -> False) \/ ?Q] |- _ =>
+ (rewrite (or_not_l_iff_1 P Q) in H;
+ [ | solve_decidable using db ]) ||
+ (rewrite (or_not_l_iff_2 P Q) in H;
+ [ | solve_decidable using db ])
+ (** simplification by or_not_r_iff_1/_2 *)
+ | H: context [?P \/ (?Q -> False)] |- _ =>
+ (rewrite (or_not_r_iff_1 P Q) in H;
+ [ | solve_decidable using db ]) ||
+ (rewrite (or_not_r_iff_2 P Q) in H;
+ [ | solve_decidable using db ])
+ (** simplification by imp_not_l *)
+ | H: context [(?P -> False) -> ?Q] |- _ =>
+ rewrite (imp_not_l P Q) in H;
+ [ | solve_decidable using db ]
+ (** rewriting by not_or_iff *)
+ | H: context [(?P -> False) /\ (?Q -> False)] |- _ =>
+ rewrite <- (not_or_iff P Q) in H
+ (** rewriting by not_and_iff *)
+ | H: context [?P -> ?Q -> False] |- _ =>
+ rewrite <- (not_and_iff P Q) in H
+ (** rewriting by not_imp_iff *)
+ | H: context [?P /\ (?Q -> False)] |- _ =>
+ rewrite <- (not_imp_iff P Q) in H;
+ [ | solve_decidable using db ]
+ (** rewriting by not_imp_rev_iff *)
+ | H: context [(?Q -> False) /\ ?P] |- _ =>
+ rewrite <- (not_imp_rev_iff P Q) in H;
+ [ | solve_decidable using db ]
+ end);
+ fold any not.
+
+ Tactic Notation "pull" "not" "in" "*" "|-" :=
+ pull not in * |- using core.
+
+ Tactic Notation "pull" "not" "in" "*" "using" ident(db) :=
+ pull not using db; pull not in * |- using db.
+ Tactic Notation "pull" "not" "in" "*" :=
+ pull not in * using core.
+
+ (** A simple test case to see how this works. *)
+ Lemma test_pull : forall P Q R : Prop,
+ decidable P ->
+ decidable Q ->
+ (~ True) ->
+ (~ False) ->
+ (~ ~ P) ->
+ (~ (P /\ Q) -> ~ R) ->
+ ((P /\ Q) \/ ~ R) ->
+ (~ (P /\ Q) \/ R) ->
+ (R \/ ~ (P /\ Q)) ->
+ (~ R \/ (P /\ Q)) ->
+ (~ P -> R) ->
+ (~ (R -> P) /\ ~ (R -> Q)) ->
+ (~ P \/ ~ R) ->
+ (P /\ ~ R) ->
+ (~ R /\ P) ->
+ True.
+ Proof.
+ intros. pull not in *. tauto.
+ Qed.
+
+ End FSetLogicalFacts.
+ Import FSetLogicalFacts.
+
+ (** * Auxiliary Tactics
+ Again, these lemmas and tactics are in a module so that
+ they do not affect the namespace if you import the
+ enclosing module [Decide]. *)
+ Module FSetDecideAuxiliary.
+
+ (** ** Generic Tactics
+ We begin by defining a few generic, useful tactics. *)
+
+ (** [if t then t1 else t2] executes [t] and, if it does not
+ fail, then [t1] will be applied to all subgoals
+ produced. If [t] fails, then [t2] is executed. *)
+ Tactic Notation
+ "if" tactic(t)
+ "then" tactic(t1)
+ "else" tactic(t2) :=
+ first [ t; first [ t1 | fail 2 ] | t2 ].
+
+ (** [prop P holds by t] succeeds (but does not modify the
+ goal or context) if the proposition [P] can be proved by
+ [t] in the current context. Otherwise, the tactic
+ fails. *)
+ Tactic Notation "prop" constr(P) "holds" "by" tactic(t) :=
+ let H := fresh in
+ assert P as H by t;
+ clear H.
+
+ (** This tactic acts just like [assert ... by ...] but will
+ fail if the context already contains the proposition. *)
+ Tactic Notation "assert" "new" constr(e) "by" tactic(t) :=
+ match goal with
+ | H: e |- _ => fail 1
+ | _ => assert e by t
+ end.
+
+ (** [subst++] is similar to [subst] except that
+ - it never fails (as [subst] does on recursive
+ equations),
+ - it substitutes locally defined variable for their
+ definitions,
+ - it performs beta reductions everywhere, which may
+ arise after substituting a locally defined function
+ for its definition.
+ *)
+ Tactic Notation "subst" "++" :=
+ repeat (
+ match goal with
+ | x : _ |- _ => subst x
+ end);
+ cbv zeta beta in *.
+
+ (** If you have a negated goal and [H] is a negated
+ hypothesis, then [contra H] exchanges your goal and [H],
+ removing the negations. (Just like [swap] but reuses
+ the same name. *)
+ Ltac contra H :=
+ let J := fresh in
+ unfold not;
+ unfold not in H;
+ intros J;
+ apply H;
+ clear H;
+ rename J into H.
+
+ (** [decompose records] calls [decompose record H] on every
+ relevant hypothesis [H]. *)
+ Tactic Notation "decompose" "records" :=
+ repeat (
+ match goal with
+ | H: _ |- _ => progress (decompose record H); clear H
+ end).
+
+ (** ** Discarding Irrelevant Hypotheses
+ We will want to clear the context of any
+ non-FSet-related hypotheses in order to increase the
+ speed of the tactic. To do this, we will need to be
+ able to decide which are relevant. We do this by making
+ a simple inductive definition classifying the
+ propositions of interest. *)
+
+ Inductive FSet_elt_Prop : Prop -> Prop :=
+ | eq_Prop : forall (S : Set) (x y : S),
+ FSet_elt_Prop (x = y)
+ | eq_elt_prop : forall x y,
+ FSet_elt_Prop (E.eq x y)
+ | In_elt_prop : forall x s,
+ FSet_elt_Prop (In x s)
+ | True_elt_prop :
+ FSet_elt_Prop True
+ | False_elt_prop :
+ FSet_elt_Prop False
+ | conj_elt_prop : forall P Q,
+ FSet_elt_Prop P ->
+ FSet_elt_Prop Q ->
+ FSet_elt_Prop (P /\ Q)
+ | disj_elt_prop : forall P Q,
+ FSet_elt_Prop P ->
+ FSet_elt_Prop Q ->
+ FSet_elt_Prop (P \/ Q)
+ | impl_elt_prop : forall P Q,
+ FSet_elt_Prop P ->
+ FSet_elt_Prop Q ->
+ FSet_elt_Prop (P -> Q)
+ | not_elt_prop : forall P,
+ FSet_elt_Prop P ->
+ FSet_elt_Prop (~ P).
+
+ Inductive FSet_Prop : Prop -> Prop :=
+ | elt_FSet_Prop : forall P,
+ FSet_elt_Prop P ->
+ FSet_Prop P
+ | Empty_FSet_Prop : forall s,
+ FSet_Prop (Empty s)
+ | Subset_FSet_Prop : forall s1 s2,
+ FSet_Prop (Subset s1 s2)
+ | Equal_FSet_Prop : forall s1 s2,
+ FSet_Prop (Equal s1 s2).
+
+ (** Here is the tactic that will throw away hypotheses that
+ are not useful (for the intended scope of the [fsetdec]
+ tactic). *)
+ Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
+ Ltac discard_nonFSet :=
+ decompose records;
+ repeat (
+ match goal with
+ | H : ?P |- _ =>
+ if prop (FSet_Prop P) holds by
+ (auto 100 with FSet_Prop)
+ then fail
+ else clear H
+ end).
+
+ (** ** Turning Set Operators into Propositional Connectives
+ The lemmas from [FSetFacts] will be used to break down
+ set operations into propositional formulas built over
+ the predicates [In] and [E.eq] applied only to
+ variables. We are going to use them with [autorewrite].
+ *)
+ Module F := FSetFacts.Facts M.
+ Hint Rewrite
+ F.empty_iff F.singleton_iff F.add_iff F.remove_iff
+ F.union_iff F.inter_iff F.diff_iff
+ : set_simpl.
+
+ (** ** Decidability of FSet Propositions *)
+
+ (** [In] is decidable. *)
+ Module D := DepOfNodep M.
+ Lemma dec_In : forall x s,
+ decidable (In x s).
+ Proof.
+ intros x s. red. destruct (D.mem x s); auto.
+ Qed.
+
+ (** [E.eq] is decidable. *)
+ Lemma dec_eq : forall (x y : E.t),
+ decidable (E.eq x y).
+ Proof.
+ intros x y. red. destruct (E.compare x y); auto.
+ Qed.
+
+ (** The hint database [FSet_decidability] will be given to
+ the [push_neg] tactic from the module [Negation]. *)
+ Hint Resolve dec_In dec_eq : FSet_decidability.
+
+ (** ** Normalizing Propositions About Equality
+ We have to deal with the fact that [E.eq] may be
+ convertible with Coq's equality. Thus, we will find the
+ following tactics useful to replace one form with the
+ other everywhere. *)
+
+ (** The next tactic, [Logic_eq_to_E_eq], mentions the term
+ [E.t]; thus, we must ensure that [E.t] is used in favor
+ of any other convertible but syntactically distinct
+ term. *)
+ Ltac change_to_E_t :=
+ repeat (
+ match goal with
+ | H : ?T |- _ =>
+ progress (change T with E.t in H);
+ repeat (
+ match goal with
+ | J : _ |- _ => progress (change T with E.t in J)
+ | |- _ => progress (change T with E.t)
+ end )
+ end).
+
+ (** These two tactics take us from Coq's built-in equality
+ to [E.eq] (and vice versa) when possible. *)
+
+ Ltac Logic_eq_to_E_eq :=
+ repeat (
+ match goal with
+ | H: _ |- _ =>
+ progress (change (@Logic.eq E.t) with E.eq in H)
+ | |- _ =>
+ progress (change (@Logic.eq E.t) with E.eq)
+ end).
+
+ Ltac E_eq_to_Logic_eq :=
+ repeat (
+ match goal with
+ | H: _ |- _ =>
+ progress (change E.eq with (@Logic.eq E.t) in H)
+ | |- _ =>
+ progress (change E.eq with (@Logic.eq E.t))
+ end).
+
+ (** This tactic works like the built-in tactic [subst], but
+ at the level of set element equality (which may not be
+ the convertible with Coq's equality). *)
+ Ltac substFSet :=
+ repeat (
+ match goal with
+ | H: E.eq ?x ?y |- _ => rewrite H in *; clear H
+ end).
+
+ (** ** Considering Decidability of Base Propositions
+ This tactic adds assertions about the decidability of
+ [E.eq] and [In] to the context. This is necessary for
+ the completeness of the [fsetdec] tactic. However, in
+ order to minimize the cost of proof search, we should be
+ careful to not add more than we need. Once negations
+ have been pushed to the leaves of the propositions, we
+ only need to worry about decidability for those base
+ propositions that appear in a negated form. *)
+ Ltac assert_decidability :=
+ (** We actually don't want these rules to fire if the
+ syntactic context in the patterns below is trivially
+ empty, but we'll just do some clean-up at the
+ afterward. *)
+ repeat (
+ match goal with
+ | H: context [~ E.eq ?x ?y] |- _ =>
+ assert new (E.eq x y \/ ~ E.eq x y) by (apply dec_eq)
+ | H: context [~ In ?x ?s] |- _ =>
+ assert new (In x s \/ ~ In x s) by (apply dec_In)
+ | |- context [~ E.eq ?x ?y] =>
+ assert new (E.eq x y \/ ~ E.eq x y) by (apply dec_eq)
+ | |- context [~ In ?x ?s] =>
+ assert new (In x s \/ ~ In x s) by (apply dec_In)
+ end);
+ (** Now we eliminate the useless facts we added (because
+ they would likely be very harmful to performance). *)
+ repeat (
+ match goal with
+ | _: ~ ?P, H : ?P \/ ~ ?P |- _ => clear H
+ end).
+
+ (** ** Handling [Empty], [Subset], and [Equal]
+ This tactic instantiates universally quantified
+ hypotheses (which arise from the unfolding of [Empty],
+ [Subset], and [Equal]) for each of the set element
+ expressions that is involved in some membership or
+ equality fact. Then it throws away those hypotheses,
+ which should no longer be needed. *)
+ Ltac inst_FSet_hypotheses :=
+ repeat (
+ match goal with
+ | H : forall a : E.t, _,
+ _ : context [ In ?x _ ] |- _ =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ | H : forall a : E.t, _
+ |- context [ In ?x _ ] =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ | H : forall a : E.t, _,
+ _ : context [ E.eq ?x _ ] |- _ =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ | H : forall a : E.t, _
+ |- context [ E.eq ?x _ ] =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ | H : forall a : E.t, _,
+ _ : context [ E.eq _ ?x ] |- _ =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ | H : forall a : E.t, _
+ |- context [ E.eq _ ?x ] =>
+ let P := type of (H x) in
+ assert new P by (exact (H x))
+ end);
+ repeat (
+ match goal with
+ | H : forall a : E.t, _ |- _ =>
+ clear H
+ end).
+
+ (** ** The Core [fsetdec] Auxiliary Tactics *)
+
+ (** Here is the crux of the proof search. Recursion through
+ [intuition]! (This will terminate if I correctly
+ understand the behavior of [intuition].) *)
+ Ltac fsetdec_rec :=
+ try (match goal with
+ | H: E.eq ?x ?x -> False |- _ => destruct H
+ end);
+ (reflexivity ||
+ contradiction ||
+ (progress substFSet; intuition fsetdec_rec)).
+
+ (** If we add [unfold Empty, Subset, Equal in *; intros;] to
+ the beginning of this tactic, it will satisfy the same
+ specification as the [fsetdec] tactic; however, it will
+ be much slower than necessary without the pre-processing
+ done by the wrapper tactic [fsetdec]. *)
+ Ltac fsetdec_body :=
+ inst_FSet_hypotheses;
+ autorewrite with set_simpl in *;
+ push not in * using FSet_decidability;
+ substFSet;
+ assert_decidability;
+ auto using E.eq_refl;
+ (intuition fsetdec_rec) ||
+ fail 1
+ "because the goal is beyond the scope of this tactic".
+
+ End FSetDecideAuxiliary.
+ Import FSetDecideAuxiliary.
+
+ (** * The [fsetdec] Tactic
+ Here is the top-level tactic (the only one intended for
+ clients of this library). It's specification is given at
+ the top of the file. *)
+ Ltac fsetdec :=
+ (** We first unfold any occurrences of [iff]. *)
+ unfold iff in *;
+ (** We fold occurrences of [not] because it is better for
+ [intros] to leave us with a goal of [~ P] than a goal of
+ [False]. *)
+ fold any not; intros;
+ (** Now we decompose conjunctions, which will allow the
+ [discard_nonFSet] and [assert_decidability] tactics to
+ do a much better job. *)
+ decompose records;
+ discard_nonFSet;
+ (** We unfold these defined propositions on finite sets. If
+ our goal was one of them, then have one more item to
+ introduce now. *)
+ unfold Empty, Subset, Equal in *; intros;
+ (** We now want to get rid of all uses of [=] in favor of
+ [E.eq]. However, the best way to eliminate a [=] in
+ the context is with [subst], so we will try that first.
+ In fact, we may as well convert uses of [E.eq] into [=]
+ where possible before we do [subst] so that we can get
+ even more mileage out of it. Then we will convert all
+ remaining uses of [=] back to [E.eq] when possible. We
+ use [change_to_E_t] to ensure that we have a canonical
+ name for set elements, so that [Logic_eq_to_E_eq] will
+ work properly. *)
+ change_to_E_t; E_eq_to_Logic_eq; subst++; Logic_eq_to_E_eq;
+ (** The next optimization is to swap a negated goal with a
+ negated hypothesis when possible. Any swap will improve
+ performance by eliminating the total number of
+ negations, but we will get the maximum benefit if we
+ swap the goal with a hypotheses mentioning the same set
+ element, so we try that first. If we reach the fourth
+ branch below, we attempt any swap. However, to maintain
+ completeness of this tactic, we can only perform such a
+ swap with a decidable proposition; hence, we first test
+ whether the hypothesis is an [FSet_elt_Prop], noting
+ that any [FSet_elt_Prop] is decidable. *)
+ pull not using FSet_decidability;
+ unfold not in *;
+ match goal with
+ | H: (In ?x ?r) -> False |- (In ?x ?s) -> False =>
+ contra H; fsetdec_body
+ | H: (In ?x ?r) -> False |- (E.eq ?x ?y) -> False =>
+ contra H; fsetdec_body
+ | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
+ contra H; fsetdec_body
+ | H: ?P -> False |- ?Q -> False =>
+ if prop (FSet_elt_Prop P) holds by
+ (auto 100 with FSet_Prop)
+ then (contra H; fsetdec_body)
+ else fsetdec_body
+ | |- _ =>
+ fsetdec_body
+ end.
+
+ (** * Examples *)
+
+ Module FSetDecideTestCases.
+
+ Lemma test_eq_trans_1 : forall x y z s,
+ E.eq x y ->
+ ~ ~ E.eq z y ->
+ In x s ->
+ In z s.
+ Proof. fsetdec. Qed.
+
+ Lemma test_eq_trans_2 : forall x y z r s,
+ In x (singleton y) ->
+ ~ In z r ->
+ ~ ~ In z (add y r) ->
+ In x s ->
+ In z s.
+ Proof. fsetdec. Qed.
+
+ Lemma test_eq_neq_trans_1 : forall w x y z s,
+ E.eq x w ->
+ ~ ~ E.eq x y ->
+ ~ E.eq y z ->
+ In w s ->
+ In w (remove z s).
+ Proof. fsetdec. Qed.
+
+ Lemma test_eq_neq_trans_2 : forall w x y z r1 r2 s,
+ In x (singleton w) ->
+ ~ In x r1 ->
+ In x (add y r1) ->
+ In y r2 ->
+ In y (remove z r2) ->
+ In w s ->
+ In w (remove z s).
+ Proof. fsetdec. Qed.
+
+ Lemma test_In_singleton : forall x,
+ In x (singleton x).
+ Proof. fsetdec. Qed.
+
+ Lemma test_Subset_add_remove : forall x s,
+ s [<=] (add x (remove x s)).
+ Proof. fsetdec. Qed.
+
+ Lemma test_eq_disjunction : forall w x y z,
+ In w (add x (add y (singleton z))) ->
+ E.eq w x \/ E.eq w y \/ E.eq w z.
+ Proof. fsetdec. Qed.
+
+ Lemma test_not_In_disj : forall x y s1 s2 s3 s4,
+ ~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
+ ~ (In x s1 \/ In x s4 \/ E.eq y x).
+ Proof. fsetdec. Qed.
+
+ Lemma test_not_In_conj : forall x y s1 s2 s3 s4,
+ ~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
+ ~ In x s1 /\ ~ In x s4 /\ ~ E.eq y x.
+ Proof. fsetdec. Qed.
+
+ Lemma test_iff_conj : forall a x s s',
+ (In a s' <-> E.eq x a \/ In a s) ->
+ (In a s' <-> In a (add x s)).
+ Proof. fsetdec. Qed.
+
+ Lemma test_set_ops_1 : forall x q r s,
+ (singleton x) [<=] s ->
+ Empty (union q r) ->
+ Empty (inter (diff s q) (diff s r)) ->
+ ~ In x s.
+ Proof. fsetdec. Qed.
+
+ Lemma eq_chain_test : forall x1 x2 x3 x4 s1 s2 s3 s4,
+ Empty s1 ->
+ In x2 (add x1 s1) ->
+ In x3 s2 ->
+ ~ In x3 (remove x2 s2) ->
+ ~ In x4 s3 ->
+ In x4 (add x3 s3) ->
+ In x1 s4 ->
+ Subset (add x4 s4) s4.
+ Proof. fsetdec. Qed.
+
+ Lemma test_too_complex : forall x y z r s,
+ E.eq x y ->
+ (In x (singleton y) -> r [<=] s) ->
+ In z r ->
+ In z s.
+ Proof.
+ (** [fsetdec] is not intended to solve this directly. *)
+ intros until s; intros Heq H Hr; lapply H; fsetdec.
+ Qed.
+
+ Lemma function_test_1 :
+ forall (f : t -> t),
+ forall (g : elt -> elt),
+ forall (s1 s2 : t),
+ forall (x1 x2 : elt),
+ Equal s1 (f s2) ->
+ E.eq x1 (g (g x2)) ->
+ In x1 s1 ->
+ In (g (g x2)) (f s2).
+ Proof. fsetdec. Qed.
+
+ Lemma function_test_2 :
+ forall (f : t -> t),
+ forall (g : elt -> elt),
+ forall (s1 s2 : t),
+ forall (x1 x2 : elt),
+ Equal s1 (f s2) ->
+ E.eq x1 (g x2) ->
+ In x1 s1 ->
+ g x2 = g (g x2) ->
+ In (g (g x2)) (f s2).
+ Proof.
+ (** [fsetdec] is not intended to solve this directly. *)
+ intros until 3. intros g_eq. rewrite <- g_eq. fsetdec.
+ Qed.
+
+ End FSetDecideTestCases.
+
+End Decide.
diff --git a/coq-Fsub/FSetNotin.v b/coq-Fsub/FSetNotin.v
new file mode 100644
index 0000000..1676bfe
--- /dev/null
+++ b/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.
diff --git a/coq-Fsub/FiniteSets.v b/coq-Fsub/FiniteSets.v
new file mode 100644
index 0000000..4fe0bf6
--- /dev/null
+++ b/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.
diff --git a/coq-Fsub/Fsub_Definitions.v b/coq-Fsub/Fsub_Definitions.v
new file mode 100644
index 0000000..b7b7e15
--- /dev/null
+++ b/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:
+ - #Syntax (pre-terms)#
+ - #Opening#
+ - #Local closure#
+ - #Environments#
+ - #Well-formedness#
+ - #Subtyping#
+ - #Typing#
+ - #Values#
+ - #Reduction#
+ - #Automation#
+*)
+
+Require Export Metatheory.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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)
+.
+
+
+
+(* ********************************************************************** *)
+(** * ## 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).
+
+(** ##Examples:## 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. *)
+
+
+(* ********************************************************************** *)
+(** * ## 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).
+
+
+(* ********************************************************************** *)
+(** * ## 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)
+.
+
+
+(* ********************************************************************** *)
+(** * ## 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
+.
+
+
+(* ********************************************************************** *)
+(** * ## 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)
+.
+
+
+(* ********************************************************************** *)
+(** * ## 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)
+.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
diff --git a/coq-Fsub/Fsub_Infrastructure.v b/coq-Fsub/Fsub_Infrastructure.v
new file mode 100644
index 0000000..1385c81
--- /dev/null
+++ b/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:
+ - #Free variables#
+ - #Substitution#
+ - #The "pick fresh" tactic#
+ - #The "pick fresh and apply" tactic#
+ - #Properties of opening and substitution#
+ - #Local closure is preserved under substitution#
+ - #Automation# *)
+
+
+Require Export Fsub_Definitions.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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).
+
+
+(* *********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* *********************************************************************** *)
+(** * ## 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.
+
+
+
+
+
+
+
+(* *********************************************************************** *)
+(** * ## 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)).
diff --git a/coq-Fsub/Fsub_Lemmas.v b/coq-Fsub/Fsub_Lemmas.v
new file mode 100644
index 0000000..50b5a34
--- /dev/null
+++ b/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:
+ - #Properties of wf_typ#
+ - #Properties of wf_env and wf_typ#
+ - #Properties of wf_env#
+ - #Properties of substitution#
+ - #Regularity lemmas#
+ - #Automation# *)
+
+Require Export Fsub_Infrastructure.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* *********************************************************************** *)
+(** * ## 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.
diff --git a/coq-Fsub/Fsub_Soundness.v b/coq-Fsub/Fsub_Soundness.v
new file mode 100644
index 0000000..a1460b8
--- /dev/null
+++ b/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:
+ - #Properties of subtyping#
+ - #Properties of typing#
+ - #Preservation#
+ - #Progress# *)
+
+Require Export Fsub_Lemmas.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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 " 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
+
+
+(* ********************************************************************** *)
+(** * ## 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.
diff --git a/coq-Fsub/ListFacts.v b/coq-Fsub/ListFacts.v
new file mode 100644
index 0000000..f45df99
--- /dev/null
+++ b/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.
diff --git a/coq-Fsub/Metatheory.v b/coq-Fsub/Metatheory.v
new file mode 100644
index 0000000..17a5eb5
--- /dev/null
+++ b/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.
diff --git a/coq-Fsub/_CoqProject b/coq-Fsub/_CoqProject
new file mode 100644
index 0000000..d9c49b4
--- /dev/null
+++ b/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
+