Library Metatheory

Library for programming languages metatheory.

Authors: Brian Aydemir and Arthur Charguéraud, with help from Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic.





Require Export AdditionalTactics.

Require Export Atom.

Require Export Environment.

Notations

Decidable equality on atoms and natural numbers may be written using natural notation.





Notation "x == y" :=

  (eq_atom_dec x y) (at level 67) : metatheory_scope.

Notation "i === j" :=

  (Peano_dec.eq_nat_dec i j) (at level 67) : metatheory_scope.

Common set operations may be written using infix notation.





Notation "E `union` F" :=

  (AtomSet.F.union E F)

  (at level 69, right associativity, format "E  `union`  '/' F")

  : set_scope.

Notation "x `in` E" :=

  (AtomSet.F.In x E) (at level 69) : set_scope.

Notation "x `notin` E" :=

  (~ AtomSet.F.In x E) (at level 69) : set_scope.

The empty set may be written similarly to informal practice.





Notation "{}" :=

  (AtomSet.F.empty) : metatheory_scope.

It is useful to have an abbreviation for constructing singleton sets.





Notation singleton := (AtomSet.F.singleton).

Open the notation scopes declared above.





Open Scope metatheory_scope.

Open Scope set_scope.

Tactic for working with cofinite quantification

Consider a rule H (equivalently, hypothesis, constructor, lemma, etc.) of the form

(forall L ..., ... -> (forall y, y `notin` L ->
    P) -> ... -> Q)

, where Q's outermost constructor is not a forall. There may be multiple hypotheses of with the indicated form in H.

The tactic (pick fresh x and apply H) applies H to the current goal, instantiating H's first argument (i.e., L) with the finite set of atoms L'. In each new subgoal arising from a hypothesis of the form (forall y, y `notin` L -> P), the atom y is introduced as x, and (y `notin` L) 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) :=

  let L := beautify_fset L in

    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.

Automation

These hints should discharge many of the freshness and inequality goals that arise in programming language metatheory proofs, in particular those arising from cofinite quantification.





Hint Resolve notin_empty notin_singleton notin_union.

Hint Extern 4 (_ `notin` _) => simpl_env; notin_solve.

Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve.