Setoid.Congruences.Certificates.Congruence¶
The per-congruence certificate checker (obligations C1–C3)¶
This is the Setoid.Congruences.Certificates.Congruence module of the Agda Universal Algebra Library.
Fix a finite finitary algebra — an algebra 𝑨 with carrier-finiteness data
𝑭 (Setoid.Algebras.Finite) and signature-finiteness data 𝑺
(Setoid.Signatures.Finite). A per-congruence certificate
(CgCert of Setoid.Congruences.Certificates.Schema) claims
the partition presented by the parent vector
≑ Cg (fromPairs P)
for its seed list P.
This module is the checker for that claim. The claimed congruence is the table
relation of the parent vector: two carrier elements are related when their
enumeration indices have the same parent — two constant-time lookups and one
Fin equality, so the relation is decidable with no appeal to the
specification-grade decision procedure Cg-dec,1
which never appears here.
The checker obligations of the design note, each search-free and linear in the trace and table size, are as follows:
- C1 (trace soundness). Every merge of the Freese trace is derivable:
seed entries point into
P, and translate entries apply onecompatiblerule of the generation datatypeGen(Setoid.Congruences.Generation) to an earlier merge. The checker constructs theGenderivations by a single fold over the trace — it never decidesGen-membership. - C2 (claimed ⊆ generated). The design note offered two implementations
and defaulted to (a), checking each forest edge of the claimed vector for
membership in the trace's merged pairs. Implementing against honest
cg2traces shows option (a) as literally stated is unattainable: the run's merged pairs need not contain the normal-form edges, because normal form re-roots every block at its least element after the run. We therefore implement the note's sanctioned option (b) in its simplest form: replay the trace's unions through an eager re-pointing root vector — no ranks, no path compression; those are engine-side devices — carrying aGen-proof invariant, and then align the replayed partition with the claimed vector by two linear sweeps (Covers). Cost:O(n · |trace|)root updates, one pass, no search. - C3 (generated ⊆ claimed). The claimed partition contains the seed pairs
(
Respects) and is a congruence: as a partition it is an equivalence for free, and operation-compatibility is checked on one translate step per coordinate per tuple (EdgeCompat) — the pair(t , t [ c ]≔ parent (t c))for every basic operation, coordinate, and argument tuple, which is Freese'sO(r · ‖A‖)bound of unary polynomial translates times forest edges. Compatibility for arbitrary pointwise-related tuples then follows by walking the coordinates and detouring through the roots, with no further checking.Cg-leastcloses the inclusion.
The headline theorems table≑Cg (with a trace) and
table≑CgEdges (the trace-free special case where the seeds are
the vector's own forest edges, used for whole-lattice congruence lists) deliver
the claim as an honest _≑_ at the working congruence level.
Every hypothesis is decidable, and each decider is a bounded sweep of
Fin comparisons; the whole-lattice checker
(Setoid.Congruences.Certificates.Lattice) instantiates them wholesale.
Positional predicates¶
Trace justifications refer to seed pairs and earlier merges by position.
AtPos P xs k asserts that the element at position k of xs
exists and satisfies P — by recursion on the list, with the out-of-range case
uninhabited, so an invalid reference is a failed check rather than a partial
lookup. atPos? decides it, and atPos-use
consumes it against an All-package of facts about the same
list (the checker's accumulated Gen proofs).
-- The element at position k exists and satisfies P. AtPos : {a p : Level} {A : Type a} (P : A → Type p) → List A → ℕ → Type p AtPos {p = p} P [] _ = Lift p ⊥ AtPos P (x ∷ xs) zero = P x AtPos P (x ∷ xs) (suc k) = AtPos P xs k -- AtPos is decidable when P is. atPos? : {a p : Level} {A : Type a} {P : A → Type p} → ((x : A) → Dec (P x)) → (xs : List A) (k : ℕ) → Dec (AtPos P xs k) atPos? P? [] k = no (λ { (lift ()) }) atPos? P? (x ∷ xs) zero = P? x atPos? P? (x ∷ xs) (suc k) = atPos? P? xs k -- Consume a positional fact together with the All-fact at the same position. atPos-use : {a p q c : Level} {A : Type a} {P : A → Type p} {Q : A → Type q} {C : Type c} → (xs : List A) (k : ℕ) → All Q xs → AtPos P xs k → ((x : A) → Q x → P x → C) → C atPos-use [] k _ (lift ()) atPos-use (x ∷ xs) zero (qx ∷ _) px use = use x qx px atPos-use (x ∷ xs) (suc k) (_ ∷ qxs) pk use = atPos-use xs k qxs pk use
The ambient finite finitary algebra¶
Everything below lives in the named module CertCheck 𝑭 𝑺,
parameterized by carrier-finiteness data 𝑭 and signature-finiteness data 𝑺,
so that downstream checkers (and emitted certificate modules) bring the whole
interface into scope with one open. As in
Setoid.Congruences.Presented, idx is a chosen enumeration index for each
carrier element. arOf
is the arity table against which certificate literals type-check (for concrete
signatures it reduces definitionally), carrierPairs reads an
index-pair list back into the carrier, and appIdx is the
index-level view of one basic-operation application: decode the index tuple,
apply the operation, re-encode.
module CertCheck {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρ} (𝑭 : FiniteAlgebra 𝑨) (𝑺 : FiniteSignature 𝑆) where open FiniteAlgebra 𝑭 using ( _≟_ ; card ; enum ; enum-sur ) open FiniteSignature 𝑺 using ( opCard ; opEnum ; opEnum-sur ; arCard ; arEnum ; arIdx ; arEnum-arIdx ) open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ; reflexive to ≈reflexive ) private -- A chosen enumeration index for each carrier element, and its correctness. idx : 𝕌[ 𝑨 ] → Fin card idx x = proj₁ (enum-sur x) idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x idx-≈ x = proj₂ (enum-sur x) -- Pairs of enumeration indices: the index-level currency of certificates. IdxPair : Type IdxPair = Fin card × Fin card -- The arity table certificates are checked against. arOf : Fin opCard → ℕ arOf fi = arCard (opEnum fi) -- Reading an index-pair list back into the carrier. carrierPairs : List IdxPair → List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ]) carrierPairs = map (λ (p₁ , p₂) → enum p₁ , enum p₂) -- The carrier tuple encoded by a tuple of carrier indices. tupleOf : (fi : Fin opCard) → Vec (Fin card) (arOf fi) → (ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]) tupleOf fi t a = enum (lookup t (arIdx (opEnum fi) a)) -- One basic-operation application, at the index level. appIdx : (fi : Fin opCard) → Vec (Fin card) (arOf fi) → Fin card appIdx fi t = idx ((opEnum fi ^ 𝑨) (tupleOf fi t))
A decidability utility: a universally quantified statement over the index
tuples of one arity is decided by sweeping the tuple enumeration
allVecs of Setoid.Congruences.Presented (whose
completeness ∈-allVecs converts the swept
All back into a Π-statement).
-- Decide a Π-statement over index tuples by sweeping the tuple enumeration. allVecsΠ? : {p : Level} {k : ℕ} {P : Vec (Fin card) k → Type p} → ((t : Vec (Fin card) k) → Dec (P t)) → Dec (∀ t → P t) allVecsΠ? {k = k} {P} P? with allL? P? (allVecs card k) ... | yes a = yes (λ t → all-lookup a (∈-allVecs t)) ... | no ¬a = no (λ h → ¬a (universal h (allVecs card k)))
The claimed partition as a relation¶
SameBlock is the index-level reading of a parent vector — two
indices related when their parents agree — and TableRel its
carrier-level reading through idx, lifted to the working congruence level.
For TableRel to be well defined on the setoid carrier the
vector must not distinguish ≈-equal enumerated elements; that is the
(decidable) Coherent condition, from which respect for ≈
follows in general (tableResp-≈).
-- Two indices lie in the same claimed block. SameBlock : ParentVec card → Fin card → Fin card → Type SameBlock pv i j = parent pv i ≡ parent pv j -- The claimed partition does not distinguish ≈-equal enumerated elements. Coherent : ParentVec card → Type ρ Coherent pv = ∀ i j → enum i ≈ enum j → SameBlock pv i j coherent? : (pv : ParentVec card) → Dec (Coherent pv) coherent? pv = all? (λ i → all? (λ j → (enum i ≟ enum j) →-dec (parent pv i ≟ᶠ parent pv j))) -- The carrier-level relation presented by a parent vector. TableRel : ParentVec card → BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) TableRel pv x y = Lift (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) (SameBlock pv (idx x) (idx y)) -- The table relation is decidable outright: two lookups and a Fin equality. tableDec : (pv : ParentVec card) → ∀ x y → Dec (TableRel pv x y) tableDec pv x y = map′ lift lower (parent pv (idx x) ≟ᶠ parent pv (idx y)) -- ≈-equal elements have same-block indices ... sameBlock-resp-≈ : (pv : ParentVec card) → Coherent pv → ∀ {x y} → x ≈ y → SameBlock pv (idx x) (idx y) sameBlock-resp-≈ pv coh {x} {y} x≈y = coh (idx x) (idx y) (≈trans (idx-≈ x) (≈trans x≈y (≈sym (idx-≈ y)))) -- ... so the table relation is reflexive over ≈ ... tableReflexive : (pv : ParentVec card) → Coherent pv → ∀ {x y} → x ≈ y → TableRel pv x y tableReflexive pv coh x≈y = lift (sameBlock-resp-≈ pv coh x≈y) -- ... and respects ≈-replacement of related elements. tableResp-≈ : (pv : ParentVec card) → Coherent pv → ∀ {x y a b} → x ≈ a → y ≈ b → TableRel pv a b → TableRel pv x y tableResp-≈ pv coh x≈a y≈b (lift ab) = lift (trans (sameBlock-resp-≈ pv coh x≈a) (trans ab (sym (sameBlock-resp-≈ pv coh y≈b))))
C3, the checked half: one translate step per coordinate¶
EdgeCompat is the certificate's compatibility obligation: for
every enumerated operation symbol, coordinate, and index tuple, replacing the
coordinate's entry by its root stays in the same claimed block. These are
exactly Freese's unary polynomial translates applied to the forest edges
(i , parent i) (a root entry makes the statement trivially reflexive), so the
sweep is linear in the operation-table size. Everything else about
compatibility is derived, not checked.
A simpler design exists and was deliberately rejected: sweeping compatibility
over all pairs of pointwise-related tuples would shrink the derivation below
to a few lines, but its decider costs O(‖A‖²) where this one is Freese's
O(r · ‖A‖) — and linear-cost checking is an acceptance criterion of the
pipeline (#457), not a nicety. The coordinate walk that follows is the price
of the bound.
-- One root-replacement translate step per symbol, coordinate, and tuple. EdgeCompat : ParentVec card → Type EdgeCompat pv = ∀ (fi : Fin opCard) (c : Fin (arOf fi)) (t : Vec (Fin card) (arOf fi)) → SameBlock pv (appIdx fi t) (appIdx fi (t [ c ]≔ parent pv (lookup t c))) edgeCompat? : (pv : ParentVec card) → Dec (EdgeCompat pv) edgeCompat? pv = all? (λ fi → all? (λ c → allVecsΠ? (λ t → parent pv (appIdx fi t) ≟ᶠ parent pv (appIdx fi (t [ c ]≔ parent pv (lookup t c))))))
The generalization from root-replacement steps to an arbitrary same-block replacement at one coordinate: detour through the root of each side.
-- Replacing one coordinate by a same-block index stays in the same block. stepSameBlock : (pv : ParentVec card) → EdgeCompat pv → (fi : Fin opCard) (c : Fin (arOf fi)) (t : Vec (Fin card) (arOf fi)) → {a b : Fin card} → SameBlock pv a b → SameBlock pv (appIdx fi (t [ c ]≔ a)) (appIdx fi (t [ c ]≔ b)) stepSameBlock pv ec fi c t {a} {b} sab = trans (toRoot a) (trans mid (sym (toRoot b))) where -- the EdgeCompat step at entry z, rewritten to a one-shot update toRoot : (z : Fin card) → SameBlock pv (appIdx fi (t [ c ]≔ z)) (appIdx fi (t [ c ]≔ parent pv z)) toRoot z = subst (λ v → SameBlock pv (appIdx fi (t [ c ]≔ z)) (appIdx fi v)) (trans (cong (λ w → (t [ c ]≔ z) [ c ]≔ parent pv w) (lookup∘update c t z)) ([]≔-idempotent t c)) (ec fi c (t [ c ]≔ z)) -- the two roots agree, so the two root-updated tuples agree mid : SameBlock pv (appIdx fi (t [ c ]≔ parent pv a)) (appIdx fi (t [ c ]≔ parent pv b)) mid = cong (λ z → parent pv (appIdx fi (t [ c ]≔ z))) sab
Walking the coordinates. overwrite replaces the entries of
t at a list of coordinates by those of the target s;
overwrite-chain shows each replacement preserves the claimed
block of the application (given blockwise-related tuples), and
overwrite-stable / overwrite-∈ show a
coordinate once replaced stays replaced, so overwriting all coordinates
reaches s pointwise.
-- Overwrite the entries of t at the listed coordinates with those of s. overwrite : {k : ℕ} → Vec (Fin card) k → List (Fin k) → Vec (Fin card) k → Vec (Fin card) k overwrite t [] s = t overwrite t (c ∷ cs) s = overwrite (t [ c ]≔ lookup s c) cs s -- Componentwise same-block relatedness of two index tuples. Blockwise : (pv : ParentVec card) {k : ℕ} → Vec (Fin card) k → Vec (Fin card) k → Type Blockwise pv t s = ∀ q → SameBlock pv (lookup t q) (lookup s q) -- Each replacement step preserves the claimed block of the application. overwrite-chain : (pv : ParentVec card) → EdgeCompat pv → (fi : Fin opCard) (cs : List (Fin (arOf fi))) (t s : Vec (Fin card) (arOf fi)) → Blockwise pv t s → SameBlock pv (appIdx fi t) (appIdx fi (overwrite t cs s)) overwrite-chain pv ec fi [] t s bw = refl overwrite-chain pv ec fi (c ∷ cs) t s bw = trans (trans self (stepSameBlock pv ec fi c t (bw c))) (overwrite-chain pv ec fi cs (t [ c ]≔ lookup s c) s bw′) where -- t is its own one-shot update at c self : SameBlock pv (appIdx fi t) (appIdx fi (t [ c ]≔ lookup t c)) self = cong (λ v → parent pv (appIdx fi v)) (sym ([]≔-lookup t c)) -- the invariant survives the update bw′ : Blockwise pv (t [ c ]≔ lookup s c) s bw′ q with q ≟ᶠ c ... | yes refl = cong (parent pv) (lookup∘update c t (lookup s c)) ... | no q≢c = subst (λ w → SameBlock pv w (lookup s q)) (sym (lookup∘update′ q≢c t (lookup s c))) (bw q) -- A coordinate that already agrees with s still agrees after overwriting. overwrite-stable : {k : ℕ} (t s : Vec (Fin card) k) (cs : List (Fin k)) → (q : Fin k) → lookup t q ≡ lookup s q → lookup (overwrite t cs s) q ≡ lookup s q overwrite-stable t s [] q eq = eq overwrite-stable t s (c ∷ cs) q eq with q ≟ᶠ c ... | yes refl = overwrite-stable _ s cs c (lookup∘update c t (lookup s c)) ... | no q≢c = overwrite-stable _ s cs q (trans (lookup∘update′ q≢c t (lookup s c)) eq) -- Overwriting at a listed coordinate lands that coordinate on s. overwrite-∈ : {k : ℕ} (t s : Vec (Fin card) k) (cs : List (Fin k)) (q : Fin k) → q ∈ cs → lookup (overwrite t cs s) q ≡ lookup s q overwrite-∈ t s (c ∷ cs) .c (here refl) = overwrite-stable _ s cs c (lookup∘update c t (lookup s c)) overwrite-∈ t s (c ∷ cs) q (there w) = overwrite-∈ _ s cs q w
Compatibility of the table relation. For an enumerated symbol: encode the two
carrier tuples as index tuples, walk all coordinates with the chain lemma, and
close the gaps — between each carrier tuple and its encoding, and between the
fully overwritten tuple and the target encoding — by ≈-congruence of the
interpretation plus Coherent. An arbitrary symbol is an
enumerated one by surjectivity of the symbol enumeration, transported with an
explicit subst on a named motive (the same elaboration-hygiene
device as in Setoid.Congruences.Presented.Decidable).
-- The table relation is compatible with every enumerated operation symbol ... tableCompatAt : (pv : ParentVec card) → Coherent pv → EdgeCompat pv → (fi : Fin opCard) {u v : ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]} → (∀ a → TableRel pv (u a) (v a)) → TableRel pv ((opEnum fi ^ 𝑨) u) ((opEnum fi ^ 𝑨) v) tableCompatAt pv coh ec fi {u} {v} h = lift (trans (sym (encodeSB u)) (trans chain (trans sbOw (encodeSB v)))) where f : OperationSymbolsOf 𝑆 f = opEnum fi -- the index tuple encoding a carrier tuple encode : (ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]) → Vec (Fin card) (arOf fi) encode u′ = tabulate (λ p → idx (u′ (arEnum f p))) -- encoding is block-transparent: an encoded tuple is pointwise ≈ its -- original (tabulate round trip plus the arity round trip), so their -- applications land in the same claimed block encodeSB : (u′ : ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]) → SameBlock pv (appIdx fi (encode u′)) (idx ((f ^ 𝑨) u′)) encodeSB u′ = sameBlock-resp-≈ pv coh (Func.cong (Algebra.Interp 𝑨) (refl , enc≈)) where enc≈ : ∀ a → tupleOf fi (encode u′) a ≈ u′ a enc≈ a = ≈trans (≈reflexive (cong enum (trans (lookup∘tabulate (λ q → idx (u′ (arEnum f q))) (arIdx f a)) (cong (λ b → idx (u′ b)) (arEnum-arIdx f a))))) (idx-≈ (u′ a)) tu tv : Vec (Fin card) (arOf fi) tu = encode u tv = encode v -- the encodings are blockwise related, by the hypothesis bw : Blockwise pv tu tv bw p = subst₂ (SameBlock pv) (sym (lookup∘tabulate (λ q → idx (u (arEnum f q))) p)) (sym (lookup∘tabulate (λ q → idx (v (arEnum f q))) p)) (lower (h (arEnum f p))) -- walking every coordinate turns tu into tv, blockwise chain : SameBlock pv (appIdx fi tu) (appIdx fi (overwrite tu (allFin (arOf fi)) tv)) chain = overwrite-chain pv ec fi (allFin (arOf fi)) tu tv bw -- the fully overwritten tuple is pointwise tv sbOw : SameBlock pv (appIdx fi (overwrite tu (allFin (arOf fi)) tv)) (appIdx fi tv) sbOw = sameBlock-resp-≈ pv coh (Func.cong (Algebra.Interp 𝑨) (refl , λ a → ≈reflexive (cong enum (overwrite-∈ tu tv (allFin (arOf fi)) (arIdx f a) (∈-allFin (arIdx f a)))))) -- ... hence with every operation symbol, by surjectivity of the enumeration. private TableCompatMotive : ParentVec card → OperationSymbolsOf 𝑆 → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) TableCompatMotive pv g = {u v : ArityOf 𝑆 g → 𝕌[ 𝑨 ]} → (∀ a → TableRel pv (u a) (v a)) → TableRel pv ((g ^ 𝑨) u) ((g ^ 𝑨) v) tableCompat : (pv : ParentVec card) → Coherent pv → EdgeCompat pv → 𝑨 ∣≈ TableRel pv tableCompat pv coh ec f = subst (TableCompatMotive pv) (proj₂ (opEnum-sur f)) (tableCompatAt pv coh ec (proj₁ (opEnum-sur f)))
The claimed partition is therefore a congruence — packaged with its
decision procedure as a DecCon whose decider is two lookups,
never a closure computation.
-- The claimed partition as a congruence at the working level ... tableCon : (pv : ParentVec card) → Coherent pv → EdgeCompat pv → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) tableCon pv coh ec = TableRel pv , mkcon (tableReflexive pv coh) (record { refl = lift refl ; sym = λ e → lift (sym (lower e)) ; trans = λ e₁ e₂ → lift (trans (lower e₁) (lower e₂)) }) (tableCompat pv coh ec) -- ... and as a decidable congruence. tableDecCon : (pv : ParentVec card) → Coherent pv → EdgeCompat pv → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) tableDecCon pv coh ec = tableCon pv coh ec , tableDec pv
C3, concluded: the generated congruence is contained in the claim¶
The seed pairs must land in the claimed blocks — the decidable
Respects sweep — and then Cg-least contains
the whole generated congruence in the table congruence.
-- Every listed pair is same-block. Respects : ParentVec card → List IdxPair → Type Respects pv ps = All (λ p → SameBlock pv (proj₁ p) (proj₂ p)) ps respects? : (pv : ParentVec card) (ps : List IdxPair) → Dec (Respects pv ps) respects? pv ps = allL? (λ p → parent pv (proj₁ p) ≟ᶠ parent pv (proj₂ p)) ps -- The presented relation of a respected seed list is contained in the -- claim: walk the list to the presenting pair; its endpoints' chosen -- indices share the listed pair's blocks by coherence. fromPairs-table-⊆ : (pv : ParentVec card) (ps : List IdxPair) → Coherent pv → Respects pv ps → ∀ {x y} → fromPairs {𝑨 = 𝑨} (carrierPairs ps) x y → TableRel pv x y fromPairs-table-⊆ pv [] coh [] () fromPairs-table-⊆ pv (p ∷ ps) coh (sb ∷ _) (here (x≈ , y≈)) = tableResp-≈ pv coh x≈ y≈ (lift (trans (bridge (proj₁ p)) (trans sb (sym (bridge (proj₂ p)))))) where -- the chosen index of an enumerated element shares its block bridge : (i : Fin card) → parent pv (idx (enum i)) ≡ parent pv i bridge i = coh (idx (enum i)) i (idx-≈ (enum i)) fromPairs-table-⊆ pv (p ∷ ps) coh (_ ∷ rsp) (there mem) = fromPairs-table-⊆ pv ps coh rsp mem -- C3: the generated congruence of a respected seed list is contained in -- the claimed congruence (by the congruence generation theorem). Cg⊑table : (pv : ParentVec card) (ps : List IdxPair) → (coh : Coherent pv) (ec : EdgeCompat pv) → Respects pv ps → ∀ {x y} → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y → TableRel pv x y Cg⊑table pv ps coh ec rsp = Cg-least (tableCon pv coh ec) (fromPairs-table-⊆ pv ps coh rsp)
The forest edges of an idempotent vector are respected by that vector itself —
each edge relates an index to its own root — so for the seed list
forestEdges pv the Respects obligation is free.
-- A vector respects its own forest edges. edgesRespected : (pv : ParentVec card) → IdempotentParent pv → Respects pv (forestEdges pv) edgesRespected pv idem = map⁺ (universal (λ i → sym (idem i)) (filter (λ i → ¬? (i ≟ᶠ parent pv i)) (allFin card)))
C1: trace soundness¶
Fix a seed list ps. GenPair ps is membership of an index
pair in the generated congruence; JustOK is the validity of
one justification against the seed list and the already-processed merges
(most-recent-first, per the schema's reference conventions), stated through
AtPos so that decidability and consumption are both structural.
-- Membership of an index pair in the congruence generated by the seeds. GenPair : List IdxPair → IdxPair → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) GenPair ps p = Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) (enum (proj₁ p)) (enum (proj₂ p)) -- Validity of one justification for merging (i , j). JustOK : (ps done : List IdxPair) (i j : Fin card) → Justification card opCard arOf → Type ρ JustOK ps done i j (seed s) = AtPos (λ p → (enum i ≈ enum (proj₁ p)) × (enum j ≈ enum (proj₂ p))) ps s JustOK ps done i j (translate fi c w r) = AtPos (λ p → (enum i ≈ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p))) × (enum j ≈ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p)))) done r justOK? : (ps done : List IdxPair) (i j : Fin card) → (ju : Justification card opCard arOf) → Dec (JustOK ps done i j ju) justOK? ps done i j (seed s) = atPos? (λ p → (enum i ≟ enum (proj₁ p)) ×-dec (enum j ≟ enum (proj₂ p))) ps s justOK? ps done i j (translate fi c w r) = atPos? (λ p → (enum i ≟ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p))) ×-dec (enum j ≟ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p)))) done r
A valid trace is a run of valid justifications, each against the merges before
it; merges is the final accumulator. Both are single
structural folds, as is the decider.
-- Validity of a trace, processing merges into the accumulator done. TraceValidFrom : (ps done : List IdxPair) → Trace card opCard arOf → Type ρ TraceValidFrom ps done [] = Lift ρ ⊤ TraceValidFrom ps done (mkMerge i j ju ∷ tr) = JustOK ps done i j ju × TraceValidFrom ps ((i , j) ∷ done) tr traceValidFrom? : (ps done : List IdxPair) (tr : Trace card opCard arOf) → Dec (TraceValidFrom ps done tr) traceValidFrom? ps done [] = yes (lift tt) traceValidFrom? ps done (mkMerge i j ju ∷ tr) = justOK? ps done i j ju ×-dec traceValidFrom? ps ((i , j) ∷ done) tr TraceValid : List IdxPair → Trace card opCard arOf → Type ρ TraceValid ps tr = TraceValidFrom ps [] tr traceValid? : (ps : List IdxPair) (tr : Trace card opCard arOf) → Dec (TraceValid ps tr) traceValid? ps tr = traceValidFrom? ps [] tr -- The merged pairs of a trace, most recent first. mergesFrom : List IdxPair → Trace card opCard arOf → List IdxPair mergesFrom done [] = done mergesFrom done (mkMerge i j _ ∷ tr) = mergesFrom ((i , j) ∷ done) tr merges : Trace card opCard arOf → List IdxPair merges = mergesFrom []
A valid seed justification is Any-membership of the pair in the presented
relation — recovered structurally, at the recorded position.
-- A valid seed reference presents the merged pair. seedAt : (ps : List IdxPair) (s : ℕ) {i j : Fin card} → AtPos (λ p → (enum i ≈ enum (proj₁ p)) × (enum j ≈ enum (proj₂ p))) ps s → fromPairs {𝑨 = 𝑨} (carrierPairs ps) (enum i) (enum j) seedAt [] s (lift ()) seedAt (p ∷ ps) zero ok = here ok seedAt (p ∷ ps) (suc s) ok = there (seedAt ps s ok)
One valid justification yields one Gen derivation: a seed by
the base rule; a translate by one
compatible rule applied to the earlier merge at
the moving coordinate and to reflexivity at the frozen coordinates, wrapped in
the recorded ≈-matches. This is obligation C1, entry by entry.
-- C1, one entry: a valid justification derives its merged pair. justGen : (ps done : List IdxPair) {i j : Fin card} → (ju : Justification card opCard arOf) → All (GenPair ps) done → JustOK ps done i j ju → GenPair ps (i , j) justGen ps done (seed s) dall ok = base (seedAt ps s ok) justGen ps done {i} {j} (translate fi c w r) dall ok = atPos-use done r dall ok derive where f : OperationSymbolsOf 𝑆 f = opEnum fi derive : (p : IdxPair) → GenPair ps p → (enum i ≈ (f ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p))) × (enum j ≈ (f ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p))) → GenPair ps (i , j) derive (x , y) gxy (ei≈ , ej≈) = transitive (rfl ei≈) (transitive (compatible f ptw) (symmetric (rfl ej≈))) where R : BinaryRel 𝕌[ 𝑨 ] (α ⊔ ρ) R = fromPairs {𝑨 = 𝑨} (carrierPairs ps) -- the two frozen tuples are pointwise generated-related: -- the moving coordinate by the earlier merge, the rest by reflexivity ptw : ∀ a → Gen {𝑨 = 𝑨} R (tupleOf fi (w [ c ]≔ x) a) (tupleOf fi (w [ c ]≔ y) a) ptw a with arIdx f a ≟ᶠ c ... | yes p = subst₂ (λ s′ t′ → Gen {𝑨 = 𝑨} R (enum s′) (enum t′)) (sym (trans (cong (lookup (w [ c ]≔ x)) p) (lookup∘update c w x))) (sym (trans (cong (lookup (w [ c ]≔ y)) p) (lookup∘update c w y))) gxy ... | no ¬p = subst₂ (λ s′ t′ → Gen {𝑨 = 𝑨} R (enum s′) (enum t′)) (sym (lookup∘update′ ¬p w x)) (sym (lookup∘update′ ¬p w y)) (rfl ≈refl)
C1, the whole trace: fold the entries, accumulating each derived pair.
-- C1: every merged pair of a valid trace is generated. traceGenFrom : (ps done : List IdxPair) (tr : Trace card opCard arOf) → All (GenPair ps) done → TraceValidFrom ps done tr → All (GenPair ps) (mergesFrom done tr) traceGenFrom ps done [] dall _ = dall traceGenFrom ps done (mkMerge i j ju ∷ tr) dall (ok , rest) = traceGenFrom ps ((i , j) ∷ done) tr (justGen ps done ju dall ok ∷ dall) rest traceGen : (ps : List IdxPair) (tr : Trace card opCard arOf) → TraceValid ps tr → All (GenPair ps) (merges tr) traceGen ps tr tv = traceGenFrom ps [] tr [] tv
C2: replaying the merges¶
The replay state is a root vector, initially the identity. Processing one
merged pair re-points every index rooted at the right root to the left root —
the eager, proofless core of a union-find, adequate because the checker replays
a given ≤ n − 1-entry list exactly once. (merges is
most-recent-first, and foldr therefore applies the head
last: the replay processes the trace in run order.)
-- Re-point one root: entries rooted at rv move to ru. repoint : Fin card → Fin card → Fin card → Fin card repoint ru rv r = if does (r ≟ᶠ rv) then ru else r -- Process one merged pair. replayStep : Vec (Fin card) card → IdxPair → Vec (Fin card) card replayStep st p = mapᵥ (repoint (lookup st (proj₁ p)) (lookup st (proj₂ p))) st -- Replay a merge list from the identity partition. replayRoots : List IdxPair → Vec (Fin card) card replayRoots ms = foldr (λ p st → replayStep st p) (tabulate (λ i → i)) ms
The soundness invariant: every index is generated-related to its current replay root. It holds initially by reflexivity and is preserved by each step — the re-pointed indices reach their new root through the merged pair.
-- Every index is generated-related to its replay root. ReplaySound : List IdxPair → Vec (Fin card) card → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) ReplaySound ps st = ∀ i → GenPair ps (i , lookup st i) -- Both containments of the claim in a generated congruence have the same -- shape: pass from the carrier pair to its chosen indices, walk each index -- (generated-relatedly) to a representative, and cross the gap with the -- given equality of representatives. Stated once, used for the replay -- roots below and for the parent pointers in the trace-free case. private viaReps : (ps : List IdxPair) (f : Fin card → Fin card) → (walk : ∀ i → GenPair ps (i , f i)) → ∀ {x y} → f (idx x) ≡ f (idx y) → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y viaReps ps f walk {x} {y} eq = transitive (symmetric (rfl (idx-≈ x))) (transitive (walk (idx x)) (transitive (rfl (≈reflexive (cong enum eq))) (transitive (symmetric (walk (idx y))) (rfl (idx-≈ y))))) private -- one re-pointed entry, with the decision exposed as an argument repoint-gen : (ps : List IdxPair) {ru rv : Fin card} (r : Fin card) → (d : Dec (r ≡ rv)) {i : Fin card} → GenPair ps (i , r) → GenPair ps (rv , ru) → GenPair ps (i , (if does d then ru else r)) repoint-gen ps r (yes q) g h = transitive g (subst (λ z → GenPair ps (z , _)) (sym q) h) repoint-gen ps r (no _) g _ = g -- One step preserves the invariant. replayStep-sound : (ps : List IdxPair) (st : Vec (Fin card) card) → (p : IdxPair) → GenPair ps p → ReplaySound ps st → ReplaySound ps (replayStep st p) replayStep-sound ps st (u , v) guv snd i = subst (λ z → GenPair ps (i , z)) (sym (lookup-map i (repoint (lookup st u) (lookup st v)) st)) (repoint-gen ps (lookup st i) (lookup st i ≟ᶠ lookup st v) (snd i) rv→ru) where -- from the old right root to the old left root, through the merged pair rv→ru : GenPair ps (lookup st v , lookup st u) rv→ru = transitive (symmetric (snd v)) (transitive (symmetric guv) (snd u)) -- The invariant holds after replaying a generated merge list. replay-sound : (ps ms : List IdxPair) → All (GenPair ps) ms → ReplaySound ps (replayRoots ms) replay-sound ps [] [] i = subst (λ z → GenPair ps (i , z)) (sym (lookup∘tabulate (λ j → j) i)) (rfl ≈refl) replay-sound ps (p ∷ ms) (g ∷ gs) = replayStep-sound ps (replayRoots ms) p g (replay-sound ps ms gs)
The alignment condition Covers: the replayed roots are
constant along the claimed parent pointers. One linear sweep, and exactly what
the containment argument consumes — if two indices share a claimed parent, they
share a replayed root, hence both are generated-related to it. (No converse
sweep is needed: the other inclusion is C3, and an over-merging trace would
merely make the two checks jointly unsatisfiable, never unsound.)
-- The replayed roots are constant along the claimed parent pointers. Covers : ParentVec card → Vec (Fin card) card → Type Covers pv rr = ∀ i → lookup rr (parent pv i) ≡ lookup rr i covers? : (pv : ParentVec card) (rr : Vec (Fin card) card) → Dec (Covers pv rr) covers? pv rr = all? (λ i → lookup rr (parent pv i) ≟ᶠ lookup rr i) -- C2: the claimed congruence is contained in the generated one. table⊑Cg : (pv : ParentVec card) (ps : List IdxPair) → (tr : Trace card opCard arOf) → TraceValid ps tr → Covers pv (replayRoots (merges tr)) → ∀ {x y} → TableRel pv x y → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y table⊑Cg pv ps tr tv cov {x} {y} (lift same) = viaReps ps (lookup rr) (replay-sound ps (merges tr) (traceGen ps tr tv)) key where rr : Vec (Fin card) card rr = replayRoots (merges tr) -- same claimed parent forces same replayed root key : lookup rr (idx x) ≡ lookup rr (idx y) key = trans (sym (cov (idx x))) (trans (cong (lookup rr) same) (cov (idx y)))
The trace-free special case: a vector generates itself from its edges¶
When the seed list is the vector's own forest edges, no trace is needed: an index reaches its root in one edge (or is a root), so the containment of the claim in the generated congruence is direct. This is the form the whole-lattice checker uses for every listed congruence.
-- Every index is edge-generated-related to its root. toRootGen : (pv : ParentVec card) (i : Fin card) → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv))) (enum i) (enum (parent pv i)) toRootGen pv i with i ≟ᶠ parent pv i ... | yes q = rfl (≈reflexive (cong enum q)) ... | no ¬q = base (lose mem (≈refl , ≈refl)) where mem : (enum i , enum (parent pv i)) ∈ carrierPairs (forestEdges pv) mem = ∈-map⁺ (λ p → enum (proj₁ p) , enum (proj₂ p)) (∈-map⁺ (λ a → a , parent pv a) (∈-filter⁺ (λ a → ¬? (a ≟ᶠ parent pv a)) (∈-allFin i) ¬q)) -- The claimed congruence is contained in the one its edges generate. table⊑CgEdges : (pv : ParentVec card) → ∀ {x y} → TableRel pv x y → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv))) x y table⊑CgEdges pv (lift same) = viaReps (forestEdges pv) (parent pv) (toRootGen pv) same
The headline theorems¶
Both directions, packaged as an honest _≑_ at the working
congruence level: with a trace, for an arbitrary seed list; and trace-free,
for a vector against its own forest edges.
-- θ ≑ Cg (fromPairs P), from a checked certificate. table≑Cg : (pv : ParentVec card) (ps : List IdxPair) → (tr : Trace card opCard arOf) → (coh : Coherent pv) (ec : EdgeCompat pv) → Respects pv ps → TraceValid ps tr → Covers pv (replayRoots (merges tr)) → tableCon pv coh ec ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) table≑Cg pv ps tr coh ec rsp tv cov = table⊑Cg pv ps tr tv cov , Cg⊑table pv ps coh ec rsp -- θ ≑ Cg (its own forest edges), with no trace at all. table≑CgEdges : (pv : ParentVec card) → (coh : Coherent pv) (ec : EdgeCompat pv) → IdempotentParent pv → tableCon pv coh ec ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv))) table≑CgEdges pv coh ec idem = table⊑CgEdges pv , Cg⊑table pv (forestEdges pv) coh ec (edgesRespected pv idem)
Finally, the bundled interface for one standalone certificate: the conjunction of all five checked conditions, its decider (one decision for the whole certificate), and the soundness theorem consuming it.
-- All checked conditions of one per-congruence certificate. CgCertOK : CgCert card opCard arOf → Type ρ CgCertOK cc = Coherent part × EdgeCompat part × Respects part seeds × TraceValid seeds trace × Covers part (replayRoots (merges trace)) where open CgCert cc cgCertOK? : (cc : CgCert card opCard arOf) → Dec (CgCertOK cc) cgCertOK? cc = coherent? part ×-dec edgeCompat? part ×-dec respects? part seeds ×-dec traceValid? seeds trace ×-dec covers? part (replayRoots (merges trace)) where open CgCert cc -- The certificate's claim, from its checked conditions. cgCertSound : (cc : CgCert card opCard arOf) (ok : CgCertOK cc) → tableCon (CgCert.part cc) (proj₁ ok) (proj₁ (proj₂ ok)) ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (CgCert.seeds cc))) cgCertSound cc (coh , ec , rsp , tv , cov) = table≑Cg (CgCert.part cc) (CgCert.seeds cc) (CgCert.trace cc) coh ec rsp tv cov