algebraic identities of plus and times discharge symbolically

4 files changed, 79 insertions, 12 deletions

diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org
index c81b58a..eda5429 100644
--- a/docs/core-design-and-pipeline.org
+++ b/docs/core-design-and-pipeline.org
@@ -117,14 +117,15 @@ two of the ladder in decision 10:
 - interval propagation over residue: contradictions fail, finite
   integer ranges enumerate;
 - symbolic discharge, first fragment: universals over infinite
-  domains decided by kind inclusion and interval entailment, with
-  refutations backed by counterexamples.
-
-Not yet present: symbolic discharge beyond the interval fragment
-(algebraic identities of relations, arithmetic decrease measures)
-and Rocq certificates as admission evidence. Each arrives as a
-strengthening of admission or planning; none changes the semantics
-of what is already admitted.
+  domains decided by kind inclusion, interval entailment, and the
+  unit identities of the numeric relations, with refutations backed
+  by counterexamples.
+
+Not yet present: symbolic discharge beyond that fragment (richer
+algebraic theories, arithmetic decrease measures) and Rocq
+certificates as admission evidence. Each arrives as a strengthening
+of admission or planning; none changes the semantics of what is
+already admitted.
 
 * What embedding means
 
diff --git a/docs/vm.org b/docs/vm.org
index a51b85a..d678acd 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -106,8 +106,11 @@ engine decides entailment algebraically. Every natural is at least
 zero: proven. Not every integer is: refuted, and the refutation is
 backed by a concrete counterexample. Every integer is a rational:
 proven, which is decision 12's subtype inclusion decided
-symbolically. A universal outside that fragment is a non total plan,
-rejected, as decision 10 requires.
+symbolically. The unit identities of the numeric relations discharge
+too: =[Plus left: X right: 0 result: X]= holds over all integers by
+the algebra of =Plus=, in the flat membership form of decision 14,
+and fails over strings, which do not add. A universal outside that
+fragment is a non total plan, rejected, as decision 10 requires.
 
 * Membership criteria as domains
 
diff --git a/lib/vm.ml b/lib/vm.ml
index 8a09f3f..4a11c4d 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -110,6 +110,7 @@ module Make (W : World.WORLD) = struct
     let value_l = forced_label "value"
     let left_l = forced_label "left"
     let right_l = forced_label "right"
+    let result_l = forced_label "result"
 
     type bound = { value : Q.t; strict : bool }
 
@@ -249,11 +250,20 @@ module Make (W : World.WORLD) = struct
       is_int : bool;  (** members are integers *)
       is_str : bool;
       has_domain : bool;  (** some domain goal declared the kind *)
+      needs_num : bool;  (** the body demands a numeric member *)
       lower : Propagate.bound option;
       upper : Propagate.bound option;
     }
 
-    let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None }
+    let free =
+      {
+        is_int = false;
+        is_str = false;
+        has_domain = false;
+        needs_num = false;
+        lower = None;
+        upper = None;
+      }
 
     (* One goal read as a constraint on [var]; None = outside the
        fragment. Goals without variables evaluate outright. *)
@@ -334,6 +344,42 @@ module Make (W : World.WORLD) = struct
                 (with_bound (not less)
                    { Propagate.value = Option.get (Propagate.numeric_value g); strict })
           | _ -> None)
+      | ("Plus" | "Times"), _, Some l, Some r -> (
+          (* The algebraic identities of the numeric relations:
+             membership statements that hold for every numeric
+             member, so a numeric quantifier discharges them and a
+             string quantifier refutes them. Anything beyond the
+             identities stays outside the fragment. *)
+          let result = Label.Map.find_opt Propagate.result_l bindings in
+          let is_zero = function
+            | Pattern.Integer z -> Z.equal z Z.zero
+            | _ -> false
+          and is_one = function
+            | Pattern.Integer z -> Z.equal z Z.one
+            | _ -> false
+          in
+          let identity =
+            match (name, l, r, result) with
+            | "Plus", v, unit_, Some v' when is_var v && is_zero unit_ && is_var v' ->
+                true
+            | "Plus", unit_, v, Some v' when is_var v && is_zero unit_ && is_var v' ->
+                true
+            | "Times", v, unit_, Some v' when is_var v && is_one unit_ && is_var v' ->
+                true
+            | "Times", unit_, v, Some v' when is_var v && is_one unit_ && is_var v' ->
+                true
+            | "Times", v, zero, Some zero' when is_var v && is_zero zero && is_zero zero'
+              ->
+                true
+            | "Times", zero, v, Some zero' when is_var v && is_zero zero && is_zero zero'
+              ->
+                true
+            | _ -> false
+          in
+          if identity then Some (`Side { side with needs_num = true })
+          else if Label.Map.for_all (fun _ p -> Pattern.vars p = []) bindings then
+            ground_goal ()
+          else None)
       | _, _, _, _ ->
           if
             Label.Map.for_all
@@ -396,7 +442,8 @@ module Make (W : World.WORLD) = struct
 
     let entails q b =
       if q.is_str then
-        if b.is_int || b.lower <> None || b.upper <> None then `Fails
+        if b.is_int || b.needs_num || b.lower <> None || b.upper <> None then
+          `Fails
         else `Holds
       else if b.is_str then `Fails
       else if b.is_int && (not q.is_int) && not (single_integer_point q) then
diff --git a/test/test_vm.ml b/test/test_vm.ml
index 16ca63c..4729841 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -292,6 +292,20 @@ let test_symbolic_interval_entailment () =
     (holds
        {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |})
 
+let test_symbolic_algebraic_identity () =
+  (* The specification's flagship symbolic example, in the flat
+     membership form of decision 14. *)
+  Alcotest.(check bool) "adding zero is the identity, over all integers" true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Plus left: X right: 0 result: X]] |});
+  Alcotest.(check bool) "multiplying by one is the identity, over all rationals"
+    true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Times left: 1 right: X result: X]] |});
+  Alcotest.(check bool) "strings do not add" false
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [String value: X] body: [Plus left: X right: 0 result: X]] |})
+
 let test_forall_outside_fragment_still_rejected () =
   match
     load
@@ -489,6 +503,8 @@ let () =
           Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion;
           Alcotest.test_case "interval entailment" `Quick
             test_symbolic_interval_entailment;
+          Alcotest.test_case "algebraic identity" `Quick
+            test_symbolic_algebraic_identity;
           Alcotest.test_case "outside fragment still rejected" `Quick
             test_forall_outside_fragment_still_rejected;
         ] );