# 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.

# Decidable equality

We prefer that "==" refer to decidable equality at eq, as defined by the EqDec_eq class from the CoqEqDec library.

Notation " x == y " := (eq_dec x y) (at level 70) : coqeqdec_scope.

Open Scope coqeqdec_scope.

# Notations for finite sets of atoms

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.
Open the notation scopes declared above.

Open Scope set_scope.
Open Scope set_hs_scope.

# Environments

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.

# Cofinite quantification

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.

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.

# Lemma aliases

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_singleton := notin_singleton_2.
Notation notin_union := notin_union_3.

# Hints

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_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.

# Ott compatibility

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.