Algebraic Metas

The source code for this module: PartI/MetasAlgebra.ard
The source code for the exercises: PartI/MetasAlgebraEx.ard

In Standard Metas for Equality we introduced metas for in-the-goal rewriting and chaining (rewrite, run, in, at). In Records and Classes we saw linarith, a meta that uses class instances to discharge linear arithmetic goals. This chapter introduces three more metas of the same flavor — simplify, equation, cong — plus the universal extensionality meta ext.

These metas all live in Algebra.Meta and Paths.Meta:

\import Algebra.Meta  -- equation, cong, linarith, simplify
\import Paths.Meta    -- ext, simp_coe

simplify: algebraic normalization

simplify normalizes monoid/group/ring/lattice expressions: it strips identity elements, eliminates double inverses and double negations, and collapses x * 0-style patterns. The meta inspects the algebraic class instance in scope and applies the laws guaranteed by that class.

\lemma simp-1 {M : Monoid} (x : M) : x = x * ide
  => simplify

\lemma simp-2 {M : Monoid} (x : M) : x * x = (x * (ide * x)) * ide
  => simplify

\lemma simp-3 {R : Ring} (x : R) : negative (negative x) = x
  => simplify

\lemma simp-4 {R : Semiring} (x : R) : zro = x * zro
  => simplify

simplify is not a full decision procedure. It does not, for example, know about commutativity (without it, x * y = y * x is genuinely unprovable — an axiom is needed) or about distributing multiplication over a sum. Use it as a first-pass normalizer, then reach for equation or rewrite for the structural rewriting it cannot perform.

The in-form of simplify normalizes a hypothesis instead of the goal:

\lemma simp-hyp {M : Monoid} (x y : M) (h : x * (ide * y) = ide) : x * y = ide
  => simplify in h

equation: chained equality, with implicit step proofs

equation a_1 ... a_n proves a goal of shape a_0 = a_{n+1} by treating a_1, ..., a_n as intermediate steps. For each adjacent pair, the meta tries to fill in the proof from local hypotheses; if it cannot, you supply that step explicitly as an implicit argument.

\lemma eq-test {M : Monoid} (x y z : M) (p : x = y) (q : y = z) : x = z
  => equation x y z

This is the meta-driven counterpart of the ==< / >== / qed chain from Proofs of Equality. The two coexist: prefer equation when the step proofs are uninteresting (or come from simplify-style normalization); prefer the explicit chain when each step has a name worth showing in the proof body.

cong: congruence closure

cong proves a goal f x_1 ... x_n = f y_1 ... y_n from contextual equalities x_i = y_i. It runs the congruence closure algorithm — a multi-argument generalization of pmap.

\lemma cong-test {A B : \Type} (f : A -> A -> B)
                 (x x' y y' : A) (p : x = x') (q : y = y')
               : f x y = f x' y'
  => cong

The hand-written equivalent would chain pmap, pmap2, or several rewrite steps; cong compresses all of them.

ext: extensionality, polymorphic over the equality’s type

ext discharges goals a = a' where the two sides have a structural form: a function, a Σ-tuple, a record, a proposition, or a type. Each form yields a different subgoal:

• On f = g for f, g : \Pi (x : A) -> B x: subgoal is pointwise equality \Pi (x : A) -> f x = g x (function extensionality).
• On t = s for \Sigma (x : A) (y : B x): subgoal is a Σ of componentwise equalities, with appropriate coe-corrections for the dependent components.
• On t = s for a record: same as the Σ case, with the option of copattern syntax ext R { | f_1 => p_1 | ... }.
• On A = B for A, B : \Prop: subgoal is \Sigma (A -> B) (B -> A) (propositional extensionality, provable in Arend).
• On A = B for A, B : \Type: subgoal is Equiv {A} {B} (univalence).
• On x = y for P : \Prop: no subgoal — the meta closes the goal because all elements of a \Prop are equal.

Examples:

\lemma ext-fun (f g : Nat -> Nat) (h : \Pi (n : Nat) -> f n = g n) : f = g
  => ext h

\lemma ext-sigma (p p' : \Sigma Nat Nat) (h1 : p.1 = p'.1) (h2 : p.2 = p'.2)
              : p = p'
  => ext (h1, h2)

\lemma ext-prop (A B : \Prop) (f : A -> B) (g : B -> A) : A = B
  => ext (f, g)

The full grammar for ext (including the record copattern form and dependent-Σ corrections) is documented at Paths metas / ext.

simp_coe (advanced)

When proofs accumulate coe/transport over Π-, Σ-, or record-types, simp_coe pushes them through the structure. It is most useful when working with higher inductive types in Part II; we mention it here only for completeness. See Paths metas / simp_coe for details.

Exercises

Exercise 1: Prove the following one-liners with simplify: (a) {M : Monoid} (x : M) : x = x * ide, (b) {R : Ring} (x : R) : negative (negative x) = x, (c) {R : Semiring} (x : R) : zro = x * zro.

Exercise 2: Find a goal that simplify cannot solve and explain why. Hint: try a goal that requires commutativity.

Exercise 3: Prove {A : \Type} (f : A -> A -> A -> A) (x x' y y' z z' : A) (p : x = x') (q : y = y') (r : z = z') : f x y z = f x' y' z' with one cong. Then write the equivalent proof using pmap/pmap2/manual rewriting and compare line counts.

Exercise 4: Prove (\lam (x : Nat) => x Nat.+ 0) = (\lam x => x) using ext.

Exercise 5: Define a 3-field \record R and prove that two values of R are equal whenever each pair of components is equal, using the copattern form ext R { | f_1 => p_1 | ... }.

Exercise 6: Prove \Pi (A B : \Prop) -> (A -> B) -> (B -> A) -> A = B using ext.