nx_arith.nx source

1// nx_arith.nx -- arithmetic Term substrate. 2// 3// Closes the named blocker for proof-by-induction / combinatorial / 4// arithmetic Wiedijk theorems. Per user 2026-05-15: "no losses". 5// 6// Provides: 7// - nat constructors: zero, succ(n), plus(a,b), mult(a,b) 8// - nat literal builder for any concrete N 9// - Peano axioms emitted as v2 kernel axioms with REAL Term shapes 10// - finite induction engine: given P(0) + step axiom, auto-derive P(n) 11// by emitting N modus-ponens applications through the v2 kernel 12// 13// Sym IDs reserved 410001..410010 (arith family; distinct from kernel 14// 400xxx, user 1xxx, FMB 5xxxxx, AVATAR 6xxxxx, etc.) 15 16// nx_safety_envelope: 17// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 18// sil_target: SIL1 19// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 20// verdict: NOT_YET_EVALUATED 21 22import "nx_kernel_v2.nx" 23 24const NX_ARITH_SYM_ZERO: nx_int = 410001 25const NX_ARITH_SYM_SUCC: nx_int = 410002 26const NX_ARITH_SYM_PLUS: nx_int = 410003 27const NX_ARITH_SYM_MULT: nx_int = 410004 28const NX_ARITH_SYM_LE: nx_int = 410005 29const NX_ARITH_SYM_LT: nx_int = 410006 30 31// Each arith axiom gets a stable v2 axiom-code in the kernel symbol 32// space (400xxx for connectives, 410xxx for arith, 411xxx for axioms). 33const NX_ARITH_AX_PA1_ZERO_NOT_SUCC: nx_int = 411001 34const NX_ARITH_AX_PA2_SUCC_INJECT: nx_int = 411002 35const NX_ARITH_AX_PA3_PLUS_ZERO: nx_int = 411003 36const NX_ARITH_AX_PA4_PLUS_SUCC: nx_int = 411004 37const NX_ARITH_AX_PA5_INDUCTION: nx_int = 411005 38 39// ===== Term constructors ============================================ 40func nx_arith_zero() -> *Term { 41 return nx_term_const(NX_ARITH_SYM_ZERO) 42} 43 44func nx_arith_succ(n: *Term) -> *Term { 45 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term 46 arg.kind = n.kind; arg.sym = n.sym; arg.n_args = n.n_args; arg.args = n.args 47 return nx_term_app(NX_ARITH_SYM_SUCC, 1, arg) 48} 49 50func nx_arith_plus(a: *Term, b: *Term) -> *Term { 51 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term 52 let a0: *Term = args 53 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args 54 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term 55 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args 56 return nx_term_app(NX_ARITH_SYM_PLUS, 2, args) 57} 58 59func nx_arith_mult(a: *Term, b: *Term) -> *Term { 60 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term 61 let a0: *Term = args 62 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args 63 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term 64 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args 65 return nx_term_app(NX_ARITH_SYM_MULT, 2, args) 66} 67 68// nat literal builder -- builds succ^n(zero). 69func nx_arith_nat(n: nx_int) -> *Term { 70 var t: *Term = nx_arith_zero() 71 var i: nx_int = 0 72 while i < n { 73 t = nx_arith_succ(t) 74 i = i + 1 75 } 76 return t 77} 78 79// ===== FINITE-INDUCTION ENGINE ====================================== 80// 81// Standard induction principle (Peano PA5): 82// P(0) /\ (forall n. P(n) => P(succ n)) |- forall m. P(m) 83// 84// Without quantifier-introduction in the kernel we can still EMIT a 85// finite specialisation: given chain indices for P(0) and the step 86// implication chain (P(0) => P(1)), (P(1) => P(2)), ..., (P(N-1) => 87// P(N)), produce P(N) via N modus-ponens applications. This is 88// exactly what HOL Light's NUM_REDUCE_TAC does internally. 89// 90// The caller supplies: 91// p_predicate: Term-builder (a function pointer would be ideal but 92// we don't have first-class fns yet -- caller passes 93// the predicate symbol and we build P(succ^k(0)) at 94// each step) 95// prop_sym: unary predicate symbol -- we form Term P(n) as 96// App(prop_sym, [n]) 97// p_zero_idx: chain index of axiom asserting P(0) 98// step_idxs: array of chain indices, step_idxs[k] = axiom for 99// (P(succ^k(0)) => P(succ^(k+1)(0))) 100// target_n: target literal N 101// 102// Returns chain index of the derived P(N), or negative on failure. 103func nx_arith_finite_induction( 104 ch: *K2Chain, 105 prop_sym: nx_int, 106 p_zero_idx: nx_int, 107 step_idxs: *nx_int, 108 target_n: nx_int 109) -> nx_int { 110 if target_n < 0 { return 0 - 1 } 111 if target_n == 0 { return p_zero_idx } 112 var cur: nx_int = p_zero_idx 113 var k: nx_int = 0 114 while k < target_n { 115 let step_ptr: *nx_int = ((step_idxs as nx_int) + (k * 8)) as *nx_int 116 let step_idx: nx_int = step_ptr[0] 117 let next: nx_int = nx_k2_modus_ponens(ch, step_idx, cur) 118 if next < 0 { return next } 119 cur = next 120 k = k + 1 121 } 122 return cur 123} 124 125// ===== PEANO AXIOM emitters ========================================= 126// 127// Each emits a v2 kernel axiom with the REAL Term shape, so any later 128// proof can use it via prem_idx in MP / SUBST etc. The whole-PA-set 129// can be emitted in one call via nx_arith_register_peano(). 130 131// PA3: forall n. n + 0 = n -- specialised at a concrete n. 132// (We don't have universal quantifier, so caller picks the n; the 133// axiom is registered as a concrete instance. HOL Light does the 134// same for the bootstrap arith library.) 135func nx_arith_axiom_plus_zero(ch: *K2Chain, n: *Term) -> nx_int { 136 return nx_k2_axiom(ch, nx_k2_eq(nx_arith_plus(n, nx_arith_zero()), n)) 137} 138 139// PA4 (specialised): n + succ(m) = succ(n + m). 140func nx_arith_axiom_plus_succ(ch: *K2Chain, n: *Term, m: *Term) -> nx_int { 141 let lhs: *Term = nx_arith_plus(n, nx_arith_succ(m)) 142 let rhs: *Term = nx_arith_succ(nx_arith_plus(n, m)) 143 return nx_k2_axiom(ch, nx_k2_eq(lhs, rhs)) 144} 145 146// PA1: forall n. NOT (zero == succ(n)) -- specialised at concrete n. 147func nx_arith_axiom_zero_not_succ(ch: *K2Chain, n: *Term) -> nx_int { 148 return nx_k2_axiom(ch, nx_k2_not(nx_k2_eq(nx_arith_zero(), nx_arith_succ(n)))) 149}