Library MetatheoryAlt
Require Export Coq.Arith.Arith.
Require Export Coq.FSets.FSets.
Require Export Coq.Lists.List.
Require Export CoqEqDec.
Require Export CoqListFacts.
Require Export LibTactics.
Require Export MetatheoryAtom.
Require Export AssumeList.
We prefer that "==" refer to decidable equality at eq, as
defined by the EqDec_eq class from the CoqEqDec library.
Common set operations and constants may be written using more
convenient notations.
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.
Notation "{}" :=
(AtomSetImpl.empty)
: set_scope.
Notation "{{ x }}" :=
(AtomSetImpl.singleton x)
: set_scope.
Notation "x `in` E" :=
(AtomSetImpl.In x E)
(at level 70)
: set_hs_scope.
Notation "x `notin` E" :=
(~ AtomSetImpl.In x E)
(at level 70)
: set_hs_scope.
Notation "E `union` F" :=
(AtomSetImpl.union E F)
(at level 65, right associativity, format "E `union` '/' F")
: set_hs_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.
Open the notation scopes declared above.
Open Scope set_scope.
Open Scope set_hs_scope.
As an alternative to the x ~ a notation, we also provide more
list-like notation for writing 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.
Consider a rule H (equivalently, constructor, lemma, etc.) whose
type begins with forall L, ... and contains hypotheses of the
form (forall 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 (forall 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 (forall 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
| |- forall _, _ `notin` _ -> _ =>
let Fr := fresh "Fr" in intros atom_name Fr
| |- forall _, _ `notin` _ -> _ =>
fail 1 "because" atom_name "is already defined"
| _ =>
idtac
end.
The following variant of the tactic excludes the set of atoms
returned by the gather_atoms tactic. Redefine gather_atoms if
you wish to modify the behavior of this tactic.
Tactic Notation
"pick" "fresh" ident(atom_name)
"and" "apply" constr(H)
:=
let L := gather_atoms in
let L := beautify_fset L in
pick fresh atom_name excluding L and apply H.
A number of useful lemmas are given standardized, if somewhat
unintuitive, names. Here, we define some intuitive aliases for
them.
Notation uniq_one := uniq_one_1.
Notation uniq_cons := uniq_cons_3.
Notation uniq_app := uniq_app_4.
Notation uniq_map := uniq_map_2.
Notation binds_one := binds_one_3.
Notation binds_cons := binds_cons_3.
Notation binds_app_l := binds_app_2.
Notation binds_app_r := binds_app_3.
Notation binds_map := binds_map_2.
Notation notin_empty := notin_empty_1.
Notation notin_add := notin_add_3.
Notation notin_singleton := notin_singleton_2.
Notation notin_union := notin_union_3.
The next block of hints is to help auto discharge many of the
inequality and freshness goals that arise in programming language
metatheory proofs.
Ltac hint_extern_solve_notin :=
autorewrite with rewr_dom in *;
destruct_notin;
repeat first [ apply notin_union_3
| apply notin_add_3
| apply notin_singleton_2
| apply notin_empty_1
];
try tauto.
Hint Extern 1 (_ <> _ :> _) => hint_extern_solve_notin.
Hint Extern 1 (_ `notin` _) => hint_extern_solve_notin.
The next block of hints are occasionally useful when reasoning
about finite sets. In some instances, they obviate the need to
use auto with set.
Hint Resolve
AtomSetImpl.add_1 AtomSetImpl.add_2 AtomSetImpl.remove_1
AtomSetImpl.remove_2 AtomSetImpl.singleton_2 AtomSetImpl.union_2
AtomSetImpl.union_3 AtomSetImpl.inter_3 AtomSetImpl.diff_3.
Implementation note (BEA): The following definitions make this
library usable with the output of Ott's locally nameless backend.
They may disappear or change as Ott changes.
Notation var := atom (only parsing).
Notation vars := atoms (only parsing).
Notation eq_var := eq_dec (only parsing).
Notation "x === y" :=
(x == y)
(at level 70, only parsing)
: coqeqdec_scope.
Notation "x \in s" :=
(x `in` s)
(at level 70, only parsing)
: set_sl_scope.
Notation "x \notin s" :=
(x `notin` s)
(at level 70, only parsing)
: set_sl_scope.
Notation "s \u t" :=
(s `union` t)
(at level 65, right associativity, only parsing)
: set_sl_scope.
Open Scope set_sl_scope.
Ltac gather_vars_with F := gather_atoms_with.
Ltac pick_fresh_gen L Y := pick fresh Y for L.
Tactic Notation "auto" "*" := auto.
Ltac apply_fresh_base H gather_vars atom_name :=
let L := gather_vars in
let L := beautify_fset L in
pick fresh x excluding L and apply H.
Definition env (A : Type) := list (atom * A).
We provide alternative names for tactics on association lists.
Ltac simpl_env :=
simpl_asnlist.
Tactic Notation "simpl_env" "in" hyp(H) :=
simpl_asnlist in H.
Tactic Notation "simpl_env" "in" "*" :=
simpl_asnlist in *.
Tactic Notation "rewrite_env" constr(E) :=
rewrite_asnlist E.
Tactic Notation "rewrite_env" constr(E) "in" hyp(H) :=
rewrite_asnlist E in H.
This page has been generated by coqdoc