Sorting term lists by the verified total order

canon sorts the leaves of an AC operator using the LinearOrder AST from MeTTaILProofs.Order. The only facts we need about the sort are that it permutes its input, that its output is sorted, and the consequence that permutation-equal inputs sort to the same list (sorted permutations are unique).

def MeTTaIL.AC.sortMS (xs : List AST) : List AST

Sort a list of terms by the verified total order on AST.

Equations

• MeTTaIL.AC.sortMS xs = xs.mergeSort fun (x1 x2 : MeTTaIL.AST) => decide (x1 ≤ x2)

theorem MeTTaIL.AC.sortMS_perm (xs : List AST) : (sortMS xs).Perm xs

The sort is a permutation of its input.

theorem MeTTaIL.AC.sortMS_sortedLE (xs : List AST) : (sortMS xs).SortedLE

The sort produces a ≤-sorted list.

theorem MeTTaIL.AC.sortMS_perm_eq {xs ys : List AST} (h : xs.Perm ys) : sortMS xs = sortMS ys

Permutation-equal lists sort to the same list. This is the heart of completeness: it turns "same multiset of leaves" into "syntactically identical canonical form", using that two sorted permutations of each other are equal.

theorem MeTTaIL.AC.sortMS_mem {x : AST} {xs : List AST} (h : x ∈ sortMS xs) : x ∈ xs

Membership is preserved by the sort.

theorem MeTTaIL.AC.sortMS_ne_nil {xs : List AST} (h : xs ≠ []) : sortMS xs ≠ []

Sorting a nonempty list yields a nonempty list.

Flatten and rebuild for a single AC label

flat l t collects the leaves of the binary l-tree at the root of t: it descends through nodes (l a b) and stops at anything that is not such a node. rebuild l xs turns a leaf list back into a right-nested l-tree. These are the two halves of the canonical form for one associative-commutative label l. flat does not recurse with canon, so it is plain structural recursion on the term.

def MeTTaIL.AC.flat (l : Label) : AST → List AST

The leaves of the binary l-tree at the root of a term. Descends through (l a b) nodes; every other shape (including the same label at a different arity) is an opaque leaf.

Equations

• MeTTaIL.AC.flat l (MeTTaIL.AST.sexp m [a, b]) = if l = m then MeTTaIL.AC.flat l a ++ MeTTaIL.AC.flat l b else [MeTTaIL.AST.sexp m [a, b]]
• MeTTaIL.AC.flat l (MeTTaIL.AST.var p) = [MeTTaIL.AST.var p]
• MeTTaIL.AC.flat l (b.subst r v) = [b.subst r v]
• MeTTaIL.AC.flat l (MeTTaIL.AST.sexp m args) = [MeTTaIL.AST.sexp m args]

def MeTTaIL.AC.rebuild (l : Label) : List AST → AST

Rebuild a leaf list into a right-nested l-tree. A single leaf rebuilds to itself; the empty list is a degenerate case that never arises from flat (which is always nonempty).

Equations

• MeTTaIL.AC.rebuild l [] = MeTTaIL.AST.sexp l []
• MeTTaIL.AC.rebuild l [x_1] = x_1
• MeTTaIL.AC.rebuild l (x_1 :: xs) = MeTTaIL.AST.sexp l [x_1, MeTTaIL.AC.rebuild l xs]

theorem MeTTaIL.AC.rebuild_singleton (l : Label) (x : AST) : rebuild l [x] = x

A one-element rebuild is the element itself.

theorem MeTTaIL.AC.rebuild_cons {l : Label} {x : AST} {w : List AST} (hw : w ≠ []) : rebuild l (x :: w) = AST.sexp l [x, rebuild l w]

Rebuilding a cons with a nonempty tail peels off the head as a binary node.

theorem MeTTaIL.AC.rebuild_cons2 (l : Label) (x y : AST) (w : List AST) : rebuild l (x :: y :: w) = AST.sexp l [x, rebuild l (y :: w)]

Rebuilding a list of at least two elements.

theorem MeTTaIL.AC.rebuild_pair (l : Label) (x y : AST) : rebuild l [x, y] = AST.sexp l [x, y]

Rebuilding a two-element list is the binary node.

theorem MeTTaIL.AC.flat_node (l : Label) (a b : AST) : flat l (AST.sexp l [a, b]) = flat l a ++ flat l b

Flattening an l-headed binary node splits into the two subtrees' leaves.

theorem MeTTaIL.AC.flat_other (l m : Label) {args : List AST} (h : ∀ (a b : AST), args = [a, b] → False) : flat l (AST.sexp m args) = [AST.sexp m args]

Flattening anything that is not an l-headed binary node returns the node as a single leaf.

theorem MeTTaIL.AC.flat_node_ne {l m : Label} (hlm : ¬l = m) (a b : AST) : flat l (AST.sexp m [a, b]) = [AST.sexp m [a, b]]

Flattening a binary node whose label is not l leaves it as a single leaf.

theorem MeTTaIL.AC.flat_ne_nil (l : Label) (t : AST) : flat l t ≠ []

flat never returns the empty list.

theorem MeTTaIL.AC.flat_flat (l : Label) (t x : AST) : x ∈ flat l t → flat l x = [x]

Every leaf produced by flat is itself l-flat: flattening it again returns just itself. This is what makes the canonical form stable, and it drives flat_rebuild_inv below.

theorem MeTTaIL.AC.flat_rebuild_inv {l : Label} {L : List AST} : (∀ x ∈ L, flat l x = [x]) → L ≠ [] → flat l (rebuild l L) = L

Rebuilding an l-flat, nonempty leaf list and flattening it again returns the same list. The leaf list produced inside canon is exactly such a list, so flattening a canonical AC subterm recovers its sorted leaves.

theorem MeTTaIL.AC.flat_canon_node {l : Label} (a b : AST) : flat l (rebuild l (sortMS (flat l a ++ flat l b))) = sortMS (flat l a ++ flat l b)

Flattening a canonicalized AC node recovers its sorted leaf list.

The AC congruence

ACEq acOp is the smallest congruence on terms generated by commutativity and associativity of the binary applications (l a b) whose label l is flagged acOp l = true. The generators (comm, assoc) fire only on binary nodes, matching a binary-curried operator like rho's |; a flagged label at another arity is inert. The congruence rules (argCong, substCongB, substCongR) close it under all term contexts; refl, symm, trans make it an equivalence.

inductive MeTTaIL.AC.ACEq (acOp : Label → Bool) : AST → AST → Prop

AC-equivalence: the congruence generated by commutativity and associativity of the binary applications of the acOp-flagged labels.

• refl {acOp : Label → Bool} (t : AST) : ACEq acOp t t
• symm {acOp : Label → Bool} {s t : AST} : ACEq acOp s t → ACEq acOp t s
• trans {acOp : Label → Bool} {s t u : AST} : ACEq acOp s t → ACEq acOp t u → ACEq acOp s u
• comm {acOp : Label → Bool} {l : Label} {a b : AST} : acOp l = true → ACEq acOp (AST.sexp l [a, b]) (AST.sexp l [b, a])
• assoc {acOp : Label → Bool} {l : Label} {a b c : AST} : acOp l = true → ACEq acOp (AST.sexp l [AST.sexp l [a, b], c]) (AST.sexp l [a, AST.sexp l [b, c]])
• argCong {acOp : Label → Bool} {l : Label} (pre : List AST) {a a' : AST} (post : List AST) : ACEq acOp a a' → ACEq acOp (AST.sexp l (pre ++ a :: post)) (AST.sexp l (pre ++ a' :: post))
• substCongB {acOp : Label → Bool} {b b' r : AST} {v : DottedPath} : ACEq acOp b b' → ACEq acOp (b.subst r v) (b'.subst r v)
• substCongR {acOp : Label → Bool} {b r r' : AST} {v : DottedPath} : ACEq acOp r r' → ACEq acOp (b.subst r v) (b.subst r' v)

theorem MeTTaIL.AC.ACEq.sexpCongr (acOp : Label → Bool) {l : Label} {cs ds : List AST} (h : List.Forall₂ (ACEq acOp) cs ds) : ACEq acOp (AST.sexp l cs) (AST.sexp l ds)

Congruence of sexp under a pointwise AC-equivalence of arguments, built by chaining single-position argCong steps across the list.

theorem MeTTaIL.AC.ACEq.sexp2_fst (acOp : Label → Bool) {l : Label} {a a' b : AST} (h : ACEq acOp a a') : ACEq acOp (AST.sexp l [a, b]) (AST.sexp l [a', b])

Congruence in the first argument of a binary node.

theorem MeTTaIL.AC.ACEq.sexp2_snd (acOp : Label → Bool) {l : Label} {a b b' : AST} (h : ACEq acOp b b') : ACEq acOp (AST.sexp l [a, b]) (AST.sexp l [a, b'])

Congruence in the second argument of a binary node.

theorem MeTTaIL.AC.ACEq.sexp2 (acOp : Label → Bool) {l : Label} {a a' b b' : AST} (ha : ACEq acOp a a') (hb : ACEq acOp b b') : ACEq acOp (AST.sexp l [a, b]) (AST.sexp l [a', b'])

Congruence of a binary node in both arguments.

Soundness lemmas: flatten, rebuild, and sort preserve AC-equivalence

theorem MeTTaIL.AC.rebuild_append (acOp : Label → Bool) {l : Label} (hac : acOp l = true) {ys : List AST} (hys : ys ≠ []) {xs : List AST} : xs ≠ [] → ACEq acOp (rebuild l (xs ++ ys)) (AST.sexp l [rebuild l xs, rebuild l ys])

Combining two rebuilt leaf lists with the binary operator is AC-equivalent to rebuilding their concatenation. This is associativity in action.

theorem MeTTaIL.AC.rebuild_flat (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (t : AST) : ACEq acOp (rebuild l (flat l t)) t

Flattening then rebuilding is AC-equivalent to the original term. This is the associativity content of the canonical form: it does not matter how an AC tree was bracketed.

theorem MeTTaIL.AC.rebuild_perm (acOp : Label → Bool) {l : Label} (hac : acOp l = true) {xs ys : List AST} : xs.Perm ys → ACEq acOp (rebuild l xs) (rebuild l ys)

Rebuilding permutation-equal leaf lists yields AC-equivalent terms. This is the commutativity content: reordering the leaves of an AC tree gives an equivalent term.

The canonical form

def MeTTaIL.AC.canonNode (acOp : Label → Bool) (l : Label) (cargs : List AST) : AST

The canonical rebuild of one node, given its already-canonical arguments. For an acOp label with exactly two arguments this flattens, sorts, and rebuilds; otherwise it is an ordinary application.

Equations

• MeTTaIL.AC.canonNode acOp l [a, b] = if acOp l = true then MeTTaIL.AC.rebuild l (MeTTaIL.AC.sortMS (MeTTaIL.AC.flat l a ++ MeTTaIL.AC.flat l b)) else MeTTaIL.AST.sexp l [a, b]
• MeTTaIL.AC.canonNode acOp l cargs = if acOp l = true then MeTTaIL.AST.sexp l cargs else MeTTaIL.AST.sexp l cargs

def MeTTaIL.AC.canon (acOp : Label → Bool) : AST → AST

The canonical form of a term: canonicalize the arguments, then canonNode each application.

Equations

• MeTTaIL.AC.canon acOp (MeTTaIL.AST.var p) = MeTTaIL.AST.var p
• MeTTaIL.AC.canon acOp (b.subst r v) = (MeTTaIL.AC.canon acOp b).subst (MeTTaIL.AC.canon acOp r) v
• MeTTaIL.AC.canon acOp (MeTTaIL.AST.sexp l args) = MeTTaIL.AC.canonNode acOp l (MeTTaIL.AC.canonList acOp args)

def MeTTaIL.AC.canonList (acOp : Label → Bool) : List AST → List AST

Pointwise canon of an argument list.

Equations

• MeTTaIL.AC.canonList acOp [] = []
• MeTTaIL.AC.canonList acOp (a :: as) = MeTTaIL.AC.canon acOp a :: MeTTaIL.AC.canonList acOp as

theorem MeTTaIL.AC.canonList_eq_map (acOp : Label → Bool) (ts : List AST) : canonList acOp ts = List.map (canon acOp) ts

canonList is the pointwise canon of a list.

@[simp]

theorem MeTTaIL.AC.canon_var (acOp : Label → Bool) (p : DottedPath) : canon acOp (AST.var p) = AST.var p

@[simp]

theorem MeTTaIL.AC.canon_subst (acOp : Label → Bool) (b r : AST) (v : DottedPath) : canon acOp (b.subst r v) = (canon acOp b).subst (canon acOp r) v

theorem MeTTaIL.AC.canon_sexp (acOp : Label → Bool) (l : Label) (args : List AST) : canon acOp (AST.sexp l args) = canonNode acOp l (canonList acOp args)

theorem MeTTaIL.AC.canonNode_pair (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (a b : AST) : canonNode acOp l [a, b] = rebuild l (sortMS (flat l a ++ flat l b))

canonNode on an acOp label with two arguments.

theorem MeTTaIL.AC.canon_pair (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (x y : AST) : canon acOp (AST.sexp l [x, y]) = rebuild l (sortMS (flat l (canon acOp x) ++ flat l (canon acOp y)))

The canonical form of an AC binary node: canonicalise the arguments, flatten, sort, rebuild.

Soundness: the canonical form is AC-equivalent to the original

theorem MeTTaIL.AC.canon_acnode_core (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (a b : AST) : ACEq acOp (rebuild l (sortMS (flat l a ++ flat l b))) (AST.sexp l [a, b])

The canonical rebuild of one AC node is AC-equivalent to the binary application of its two canonical arguments: sorting permutes the flattened leaves (commutativity) and rebuild-of-flatten re-associates them (associativity).

theorem MeTTaIL.AC.canonNode_sound (acOp : Label → Bool) {l : Label} {cargs args : List AST} (h : List.Forall₂ (ACEq acOp) cargs args) : ACEq acOp (canonNode acOp l cargs) (AST.sexp l args)

canonNode with already-sound arguments is AC-equivalent to the application.

theorem MeTTaIL.AC.canon_sound (acOp : Label → Bool) (t : AST) : ACEq acOp (canon acOp t) t

Soundness of the canonical form: canon t is AC-equivalent to t.

theorem MeTTaIL.AC.canonList_sound (acOp : Label → Bool) (ts : List AST) : List.Forall₂ (ACEq acOp) (canonList acOp ts) ts

Pointwise soundness for argument lists.

Completeness: the canonical form is invariant under AC-equivalence

theorem MeTTaIL.AC.canon_complete (acOp : Label → Bool) {s t : AST} (h : ACEq acOp s t) : canon acOp s = canon acOp t

Completeness of the canonical form: AC-equivalent terms have identical canonical forms. Proved by induction on the AC-equivalence derivation. The comm case reduces to permutation-invariance of the sort; the assoc case to associativity of append under the sort; the congruence cases to the pointwise canonicalization of arguments.

theorem MeTTaIL.AC.canon_idem (acOp : Label → Bool) (t : AST) : canon acOp (canon acOp t) = canon acOp t

The canonical form is idempotent: it is a genuine normal form for AC-equivalence. Immediate from soundness (canon t is AC-equivalent to t) and completeness (AC-equivalent terms canonicalize alike).

The decision procedure

theorem MeTTaIL.AC.acEq_iff_canon (acOp : Label → Bool) {s t : AST} : ACEq acOp s t ↔ canon acOp s = canon acOp t

AC-equivalence is decided by equality of canonical forms. Soundness gives the reverse direction: if the canonical forms are equal then both terms are AC-equivalent to that common form.

@[implicit_reducible]

instance MeTTaIL.AC.instDecidableACEq (acOp : Label → Bool) (s t : AST) : Decidable (ACEq acOp s t)

AC-equivalence is decidable: compute and compare canonical forms.

Equations

• MeTTaIL.AC.instDecidableACEq acOp s t = decidable_of_iff (MeTTaIL.AC.canon acOp s = MeTTaIL.AC.canon acOp t) ⋯