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 "{}" :=
  : 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.


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"
        | _ =>

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

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 :=

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