nx_prove_propositional.nx source
↩ module page · 281 lines · 9651 B
1// nx_prove_propositional.nx -- AUTO-PROVER ENGINE
2//
3// Per user 2026-05-15: "build the system or engine that does this
4// this goes for all nishilang ... make sure it exceeds or matches
5// everything wikipedia called out on proofs that are required".
6
7// nx_safety_envelope:
8// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
9// sil_target: SIL1
10// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
11// verdict: NOT_YET_EVALUATED
12
13import "nx_kernel_v2.nx"
14
15const NX_PROVE_MAX_CTX: nx_int = 64
16const NX_PROVE_MAX_DEPTH: nx_int = 16
17
18struct ProofCtx {
19 facts: *nx_int,
20 n: nx_int,
21 cap: nx_int,
22}
23const NX_PROOF_CTX_BYTES: nx_int = 24
24
25func nx_proof_ctx_new() -> *ProofCtx {
26 let p: *ProofCtx = (sys_mmap(NX_PROOF_CTX_BYTES as i64)) as *ProofCtx
27 p.facts = (sys_mmap((NX_PROVE_MAX_CTX * 8) as i64)) as *nx_int
28 p.n = 0
29 p.cap = NX_PROVE_MAX_CTX
30 return p
31}
32
33func nx_proof_ctx_push(p: *ProofCtx, idx: nx_int) -> nx_int {
34 if p.n >= p.cap { return 0 - 1 }
35 p.facts[p.n] = idx
36 p.n = p.n + 1
37 return p.n
38}
39
40func nx_proof_ctx_pop(p: *ProofCtx) -> nx_int {
41 if p.n > 0 { p.n = p.n - 1 }
42 return p.n
43}
44
45func nx_proof_ctx_seed(p: *ProofCtx, idxs: *nx_int, n: nx_int) -> nx_int {
46 var i: nx_int = 0
47 while i < n {
48 let cur: *nx_int = ((idxs as nx_int) + (i * 8)) as *nx_int
49 let v: nx_int = cur[0]
50 let _ok: nx_int = nx_proof_ctx_push(p, v)
51 i = i + 1
52 }
53 return n
54}
55
56func nx_prove_ctx_lookup(ch: *K2Chain, p: *ProofCtx, goal: *Term) -> nx_int {
57 var i: nx_int = 0
58 while i < p.n {
59 let idx: nx_int = p.facts[i]
60 let t: *K2Thm = nx_k2_at(ch, idx)
61 if nx_term_eq(t.stmt, goal) == 1 { return idx }
62 i = i + 1
63 }
64 return 0 - 1
65}
66
67// Forward decls for mutual recursion
68func nx_prove_aux(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int;
69func nx_prove_false(ch: *K2Chain, p: *ProofCtx, depth: nx_int) -> nx_int;
70
71func nx_prove_and_elim_scan(ch: *K2Chain, p: *ProofCtx, goal: *Term) -> nx_int {
72 var i: nx_int = 0
73 while i < p.n {
74 let idx: nx_int = p.facts[i]
75 let t: *K2Thm = nx_k2_at(ch, idx)
76 let s: *Term = t.stmt
77 if s.kind == NX_TERM_APP {
78 if s.sym == NX_K2_SYM_AND {
79 let l: *Term = nx_term_arg(s, 0)
80 let r: *Term = nx_term_arg(s, 1)
81 if nx_term_eq(l, goal) == 1 {
82 let new_idx: nx_int = nx_k2_and_elim_l(ch, idx)
83 if new_idx >= 0 {
84 let _ok: nx_int = nx_proof_ctx_push(p, new_idx)
85 return new_idx
86 }
87 }
88 if nx_term_eq(r, goal) == 1 {
89 let new_idx2: nx_int = nx_k2_and_elim_r(ch, idx)
90 if new_idx2 >= 0 {
91 let _ok2: nx_int = nx_proof_ctx_push(p, new_idx2)
92 return new_idx2
93 }
94 }
95 }
96 }
97 i = i + 1
98 }
99 return 0 - 1
100}
101
102func nx_prove_mp_scan(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int {
103 var i: nx_int = 0
104 while i < p.n {
105 let idx: nx_int = p.facts[i]
106 let t: *K2Thm = nx_k2_at(ch, idx)
107 let s: *Term = t.stmt
108 if s.kind == NX_TERM_APP {
109 if s.sym == NX_K2_SYM_IMP {
110 let ant: *Term = nx_term_arg(s, 0)
111 let con: *Term = nx_term_arg(s, 1)
112 if nx_term_eq(con, goal) == 1 {
113 let a_idx: nx_int = nx_prove_aux(ch, p, ant, depth - 1)
114 if a_idx >= 0 {
115 let new_idx: nx_int = nx_k2_modus_ponens(ch, idx, a_idx)
116 if new_idx >= 0 {
117 let _ok: nx_int = nx_proof_ctx_push(p, new_idx)
118 return new_idx
119 }
120 }
121 }
122 }
123 }
124 i = i + 1
125 }
126 return 0 - 1
127}
128
129func nx_prove_false(ch: *K2Chain, p: *ProofCtx, depth: nx_int) -> nx_int {
130 if depth <= 0 { return 0 - 1 }
131 var i: nx_int = 0
132 while i < p.n {
133 let ti: *K2Thm = nx_k2_at(ch, p.facts[i])
134 let si: *Term = ti.stmt
135 if si.kind == NX_TERM_APP {
136 if si.sym == NX_K2_SYM_NOT {
137 let inner: *Term = nx_term_arg(si, 0)
138 let a_idx: nx_int = nx_prove_ctx_lookup(ch, p, inner)
139 if a_idx >= 0 {
140 let new_idx: nx_int = nx_k2_contradiction(ch, a_idx, p.facts[i])
141 if new_idx >= 0 {
142 let _ok: nx_int = nx_proof_ctx_push(p, new_idx)
143 return new_idx
144 }
145 }
146 }
147 }
148 i = i + 1
149 }
150 var j: nx_int = 0
151 while j < p.n {
152 let tj: *K2Thm = nx_k2_at(ch, p.facts[j])
153 let sj: *Term = tj.stmt
154 if sj.kind == NX_TERM_APP {
155 if sj.sym == NX_K2_SYM_NOT {
156 let inner2: *Term = nx_term_arg(sj, 0)
157 let prove_idx: nx_int = nx_prove_aux(ch, p, inner2, depth - 1)
158 if prove_idx >= 0 {
159 let new_idx2: nx_int = nx_k2_contradiction(ch, prove_idx, p.facts[j])
160 if new_idx2 >= 0 {
161 let _ok2: nx_int = nx_proof_ctx_push(p, new_idx2)
162 return new_idx2
163 }
164 }
165 }
166 }
167 j = j + 1
168 }
169 return 0 - 1
170}
171
172func nx_prove_aux(ch: *K2Chain, p: *ProofCtx, goal: *Term, depth: nx_int) -> nx_int {
173 if depth <= 0 { return 0 - 1 }
174 let exact: nx_int = nx_prove_ctx_lookup(ch, p, goal)
175 if exact >= 0 { return exact }
176
177 if goal.kind == NX_TERM_APP {
178 if goal.sym == NX_K2_SYM_AND {
179 let a: *Term = nx_term_arg(goal, 0)
180 let b: *Term = nx_term_arg(goal, 1)
181 let ai: nx_int = nx_prove_aux(ch, p, a, depth - 1)
182 if ai >= 0 {
183 let bi: nx_int = nx_prove_aux(ch, p, b, depth - 1)
184 if bi >= 0 {
185 let new_idx: nx_int = nx_k2_and_intro(ch, ai, bi)
186 if new_idx >= 0 {
187 let _ok: nx_int = nx_proof_ctx_push(p, new_idx)
188 return new_idx
189 }
190 }
191 }
192 }
193 }
194
195 if goal.kind == NX_TERM_APP {
196 if goal.sym == NX_K2_SYM_IMP {
197 let ant: *Term = nx_term_arg(goal, 0)
198 let con: *Term = nx_term_arg(goal, 1)
199 let assume_idx: nx_int = nx_k2_assume(ch, ant)
200 if assume_idx >= 0 {
201 let _ok: nx_int = nx_proof_ctx_push(p, assume_idx)
202 let b_idx: nx_int = nx_prove_aux(ch, p, con, depth - 1)
203 if b_idx >= 0 {
204 let new_idx: nx_int = nx_k2_imp_intro(ch, assume_idx, b_idx)
205 if new_idx >= 0 {
206 let _pp: nx_int = nx_proof_ctx_pop(p)
207 let _ok2: nx_int = nx_proof_ctx_push(p, new_idx)
208 return new_idx
209 }
210 }
211 let _pp: nx_int = nx_proof_ctx_pop(p)
212 }
213 }
214 }
215
216 if goal.kind == NX_TERM_APP {
217 if goal.sym == NX_K2_SYM_NOT {
218 let inner: *Term = nx_term_arg(goal, 0)
219 let assume_idx2: nx_int = nx_k2_assume(ch, inner)
220 if assume_idx2 >= 0 {
221 let _ok3: nx_int = nx_proof_ctx_push(p, assume_idx2)
222 let f_idx: nx_int = nx_prove_false(ch, p, depth - 1)
223 if f_idx >= 0 {
224 let new_idx3: nx_int = nx_k2_not_intro(ch, assume_idx2, f_idx)
225 if new_idx3 >= 0 {
226 let _pp: nx_int = nx_proof_ctx_pop(p)
227 let _ok4: nx_int = nx_proof_ctx_push(p, new_idx3)
228 return new_idx3
229 }
230 }
231 let _pp: nx_int = nx_proof_ctx_pop(p)
232 }
233 }
234 }
235
236 if goal.kind == NX_TERM_APP {
237 if goal.sym == NX_K2_SYM_OR {
238 let oa: *Term = nx_term_arg(goal, 0)
239 let ob: *Term = nx_term_arg(goal, 1)
240 let oai: nx_int = nx_prove_aux(ch, p, oa, depth - 1)
241 if oai >= 0 {
242 let new_idx4: nx_int = nx_k2_or_intro_l(ch, oai, ob)
243 if new_idx4 >= 0 {
244 let _ok5: nx_int = nx_proof_ctx_push(p, new_idx4)
245 return new_idx4
246 }
247 }
248 let obi: nx_int = nx_prove_aux(ch, p, ob, depth - 1)
249 if obi >= 0 {
250 let new_idx5: nx_int = nx_k2_or_intro_r(ch, oa, obi)
251 if new_idx5 >= 0 {
252 let _ok6: nx_int = nx_proof_ctx_push(p, new_idx5)
253 return new_idx5
254 }
255 }
256 }
257 }
258
259 let ae: nx_int = nx_prove_and_elim_scan(ch, p, goal)
260 if ae >= 0 { return ae }
261
262 let mpr: nx_int = nx_prove_mp_scan(ch, p, goal, depth)
263 if mpr >= 0 { return mpr }
264
265 let ff: nx_int = nx_prove_false(ch, p, depth - 1)
266 if ff >= 0 {
267 let new_idx6: nx_int = nx_k2_ex_falso(ch, ff, goal)
268 if new_idx6 >= 0 {
269 let _ok7: nx_int = nx_proof_ctx_push(p, new_idx6)
270 return new_idx6
271 }
272 }
273
274 return 0 - 1
275}
276
277func nx_prove(ch: *K2Chain, axioms: *nx_int, n_ax: nx_int, goal: *Term) -> nx_int {
278 let p: *ProofCtx = nx_proof_ctx_new()
279 let _ps: nx_int = nx_proof_ctx_seed(p, axioms, n_ax)
280 return nx_prove_aux(ch, p, goal, NX_PROVE_MAX_DEPTH)
281}