Library Metatheory
Require Export Arith.
Require Export FSets.
Require Export List.
Require Export AdditionalTactics.
Require Export Atom.
Require Export AtomEnv.
Require Export AtomSet.
Require Export ListFacts.
Require Export PennFSetDecide.
lt_ge_dec is a useful comparison operation when defining the
"close" operation on locally nameless terms.
Definition lt_ge_dec (n m : nat) : {n < m} + {n ≥ m} :=
match Compare_dec.le_gt_dec m n with
| left pf ⇒ right _ pf
| right pf ⇒ left _ pf
end.
We export the types, functions, lemmas, etc. provided by the
implementations of association lists whose keys are atoms (from
the AtomEnv library).
Implementation note: We specifically do not Export the AtomImpl and AtomSetImpl modules in order to avoid polluting Coq's namespace. Commonly used fields from those modules are given convenient definitions and notations, either here or in the libraries that provide those modules.
Implementation note: We specifically do not Export the AtomImpl and AtomSetImpl modules in order to avoid polluting Coq's namespace. Commonly used fields from those modules are given convenient definitions and notations, either here or in the libraries that provide those modules.
Export AtomEnvImpl.
Given the atomsetdec tactic (from the AtomSet library), we
typically do not need to refer to specific lemmas about finite
sets. However, instantiating functors from the FSets library
makes a number of setoid rewrites available. These rewrites are
crucial to developments since they allow us to replace a set with
an extensionally equal set (see the Equal relation on finite
sets) in propositions about finite sets.
Module AtomSetFacts := FSetFacts.WFacts AtomSetImpl.
Module AtomSetProperties := FSetProperties.WProperties AtomSetImpl.
Decidable equality on atoms and natural numbers may be written
using suggestive notation.
Implementation note: These notations overlap with similar ones in the Equivalence and EquivDec libraries of Coq's standard library.
Implementation note: These notations overlap with similar ones in the Equivalence and EquivDec libraries of Coq's standard library.
Notation "x == y" :=
(AtomImpl.eq_dec x y)
(at level 70)
: metatheory_scope.
Notation "i === j" :=
(Peano_dec.eq_nat_dec i j)
(at level 70)
: metatheory_scope.
We can use list-like notation to write association lists
consisting of a single binding.
Implementation note: The following notation overlaps with the standard recursive notation for lists, e.g., the one found in the Program library of Coq's standard library.
Implementation note: The following notation overlaps with the standard recursive notation for lists, e.g., the one found in the Program library of Coq's standard library.
Common set operations may be written using infix notation. The
ones for equality and subset match the notations used in the FSets
library.
Notation "E `union` F" :=
(AtomSetImpl.union E F)
(at level 65, right associativity, format "E `union` '/' F")
: set_scope.
Notation "x `in` E" :=
(AtomSetImpl.In x E)
(at level 70)
: set_scope.
Notation "x `notin` E" :=
(~ AtomSetImpl.In x E)
(at level 70)
: set_scope.
Notation "E [=] F" :=
(AtomSetImpl.Equal E F)
(at level 70, no associativity)
: set_scope.
Notation "E [<=] F" :=
(AtomSetImpl.Subset E F)
(at level 70, no associativity)
: set_scope.
We define some abbreviations for the empty set, singleton
sets, and the union of two sets.
Notation add := AtomSetImpl.add.
Notation empty := AtomSetImpl.empty.
Notation remove := AtomSetImpl.remove.
Notation singleton := AtomSetImpl.singleton.
Notation union := AtomSetImpl.union.
We define some abbreviations for some lemmas about set
non-membership.
Notation notin_add := AtomSetNotin.notin_add.
Notation notin_empty := AtomSetNotin.notin_empty.
Notation notin_remove_1 := AtomSetNotin.notin_remove_1.
Notation notin_remove_2 := AtomSetNotin.notin_remove_2.
Notation notin_remove_3 := AtomSetNotin.notin_remove_3.
Notation notin_singleton := AtomSetNotin.notin_singleton.
Notation notin_union := AtomSetNotin.notin_union.
Open the notation scopes declared above.
Open Scope metatheory_scope.
Open Scope set_scope.
Consider a rule H (equivalently, constructor, lemma, etc.) whose
type begins with ∀ L, ... and contains hypotheses of the
form (∀ y, y `notin` L → ...).
The tactic (pick fresh x excluding F and apply H) applies H to the current goal, instantiating H's first argument (L) with the finite set of atoms F. In each new subgoal of the form (∀ y, y `notin` F → ...), the atom y is introduced as x, and (y `notin` F) 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.
The tactic (pick fresh x excluding F and apply H) applies H to the current goal, instantiating H's first argument (L) with the finite set of atoms F. In each new subgoal of the form (∀ y, y `notin` F → ...), the atom y is introduced as x, and (y `notin` F) 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)
:=
first [apply (@H L) | eapply (@H L)];
match goal with
| |- ∀ _, _ `notin` _ → _ ⇒
let Fr := fresh "Fr" in intros atom_name Fr
| |- ∀ _, _ `notin` _ → _ ⇒
fail 1 "because" atom_name "is already defined"
| _ ⇒
idtac
end.
The next two blocks of hints should discharge many of the
freshness and inequality goals that arise in programming language
metatheory proofs, in particular those arising from cofinite
quantification.
Implementation note: The invocation of simpl_env is risky since autorewrite does not interact nicely with the existential variables introduced by eauto. In practice, this does not seem to be a problem. However, practice also shows that a similar problem does occurs if we use fsetdec instead of solve_notin.
Implementation note: The invocation of simpl_env is risky since autorewrite does not interact nicely with the existential variables introduced by eauto. In practice, this does not seem to be a problem. However, practice also shows that a similar problem does occurs if we use fsetdec instead of solve_notin.
Hint Resolve AtomSetNotin.notin_add.
Hint Resolve AtomSetNotin.notin_empty.
Hint Resolve AtomSetNotin.notin_remove_1.
Hint Resolve AtomSetNotin.notin_remove_2.
Hint Resolve AtomSetNotin.notin_remove_3.
Hint Resolve AtomSetNotin.notin_singleton.
Hint Resolve AtomSetNotin.notin_union.
BEA IMPLEMENTATION WARNING: In the three hints below, the
eassumption step is intended to reduce the chance that
simpl_env will trigger a rewriting bug in Coq.
Hint Extern 4 (_ `notin` _) ⇒
try eassumption; simpl_env in *; solve_notin.
Hint Extern 4 (_ ≠ _ :> atom) ⇒
try eassumption; simpl_env in *; solve_notin.
Hint Extern 4 (_ ≠ _ :> AtomSetImpl.elt) ⇒
try eassumption; simpl_env in *; solve_notin.
The following are hints for equalities on environments.
Hint Resolve cons_app_one cons_app_assoc.
Hint Resolve app_assoc app_nil_1 app_nil_2.
Hint Resolve nil_neq_one_mid one_mid_neq_nil.
Hint Resolve map_nil map_cons map_one map_app.
Hint Resolve dom_nil dom_cons dom_one dom_app dom_map.
The following hints are primarily about uniq.
Hint Resolve uniq_nil uniq_push uniq_cons uniq_one.
Hint Resolve uniq_map_2.
Hint Resolve uniq_insert_mid.
Hint Immediate uniq_remove_mid.
Hint Resolve uniq_map_app_l.
Hint Immediate fresh_mid_tail fresh_mid_head.
The following hints are primarily about binds.
Hint Resolve binds_one_1 binds_app_1 binds_app_2.
Hint Resolve binds_map binds_weaken.
Hint Immediate binds_remove_mid binds_In.
This page has been generated by coqdoc