96 lines
3.2 KiB
Coq
96 lines
3.2 KiB
Coq
|
(** 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.
|