Library MetatheoryAtom
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.Max.
Require Import Coq.Classes.EquivDec.
Require Import Coq.Lists.List.
Require Import Coq.Logic.DecidableTypeEx.
Require Import CoqFSetDecide.
Require Import CoqListFacts.
Require Import FSetExtra.
Require Import FSetWeakNotin.
Require Import LibTactics.
Atoms are structureless objects such that we can always generate
one fresh from a finite collection. Equality on atoms is eq and
decidable. We use Coq's module system to make abstract the
implementation of atoms.
Module Type ATOM.
Parameter atom : Set.
Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}.
Parameter atom_fresh_for_list :
forall (xs : list atom), {x : atom | ~ List.In x xs}.
Hint Resolve eq_atom_dec.
End ATOM.
The implementation of the above interface is hidden for
documentation purposes.
We make atom, eq_atom_dec, and atom_fresh_for_list available
without qualification.
Export AtomImpl.
It is trivial to implement the DecidableType interface with atom.
Module AtomDT <: UsualDecidableType with Definition t := atom.
Definition t := atom.
Definition eq := @eq t.
Definition eq_refl := @refl_equal t.
Definition eq_sym := @sym_eq t.
Definition eq_trans := @trans_eq t.
Definition eq_dec := eq_atom_dec.
End AtomDT.
It is trivial to declare an instance of EqDec for atom.
We use our implementation of atoms to obtain an implementation of
finite sets of atoms. We give the resulting type an intuitive
name, as well as import names of set operations for use within
this library. In order to avoid polluting Coq's namespace, we do
not use Module Export.
Module Import AtomSetImpl : FSetExtra.WSfun AtomDT :=
FSetExtra.Make AtomDT.
Notation atoms :=
AtomSetImpl.t.
The AtomSetDecide module provides the fsetdec tactic for
solving facts about finite sets of atoms.
The AtomSetNotin module provides the destruct_notin and
solve_notin for reasoning about non-membership in finite sets of
atoms, as well as a variety of lemmas about non-membership.
Given the fsetdec tactic, we typically do not need to refer to
specific lemmas about finite sets. However, instantiating
functors from the FSets library makes a number of setoid rewrites
available. These rewrites are crucial to developments since they
allow us to replace a set with an extensionally equal set (see the
Equal relation on finite sets) in propositions about finite
sets.
Module AtomSetFacts := FSetFacts.WFacts_fun AtomDT AtomSetImpl.
Module AtomSetProperties := FSetProperties.WProperties_fun AtomDT AtomSetImpl.
For any given finite set of atoms, we can generate an atom fresh
for it.
gather_atoms_with F returns the union of all the finite sets
F x where x is a variable from the context such that F x
type checks.
Ltac gather_atoms_with F :=
let apply_arg x :=
match type of F with
| _ -> _ -> _ -> _ => constr:(@F _ _ x)
| _ -> _ -> _ => constr:(@F _ x)
| _ -> _ => constr:(@F x)
end in
let rec gather V :=
match goal with
| H : _ |- _ =>
let FH := apply_arg H in
match V with
| context [FH] => fail 1
| _ => gather (union FH V)
end
| _ => V
end in
let L := gather empty in eval simpl in L.
beautify_fset V assumes that V is built as a union of finite
sets and returns the same set cleaned up: empty sets are removed
and items are laid out in a nicely parenthesized way.
Ltac beautify_fset V :=
let rec go Acc E :=
match E with
| union ?E1 ?E2 => let Acc2 := go Acc E2 in go Acc2 E1
| empty => Acc
| ?E1 => match Acc with
| empty => E1
| _ => constr:(union E1 Acc)
end
end
in go empty V.
The tactic pick fresh Y for L takes a finite set of atoms L
and a fresh name Y, and adds to the context an atom with name
Y and a proof that ~ In Y L, i.e., that Y is fresh for L.
The tactic will fail if Y is already declared in the context.
The variant pick fresh Y is similar, except that Y is fresh for "all atoms in the context." This version depends on the tactic gather_atoms, which is responsible for returning the set of "all atoms in the context." By default, it returns the empty set, but users are free (and expected) to redefine it.
The variant pick fresh Y is similar, except that Y is fresh for "all atoms in the context." This version depends on the tactic gather_atoms, which is responsible for returning the set of "all atoms in the context." By default, it returns the empty set, but users are free (and expected) to redefine it.
Ltac gather_atoms :=
constr:empty.
Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
let Fr := fresh "Fr" in
let L := beautify_fset L in
(destruct (atom_fresh L) as [Y Fr]).
Tactic Notation "pick" "fresh" ident(Y) :=
let L := gather_atoms in
pick fresh Y for L.
Ltac pick_fresh y :=
pick fresh y.
Example: We can redefine gather_atoms to return all the
"obvious" atoms in the context using the gather_atoms_with thus
giving us a "useful" version of the "pick fresh" tactic.
Ltac gather_atoms ::=
let A := gather_atoms_with (fun x : atoms => x) in
let B := gather_atoms_with (fun x : atom => singleton x) in
constr:(union A B).
Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3: atoms), True.
Proof.
intros x y z L1 L2 L3.
pick fresh k.
At this point in the proof, we have a new atom k and a
hypothesis Fr that k is fresh for x, y, z, L1, L2,
and L3.
trivial.
Qed.
This page has been generated by coqdoc