# Library Metatheory

Require Export Coq.Arith.Arith.

Require Export Coq.FSets.FSets.

Require Export Coq.Lists.List.

Require Export AssocList.

Require Export CoqEqDec.

Require Export CoqListFacts.

Require Export LibTactics.

Require Export MetatheoryAtom.

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.

We can use our implementation of association lists (in AssocList)
to implement association lists whose keys are atoms. Thanks to
parameter inlining, the types in the instantiated functor will all
use atom for the type for keys.

We provide alternative names for the tactics on association lists
to reflect our use of association lists for environments.

Ltac simpl_env :=

simpl_alist.

Tactic Notation "simpl_env" "in" hyp(H) :=

simpl_alist in H.

Tactic Notation "simpl_env" "in" "*" :=

simpl_alist in *.

Tactic Notation "rewrite_env" constr(E) :=

rewrite_alist E.

Tactic Notation "rewrite_env" constr(E) "in" hyp(H) :=

rewrite_alist E in H.

Tactic Notation "env" "induction" ident(E) :=

alist induction E.

Tactic Notation "env" "induction" ident(E) "as" simple_intropattern(P) :=

alist induction E as P.

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.

Implementation note (BEA): The eassumption step is intended to address those cases where eauto tries to use a cofinite rule. The pattern goes something like this:

This ensures that the autorewrite step does not trigger an infinite loop.

Implementation note (BEA): The eassumption step is intended to address those cases where eauto tries to use a cofinite rule. The pattern goes something like this:

- Apply a cofinite rule with no idea what "L" should be. This adds a hypothesis x `notin` ?1 to the context.
- Apply the IH.
- eassumption resolves the x `notin` L obligation of the IH against the previously introduced x `notin` ?1 hypothesis.

This ensures that the autorewrite step does not trigger an infinite loop.

Ltac hint_extern_solve_notin :=

try eassumption;

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.

This page has been generated by coqdoc