Standard Metas for Equality

The source code for this module: PartI/MetasEquality.ard
The source code for the exercises: PartI/MetasEqualityEx.ard

Up to this point, equality proofs were assembled from the kernel primitives idp, pmap, transport, inv, and *>. As proofs grow these primitives become tedious to thread by hand. The Arend standard library ships metas — macros that expand into ordinary kernel terms post-elaboration. They are not a separate logic; they are surface syntax for the same transport/pmap machinery the previous chapters introduced.

In this chapter we introduce the metas most useful for equality proofs: rewrite, rewriteI, run, in, and at. We also cover the language features rewrite relies on: partial application of functions and infix sections. The full reference for each meta lives at Standard Metas.

Metas are organized into several modules. Throughout this chapter we will assume the following imports:

\import Paths        -- inv, *>, transport, transportInv, idp, pmap
\import Paths.Meta   -- rewrite, rewriteI, ext, simp_coe, simplify
\import Meta         -- run, in, at, cases, mcases, unfold, ...
\import Function.Meta -- $, #, repeat

rewrite

rewrite p t, where p : a = b, looks at the expected type, replaces every occurrence of a with b, and uses t as a proof of the rewritten type. It is exactly sugar for transportInv:

-- These two definitions are equivalent:
\func test (n m : Nat) (p : n = m) (q : m = 0) : n = 0
  => rewrite p q

\func test' (n m : Nat) (p : n = m) (q : m = 0) : n = 0
  => transportInv (\lam x => x = 0) p q

The companion meta rewriteI p is shorthand for rewrite (inv p): it rewrites in the opposite direction. Use rewriteI when the equation you have is “wrong-way-round” relative to the goal.

\func test1 (a : Nat) (p : a = 0) : a Nat.+ a = 0
  => rewrite p idp

\func test2 (a : Nat) (p : 0 = a) : a Nat.+ a = 0
  => rewriteI p idp

The associativity of + from Indexed Data Types compresses noticeably with rewrite:

\open Nat(+)

\lemma +-assoc (a b c : Nat) : a + b + c = a + (b + c) \elim c
  | 0 => idp
  | suc c => rewrite (+-assoc a b c) idp

The seed idp proves the goal after the rewrite has been applied; once both sides have been normalized to the same shape, reflexivity finishes the proof.

Selective occurrences

When the LHS appears multiple times in the goal, rewriting all occurrences is sometimes wrong. rewrite {n_1, n_2, ...} p t rewrites only the listed occurrences (counting in left-to-right order, after each replacement). For example:

\func test {x : Nat} (p : suc x = suc (suc x))
         : suc (suc x) = x Nat.+ 3
  => rewrite {1} p idp

Here suc x appears multiple times in the goal after normalization; without {1} the rewrite would chase its own tail.

Partial application and infix sections

Arend allows partial application of any function or infix operator. Two forms appear constantly in proofs assembled with metas:

• pmap suc is a value of type {a a' : Nat} -> a = a' -> suc a = suc a' — a unary function that consumes a path. Perfectly usable as a building block.
• For infix operators like *>, the expressions (p *>) and (`*> q) are sections: the former precomposes with p on the left, the latter composes with q on the right. Each is a unary function on paths.
• __ (double underscore) is the explicit anonymous-section placeholder: __ + 1, f __ x, etc.

\func ex-pmap (n m : Nat) (p : n = m) : suc n = suc m
  => pmap suc p

\func ex-section-left (a b c : Nat) (p : a = b) (q : b = c) : a = c
  => (p *>) q   -- equivalent to p *> q

\func ex-double-underscore : Nat -> Nat
  => __ Nat.+ 1

These are language features, not meta features — but they are what makes the next section’s run-blocks readable.

run for chaining

Nested rewrite calls grow ugly:

-- Hard to scan:
rewrite p (rewrite q (rewrite r idp))

The run meta lets you write the same chain top-to-bottom as a comma-separated list:

\func ex-run {A : \Type} (a b c d : A) (p : a = b) (q : b = c) (r : c = d) : a = d
  => run {
    rewrite p,
    rewrite q,
    rewrite r,
    idp
  }

The semantics: run { f_1, f_2, ..., f_n, t } expands to f_1 (f_2 (... (f_n t))). The last entry is the seed (the innermost proof); each entry above is a unary function applied to the chain so far.

A run-block can mix rewrite, pmap f, infix sections like p *>, and any other unary function on proofs. For occasional advanced uses, run also accepts entries of the form \let | x => e \in {} or \lam x => {} (with empty bodies); these wrap the rest of the chain in a let-binding or a lambda respectively.

rewrite itself also accepts a tuple of paths in place of a single path: rewrite (p_1, p_2, ..., p_n) t is equivalent to rewrite p_1 (rewrite p_2 (... (rewrite p_n t))). Each p_i is applied in left-to-right order, with the previous rewrites already reflected in the goal by the time the next one runs. This is a more compact alternative to run when every step is itself a rewrite:

\func ex-rewrite-tuple {A : \Type} (a b c d : A) (p : a = b) (q : b = c) (r : c = d) : a = d
  => rewrite (p, q, r) idp

Reach for run when the chain mixes different metas; reach for the tuple form when it is purely rewrites.

in: applying a meta to a value

f in x runs f x but with one important subtlety: it discards the surrounding expected type. Internally, in elaborates to \let r => f x \in r, and that \let is typechecked without the goal’s type information flowing in.

For most metas this difference is invisible. For rewrite, which inspects the expected type to decide what to rewrite, the difference is observable:

-- Direct application uses the expected type:
\func test1 (x y : Nat) (p : x = zero) (q : zero = y) : x = y
  => rewrite p q   -- rewrites x → zero in the goal x = y, giving zero = y; matches q

-- `in` uses t's type instead:
\func test2 (x y : Nat) (p : zero = x) (q : zero = y) : x = y
  => rewrite p in q   -- rewrites zero → x in q's type zero = y, giving x = y

Use f in x when you want the meta to operate on the value’s type rather than the goal — for example, when there is no annotated result type, or when you want a “rewrite in the hypothesis itself” effect on the seed.

in chains: (f_1, f_2, ..., f_n) in x ≡ f_1 (f_2 (... (f_n x))). Each step runs without an expected type.

in has loose precedence (priority 1, right-associative). To apply the result of f in x to further arguments, parens are required:

(simp_coe in t) b      -- applies simp_coe in t, then applies result to b
-- simp_coe in t b     -- parses as simp_coe in (t b) — different proof

at: modifying a hypothesis

f at h shadows the local binding h with f h for the rest of the expression — Arend’s analogue of “rewrite in a hypothesis.” It is the right tool when a hypothesis needs reshaping before it can be used.

There are three equivalent surface forms:

\func test1 (x : Nat) (p : x = zero) (q : x = suc zero) : Empty
  => (rewrite p at q) (\case q \with {})

\func test2 (x : Nat) (p : x = zero) (q : x = suc zero) : Empty
  => rewrite p at q $ \case q \with {}

\func test3 (x : Nat) (p : x = zero) (q : x = suc zero) : Empty
  => run {
    rewrite p at q,
    \case q \with {}
  }

After rewrite p at q, the local q has type zero = suc zero instead of x = suc zero. The empty \case then derives Empty from the constructor disjointness of zero and suc zero.

Like in, at accepts a tuple-chaining form:

\func test {x y : Nat} (p1 : x = zero) (p2 : y = suc zero) (q : x = y) : Empty
  => (rewrite p1, rewrite p2) at q $ \case q \with {}

at works on any local binding — function parameters, \let-bindings, and \have-bindings.

When to use what

Situation	Use
Rewrite in the goal	rewrite p t
Rewrite the goal in the opposite direction	rewriteI p t
Rewrite when expected type is unknown / use t’s type	rewrite p in t
Modify a hypothesis	rewrite p at h $ ...
Chain several rewrites	run { rewrite p, rewrite q, ..., idp }
Multi-step chain with named intermediate values	==< / >== / qed, see Proofs of Equality

Exercises

Exercise 1: Reprove +-comm from Proofs of Equality using only rewrite, rewriteI, and idp — no pmap, no *>, no equational reasoning. Compare the line count.

Exercise 2: Predict which of the following typecheck and explain why. Then run them to verify.

\func test1 (x y : Nat) (p : x = zero) (q : zero = y) : x = y => rewrite p q
\func test2 (x y : Nat) (p : x = zero) (q : zero = y) : x = y => rewrite p in q
\func test3 (x y : Nat) (p : zero = x) (q : zero = y) : x = y => rewrite p q
\func test4 (x y : Nat) (p : zero = x) (q : zero = y) : x = y => rewrite p in q

Exercise 3: State a lemma where rewrite would replace too many occurrences. Use occurrence selection rewrite {n} p t to make the proof go through.

Exercise 4: Take the proof of reverse-isInvolutive from Indexed Data Types (which uses rev-isInv and *>-chains in similar style) and rewrite its body as a single run-block.

Exercise 5: Given (x : Nat) (p : x = 0) (q : x = 1), prove Empty. Write three solutions: (a) using at, (b) introducing a fresh binding via \have, (c) chaining *>-style with inv.

Exercise 6: Use pmap suc at p to convert a hypothesis p : x = 0 into p : suc x = 1, then use it to discharge a goal suc x = 1.