Automation for the lattice theory #
This module registers the automation lemmas of the lattice theory with simp and grind.
A lemma gets simp and grind norm if and only if it is an unconditional equation (or Iff)
whose right side removes lattice vocabulary, moves it to a smaller carrier (pointwise application,
pair components), or moves it into the Prop argument of ⌜·⌝. Such an equation holds in every
context, including under binders, and rewriting with the whole set terminates.
grind has theories for the vocabulary of Prop and none for complete lattices. So grind also
unfolds ⊑ at function and pair carriers into Prop, although the unfolded term is larger:
le_pi_eq_forall is a grind norm lemma, and le_prod_eq_and is a grind = lemma. Neither is a
simp lemma.
grind rewrites with grind norm lemmas while it preprocesses the goal, before E-matching, and it
rewrites under binders. For example, at carrier Prop the hypothesis
h : ¬ ⨆ r, ⌜some false = some r⌝ ⊓ (r = false ∧ q)
normalizes to ¬ ∃ r, some false = some r ∧ r = false ∧ q. The body of the ∃ is in the
vocabulary of grind, so E-matching instantiates r := false from the ground term some false,
and h yields ¬ q.