take over Metatheory, FiniteSet & Atom libraries from popl-tutorial

coq/AdditionalTactics.v

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

coq/Atom.v

@@ -0,0 +1,265 @@
+(** 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.
+Require Import Psatz.
+
+Require Import AdditionalTactics.
+Require AdditionalTactics.
+
+(* ********************************************************************** *)
+(** * 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. lia. 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)). lia. trivial.
+  Qed.
+
+  Module Atom_as_OT := Nat_as_OT.
+  Module Facts := OrderedTypeFacts Atom_as_OT.
+
+  Definition eq_atom_dec : forall x y : atom, {x = y} + {x <> y} :=
+    Facts.eq_dec.
+
+  (* end hide *)
+
+End AtomImpl.
+
+Export AtomImpl.
+
+
+(* ********************************************************************** *)
+(** * Finite sets of atoms *)
+
+
+(* ********************************************************************** *)
+(** ** Definitions *)
+
+Module AtomSet : FiniteSets.S with Module E := Atom_as_OT :=
+  FiniteSets.Make Atom_as_OT.
+
+(** The type [atoms] is the type of finite sets of [atom]s. *)
+
+Notation atoms := AtomSet.F.t.
+
+(** Basic operations on finite sets of atoms are available, in the
+    remainder of this file, without qualification.  We use [Import]
+    instead of [Export] in order to avoid unnecessary namespace
+    pollution. *)
+
+Import AtomSet.F.
+
+(** We instantiate two modules which provide useful lemmas and tactics
+    work working with finite sets of atoms. *)
+
+Module AtomSetDecide := FSetDecide.Decide AtomSet.F.
+Module AtomSetNotin  := FSetNotin.Notin   AtomSet.F.
+
+
+(* *********************************************************************** *)
+(** ** Tactics for working with finite sets of atoms *)
+
+(** The tactic [fsetdec] is a general purpose decision procedure
+    for solving facts about finite sets of atoms. *)
+
+Ltac fsetdec := try apply AtomSet.eq_if_Equal; AtomSetDecide.fsetdec.
+
+(** The tactic [notin_simpl] simplifies all hypotheses of the form [(~
+    In x F)], where [F] is constructed from the empty set, singleton
+    sets, and unions. *)
+
+Ltac notin_simpl := AtomSetNotin.notin_simpl_hyps.
+
+(** The tactic [notin_solve], solves goals of the form [(~ In x F)],
+    where [F] is constructed from the empty set, singleton sets, and
+    unions.  The goal must be provable from hypothesis of the form
+    simplified by [notin_simpl]. *)
+
+Ltac notin_solve := AtomSetNotin.notin_solve.
+
+
+(* *********************************************************************** *)
+(** ** Lemmas for working with finite sets of atoms *)
+
+(** We make some lemmas about finite sets of atoms available without
+    qualification by using abbreviations. *)
+
+Notation eq_if_Equal        := AtomSet.eq_if_Equal.
+Notation notin_empty        := AtomSetNotin.notin_empty.
+Notation notin_singleton    := AtomSetNotin.notin_singleton.
+Notation notin_singleton_rw := AtomSetNotin.notin_singleton_rw.
+Notation notin_union        := AtomSetNotin.notin_union.
+
+
+(* ********************************************************************** *)
+(** * Additional properties *)
+
+(** One can generate an atom fresh for a given finite set of atoms. *)
+
+Lemma atom_fresh_for_set : forall L : atoms, { x : atom | ~ In x L }.
+Proof.
+  intros L. destruct (atom_fresh_for_list (elements L)) as [a H].
+  exists a. intros J. contradiction H.
+  rewrite <- InA_iff_In. auto using elements_1.
+Qed.
+
+
+(* ********************************************************************** *)
+(** * Additional tactics *)
+
+
+(* ********************************************************************** *)
+(** ** #<a name="pick_fresh"></a># Picking a fresh atom *)
+
+(** We define three tactics which, when combined, provide a simple
+    mechanism for picking a fresh atom.  We demonstrate their use
+    below with an example, the [example_pick_fresh] tactic.
+
+   [(gather_atoms_with F)] returns the union of [(F x)], where [x]
+   ranges over all objects in the context such that [(F x)] is
+   well typed.  The return type of [F] should be [atoms].  The
+   complexity of this tactic is due to the fact that there is no
+   support in [Ltac] for folding a function over the context. *)
+
+Ltac gather_atoms_with F :=
+  let rec gather V :=
+    match goal with
+    | H: ?S |- _ =>
+      let FH := constr:(F H) in
+      match V with
+      | empty => gather FH
+      | context [FH] => fail 1
+      | _ => gather (union FH V)
+      end
+    | _ => V
+    end in
+  let L := gather empty in eval simpl in L.
+
+(** [(beautify_fset V)] takes a set [V] built as a union of finite
+    sets and returns the same set with empty sets removed and union
+    operations associated to the right.  Duplicate sets are also
+    removed from the union. *)
+
+Ltac beautify_fset V :=
+  let rec go Acc E :=
+     match E with
+     | union ?E1 ?E2 => let Acc1 := go Acc E2 in go Acc1 E1
+     | empty => Acc
+     | ?E1 => match Acc with
+              | empty => E1
+              | context [E1] => Acc
+              | _ => constr:(union E1 Acc)
+              end
+     end
+  in go empty V.
+
+(** The tactic [(pick fresh Y for L)] takes a finite set of atoms [L]
+    and a fresh name [Y], and adds to the context an atom with name
+    [Y] and a proof that [(~ In Y L)], i.e., that [Y] is fresh for
+    [L].  The tactic will fail if [Y] is already declared in the
+    context. *)
+
+Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
+  let Fr := fresh "Fr" in
+  let L := beautify_fset L in
+  (destruct (atom_fresh_for_set L) as [Y Fr]).
+
+
+(* ********************************************************************** *)
+(** ** Demonstration *)
+
+(** The [example_pick_fresh] tactic below illustrates the general
+    pattern for using the above three tactics to define a tactic which
+    picks a fresh atom.  The pattern is as follows:
+      - Repeatedly invoke [gather_atoms_with], using functions with
+        different argument types each time.
+      - Union together the result of the calls, and invoke
+        [(pick fresh ... for ...)] with that union of sets. *)
+
+Ltac example_pick_fresh Y :=
+  let A := gather_atoms_with (fun x : atoms => x) in
+  let B := gather_atoms_with (fun x : atom => singleton x) in
+  pick fresh Y for (union A B).
+
+Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3: atoms), True.
+(* begin show *)
+Proof.
+  intros x y z L1 L2 L3. example_pick_fresh k.
+
+  (** At this point in the proof, we have a new atom [k] and a
+      hypothesis [Fr : ~ In k (union L1 (union L2 (union L3 (union
+      (singleton x) (union (singleton y) (singleton z))))))]. *)
+
+  trivial.
+Qed.
+(* end show *)

coq/FSetNotin.v

@@ -0,0 +1,185 @@
+(** 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.
+Require Import AdditionalTactics.
+Require AdditionalTactics.
+
+(* *********************************************************************** *)
+(** * Implementation *)
+
+Module Notin (X : FSetInterface.S).
+
+Import X.
+Import AdditionalTactics.
+
+(* *********************************************************************** *)
+(** ** Facts about set (non-)membership *)
+
+Lemma in_singleton : forall x,
+  In x (singleton x).
+Proof.
+  intros.
+  apply singleton_2.
+  generalize dependent x.
+  apply E.eq_refl.
+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). auto with *.
+Qed.
+
+Lemma elim_notin_singleton : forall x y,
+  ~ In x (singleton y) -> ~ E.eq x y.
+Proof.
+  intros x y H J.
+  contradiction H.
+  apply singleton_2.
+  generalize x y J.
+  apply E.eq_sym.
+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. auto with *.
+  contradict H0.
+  rewrite H0.
+  apply E.eq_refl.
+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.
+
+(*
+  apply notin_singleton.
+  generalize H.
+  apply notin_union.
+*)
+Admitted.
+
+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.*)
+Admitted.
+
+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.*)
+Admitted.
+
+End Notin.

coq/FiniteSets.v

@@ -0,0 +1,65 @@
+(** A library for finite sets with extensional equality.
+
+    Author: Brian Aydemir. *)
+
+Require Import FSets.
+Require Import ListFacts.
+Require Import AdditionalTactics.
+Require AdditionalTactics.
+
+
+(* *********************************************************************** *)
+(** * 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.MSet.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.
+  *)
+  Admitted.
+
+  (* end hide *)
+
+End Make.

coq/ListFacts.v

@@ -0,0 +1,299 @@
+(** 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.
+Require Import AdditionalTactics.
+
+Include AdditionalTactics.
+
+(* ********************************************************************** *)
+(** * 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.
+Admitted.
+
+
+(* ********************************************************************* *)
+(** * 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...
+Admitted.
+(*
+    (* 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...
+  Admitted.
+  (*
+    (* 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.
+
+Create HintDb ListHints.
+Hint Resolve ltA_trans :ListHints.
+Hint Immediate ltA_eqA eqA_ltA :ListHints.
+
+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.
+Admitted.
+
+(*
+      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.
+Admitted.
+(*
+  assert (ltA y x) by (refine (SortA_InfA_InA _ _ _ _ _ H6 H7 H1); auto).
+  assert (ltA x y) by (refine (SortA_InfA_InA _ _ _ _ _ H2 H3 H4); auto).
+  assert (y <> y) by eauto.
+  intuition.
+Qed.
+*)
+
+Lemma Sort_InA_eq_ext :
+  forall xs ys,
+  Sort xs ->
+  Sort ys ->
+  (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys) ->
+  xs = ys.
+Proof.
+  induction xs as [ | x xs IHxs ]; induction ys as [ | y ys IHys ];
+      intros SortXS SortYS H; auto.
+  (* xs -> nil, ys -> y :: ys *)
+  assert (Q : InA (@eq A) y nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> nil *)
+  assert (Q : InA (@eq A) x nil) by firstorder.
+  inversion Q.
+  (* xs -> x :: xs, ys -> y :: ys *)
+  inversion SortXS; inversion SortYS; subst.
+  assert (x = y) by eauto using Sort_eq_head.
+  cut (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys).
+  intros. assert (xs = ys) by auto. subst. auto.
+  intros a; split; intros L.
+    assert (Q2 : InA (@eq A) a (y :: ys)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y xs) by auto using not_InA_if_Sort_Inf.
+      intuition.
+    assert (Q2 : InA (@eq A) a (x :: xs)) by firstorder.
+      inversion Q2; subst; auto.
+      assert (Q5 : ~ InA (@eq A) y ys) by auto using not_InA_if_Sort_Inf.
+      intuition.
+Qed.
+
+End Equality_ext.

coq/Metatheory.v

@@ -0,0 +1,100 @@
+(** 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 *)
+
+Declare Scope metatheory_scope.
+Declare Scope set_scope.
+
+(** 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. *)
+
+Create HintDb MetatheoryHints.
+Hint Resolve notin_empty notin_singleton notin_union :MetatheoryHints.
+(*Hint Extern 4 (_ `notin` _) => simpl_env; notin_solve :MetatheoryHints.
+Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve :MetatheoryHints.
+*)

coq/_CoqProject

@@ -1,4 +1,10 @@
 -R . LadderTypes
+AdditionalTactics.v
+ListFacts.v
+FiniteSets.v
+FSetNotin.v
+Atom.v
+Metatheory.v
 terms.v
 terms_debruijn.v
 equiv.v