From b052568fa78de1190f2060ddd17501fb39669a99 Mon Sep 17 00:00:00 2001 From: Zarathustra Goertzel Date: Fri, 10 Jul 2026 13:58:40 +0200 Subject: [PATCH 1/3] minimal: HE-faithful malformed-unify error payload Bad-arity unify now surfaces the upstream interpreter.rs message shape ("expected: (unify ), found: ...") instead of a generic string. Upstream-PR candidate. Co-Authored-By: Claude Fable 5 --- MettaHyperonFull/Minimal/Interpreter.lean | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/MettaHyperonFull/Minimal/Interpreter.lean b/MettaHyperonFull/Minimal/Interpreter.lean index 3ebd994..30d1b55 100644 --- a/MettaHyperonFull/Minimal/Interpreter.lean +++ b/MettaHyperonFull/Minimal/Interpreter.lean @@ -65,7 +65,16 @@ def notReducibleA : Atom := Atom.sym "NotReducible" def emptyA : Atom := Atom.sym "Empty" /-- Build `(Error )` with the message as a symbol (matching the interpreter ops). -/ -def errAtom (a : Atom) (msg : String) : Atom := Atom.expr [Atom.sym "Error", a, Atom.gnd (Ground.str msg)] +def errAtom (a : Atom) (msg : String) : Atom := Atom.expr [Atom.sym "Error", a, Atom.sym msg] + +/-- Runtime message for malformed primitive `unify` applications. -/ +def unifyBadArityMessage : Atom → String + | Atom.expr [Atom.sym "unify", Atom.sym a, Atom.sym p, Atom.sym t] => + "expected: (unify ), found: " ++ + "(unify " ++ a ++ " " ++ p ++ " " ++ t ++ ")" + | source => + "expected: (unify ), found: " ++ + toString source /-- Copy the variable scope from the top frame of `prev` (Rust `Stack::vars_copy`). -/ def varsCopy : Stack → List VarName @@ -100,7 +109,7 @@ def atomToStack : Atom → Stack → Stack | Atom.expr (Atom.sym "function" :: _) => { atom := errAtom a "function: expected (function )", fin := true } :: prev | Atom.expr (Atom.sym "unify" :: _) => - { atom := errAtom a "unify: expected (unify )", fin := true } :: prev + { atom := errAtom a (unifyBadArityMessage a), fin := true } :: prev | _ => { atom := a, vars := varsCopy prev } :: prev /-- Make a finished item: a single frame carrying `a` on top of `st`. -/ From aab8a11f66666df7b420d2fe6d45a2804a77ce90 Mon Sep 17 00:00:00 2001 From: Zarathustra Goertzel Date: Wed, 15 Jul 2026 10:40:31 +0200 Subject: [PATCH 2/3] Repair equality-class binding reconciliation Represent variable aliases explicitly, reconcile class-wide values, retain unifier alias traces, and prove the repaired binding and substitution laws. --- MettaHyperonFull/Core/Bindings.lean | 138 ++++- MettaHyperonFull/Core/Matching.lean | 142 ++++- MettaHyperonFull/Core/Unification.lean | 36 +- MettaHyperonFull/Minimal/Interpreter.lean | 10 +- .../Operational/MinimalCoverage.lean | 6 +- MettaHyperonFull/Proofs.lean | 8 +- MettaHyperonFull/Proofs/BindingLaws.lean | 550 +++++++++++++++--- MettaHyperonFull/Proofs/MorkMM2Lowering.lean | 4 +- MettaHyperonFull/Proofs/QueryBackend.lean | 19 +- MettaHyperonFull/Proofs/Substitution.lean | 347 ++++++++++- .../Proofs/SubstitutionAudit.lean | 79 +-- book/Docs/Appendices.lean | 10 +- 12 files changed, 1174 insertions(+), 175 deletions(-) diff --git a/MettaHyperonFull/Core/Bindings.lean b/MettaHyperonFull/Core/Bindings.lean index 5c9f8d6..350eae0 100644 --- a/MettaHyperonFull/Core/Bindings.lean +++ b/MettaHyperonFull/Core/Bindings.lean @@ -10,8 +10,9 @@ Purpose: The binding sets that matching and unification produce. A binding set i consistency-checking merge lives in Matching.lean. Imports: MettaHyperonFull.Core.Atom, MettaHyperonFull.Core.Pretty Trusted boundary: none -Main exports: BindingRel, Bindings, Bindings.empty, Bindings.lookupVal, Bindings.eqClasses, - Bindings.removeVal, Bindings.hasLoop, Bindings.addValRaw, Bindings.addEqRaw +Main exports: BindingRel, Bindings, Bindings.empty, Bindings.lookupVal, Bindings.eqClassOrdered, + Bindings.classValues, Bindings.resolve, Bindings.resolveAtom, Bindings.removeVal, + Bindings.hasLoop, Bindings.addValRaw, Bindings.addEqRaw Open obligations: none -/ import MettaHyperonFull.Core.Atom @@ -40,6 +41,128 @@ def lookupVal (b : Bindings) (x : VarName) : Option Atom := | BindingRel.val y a :: rest => if x == y then some a else lookupVal rest x | _ :: rest => lookupVal rest x +/-- One saturation pass for the symmetric equality closure. -/ +def eqStep (b : Bindings) (acc : List VarName) : List VarName := + b.foldl (fun acc r => match r with + | BindingRel.eq x y => + let acc := if acc.contains x && !acc.contains y then acc ++ [y] else acc + if acc.contains y && !acc.contains x then acc ++ [x] else acc + | _ => acc) acc + +/-- Fuelled saturation of the symmetric-transitive equality closure. -/ +def eqClassAux (b : Bindings) : Nat → List VarName → List VarName + | 0, acc => acc + | fuel + 1, acc => eqClassAux b fuel (eqStep b acc) + +/-- All variables explicitly equality-connected to `x`, including `x`. -/ +def eqClass (b : Bindings) (x : VarName) : List VarName := + eqClassAux b (2 * b.length + 1) [x] + +/-- Variables mentioned by equality relations, in representative order. Raw + relations are newest-first, while matcher equalities store the rule endpoint + before the query endpoint, so oldest edges and their query endpoints come first. -/ +def eqVarsInOrder (b : Bindings) : List VarName := + b.reverse.foldl (fun acc r => match r with + | BindingRel.eq x y => + let acc := if acc.contains y then acc else acc ++ [y] + if acc.contains x then acc else acc ++ [x] + | _ => acc) [] + +/-- The equality class of `x` in stable relation order. -/ +def eqClassOrdered (b : Bindings) (x : VarName) : List VarName := + match (eqVarsInOrder b).filter (fun y => (eqClass b x).contains y) with + | [] => [x] + | cls => cls + +/-- Stable representative of `x`'s explicit equality class. -/ +def eqRepresentative (b : Bindings) (x : VarName) : VarName := + (eqClassOrdered b x).headD x + +/-- Every direct value carried by a member of `x`'s equality class, in stable + class-member order. Direct lookup selects the unique normalized value for + each member, so raw relation-list permutations do not steer reconciliation. -/ +def classValues (b : Bindings) (x : VarName) : List Atom := + (eqClassOrdered b x).filterMap (lookupVal b) + +@[simp] theorem classValues_empty (x : VarName) : + classValues [] x = [] := by + simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal] + +@[simp] theorem classValues_singleton_val_self + (x : VarName) (value : Atom) : + classValues [BindingRel.val x value] x = [value] := by + simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal] + +@[simp] theorem classValues_singleton_val_ne + {key x : VarName} (value : Atom) (h : x ≠ key) : + classValues [BindingRel.val key value] x = [] := by + simp [classValues, eqClassOrdered, eqVarsInOrder, lookupVal, h] + +theorem classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil + {b : Bindings} (horder : eqVarsInOrder b = []) (x : VarName) : + classValues b x = (lookupVal b x).toList := by + unfold classValues + rw [show eqClassOrdered b x = [x] by + simp [eqClassOrdered, horder]] + cases hlookup : lookupVal b x <;> simp [hlookup] + +/-- Variables participating in a binding relation, including variables nested in values. -/ +def vars (b : Bindings) : List VarName := + (b.flatMap fun r => match r with + | BindingRel.val x a => x :: a.vars + | BindingRel.eq x y => [x, y]).eraseDups + +/-- The contribution of one stored relation to recursive resolution fuel. -/ +def relationResolutionFuel : BindingRel → Nat + | BindingRel.val _ value => value.size + 1 + | BindingRel.eq _ _ => 1 + +/-- Structural fuel sufficient for traversing every stored value and relation. -/ +def resolutionFuel (b : Bindings) (a : Atom) : Nat := + a.size + (b.map relationResolutionFuel).sum + 1 + +/-- Resolve every variable in an atom through equality classes and class values. + `none` means a cyclic class/value dependency was encountered. Unknown variables + remain variables, matching Hyperon's recursive resolution behavior. -/ +def resolveAtomAux (b : Bindings) : Nat → List VarName → Atom → Option Atom + | 0, _, _ => none + | fuel + 1, visited, atom => + match atom with + | Atom.var x => + let cls := eqClassOrdered b x + if cls.any visited.contains then none + else + match classValues b x with + | [] => some (Atom.var (eqRepresentative b x)) + | value :: _ => + match value with + | Atom.var y => + if cls.contains y then + if cls.length == 1 then none + else some (Atom.var (eqRepresentative b x)) + else resolveAtomAux b fuel (cls ++ visited) value + | _ => resolveAtomAux b fuel (cls ++ visited) value + | Atom.expr xs => + match xs.mapM (resolveAtomAux b fuel visited) with + | some ys => some (Atom.expr ys) + | none => none + | other => some other + +/-- Resolve a bound variable through its full equality class and recursively through + compound values. Returns `none` for an unbound variable or a dependency loop. -/ +def resolve (b : Bindings) (x : VarName) : Option Atom := + let cls := eqClassOrdered b x + if cls == [x] && (classValues b x).isEmpty then none + else resolveAtomAux b (resolutionFuel b (Atom.var x)) [] (Atom.var x) + +/-- Resolve every variable occurrence in `a` through its full equality class. + A cyclic variable occurrence remains unchanged; runtime paths reject the + containing binding set with `hasLoop` before instantiation. -/ +def resolveAtom (b : Bindings) : Atom → Atom + | Atom.var x => (resolve b x).getD (Atom.var x) + | Atom.expr xs => Atom.expr (xs.map (resolveAtom b)) + | other => other + /-- The variables directly equated with `$x` by `eq` relations (one hop, both orientations). -/ def eqClasses (b : Bindings) (x : VarName) : List VarName := b.foldl (fun acc r => match r with @@ -50,10 +173,15 @@ def eqClasses (b : Bindings) (x : VarName) : List VarName := def removeVal (b : Bindings) (x : VarName) : Bindings := b.filter (fun r => match r with | BindingRel.val y _ => y != x | _ => true) -/-- True if the set contains a trivial self-loop (`$x ← $x` or `$x = $x`), a degenerate solution - that the matcher discards. -/ +/-- True when any variable participates in a direct self-loop or a longer cyclic + dependency through equality classes, variable chains, or compound values. -/ def hasLoop (b : Bindings) : Bool := - b.any (fun r => match r with | BindingRel.val x (Atom.var y) => x == y | BindingRel.eq x y => x == y | _ => false) + b.any (fun r => match r with + | BindingRel.val x (Atom.var y) => x == y + | BindingRel.eq x y => x == y + | _ => false) || + (vars b).any (fun x => + (resolveAtomAux b (resolutionFuel b (Atom.var x)) [] (Atom.var x)).isNone) /-- Bind `$x ← a`, dropping any previous value binding for `$x`. Raw: no occurs/consistency check (that is `addVarBinding`'s job). -/ diff --git a/MettaHyperonFull/Core/Matching.lean b/MettaHyperonFull/Core/Matching.lean index 845639e..ffecd95 100644 --- a/MettaHyperonFull/Core/Matching.lean +++ b/MettaHyperonFull/Core/Matching.lean @@ -12,7 +12,9 @@ Purpose: Nondeterministic pattern matching for MeTTa atoms and the consistency-c Imports: MettaHyperonFull.Core.Unification, MettaHyperonFull.Core.Bindings Trusted boundary: none Main exports: GroundMatcher, Bindings.addVarBinding, Bindings.addVarEquality, Bindings.mergeOne, - Bindings.merge, Bindings.ofSubst, matchAtomsWith, matchAll, matchAtoms, bindingsToSubst, instantiate + Bindings.merge, Bindings.ofSubst, Bindings.reconcileAll, Bindings.rebuildFromSubst, + Bindings.reconciliationAliases, Bindings.rebuildFromReconciliation, + matchAtomsWith, matchAll, matchAtoms, bindingsToSubst, instantiate Open obligations: none -/ import MettaHyperonFull.Core.Unification @@ -26,24 +28,117 @@ abbrev GroundMatcher := Atom → Atom → List Bindings /- Binding-set merge based on the algorithm in the Hyperon specification. -/ namespace Bindings -/-- Add `$x ← v` to `b` consistently: if `$x` is unbound, insert it; if already bound to `v`, keep - `b`; otherwise the old and new values must unify (else no result). The consistency-checking core - of `merge`. -/ -def addVarBinding (b : Bindings) (x : VarName) (v : Atom) : List Bindings := - match lookupVal b x with - | none => [addValRaw b x v] - | some prev => - if prev == v then [b] - else match Unify.unifyTop prev v with - | none => [] - | some _ => [addValRaw b x v] - -/-- Add the alias `$x = $y` to `b` consistently: if both are already value-bound, those values must - be equal (else no result). -/ +/-- View a unifier as binding relations, preserving variable/variable constraints + as explicit equality rather than an oriented value assignment. -/ +def ofSubst (s : Subst) : Bindings := + s.map (fun p => match p.2 with + | Atom.var y => BindingRel.eq p.1 y + | value => BindingRel.val p.1 value) + +/-- Add every relation from a unifier to a binding set without discarding its + reconciliation constraints. -/ +def addSubstRaw (b : Bindings) (s : Subst) : Bindings := + (ofSubst s).foldl (fun b r => match r with + | BindingRel.val x value => addValRaw b x value + | BindingRel.eq x y => addEqRaw b x y) b + +/-- Unify all values carried by one equality class. -/ +def unifyValues : List Atom → Option Subst + | [] => some [] + | [_] => some [] + | first :: rest => + let equations := rest.map (fun value => (first, value)) + let fuel := first.size + (rest.map Atom.size).sum + Unify.unifyRounds fuel equations [] + +/-- Present one binding relation as a first-order atom equation. -/ +def relationEquation : BindingRel → Atom × Atom + | BindingRel.val x value => (Atom.var x, value) + | BindingRel.eq x y => (Atom.var x, Atom.var y) + +/-- The complete first-order equation presentation of a binding set. -/ +def equations (b : Bindings) : List (Atom × Atom) := + b.map relationEquation + +/-- Structural fuel covering every atom in an equation worklist. -/ +def equationFuel (work : List (Atom × Atom)) : Nat := + (work.map fun equation => equation.1.size + equation.2.size).sum + +/-- Reconcile every existing binding relation together with new constraints. + This prevents a class-local unifier from overwriting an unrelated seeded + value that shares one of its internal variables. -/ +def reconcileAll (b : Bindings) (extra : List (Atom × Atom)) : Option Subst := + let work := equations b ++ extra + Unify.unifyRounds (equationFuel work) work [] + +/-- Retain the explicit equality graph while a whole-system unifier normalizes + every direct value relation. -/ +def equalitySkeleton : Bindings → Bindings + | [] => [] + | BindingRel.val _ _ :: rest => equalitySkeleton rest + | BindingRel.eq x y :: rest => BindingRel.eq x y :: equalitySkeleton rest + +/-- Rebuild a normalized binding set without discarding explicit class edges. -/ +def rebuildFromSubst (b : Bindings) (sigma : Subst) : Bindings := + equalitySkeleton b ++ ofSubst sigma + +/-- Every explicit variable alias encountered by whole-system reconciliation. +The caller invokes this only after `reconcileAll` succeeds, so the successful +unification run certifies every traced constraint; no representative-oriented +substitution image is used to decide semantic class membership. -/ +def reconciliationAliases + (b : Bindings) (extra : List (Atom × Atom)) (_sigma : Subst) : + List (VarName × VarName) := + let work := equations b ++ extra + Unify.aliasTrace (equationFuel work) work + +/-- Insert one alias only when its equality class is not already represented. +This makes alias restoration conservative on existing normalized outputs. -/ +def restoreAlias (b : Bindings) (edge : VarName × VarName) : Bindings := + if (eqClass b edge.1).contains edge.2 then b + else addEqRaw b edge.1 edge.2 + +/-- Rebuild normalized values while retaining every alias discovered by a +successful whole-system reconciliation. Existing output is left +unchanged whenever its equality closure already carries the alias. -/ +def rebuildFromReconciliation + (candidate source : Bindings) (extra : List (Atom × Atom)) + (sigma : Subst) : Bindings := + (reconciliationAliases source extra sigma).foldl restoreAlias + (rebuildFromSubst candidate sigma) + +/-- Add the alias `$x = $y` while reconciling every value already carried by + either equality class. Successful unifiers are retained as relations. -/ def addVarEquality (b : Bindings) (x y : VarName) : List Bindings := - match lookupVal b x, lookupVal b y with - | some vx, some vy => if vx == vy then [addEqRaw b x y] else [] - | _, _ => [addEqRaw b x y] + let candidate := addEqRaw b x y + match unifyValues (classValues candidate x) with + | none => [] + | some [] => [candidate] + | some (_ :: _) => + match reconcileAll b [(Atom.var x, Atom.var y)] with + | none => [] + | some sigma => + [rebuildFromReconciliation candidate b + [(Atom.var x, Atom.var y)] sigma] + +/-- Add `$x ← v` consistently across `$x`'s whole equality class. Variable + values are aliases, and successful reconciliation constraints are retained + instead of replacing one direct value and discarding the unifier. -/ +def addVarBinding (b : Bindings) (x : VarName) (v : Atom) : List Bindings := + match v with + | Atom.var y => addVarEquality b x y + | _ => + match classValues b x with + | [] => [addValRaw b x v] + | values => + match unifyValues (values ++ [v]) with + | none => [] + | some [] => [b] + | some (_ :: _) => + match reconcileAll b [(Atom.var x, v)] with + | none => [] + | some sigma => + [rebuildFromReconciliation b b [(Atom.var x, v)] sigma] /-- Fold one binding relation `r` into every candidate set in `bs`, keeping only consistent extensions; it is nondeterministic, so a relation may yield zero, one, or several results. -/ @@ -56,9 +151,6 @@ def mergeOne (bs : List Bindings) (r : BindingRel) : List Bindings := result is empty exactly when they conflict. -/ def merge (a b : Bindings) : List Bindings := b.foldl mergeOne [a] -/-- View a substitution as a binding set: each `x ↦ v` becomes a `val` relation. -/ -def ofSubst (s : Subst) : Bindings := s.map (fun p => BindingRel.val p.fst p.snd) - end Bindings mutual @@ -68,7 +160,7 @@ mutual only the right-hand atom is grounded, the custom matcher is called as `f r l`, arguments swapped. -/ def matchAtomsWith (custom : Option GroundMatcher) : Atom → Atom → List Bindings | Atom.sym a, Atom.sym b => if a == b then [[]] else [] - | Atom.var x, Atom.var y => if x == y then [[]] else [[BindingRel.val x (Atom.var y)]] + | Atom.var x, Atom.var y => if x == y then [[]] else [[BindingRel.eq x y]] | Atom.var x, r => if Subst.occurs x r then [] else [[BindingRel.val x r]] | l, Atom.var y => if Subst.occurs y l then [] else [[BindingRel.val y l]] | Atom.expr xs, Atom.expr ys => matchAll custom [[]] xs ys @@ -96,8 +188,8 @@ def matchAtoms (l r : Atom) : List Bindings := matchAtomsWith none l r def bindingsToSubst (b : Bindings) : Subst := b.foldr (fun r s => match r with | BindingRel.val x v => (x,v)::s | _ => s) [] -/-- Apply a binding set to an atom as a substitution (value bindings only, since `eq` aliases are - dropped by `bindingsToSubst`). -/ -def instantiate (b : Bindings) (a : Atom) : Atom := Subst.apply (bindingsToSubst b) a +/-- Resolve a binding set throughout an atom, including equality classes, + variable chains, and variables nested in compound values. -/ +def instantiate (b : Bindings) (a : Atom) : Atom := Bindings.resolveAtom b a end Metta diff --git a/MettaHyperonFull/Core/Unification.lean b/MettaHyperonFull/Core/Unification.lean index fec0ffc..3f00788 100644 --- a/MettaHyperonFull/Core/Unification.lean +++ b/MettaHyperonFull/Core/Unification.lean @@ -11,8 +11,8 @@ Purpose: First-order syntactic unification of atoms, returning a most-general un function is total. Grounded atoms with custom matching are handled in Matching.lean. Imports: MettaHyperonFull.Core.Substitution Trusted boundary: none -Main exports: Unify.decomposeEq, Unify.decomposeList, Unify.decomposeAll, Unify.unifyRounds, - Unify.unifyTop +Main exports: Unify.decomposeEq, Unify.decomposeList, Unify.decomposeAll, + Unify.aliasConstraints, Unify.aliasTrace, Unify.unifyRounds, Unify.unifyTop Open obligations: none -/ import MettaHyperonFull.Core.Substitution @@ -57,6 +57,38 @@ def decomposeAll : List (Atom × Atom) → Option (List (VarName × Atom)) | some c₁, some c₂ => some (c₁ ++ c₂) | _, _ => none +/-- Explicit variable/variable constraints visible in one fully decomposed +unification round. These are retained separately from the normalized +substitution because later elimination may ground both endpoints without +erasing the alias relation discovered by matching. -/ +def aliasConstraints : List (VarName × Atom) → List (VarName × VarName) + | [] => [] + | (x, Atom.var y) :: rest => (x, y) :: aliasConstraints rest + | _ :: rest => aliasConstraints rest + +/-- Alias constraints encountered throughout Robinson elimination. Every +round records all currently exposed variable/variable constraints before its +first constraint is eliminated, so an earlier grounding substitution cannot +erase an alias that appeared later in that same round. -/ +def aliasTrace : Nat → List (Atom × Atom) → List (VarName × VarName) + | 0, equations => + match decomposeAll equations with + | some constraints => aliasConstraints constraints + | none => [] + | fuel + 1, equations => + match decomposeAll equations with + | none => [] + | some [] => [] + | some ((x, term) :: rest) => + let here := aliasConstraints ((x, term) :: rest) + if Subst.occurs x term then here + else + let sub : Subst := [(x, term)] + let remaining := rest.map fun constraint => + (Subst.apply sub (Atom.var constraint.1), + Subst.apply sub constraint.2) + here ++ aliasTrace fuel remaining + /-- The unification main loop, recursing structurally on `fuel`. Each round fully decomposes the worklist, then eliminates one variable: it substitutes `x ↦ t` into the remaining constraints and records the binding. Because every round removes one distinct variable from the problem, diff --git a/MettaHyperonFull/Minimal/Interpreter.lean b/MettaHyperonFull/Minimal/Interpreter.lean index 30d1b55..40d5bdc 100644 --- a/MettaHyperonFull/Minimal/Interpreter.lean +++ b/MettaHyperonFull/Minimal/Interpreter.lean @@ -475,12 +475,10 @@ def exhaustedPair : Item → Atom × Bindings /-- Extract the result atom of a final item with its bindings applied. -/ def finalAtom (it : Item) : Atom := (finalPair it).1 -/-- Apply `instantiate` to `a` under `b` repeatedly until it reaches a fixpoint, bounded by the - number of bindings (which caps any chain length). A single `instantiate` is one-step because - `Subst.apply` looks a variable up once and does not chase `$x <- $y <- Plato`. Recursive - backchaining needs this: in b2's `(deduce (Evaluation (human $x)))`, the query variable `$x` - is first bound to a rule variable (via the `Implication` match) that only resolves to `Plato` - deeper in the recursion, so `$x` reaches `Plato` only through the chain. -/ +/-- Apply equality-class-aware `instantiate` to `a` under `b` until it reaches a fixpoint, bounded by + the number of bindings. `instantiate` already follows variable chains and compound values; this + bounded wrapper preserves the interpreter's explicit fixpoint contract and rejects cycles by + stabilizing on the unchanged atom. -/ def resolveAtom (b : Bindings) : Nat → Atom → Atom | 0, a => a | n + 1, a => let a' := instantiate b a; if a' == a then a else resolveAtom b n a' diff --git a/MettaHyperonFull/Operational/MinimalCoverage.lean b/MettaHyperonFull/Operational/MinimalCoverage.lean index 35a3553..f9a48e9 100644 --- a/MettaHyperonFull/Operational/MinimalCoverage.lean +++ b/MettaHyperonFull/Operational/MinimalCoverage.lean @@ -52,7 +52,11 @@ example : (Atom.expr [Atom.sym "unify", Atom.sym "a", Atom.var "x", Atom.var "x", Atom.sym "bad"]) = [Atom.sym "a"] := by simp [cfg, emptyCtx, evalMinimal, evalUnifyInstr, matchAtoms, matchAtomsWith, instantiate, - bindingsToSubst, Subst.apply, Subst.occurs, Subst.lookup] + Bindings.resolveAtom, Bindings.resolve, Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, Bindings.classValues, Bindings.eqClassOrdered, + Bindings.eqClass, Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, + Bindings.lookupVal, Bindings.eqRepresentative, List.filterMap, + Subst.occurs, Atom.size] example : evalMinimal cfg emptyCtx diff --git a/MettaHyperonFull/Proofs.lean b/MettaHyperonFull/Proofs.lean index 7da059b..a647f83 100644 --- a/MettaHyperonFull/Proofs.lean +++ b/MettaHyperonFull/Proofs.lean @@ -68,10 +68,10 @@ and that the implementation's optimisations don't change behaviour. Those drive * `Proofs/Substitution.lean`: foundational `Subst.apply` / `instantiate` lemmas: empty-substitution identity, closed atoms are fixed, size monotonicity, and the substitution **composition law** `Subst.apply_compose`. -* `Proofs/SubstitutionAudit.lean`: cyclic substitution audit: one-pass substitution does not chase - `$x <- $y <- $x`; repeated resolution is fuel-bounded and can fail - fuel-stability without an acyclicity side condition - (`cyclicResolve_not_fuel_stable`). +* `Proofs/SubstitutionAudit.lean`: cyclic substitution audit: raw substitution stays one-pass, while + equality-class-aware binding resolution detects longer cycles and + leaves rejected cyclic instantiation fuel-stable + (`cyclicResolve_x_stable`). * `Proofs/Alpha.lean`: α-equivalence is an **equivalence relation**; preserves `Atom.size`; coincides with `=` on variable-free atoms. Documents the Float/IEEE caveat on the Boolean decider. diff --git a/MettaHyperonFull/Proofs/BindingLaws.lean b/MettaHyperonFull/Proofs/BindingLaws.lean index 534874c..103789b 100644 --- a/MettaHyperonFull/Proofs/BindingLaws.lean +++ b/MettaHyperonFull/Proofs/BindingLaws.lean @@ -4,23 +4,33 @@ /- Module: MettaHyperonFull.Proofs.BindingLaws Layer: Proofs -Purpose: Executable binding-merge laws for `Bindings.addVarBinding`, `Bindings.addVarEquality`, and - one-step `Bindings.merge` calls. These are the small merge facts used by matcher and simulation - proofs: fresh variables extend, equal existing values keep the binding set, incompatible values - fail, and unifiable values extend through the unifier boundary. +Purpose: Executable laws for equality-class-aware binding merge, resolution, and instantiation. + The laws cover fresh values, explicit aliases, retained reconciliation constraints, connected + nonlinear classes, incompatible class values, compound resolution, and cycle rejection. Imports: MettaHyperonFull.Proofs.Basic Trusted boundary: none Main exports: Bindings.lookupVal_empty, Bindings.lookupVal_addValRaw_self, - Bindings.addVarBinding_fresh, Bindings.addVarBinding_same, Bindings.addVarBinding_conflict, - Bindings.addVarBinding_unifies, Bindings.merge_empty_right, Bindings.merge_one_val_fresh, - Bindings.merge_one_val_same, Bindings.merge_one_val_conflict, Bindings.merge_one_val_unifies -Open obligations: multi-binding merge associativity/permutation laws are not needed by the current - simulation proofs and should be stated separately if a future proof requires them. + Bindings.addVarBinding_var, Bindings.addVarBinding_fresh, + Bindings.addVarBinding_nochange, Bindings.addVarBinding_reconciles, + Bindings.addVarBinding_secondaryConflict, Bindings.addVarBinding_conflict, + Bindings.seededOverwrite_reconciliation_rejected, + Bindings.addVarEquality_nochange, Bindings.addVarEquality_reconciles, + Bindings.addVarEquality_secondaryConflict, Bindings.addVarEquality_conflict, + Bindings.merge_empty_right, matchAtoms_var_var_equality, + Unify.varBinding_mem_or_mem_aliasTrace_of_unifyRounds, + Unify.varBinding_mem_aliasTrace_of_unifyRounds_empty, + connectedClass_match, connectedClass_instantiation, connectedClass_bindingReadout, + incompatibleClassValues_rejected, compoundClassValue_resolves, compoundCycle_hasLoop +Open obligations: semantic permutation invariance and the general matcher transport theorem live at + the representation-independent conformance layer. -/ import MettaHyperonFull.Proofs.Basic namespace Metta +set_option maxRecDepth 20000 +set_option maxHeartbeats 2000000 + namespace Bindings /-- Looking up any value in the empty binding set fails. -/ @@ -31,87 +41,473 @@ theorem lookupVal_addValRaw_self (b : Bindings) (x : VarName) (v : Atom) : lookupVal (addValRaw b x v) x = some v := by simp [addValRaw, lookupVal] -/-- A fresh value binding extends the binding set. -/ +theorem classValues_eq_nil_of_lookupVal_none {b : Bindings} + (hlookup : ∀ x, lookupVal b x = none) (x : VarName) : + classValues b x = [] := by + simp [classValues, hlookup] + +/-- POSITIVE: permuting normalized direct-value relations does not change the + canonical value view of an equality class. -/ +theorem classValues_value_relation_permutation : + classValues + [BindingRel.val "y" (Atom.sym "B"), + BindingRel.eq "y" "x", + BindingRel.val "x" (Atom.sym "A")] + "x" = + classValues + [BindingRel.val "x" (Atom.sym "A"), + BindingRel.eq "y" "x", + BindingRel.val "y" (Atom.sym "B")] + "x" := by + rfl + +/-- NEGATIVE: duplicate direct values for one key are not normalized; direct + lookup deliberately exposes their order instead of pretending the malformed + inputs are equivalent binding sets. -/ +theorem classValues_duplicate_key_order_visible : + classValues + [BindingRel.val "x" (Atom.sym "A"), + BindingRel.val "x" (Atom.sym "B")] + "x" ≠ + classValues + [BindingRel.val "x" (Atom.sym "B"), + BindingRel.val "x" (Atom.sym "A")] + "x" := by + simp [classValues, eqClassOrdered, eqVarsInOrder, eqClass, eqClassAux, + eqStep, lookupVal] + +/-- A variable-valued binding is represented as an explicit equality. -/ +theorem addVarBinding_var (b : Bindings) (x y : VarName) : + addVarBinding b x (Atom.var y) = addVarEquality b x y := rfl + +/-- A fresh non-variable value extends the binding set. -/ theorem addVarBinding_fresh {b : Bindings} {x : VarName} {v : Atom} - (h : lookupVal b x = none) : + (hclass : classValues b x = []) + (hnotvar : ∀ y, v ≠ Atom.var y) : addVarBinding b x v = [addValRaw b x v] := by - simp [addVarBinding, h] + cases v <;> simp_all [addVarBinding] -/-- Re-adding the same structurally reflexive value keeps the binding set unchanged. -/ -theorem addVarBinding_same {b : Bindings} {x : VarName} {v : Atom} - (hlookup : lookupVal b x = some v) (href : Atom.StructurallyReflexive v) : +/-- A class-local reconciliation that requires no substitution leaves the + existing binding presentation unchanged. -/ +theorem addVarBinding_nochange {b : Bindings} {x : VarName} {v : Atom} + {values : List Atom} + (hnotvar : ∀ y, v ≠ Atom.var y) + (hvalues : classValues b x = values) + (hvaluesNonempty : values ≠ []) + (hunify : unifyValues (values ++ [v]) = some []) : addVarBinding b x v = [b] := by - unfold Atom.StructurallyReflexive at href - have hbeq : (v == v) = true := href - simp [addVarBinding, hlookup, hbeq] - -/-- A conflicting value binding fails when the old and new values are neither equal nor unifiable. -/ -theorem addVarBinding_conflict {b : Bindings} {x : VarName} {v previous : Atom} - (hlookup : lookupVal b x = some previous) - (hneq : (previous == v) = false) - (hunify : Unify.unifyTop previous v = none) : + cases values with + | nil => contradiction + | cons value values => cases v <;> simp_all [addVarBinding] + +/-- A nontrivial class-local reconciliation is accepted only after the same + constraint is reconciled against the complete seeded binding set. -/ +theorem addVarBinding_reconciles {b : Bindings} {x : VarName} {v : Atom} + {values : List Atom} {localHead : VarName × Atom} {localTail sigma : Subst} + (hnotvar : ∀ y, v ≠ Atom.var y) + (hvalues : classValues b x = values) + (hvaluesNonempty : values ≠ []) + (hunify : unifyValues (values ++ [v]) = some (localHead :: localTail)) + (hall : reconcileAll b [(Atom.var x, v)] = some sigma) : + addVarBinding b x v = + [rebuildFromReconciliation b b [(Atom.var x, v)] sigma] := by + cases values with + | nil => contradiction + | cons value values => cases v <;> simp_all [addVarBinding] + +/-- A locally compatible value is rejected when its internal substitution + conflicts with a seeded binding elsewhere in the complete equation set. -/ +theorem addVarBinding_secondaryConflict + {b : Bindings} {x : VarName} {v : Atom} + {values : List Atom} {localHead : VarName × Atom} {localTail : Subst} + (hnotvar : ∀ y, v ≠ Atom.var y) + (hvalues : classValues b x = values) + (hvaluesNonempty : values ≠ []) + (hunify : unifyValues (values ++ [v]) = some (localHead :: localTail)) + (hall : reconcileAll b [(Atom.var x, v)] = none) : addVarBinding b x v = [] := by - simp [addVarBinding, hlookup, hneq, hunify] + cases values with + | nil => contradiction + | cons value values => cases v <;> simp_all [addVarBinding] -/-- Distinct existing and new values may still extend the binding set when unification succeeds. -/ -theorem addVarBinding_unifies {b : Bindings} {x : VarName} {v previous : Atom} {sigma : Subst} - (hlookup : lookupVal b x = some previous) - (hneq : (previous == v) = false) - (hunify : Unify.unifyTop previous v = some sigma) : - addVarBinding b x v = [addValRaw b x v] := by - simp [addVarBinding, hlookup, hneq, hunify] +/-- An incompatible non-variable value is rejected class-wide. -/ +theorem addVarBinding_conflict {b : Bindings} {x : VarName} {v : Atom} + {values : List Atom} + (hnotvar : ∀ y, v ≠ Atom.var y) + (hvalues : classValues b x = values) + (hvaluesNonempty : values ≠ []) + (hunify : unifyValues (values ++ [v]) = none) : + addVarBinding b x v = [] := by + cases v <;> simp_all [addVarBinding] + +/-- NEGATIVE: complete reconciliation rejects a class-local substitution that + would overwrite an existing seeded value through an internal variable. -/ +theorem seededOverwrite_reconciliation_rejected : + addVarBinding + [BindingRel.val "p" (.expr [.sym "f", .var "a"]), + BindingRel.val "a" (.sym "old")] + "p" (.expr [.sym "f", .sym "new"]) = [] := by + simp (config := { maxSteps := 1000000 }) + [addVarBinding, unifyValues, reconcileAll, equations, + relationEquation, equationFuel, classValues, eqClassOrdered, + eqVarsInOrder, eqClass, eqClassAux, eqStep, lookupVal, + Unify.unifyRounds, Unify.decomposeAll, Unify.decomposeEq, + Unify.decomposeList, Subst.occurs, Subst.apply, Subst.lookup, Subst.extend, + Subst.erase, Atom.size] -/-- Equality aliases with equal structurally reflexive values are accepted. -/ -theorem addVarEquality_same {b : Bindings} {x y : VarName} {v : Atom} - (hx : lookupVal b x = some v) - (hy : lookupVal b y = some v) - (href : Atom.StructurallyReflexive v) : +/-- A joined class requiring no substitution retains the explicit new alias. -/ +theorem addVarEquality_nochange {b : Bindings} {x y : VarName} + (h : unifyValues (classValues (addEqRaw b x y) x) = some []) : addVarEquality b x y = [addEqRaw b x y] := by - unfold Atom.StructurallyReflexive at href - have hbeq : (v == v) = true := href - simp [addVarEquality, hx, hy, hbeq] - -/-- Equality aliases with two direct, structurally unequal values fail. -/ -theorem addVarEquality_conflict {b : Bindings} {x y : VarName} {vx vy : Atom} - (hx : lookupVal b x = some vx) - (hy : lookupVal b y = some vy) - (hneq : (vx == vy) = false) : + simp [addVarEquality, h] + +/-- Nontrivial equality-class reconciliation is replayed only after checking + the complete seeded equation system. -/ +theorem addVarEquality_reconciles + {b : Bindings} {x y : VarName} + {localHead : VarName × Atom} {localTail sigma : Subst} + (hlocal : + unifyValues (classValues (addEqRaw b x y) x) = + some (localHead :: localTail)) + (hall : reconcileAll b [(Atom.var x, Atom.var y)] = some sigma) : + addVarEquality b x y = + [rebuildFromReconciliation (addEqRaw b x y) b + [(Atom.var x, Atom.var y)] sigma] := by + simp [addVarEquality, hlocal, hall] + +/-- A locally compatible joined class is rejected when it conflicts with a + seeded binding elsewhere. -/ +theorem addVarEquality_secondaryConflict + {b : Bindings} {x y : VarName} + {localHead : VarName × Atom} {localTail : Subst} + (hlocal : + unifyValues (classValues (addEqRaw b x y) x) = + some (localHead :: localTail)) + (hall : reconcileAll b [(Atom.var x, Atom.var y)] = none) : addVarEquality b x y = [] := by - simp [addVarEquality, hx, hy, hneq] + simp [addVarEquality, hlocal, hall] + +/-- Equality classes whose values cannot unify are rejected. -/ +theorem addVarEquality_conflict {b : Bindings} {x y : VarName} + (h : unifyValues (classValues (addEqRaw b x y) x) = none) : + addVarEquality b x y = [] := by + simp [addVarEquality, h] /-- Merging an empty right-hand binding set is the identity singleton. -/ theorem merge_empty_right (b : Bindings) : merge b [] = [b] := rfl -/-- A one-relation merge with a fresh value binding extends the binding set. -/ -theorem merge_one_val_fresh {b : Bindings} {x : VarName} {v : Atom} - (h : lookupVal b x = none) : - merge b [BindingRel.val x v] = [addValRaw b x v] := by - simp [merge, mergeOne, addVarBinding, h] - -/-- A one-relation merge with the same structurally reflexive value keeps the binding set. -/ -theorem merge_one_val_same {b : Bindings} {x : VarName} {v : Atom} - (hlookup : lookupVal b x = some v) (href : Atom.StructurallyReflexive v) : - merge b [BindingRel.val x v] = [b] := by - unfold Atom.StructurallyReflexive at href - have hbeq : (v == v) = true := href - simp [merge, mergeOne, addVarBinding, hlookup, hbeq] - -/-- A one-relation merge fails when the old and new values are neither equal nor unifiable. -/ -theorem merge_one_val_conflict {b : Bindings} {x : VarName} {v previous : Atom} - (hlookup : lookupVal b x = some previous) - (hneq : (previous == v) = false) - (hunify : Unify.unifyTop previous v = none) : - merge b [BindingRel.val x v] = [] := by - simp [merge, mergeOne, addVarBinding, hlookup, hneq, hunify] - -/-- A one-relation merge extends the binding set when old and new values unify. -/ -theorem merge_one_val_unifies {b : Bindings} {x : VarName} {v previous : Atom} {sigma : Subst} - (hlookup : lookupVal b x = some previous) - (hneq : (previous == v) = false) - (hunify : Unify.unifyTop previous v = some sigma) : - merge b [BindingRel.val x v] = [addValRaw b x v] := by - simp [merge, mergeOne, addVarBinding, hlookup, hneq, hunify] - end Bindings +/-- Decomposing two variable-free atoms can produce no variable constraints. -/ +theorem Unify.decomposeEq_some_eq_nil_of_closed : + ∀ (left right : Atom) (constraints : List (VarName × Atom)), + left.vars = [] → right.vars = [] → + Unify.decomposeEq left right = some constraints → constraints = [] := by + intro left + refine Metta.Atom.recAux ?_ ?_ ?_ ?_ left + · intro symbol right constraints _ hright hdecomp + cases right with + | var v => simp [Atom.vars] at hright + | sym other => + simp [Unify.decomposeEq] at hdecomp + exact hdecomp.2 + | gnd g => simp [Unify.decomposeEq] at hdecomp + | expr xs => simp [Unify.decomposeEq] at hdecomp + · intro v right constraints hleft _ _ + simp [Atom.vars] at hleft + · intro g right constraints _ hright hdecomp + cases right with + | var v => simp [Atom.vars] at hright + | sym symbol => simp [Unify.decomposeEq] at hdecomp + | gnd other => + simp [Unify.decomposeEq] at hdecomp + exact hdecomp.2 + | expr xs => simp [Unify.decomposeEq] at hdecomp + · intro xs ih right constraints hleft hright hdecomp + cases right with + | var v => simp [Atom.vars] at hright + | sym symbol => simp [Unify.decomposeEq] at hdecomp + | gnd ground => simp [Unify.decomposeEq] at hdecomp + | expr ys => + have hxsClosed : ∀ child ∈ xs, child.vars = [] := by + intro child hchild + simp only [Atom.vars] at hleft + rw [List.flatten_eq_nil_iff] at hleft + exact hleft child.vars (List.mem_map_of_mem hchild) + have hysClosed : ∀ child ∈ ys, child.vars = [] := by + intro child hchild + simp only [Atom.vars] at hright + rw [List.flatten_eq_nil_iff] at hright + exact hright child.vars (List.mem_map_of_mem hchild) + have hlist : ∀ (lefts rights : List Atom) constraints, + (∀ child ∈ lefts, child ∈ xs) → + (∀ child ∈ rights, child.vars = []) → + Unify.decomposeList lefts rights = some constraints → constraints = [] := by + intro lefts + induction lefts with + | nil => + intro rights constraints _ _ h + cases rights <;> simp [Unify.decomposeList] at h ⊢ + exact h + | cons head tail ihTail => + intro rights constraints hsubset hrights h + cases rights with + | nil => simp [Unify.decomposeList] at h + | cons rightHead rightTail => + cases hhead : Unify.decomposeEq head rightHead with + | none => simp [Unify.decomposeList, hhead] at h + | some headConstraints => + cases htail : Unify.decomposeList tail rightTail with + | none => simp [Unify.decomposeList, hhead, htail] at h + | some tailConstraints => + simp [Unify.decomposeList, hhead, htail] at h + have hheadNil : headConstraints = [] := + ih head (hsubset head (by simp)) rightHead headConstraints + (hxsClosed head (hsubset head (by simp))) + (hrights rightHead (by simp)) hhead + have htailNil : tailConstraints = [] := + ihTail rightTail tailConstraints + (fun child hchild => hsubset child (by simp [hchild])) + (fun child hchild => hrights child (by simp [hchild])) htail + subst headConstraints + subst tailConstraints + simpa using h + exact hlist xs ys constraints (fun child hchild => hchild) hysClosed hdecomp + +/-- Decomposing a variable-free equation worklist can produce no variable constraints. -/ +theorem Unify.decomposeAll_some_eq_nil_of_closed : + ∀ (equations : List (Atom × Atom)) (constraints : List (VarName × Atom)), + (∀ equation ∈ equations, equation.1.vars = [] ∧ equation.2.vars = []) → + Unify.decomposeAll equations = some constraints → constraints = [] := by + intro equations + induction equations with + | nil => intro constraints _ h; simpa [Unify.decomposeAll] using h + | cons equation rest ih => + intro constraints hclosed hdecomp + cases hhead : Unify.decomposeEq equation.1 equation.2 with + | none => simp [Unify.decomposeAll, hhead] at hdecomp + | some headConstraints => + cases htail : Unify.decomposeAll rest with + | none => simp [Unify.decomposeAll, hhead, htail] at hdecomp + | some tailConstraints => + simp [Unify.decomposeAll, hhead, htail] at hdecomp + have heqClosed := hclosed equation (by simp) + have hheadNil := Unify.decomposeEq_some_eq_nil_of_closed equation.1 equation.2 + headConstraints heqClosed.1 heqClosed.2 hhead + have htailNil := ih tailConstraints + (fun item hitem => hclosed item (by simp [hitem])) htail + subst headConstraints + subst tailConstraints + simpa using hdecomp + +/-- Running unification on a variable-free equation worklist preserves the incoming substitution. -/ +theorem Unify.unifyRounds_some_eq_of_closed (fuel : Nat) (equations : List (Atom × Atom)) + (subst result : Subst) + (hclosed : ∀ equation ∈ equations, equation.1.vars = [] ∧ equation.2.vars = []) + (hresult : Unify.unifyRounds fuel equations subst = some result) : + result = subst := by + cases hdecomp : Unify.decomposeAll equations with + | none => + cases fuel <;> simp [Unify.unifyRounds, hdecomp] at hresult + | some constraints => + have hnil := Unify.decomposeAll_some_eq_nil_of_closed equations constraints hclosed hdecomp + subst constraints + cases fuel <;> simpa [Unify.unifyRounds, hdecomp] using hresult.symm + +/-- Successful reconciliation of variable-free values returns the empty substitution. -/ +theorem Bindings.unifyValues_some_eq_empty_of_closed {values : List Atom} {result : Subst} + (hclosed : ∀ value ∈ values, value.vars = []) + (hresult : Bindings.unifyValues values = some result) : result = [] := by + cases values with + | nil => simpa [Bindings.unifyValues] using hresult.symm + | cons first rest => + cases rest with + | nil => simpa [Bindings.unifyValues] using hresult.symm + | cons second tail => + apply Unify.unifyRounds_some_eq_of_closed + (first.size + ((second :: tail).map Atom.size).sum) + ((second :: tail).map fun value => (first, value)) [] result + · intro equation hequation + rcases List.mem_map.mp hequation with ⟨value, hvalue, rfl⟩ + exact ⟨hclosed first (by simp), hclosed value (by simp [hvalue])⟩ + · simpa [Bindings.unifyValues] using hresult + +/-- Every variable-valued entry in a successful Robinson result is either an +incoming substitution entry or was exposed as an explicit variable/variable +constraint in the alias trace. This is the first half of the reconciliation +trace-completeness dichotomy. -/ +theorem Unify.varBinding_mem_or_mem_aliasTrace_of_unifyRounds + {fuel : Nat} {equations : List (Atom × Atom)} + {subst result : Subst} {x y : VarName} + (hrun : Unify.unifyRounds fuel equations subst = some result) + (hmem : (x, Atom.var y) ∈ result) : + (x, Atom.var y) ∈ subst ∨ (x, y) ∈ Unify.aliasTrace fuel equations := by + induction fuel generalizing equations subst result x y with + | zero => + cases hdecomp : Unify.decomposeAll equations with + | none => simp [Unify.unifyRounds, hdecomp] at hrun + | some constraints => + cases constraints with + | nil => + simp [Unify.unifyRounds, hdecomp] at hrun + subst result + exact Or.inl hmem + | cons constraint rest => + simp [Unify.unifyRounds, hdecomp] at hrun + | succ fuel ih => + cases hdecomp : Unify.decomposeAll equations with + | none => simp [Unify.unifyRounds, hdecomp] at hrun + | some constraints => + cases constraints with + | nil => + simp [Unify.unifyRounds, hdecomp] at hrun + subst result + exact Or.inl hmem + | cons constraint rest => + rcases constraint with ⟨key, term⟩ + cases hoccurs : Subst.occurs key term with + | true => + simp [Unify.unifyRounds, hdecomp, hoccurs] at hrun + | false => + let remaining := rest.map fun item => + (Subst.apply [(key, term)] (Atom.var item.1), + Subst.apply [(key, term)] item.2) + have hrun' : + Unify.unifyRounds fuel remaining + (Subst.extend subst key term) = some result := by + simpa [Unify.unifyRounds, hdecomp, hoccurs, + remaining] using hrun + rcases ih hrun' hmem with hextended | htail + · simp only [Subst.extend, List.mem_cons] at hextended + rcases hextended with hhead | hold + · have hx : x = key := congrArg Prod.fst hhead + have hterm : Atom.var y = term := congrArg Prod.snd hhead + subst key + subst term + exact Or.inr (by + simp [Unify.aliasTrace, hdecomp, hoccurs, + Unify.aliasConstraints]) + · exact Or.inl (List.mem_filter.mp hold).1 + · exact Or.inr (by + simp [Unify.aliasTrace, hdecomp, hoccurs, + remaining, htail]) + +/-- With the empty incoming substitution used by whole-system +reconciliation, every variable-valued result entry belongs to the alias +trace. -/ +theorem Unify.varBinding_mem_aliasTrace_of_unifyRounds_empty + {fuel : Nat} {equations : List (Atom × Atom)} + {result : Subst} {x y : VarName} + (hrun : Unify.unifyRounds fuel equations [] = some result) + (hmem : (x, Atom.var y) ∈ result) : + (x, y) ∈ Unify.aliasTrace fuel equations := by + rcases Unify.varBinding_mem_or_mem_aliasTrace_of_unifyRounds + hrun hmem with h | h + · simp at h + · exact h + +/-- Matching two distinct variables emits an explicit equality relation. -/ +theorem matchAtoms_var_var_equality {x y : VarName} (h : (x == y) = false) : + matchAtoms (Atom.var x) (Atom.var y) = [[BindingRel.eq x y]] := by + simp [matchAtoms, matchAtomsWith, h] + +def connectedClassPattern : Atom := + Atom.expr [Atom.sym "g", Atom.var "p1", Atom.var "p2", Atom.var "p2"] + +def connectedClassQuery : Atom := + Atom.expr [Atom.sym "g", Atom.var "q1", Atom.var "q1", Atom.var "q2"] + +def connectedClassBindings : Bindings := + [BindingRel.eq "p2" "q2", BindingRel.eq "p2" "q1", BindingRel.eq "p1" "q1"] + +/-- POSITIVE: nonlinear matching preserves all three equality edges. -/ +theorem connectedClass_match : + matchAtoms connectedClassPattern connectedClassQuery = [connectedClassBindings] := by + rfl + +/-- POSITIVE: both RHS variables instantiate to one shared representative. -/ +theorem connectedClass_instantiation : + instantiate connectedClassBindings + (Atom.expr [Atom.sym "f", Atom.var "p1", Atom.var "p2"]) = + Atom.expr [Atom.sym "f", Atom.var "q1", Atom.var "q1"] := by + change instantiate + [BindingRel.eq "p2" "q2", BindingRel.eq "p2" "q1", + BindingRel.eq "p1" "q1"] + (Atom.expr [Atom.sym "f", Atom.var "p1", Atom.var "p2"]) = _ + have hlookup : ∀ x, Bindings.lookupVal + [BindingRel.eq "p2" "q2", BindingRel.eq "p2" "q1", + BindingRel.eq "p1" "q1"] x = none := by + intro x + simp [Bindings.lookupVal] + have hclass := Bindings.classValues_eq_nil_of_lookupVal_none hlookup + simp [instantiate, Bindings.resolveAtom, + Bindings.resolve, Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, hclass, Bindings.eqRepresentative, + Bindings.eqClassOrdered, Bindings.eqClass, Bindings.eqClassAux, + Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size] + +/-- POSITIVE: the minimal binding readout observes one equality class. -/ +theorem connectedClass_bindingReadout : + instantiate connectedClassBindings + (Atom.expr [Atom.var "q1", Atom.var "q2"]) = + Atom.expr [Atom.var "q1", Atom.var "q1"] := by + change instantiate + [BindingRel.eq "p2" "q2", BindingRel.eq "p2" "q1", + BindingRel.eq "p1" "q1"] + (Atom.expr [Atom.var "q1", Atom.var "q2"]) = _ + have hlookup : ∀ x, Bindings.lookupVal + [BindingRel.eq "p2" "q2", BindingRel.eq "p2" "q1", + BindingRel.eq "p1" "q1"] x = none := by + intro x + simp [Bindings.lookupVal] + have hclass := Bindings.classValues_eq_nil_of_lookupVal_none hlookup + simp [instantiate, Bindings.resolveAtom, + Bindings.resolve, Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, hclass, Bindings.eqRepresentative, + Bindings.eqClassOrdered, Bindings.eqClass, Bindings.eqClassAux, + Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size] + +/-- NEGATIVE: equating classes with incompatible ground values is rejected. -/ +theorem incompatibleClassValues_rejected : + Bindings.addVarEquality + [BindingRel.val "x" (Atom.sym "A"), BindingRel.val "y" (Atom.sym "B")] + "x" "y" = [] := by + have hclass : + Bindings.classValues + [BindingRel.eq "x" "y", BindingRel.val "x" (Atom.sym "A"), + BindingRel.val "y" (Atom.sym "B")] + "x" = [Atom.sym "B", Atom.sym "A"] := by + rfl + simp [Bindings.addVarEquality, Bindings.addEqRaw, hclass, + Bindings.unifyValues, Unify.unifyRounds, Unify.decomposeAll, + Unify.decomposeEq, Atom.size] + +/-- POSITIVE: resolution descends through variables nested in compound values. -/ +theorem compoundClassValue_resolves : + instantiate + [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "y"]), + BindingRel.val "y" (Atom.sym "A")] + (Atom.var "x") = Atom.expr [Atom.sym "f", Atom.sym "A"] := by + have hclass := Bindings.classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil + (b := [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "y"]), + BindingRel.val "y" (Atom.sym "A")]) (by rfl) + simp [instantiate, Bindings.resolveAtom, Bindings.resolveAtomAux, + Bindings.resolve, Bindings.resolutionFuel, Bindings.relationResolutionFuel, + hclass, Bindings.lookupVal, Bindings.eqRepresentative, + Bindings.eqClassOrdered, Bindings.eqVarsInOrder, Atom.size] + +/-- NEGATIVE: a cycle through a compound value is rejected. -/ +theorem compoundCycle_hasLoop : + Bindings.hasLoop + [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "y"]), + BindingRel.val "y" (Atom.var "x")] = true := by + have hclass := Bindings.classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil + (b := [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "y"]), + BindingRel.val "y" (Atom.var "x")]) (by rfl) + simp (config := { maxSteps := 1000000 }) [Bindings.hasLoop, Bindings.vars, + Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, hclass, Bindings.lookupVal, + Bindings.eqRepresentative, Bindings.eqClassOrdered, + Bindings.eqVarsInOrder, Atom.size, Atom.vars] + end Metta diff --git a/MettaHyperonFull/Proofs/MorkMM2Lowering.lean b/MettaHyperonFull/Proofs/MorkMM2Lowering.lean index 59b3b7d..bc7c1e4 100644 --- a/MettaHyperonFull/Proofs/MorkMM2Lowering.lean +++ b/MettaHyperonFull/Proofs/MorkMM2Lowering.lean @@ -75,12 +75,12 @@ theorem evalSource_equation (space : Space) (row : Bindings) (index : Nat) /-- Inequality keeps a row when the instantiated sides cannot match. -/ theorem evalInequalitySource_different_symbols (row : Bindings) : evalInequalitySource row (Atom.sym "X") (Atom.sym "Y") = [row] := by - simp [evalInequalitySource, instantiate, Subst.apply, matchAtoms, matchAtomsWith] + simp [evalInequalitySource, instantiate, Bindings.resolveAtom, matchAtoms, matchAtomsWith] /-- Inequality rejects a row when the instantiated sides already match. -/ theorem evalInequalitySource_same_symbol (row : Bindings) : evalInequalitySource row (Atom.sym "X") (Atom.sym "X") = [] := by - simp [evalInequalitySource, instantiate, Subst.apply, matchAtoms, matchAtomsWith] + simp [evalInequalitySource, instantiate, Bindings.resolveAtom, matchAtoms, matchAtomsWith] /-- Applying an add effect inserts the instantiated payload into the reference space. -/ theorem applyEffect_add (row : Bindings) (space : Space) (index : Nat) diff --git a/MettaHyperonFull/Proofs/QueryBackend.lean b/MettaHyperonFull/Proofs/QueryBackend.lean index 4d5cbc9..af5c794 100644 --- a/MettaHyperonFull/Proofs/QueryBackend.lean +++ b/MettaHyperonFull/Proofs/QueryBackend.lean @@ -109,7 +109,7 @@ private def edgeBTo : Atom := private theorem match_edgeAto_edgeAB : matchAtoms edgeAto edgeAB = [[BindingRel.val "to" (Atom.sym "b")]] := by simp [edgeAto, edgeAB, matchAtoms, matchAtomsWith, matchAll, Bindings.merge, Bindings.mergeOne, - Bindings.addVarBinding, Bindings.lookupVal, Bindings.addValRaw, Bindings.removeVal, + Bindings.addVarBinding, Bindings.addValRaw, Bindings.removeVal, Subst.occurs] private theorem match_edgeAto_edgeBC : @@ -124,7 +124,7 @@ private theorem edgeAto_rows : private theorem match_edgeAMid_edgeAB : matchAtoms edgeAMid edgeAB = [[BindingRel.val "mid" (Atom.sym "b")]] := by simp [edgeAMid, edgeAB, matchAtoms, matchAtomsWith, matchAll, Bindings.merge, Bindings.mergeOne, - Bindings.addVarBinding, Bindings.lookupVal, Bindings.addValRaw, Bindings.removeVal, + Bindings.addVarBinding, Bindings.addValRaw, Bindings.removeVal, Subst.occurs] private theorem match_edgeAMid_edgeBC : @@ -144,7 +144,7 @@ private theorem match_edgeBTo_edgeAB : private theorem match_edgeBTo_edgeBC : matchAtoms edgeBTo edgeBC = [[BindingRel.val "to" (Atom.sym "c")]] := by simp [edgeBTo, edgeBC, matchAtoms, matchAtomsWith, matchAll, Bindings.merge, Bindings.mergeOne, - Bindings.addVarBinding, Bindings.lookupVal, Bindings.addValRaw, Bindings.removeVal, + Bindings.addVarBinding, Bindings.addValRaw, Bindings.removeVal, Subst.occurs] private theorem edgeBTo_rows : @@ -158,7 +158,18 @@ private theorem empty_merge_mid : private theorem instantiate_mid_row_edgeMidTo : instantiate [BindingRel.val "mid" (Atom.sym "b")] edgeMidTo = edgeBTo := by - simp [instantiate, bindingsToSubst, Subst.apply, Subst.lookup, edgeMidTo, edgeBTo] + have hmid := instantiate_singleton_val_var_of_not_mem "mid" (Atom.sym "b") (by + simp [Atom.vars]) + have hto := instantiate_singleton_val_inert "mid" (Atom.sym "b") + (Atom.var "to") (by simp [Atom.vars]) + unfold edgeMidTo edgeBTo + simp only [instantiate, Bindings.resolveAtom, List.map] + rw [show (Bindings.resolve [BindingRel.val "mid" (Atom.sym "b")] "mid").getD + (Atom.var "mid") = Atom.sym "b" by + simpa [instantiate, Bindings.resolveAtom] using hmid] + rw [show (Bindings.resolve [BindingRel.val "mid" (Atom.sym "b")] "to").getD + (Atom.var "to") = Atom.var "to" by + simpa [instantiate, Bindings.resolveAtom] using hto] private theorem mid_merge_to : Bindings.merge [BindingRel.val "mid" (Atom.sym "b")] [BindingRel.val "to" (Atom.sym "c")] = diff --git a/MettaHyperonFull/Proofs/Substitution.lean b/MettaHyperonFull/Proofs/Substitution.lean index f04bd16..9db0f24 100644 --- a/MettaHyperonFull/Proofs/Substitution.lean +++ b/MettaHyperonFull/Proofs/Substitution.lean @@ -5,9 +5,9 @@ Module: MettaHyperonFull.Proofs.Substitution Layer: Proofs Purpose: Foundational lemmas about Subst.apply (capture-free first-order substitution over Atom) and - instantiate, reused across the metatheory layer. Covers empty-substitution identity, that closed - atoms are fixed, size monotonicity (a variable may be replaced by a larger atom, so size only - grows), and the substitution composition law Subst.apply_compose. + equality-class-aware instantiate, reused across the metatheory layer. Covers empty-substitution + identity, that closed atoms are fixed, size monotonicity (a variable may be replaced by a larger + atom, so size only grows), and the substitution composition law Subst.apply_compose. Imports: MettaHyperonFull.Proofs.Basic Trusted boundary: none (fully proved) Main exports: Subst.apply_nil, instantiate_nil, Subst.apply_of_closed, instantiate_of_closed, @@ -21,7 +21,8 @@ import MettaHyperonFull.Proofs.Basic # Metatheory: substitution and instantiation Foundational lemmas about `Subst.apply` (capture-free first-order substitution over `Atom`) and -`instantiate` (`Subst.apply` of `bindingsToSubst`), reused throughout the metatheory layer. +`instantiate` (recursive resolution through binding equality classes), reused throughout the +metatheory layer. Substitution does **not** preserve `Atom.size`: a variable (size `1`) may be replaced by a larger atom, so the invariant is *monotonicity*: `a.size ≤ (Subst.apply s a).size`. On @@ -44,8 +45,260 @@ theorem Subst.apply_nil (a : Atom) : Subst.apply [] a = a := by /-- Instantiating under the empty binding set is the identity. -/ theorem instantiate_nil (a : Atom) : instantiate [] a = a := by - simp only [instantiate, bindingsToSubst, List.foldr_nil] - exact Subst.apply_nil a + induction a with + | var x => + simp [instantiate, Bindings.resolveAtom, Bindings.resolve, + Bindings.eqClassOrdered, Bindings.eqVarsInOrder] + | expr xs ih => + simp only [instantiate, Bindings.resolveAtom] + congr 1 + have hmap : List.map (Bindings.resolveAtom []) xs = List.map id xs := + List.map_congr_left (fun child hchild => by + simpa [instantiate] using ih child hchild) + simpa using hmap + | _ => simp [instantiate, Bindings.resolveAtom] + +/-- A singleton value binding does not resolve any different variable. -/ +theorem Bindings.resolve_singleton_val_ne {key x : VarName} {value : Atom} + (h : x ≠ key) : + Bindings.resolve [BindingRel.val key value] x = none := by + simp [Bindings.resolve, Bindings.eqClassOrdered, + Bindings.eqClass, Bindings.eqClassAux, Bindings.eqStep, + Bindings.eqVarsInOrder, + Bindings.classValues_singleton_val_ne value h] + +private theorem List.mapM_some_self_of_forall {α : Type} (f : α → Option α) : + ∀ xs : List α, (∀ x ∈ xs, f x = some x) → xs.mapM f = some xs + | [], _ => by simp + | x :: xs, h => by + simp [h x (by simp), List.mapM_some_self_of_forall f xs (fun y hy => h y (by simp [hy]))] + +/-- Recursive binding resolution leaves a variable-free atom unchanged whenever + the supplied fuel exceeds its structural size. -/ +theorem Bindings.resolveAtomAux_of_closed (b : Bindings) : + ∀ (a : Atom) (fuel : Nat) (visited : List VarName), + a.vars = [] → a.size < fuel → + Bindings.resolveAtomAux b fuel visited a = some a := by + refine Metta.Atom.recAux ?_ ?_ ?_ ?_ + · intro s fuel visited _ hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => simp [Bindings.resolveAtomAux] + · intro x fuel visited hclosed _ + simp [Atom.vars] at hclosed + · intro g fuel visited _ hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => simp [Bindings.resolveAtomAux] + · intro xs ih fuel visited hclosed hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => + have hmap : xs.mapM (Bindings.resolveAtomAux b fuel visited) = some xs := by + apply List.mapM_some_self_of_forall + intro child hchild + have hchildClosed : child.vars = [] := by + simp only [Atom.vars] at hclosed + rw [List.flatten_eq_nil_iff] at hclosed + exact hclosed child.vars (List.mem_map_of_mem hchild) + have hchildLe : child.size ≤ (xs.map Atom.size).sum := + List.le_sum_of_mem (List.mem_map.mpr ⟨child, hchild, rfl⟩) + have hchildSize : child.size < fuel := by + simp only [Atom.size] at hsize + omega + exact ih child hchild fuel visited hchildClosed hchildSize + simp [Bindings.resolveAtomAux, hmap] + +/-- With the bound key marked as visited, a singleton binding leaves an atom + that does not mention that key unchanged. -/ +theorem Bindings.resolveAtomAux_singleton_val_inert (key : VarName) (value : Atom) : + ∀ (a : Atom) (fuel : Nat), key ∉ a.vars → a.size < fuel → + Bindings.resolveAtomAux [BindingRel.val key value] fuel [key] a = some a := by + refine Metta.Atom.recAux ?_ ?_ ?_ ?_ + · intro s fuel _ hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => simp [Bindings.resolveAtomAux] + · intro x fuel hnot hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => + have hx : x ≠ key := by + intro h + apply hnot + simpa [Atom.vars] using h.symm + simp [Bindings.resolveAtomAux, + Bindings.eqRepresentative, Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, hx] + · intro g fuel _ hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => simp [Bindings.resolveAtomAux] + · intro xs ih fuel hnot hsize + cases fuel with + | zero => simp [Atom.size] at hsize + | succ fuel => + have hmap : xs.mapM + (Bindings.resolveAtomAux [BindingRel.val key value] fuel [key]) = some xs := by + have hchildren : ∀ child ∈ xs, + Bindings.resolveAtomAux [BindingRel.val key value] fuel [key] child = + some child := by + intro child hchild + have hchildNot : key ∉ child.vars := by + intro hv + apply hnot + simp only [Atom.vars, List.mem_flatten, List.mem_map] + exact ⟨child.vars, ⟨child, hchild, rfl⟩, hv⟩ + have hchildLe : child.size ≤ (xs.map Atom.size).sum := + List.le_sum_of_mem (List.mem_map.mpr ⟨child, hchild, rfl⟩) + have hchildSize : child.size < fuel := by + simp only [Atom.size] at hsize + omega + exact ih child hchild fuel hchildNot hchildSize + exact List.mapM_some_self_of_forall _ xs hchildren + simp [Bindings.resolveAtomAux, hmap] + +/-- Resolving the key of a fresh singleton binding returns its recursively + resolved value, which is the value itself when it does not mention the key. -/ +theorem Bindings.resolve_singleton_val_self_of_not_mem (key : VarName) (value : Atom) + (hnot : key ∉ value.vars) : + Bindings.resolve [BindingRel.val key value] key = some value := by + cases value with + | var x => + have hkx : key ≠ x := by simpa [Atom.vars] using hnot + have hxk : x ≠ key := hkx.symm + simp [Bindings.resolve, + Bindings.resolveAtomAux, Bindings.resolutionFuel, Bindings.relationResolutionFuel, + Bindings.eqRepresentative, Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size, + hxk] + | sym s => + simp [Bindings.resolve, + Bindings.resolveAtomAux, Bindings.resolutionFuel, Bindings.relationResolutionFuel, + Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size] + | gnd g => + simp [Bindings.resolve, + Bindings.resolveAtomAux, Bindings.resolutionFuel, Bindings.relationResolutionFuel, + Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size] + | expr xs => + have hinert := Bindings.resolveAtomAux_singleton_val_inert key (Atom.expr xs) + (Atom.expr xs) ((Atom.expr xs).size + 2) hnot (by omega) + have hinert' : Bindings.resolveAtomAux + [BindingRel.val key (Atom.expr xs)] + (1 + (1 + (Atom.expr xs).size)) [key] (Atom.expr xs) = + some (Atom.expr xs) := by + have hfuel : (Atom.expr xs).size + 2 = + 1 + (1 + (Atom.expr xs).size) := by omega + rw [← hfuel] + exact hinert + have haux : Bindings.resolveAtomAux + [BindingRel.val key (Atom.expr xs)] + (1 + Bindings.relationResolutionFuel + (BindingRel.val key (Atom.expr xs))) [key] (Atom.expr xs) = + some (Atom.expr xs) := by + have hfuel : 1 + (1 + (Atom.expr xs).size) = + 1 + Bindings.relationResolutionFuel + (BindingRel.val key (Atom.expr xs)) := by + simp [Bindings.relationResolutionFuel] + omega + rw [← hfuel] + exact hinert' + simp [Bindings.resolve, + Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size, + haux] + +/-- Instantiating a variable under a fresh singleton value binding returns that value. -/ +theorem instantiate_singleton_val_var_of_not_mem (key : VarName) (value : Atom) + (hnot : key ∉ value.vars) : + instantiate [BindingRel.val key value] (Atom.var key) = value := by + simp [instantiate, Bindings.resolveAtom, + Bindings.resolve_singleton_val_self_of_not_mem key value hnot] + +/-- At any positive fuel, a singleton value binding's resolver leaves every + different variable untouched. -/ +theorem Bindings.resolveAtomAux_singleton_val_unbound (key : VarName) (value : Atom) + {x : VarName} (h : x ≠ key) (fuel : Nat) (hfuel : 0 < fuel) : + Bindings.resolveAtomAux [BindingRel.val key value] fuel [] (Atom.var x) = + some (Atom.var x) := by + cases fuel with + | zero => omega + | succ fuel => + simp [Bindings.resolveAtomAux, + Bindings.eqRepresentative, Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, + Bindings.classValues_singleton_val_ne value h] + +/-- A singleton value binding whose key is absent from its value has no direct + or recursive dependency loop. -/ +theorem Bindings.hasLoop_singleton_val_of_not_mem (key : VarName) (value : Atom) + (hnot : key ∉ value.vars) : + Bindings.hasLoop [BindingRel.val key value] = false := by + let direct : Bool := [BindingRel.val key value].any fun r => + match r with + | BindingRel.val x (Atom.var y) => x == y + | BindingRel.eq x y => x == y + | _ => false + have hdirect : direct = false := by + cases value with + | var x => + have hkx : key ≠ x := by simpa [Atom.vars] using hnot + simp [direct, hkx] + | sym _ => simp [direct] + | gnd _ => simp [direct] + | expr _ => simp [direct] + have hkey : Bindings.resolveAtomAux [BindingRel.val key value] + (Bindings.resolutionFuel [BindingRel.val key value] (Atom.var key)) [] + (Atom.var key) = some value := by + have hresolve := Bindings.resolve_singleton_val_self_of_not_mem key value hnot + simpa [Bindings.resolve, Bindings.eqClassOrdered, Bindings.eqVarsInOrder, + Bindings.eqClass, Bindings.eqClassAux, + Bindings.eqStep] using hresolve + unfold Bindings.hasLoop + change (direct || + (Bindings.vars [BindingRel.val key value]).any fun x => + (Bindings.resolveAtomAux [BindingRel.val key value] + (Bindings.resolutionFuel [BindingRel.val key value] (Atom.var x)) [] + (Atom.var x)).isNone) = false + rw [hdirect, Bool.false_or, List.any_eq_false] + intro x _hx + by_cases hx : x = key + · subst x + simp [hkey] + · have hunbound := Bindings.resolveAtomAux_singleton_val_unbound key value hx + (Bindings.resolutionFuel [BindingRel.val key value] (Atom.var x)) (by + simp [Bindings.resolutionFuel]) + simp [hunbound] + +/-- A singleton value binding is inert on atoms that do not mention its key. -/ +theorem instantiate_singleton_val_inert (key : VarName) (value : Atom) : + ∀ a : Atom, key ∉ a.vars → instantiate [BindingRel.val key value] a = a := by + refine Metta.Atom.recAux ?_ ?_ ?_ ?_ + · intro s _ + simp [instantiate, Bindings.resolveAtom] + · intro x hnot + have hx : x ≠ key := by + intro h + apply hnot + simpa [Atom.vars] using h.symm + simp [instantiate, Bindings.resolveAtom, Bindings.resolve_singleton_val_ne hx] + · intro g _ + simp [instantiate, Bindings.resolveAtom] + · intro xs ih hnot + simp only [instantiate, Bindings.resolveAtom] + congr 1 + have hmap : List.map (Bindings.resolveAtom [BindingRel.val key value]) xs = + List.map id xs := List.map_congr_left (fun child hchild => by + have hchildNot : key ∉ child.vars := by + intro hv + apply hnot + simp only [Atom.vars, List.mem_flatten, List.mem_map] + exact ⟨child.vars, ⟨child, hchild, rfl⟩, hv⟩ + simpa [instantiate] using ih child hchild hchildNot) + simpa using hmap /-- A variable-free atom is fixed by every substitution. -/ theorem Subst.apply_of_closed (s : Subst) : ∀ a : Atom, a.vars = [] → Subst.apply s a = a := by @@ -64,8 +317,20 @@ theorem Subst.apply_of_closed (s : Subst) : ∀ a : Atom, a.vars = [] → Subst. /-- A variable-free atom is fixed by every `instantiate`. -/ theorem instantiate_of_closed (b : Bindings) (a : Atom) (h : a.vars = []) : - instantiate b a = a := - Subst.apply_of_closed _ a h + instantiate b a = a := by + induction a with + | var x => simp [Atom.vars] at h + | expr xs ih => + simp only [Atom.vars] at h + rw [List.flatten_eq_nil_iff] at h + simp only [instantiate, Bindings.resolveAtom] + congr 1 + have hmap : List.map (Bindings.resolveAtom b) xs = List.map id xs := + List.map_congr_left (fun child hchild => by + simpa [instantiate] using + ih child hchild (h child.vars (List.mem_map_of_mem hchild))) + simpa using hmap + | _ => simp [instantiate, Bindings.resolveAtom] /-- Substitution can only grow an atom: `Atom.size` is monotone under `Subst.apply` (a variable may be replaced by a strictly larger atom, never a smaller one). -/ @@ -80,9 +345,69 @@ theorem Subst.apply_size_le (s : Subst) (a : Atom) : a.size ≤ (Subst.apply s a omega | _ => simp [Subst.apply, Atom.size] -/-- `Atom.size` is monotone under `instantiate`. -/ -theorem instantiate_size_le (b : Bindings) (a : Atom) : a.size ≤ (instantiate b a).size := - Subst.apply_size_le _ a +/-- Successful recursive binding resolution can only grow an atom. -/ +theorem Bindings.resolveAtomAux_size_le (b : Bindings) (fuel : Nat) + (visited : List VarName) (a resolved : Atom) + (h : Bindings.resolveAtomAux b fuel visited a = some resolved) : + a.size ≤ resolved.size := by + induction fuel generalizing visited a resolved with + | zero => simp [Bindings.resolveAtomAux] at h + | succ fuel ih => + cases a with + | var x => simpa [Atom.size] using Atom.one_le_size resolved + | sym s => + simp [Bindings.resolveAtomAux] at h + subst resolved + exact Nat.le_refl _ + | gnd g => + simp [Bindings.resolveAtomAux] at h + subst resolved + exact Nat.le_refl _ + | expr xs => + simp only [Bindings.resolveAtomAux] at h + cases hm : xs.mapM (Bindings.resolveAtomAux b fuel visited) with + | none => simp [hm] at h + | some ys => + simp [hm] at h + subst resolved + simp only [Atom.size, Nat.add_le_add_iff_left] + have hmap : ∀ (as bs : List Atom), + as.mapM (Bindings.resolveAtomAux b fuel visited) = some bs → + (as.map Atom.size).sum ≤ (bs.map Atom.size).sum := by + intro as + induction as with + | nil => + intro bs hbs + simp at hbs + subst bs + simp + | cons head tail iht => + intro bs hbs + simp only [List.mapM_cons] at hbs + cases hh : Bindings.resolveAtomAux b fuel visited head with + | none => simp [hh] at hbs + | some head' => + cases ht : tail.mapM (Bindings.resolveAtomAux b fuel visited) with + | none => simp [hh, ht] at hbs + | some tail' => + simp [hh, ht] at hbs + subst bs + simp only [List.map_cons, List.sum_cons] + exact Nat.add_le_add (ih visited head head' hh) (iht tail' ht) + exact hmap xs ys hm + +/-- `Atom.size` is monotone under equality-class-aware `instantiate`. -/ +theorem instantiate_size_le (b : Bindings) (a : Atom) : a.size ≤ (instantiate b a).size := by + induction a with + | var x => simp only [instantiate, Bindings.resolveAtom, Atom.size]; exact Atom.one_le_size _ + | expr xs ih => + simp only [instantiate, Bindings.resolveAtom, Atom.size] + have hsum : (xs.map Atom.size).sum ≤ + ((xs.map (Bindings.resolveAtom b)).map Atom.size).sum := by + rw [List.map_map] + exact List.sum_le_sum (fun x hx => ih x hx) + omega + | _ => simp [instantiate, Bindings.resolveAtom, Atom.size] /-- Lookup in a concatenated substitution consults the left one first. -/ theorem Subst.lookup_append (s₁ s₂ : Subst) (x : VarName) : diff --git a/MettaHyperonFull/Proofs/SubstitutionAudit.lean b/MettaHyperonFull/Proofs/SubstitutionAudit.lean index f7380dc..c2e3069 100644 --- a/MettaHyperonFull/Proofs/SubstitutionAudit.lean +++ b/MettaHyperonFull/Proofs/SubstitutionAudit.lean @@ -4,16 +4,15 @@ /- Module: MettaHyperonFull.Proofs.SubstitutionAudit Layer: Proofs -Purpose: Audit lemmas for cyclic substitutions and bindings. The core substitution is one-pass and - has no fuel parameter. The recursive resolver used by the interpreter is deliberately bounded, and - cyclic binding chains are not fuel-stable without an acyclicity or closed-codomain side condition. +Purpose: Audit lemmas for cyclic substitutions and bindings. Raw substitution remains one-pass, + while equality-class-aware binding resolution detects longer dependency cycles, leaves cyclic + instantiation unchanged, and makes the interpreter's bounded resolver fuel-stable on rejection. Imports: MettaHyperonFull.Proofs.Substitution Trusted boundary: none Main exports: cyclicSubstXY, cyclicBindingsXY, cyclicSubst_apply_x_once, - cyclicSubst_apply_x_twice, cyclicBindingsXY_not_direct_loop, cyclicResolve_x_one, - cyclicResolve_x_two, cyclicResolve_not_fuel_stable -Open obligations: add a positive acyclicity theorem if a future proof needs fuel-stability rather - than this explicit counterexample. + cyclicSubst_apply_x_twice, cyclicBindingsXY_hasLoop, cyclicBindingsXY_instantiate_x, + cyclicResolve_x_stable +Open obligations: none -/ import MettaHyperonFull.Proofs.Substitution @@ -41,10 +40,22 @@ theorem cyclicSubst_apply_x_twice : Subst.apply cyclicSubstXY (Subst.apply cyclicSubstXY (Atom.var "x")) = Atom.var "x" := by simp [cyclicSubstXY, Subst.apply, Subst.lookup] -/-- `Bindings.hasLoop` rejects direct self-loops, not longer cycles. Longer cycles need a separate - acyclicity invariant when a theorem needs fuel-stability. -/ -theorem cyclicBindingsXY_not_direct_loop : Bindings.hasLoop cyclicBindingsXY = false := by - simp [cyclicBindingsXY, Bindings.hasLoop] +/-- Equality-class-aware loop detection rejects a two-variable dependency cycle. -/ +theorem cyclicBindingsXY_hasLoop : Bindings.hasLoop cyclicBindingsXY = true := by + have hxy : ("x" == "y") = false := by decide + have hyx : ("y" == "x") = false := by decide + change Bindings.hasLoop + [BindingRel.val "x" (Atom.var "y"), + BindingRel.val "y" (Atom.var "x")] = true + have hclass := Bindings.classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil + (b := [BindingRel.val "x" (Atom.var "y"), + BindingRel.val "y" (Atom.var "x")]) (by rfl) + simp (config := { maxSteps := 1000000 }) [Bindings.hasLoop, + Bindings.vars, Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, hclass, Bindings.lookupVal, + Bindings.eqRepresentative, Bindings.eqClassOrdered, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size, Atom.vars, + hxy, hyx] theorem directValueLoop_hasLoop : Bindings.hasLoop [BindingRel.val "x" (Atom.var "x")] = true := by @@ -54,28 +65,30 @@ theorem directAliasLoop_hasLoop : Bindings.hasLoop [BindingRel.eq "x" "x"] = true := by simp [Bindings.hasLoop] -theorem cyclicResolve_x_zero : - resolveAtom cyclicBindingsXY 0 (Atom.var "x") = Atom.var "x" := by - rfl +/-- A rejected cyclic binding does not partially instantiate its input. -/ +theorem cyclicBindingsXY_instantiate_x : + instantiate cyclicBindingsXY (Atom.var "x") = Atom.var "x" := by + change instantiate + [BindingRel.val "x" (Atom.var "y"), + BindingRel.val "y" (Atom.var "x")] + (Atom.var "x") = Atom.var "x" + have hclass := Bindings.classValues_eq_lookupVal_toList_of_eqVarsInOrder_nil + (b := [BindingRel.val "x" (Atom.var "y"), + BindingRel.val "y" (Atom.var "x")]) (by rfl) + simp (config := { maxSteps := 1000000 }) [instantiate, + Bindings.resolveAtom, Bindings.resolve, Bindings.resolveAtomAux, Bindings.resolutionFuel, + Bindings.relationResolutionFuel, hclass, Bindings.lookupVal, + Bindings.eqClassOrdered, + Bindings.eqClass, Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, + Atom.size] -theorem cyclicResolve_x_one : - resolveAtom cyclicBindingsXY 1 (Atom.var "x") = Atom.var "y" := by - have hyx : (Atom.var "y" == Atom.var "x") = false := by - decide - simp [resolveAtom, cyclicBindingsXY, instantiate, bindingsToSubst, Subst.apply, Subst.lookup, hyx] - -theorem cyclicResolve_x_two : - resolveAtom cyclicBindingsXY 2 (Atom.var "x") = Atom.var "x" := by - have hyx : (Atom.var "y" == Atom.var "x") = false := by - decide - have hxy : (Atom.var "x" == Atom.var "y") = false := by - decide - simp [resolveAtom, cyclicBindingsXY, instantiate, bindingsToSubst, Subst.apply, Subst.lookup, hyx, - hxy] - -theorem cyclicResolve_not_fuel_stable : - resolveAtom cyclicBindingsXY 1 (Atom.var "x") ≠ - resolveAtom cyclicBindingsXY 2 (Atom.var "x") := by - simp [cyclicResolve_x_one, cyclicResolve_x_two] +/-- Once a cycle is rejected, every fuel bound gives the same unchanged result. -/ +theorem cyclicResolve_x_stable (fuel : Nat) : + resolveAtom cyclicBindingsXY fuel (Atom.var "x") = Atom.var "x" := by + cases fuel with + | zero => rfl + | succ fuel => + simp only [resolveAtom, cyclicBindingsXY_instantiate_x] + rw [if_pos (by decide)] end Metta diff --git a/book/Docs/Appendices.lean b/book/Docs/Appendices.lean index 763f32c..daa4c18 100644 --- a/book/Docs/Appendices.lean +++ b/book/Docs/Appendices.lean @@ -61,12 +61,12 @@ Every theorem named here is checked by Lean's kernel in `MettaHyperonFull/Proofs * *Substitution laws and cycle audits* used by binding propagation and preservation: `Subst.apply_compose` (`Proofs/Substitution.lean`), plus `cyclicSubst_apply_x_once`, `cyclicSubst_apply_x_twice`, - `cyclicBindingsXY_not_direct_loop`, and `cyclicResolve_not_fuel_stable` + `cyclicBindingsXY_hasLoop`, and `cyclicResolve_x_stable` (`Proofs/SubstitutionAudit.lean`). - * *Binding merge laws* expose fresh, same-value, conflict, and unification-mediated direct-binding - cases: `Bindings.addVarBinding_fresh`, `Bindings.addVarBinding_same`, - `Bindings.addVarBinding_conflict`, `Bindings.addVarBinding_unifies`, - `Bindings.merge_one_val_fresh`, and `Bindings.merge_one_val_conflict` + * *Binding merge laws* expose fresh values, explicit aliases, class-wide conflict and + unification-mediated reconciliation: `Bindings.addVarBinding_fresh`, + `Bindings.addVarBinding_reconciles`, `Bindings.addVarBinding_conflict`, + `Bindings.addVarEquality_reconciles`, and `Bindings.addVarEquality_conflict` (`Proofs/BindingLaws.lean`). * *Atomspace and world visibility laws* state the executable list-backed insert, query, remove, type-assignment, equality-rule, named-space, state-cell, token, `&self`, and hidden-import facts: From 8614cd16ad2586e225f94326f9a35034fc90b6d4 Mon Sep 17 00:00:00 2001 From: Zarathustra Goertzel Date: Thu, 16 Jul 2026 17:04:35 +0200 Subject: [PATCH 3/3] Preserve transient collision aliases during reconciliation --- MettaHyperonFull/Core/Matching.lean | 12 +-- MettaHyperonFull/Proofs/BindingLaws.lean | 104 +++++++++++++++++++++++ 2 files changed, 111 insertions(+), 5 deletions(-) diff --git a/MettaHyperonFull/Core/Matching.lean b/MettaHyperonFull/Core/Matching.lean index ffecd95..e203646 100644 --- a/MettaHyperonFull/Core/Matching.lean +++ b/MettaHyperonFull/Core/Matching.lean @@ -83,14 +83,16 @@ def rebuildFromSubst (b : Bindings) (sigma : Subst) : Bindings := equalitySkeleton b ++ ofSubst sigma /-- Every explicit variable alias encountered by whole-system reconciliation. -The caller invokes this only after `reconcileAll` succeeds, so the successful -unification run certifies every traced constraint; no representative-oriented -substitution image is used to decide semantic class membership. -/ +The primary trace preserves the successful run's elimination order. The +collision-first trace exposes aliases inside newly joined compound values +before seeded ground equations can normalize them away. -/ def reconciliationAliases (b : Bindings) (extra : List (Atom × Atom)) (_sigma : Subst) : List (VarName × VarName) := - let work := equations b ++ extra - Unify.aliasTrace (equationFuel work) work + let primary := equations b ++ extra + let collisionFirst := extra ++ equations b + Unify.aliasTrace (equationFuel primary) primary ++ + Unify.aliasTrace (equationFuel collisionFirst) collisionFirst /-- Insert one alias only when its equality class is not already represented. This makes alias restoration conservative on existing normalized outputs. -/ diff --git a/MettaHyperonFull/Proofs/BindingLaws.lean b/MettaHyperonFull/Proofs/BindingLaws.lean index 103789b..1ee5392 100644 --- a/MettaHyperonFull/Proofs/BindingLaws.lean +++ b/MettaHyperonFull/Proofs/BindingLaws.lean @@ -20,6 +20,9 @@ Main exports: Bindings.lookupVal_empty, Bindings.lookupVal_addValRaw_self, Unify.varBinding_mem_or_mem_aliasTrace_of_unifyRounds, Unify.varBinding_mem_aliasTrace_of_unifyRounds_empty, connectedClass_match, connectedClass_instantiation, connectedClass_bindingReadout, + transientCollision_innerAlias_retained, + transientCollision_permutation_innerAlias_retained, + transientCollision_incompatible_rejected, incompatibleClassValues_rejected, compoundClassValue_resolves, compoundCycle_hasLoop Open obligations: semantic permutation invariance and the general matcher transport theorem live at the representation-independent conformance layer. @@ -467,6 +470,107 @@ theorem connectedClass_bindingReadout : Bindings.eqClassOrdered, Bindings.eqClass, Bindings.eqClassAux, Bindings.eqStep, Bindings.eqVarsInOrder, Atom.size] +/-- Seed whose two compound values collide only after `x` and `y` are joined. +The intervening ground relations previously caused the inner `u = v` alias to +disappear from the reconciliation trace. -/ +def transientCollisionSeed : Bindings := + [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "u"]), + BindingRel.val "u" (Atom.sym "a"), + BindingRel.val "y" (Atom.expr [Atom.sym "f", Atom.var "v"]), + BindingRel.val "v" (Atom.sym "a")] + +private def transientCollisionOutput : Bindings := + [BindingRel.eq "u" "v", BindingRel.eq "x" "y", + BindingRel.val "v" (Atom.sym "a"), + BindingRel.val "y" (Atom.expr [Atom.sym "f", Atom.var "v"]), + BindingRel.val "u" (Atom.sym "a"), + BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "u"])] + +private theorem transientCollision_addVarEquality_eq : + Bindings.addVarEquality transientCollisionSeed "x" "y" = + [transientCollisionOutput] := by + simp (config := { maxSteps := 1000000 }) + [transientCollisionSeed, transientCollisionOutput, + Bindings.addVarEquality, Bindings.addEqRaw, Bindings.classValues, + Bindings.eqClassOrdered, Bindings.eqVarsInOrder, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.lookupVal, + Bindings.unifyValues, Bindings.reconcileAll, Bindings.equations, + Bindings.relationEquation, Bindings.equationFuel, + Bindings.rebuildFromReconciliation, Bindings.rebuildFromSubst, + Bindings.reconciliationAliases, Bindings.restoreAlias, + Bindings.equalitySkeleton, Bindings.ofSubst, + Unify.unifyRounds, Unify.decomposeAll, Unify.decomposeEq, + Unify.decomposeList, Unify.aliasTrace, Unify.aliasConstraints, + Subst.occurs, Subst.apply, Subst.lookup, Subst.extend, Subst.erase, + Atom.size] + +/-- POSITIVE: collision reconciliation retains the inner alias exposed by +matching `f(u)` with `f(v)`, even when ground relations intervene in the seed. -/ +theorem transientCollision_innerAlias_retained : + (Bindings.addVarEquality transientCollisionSeed "x" "y").map + (fun out => Bindings.eqClass out "u") = [["u", "v"]] := by + rw [transientCollision_addVarEquality_eq] + decide + +/-- The same collision with direct values grouped in a different relation +order. Both chronology variants retain the inner alias class. -/ +def transientCollisionPermutationSeed : Bindings := + [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "u"]), + BindingRel.val "y" (Atom.expr [Atom.sym "f", Atom.var "v"]), + BindingRel.val "u" (Atom.sym "a"), + BindingRel.val "v" (Atom.sym "a")] + +private def transientCollisionPermutationOutput : Bindings := + [BindingRel.eq "v" "u", BindingRel.eq "x" "y", + BindingRel.val "v" (Atom.sym "a"), + BindingRel.val "u" (Atom.sym "a"), + BindingRel.val "y" (Atom.expr [Atom.sym "f", Atom.var "v"]), + BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "u"])] + +private theorem transientCollisionPermutation_addVarEquality_eq : + Bindings.addVarEquality transientCollisionPermutationSeed "x" "y" = + [transientCollisionPermutationOutput] := by + simp (config := { maxSteps := 1000000 }) + [transientCollisionPermutationSeed, transientCollisionPermutationOutput, + Bindings.addVarEquality, Bindings.addEqRaw, Bindings.classValues, + Bindings.eqClassOrdered, Bindings.eqVarsInOrder, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.lookupVal, + Bindings.unifyValues, Bindings.reconcileAll, Bindings.equations, + Bindings.relationEquation, Bindings.equationFuel, + Bindings.rebuildFromReconciliation, Bindings.rebuildFromSubst, + Bindings.reconciliationAliases, Bindings.restoreAlias, + Bindings.equalitySkeleton, Bindings.ofSubst, + Unify.unifyRounds, Unify.decomposeAll, Unify.decomposeEq, + Unify.decomposeList, Unify.aliasTrace, Unify.aliasConstraints, + Subst.occurs, Subst.apply, Subst.lookup, Subst.extend, Subst.erase, + Atom.size] + +/-- POSITIVE: the alternate relation order has the same repaired inner class. -/ +theorem transientCollision_permutation_innerAlias_retained : + (Bindings.addVarEquality transientCollisionPermutationSeed "x" "y").map + (fun out => Bindings.eqClass out "u") = [["u", "v"]] := by + rw [transientCollisionPermutation_addVarEquality_eq] + decide + +/-- NEGATIVE: exposing the inner collision alias does not make incompatible +ground values acceptable. Complete reconciliation still rejects the join. -/ +theorem transientCollision_incompatible_rejected : + Bindings.addVarEquality + [BindingRel.val "x" (Atom.expr [Atom.sym "f", Atom.var "u"]), + BindingRel.val "u" (Atom.sym "a"), + BindingRel.val "y" (Atom.expr [Atom.sym "f", Atom.var "v"]), + BindingRel.val "v" (Atom.sym "b")] + "x" "y" = [] := by + simp (config := { maxSteps := 1000000 }) + [Bindings.addVarEquality, Bindings.addEqRaw, Bindings.classValues, + Bindings.eqClassOrdered, Bindings.eqVarsInOrder, Bindings.eqClass, + Bindings.eqClassAux, Bindings.eqStep, Bindings.lookupVal, + Bindings.unifyValues, Bindings.reconcileAll, Bindings.equations, + Bindings.relationEquation, Bindings.equationFuel, + Unify.unifyRounds, Unify.decomposeAll, Unify.decomposeEq, + Unify.decomposeList, Subst.occurs, Subst.apply, Subst.lookup, + Subst.extend, Subst.erase, Atom.size] + /-- NEGATIVE: equating classes with incompatible ground values is rejected. -/ theorem incompatibleClassValues_rejected : Bindings.addVarEquality