nx_kernel_v2_discharge_test.nx source
↩ module page · 152 lines · 8448 B
1// nx_kernel_v2_discharge_test.nx -- ASSUMPTION + IMP_INTRO + NOT_INTRO
2// + OR_INTRO + EQ_SYM + EQ_TRANS exercises.
3//
4// These rules are what turn the kernel from "stops at contradiction"
5// to "produces real theorems".
6
7import "nx_syscalls.nx"
8import "nx_runtime.nx"
9import "nx_tier.nx"
10import "nx_kernel_v2.nx"
11
12const SYM_P: nx_int = 1001
13const SYM_Q: nx_int = 1002
14const SYM_A: nx_int = 1100
15const SYM_B: nx_int = 1101
16const SYM_C: nx_int = 1102
17
18func main() -> nx_exit {
19 println("=== nx_kernel_v2 discharge + OR + EQ tests ===" as *u8)
20
21 // ---- T4: IMP_INTRO -- discharge assumption into A => A ----
22 println("[T4] IMP_INTRO: assume A, conclude A => A (identity implication):" as *u8)
23 let ch4: *K2Chain = nx_k2_chain_new(8)
24 let a: *Term = nx_term_const(SYM_A)
25 let i0: nx_int = nx_k2_assume(ch4, a)
26 let i1: nx_int = nx_k2_imp_intro(ch4, i0, i0)
27 if i1 < 0 { println(" FAIL: IMP_INTRO returned error" as *u8); return 1 }
28 let n1: *K2Thm = nx_k2_at(ch4, i1)
29 if n1.n_hyps != 0 { println(" FAIL: discharge did not close all hypotheses" as *u8); return 1 }
30 if n1.stmt.kind != NX_TERM_APP { println(" FAIL: not an implication" as *u8); return 1 }
31 if n1.stmt.sym != NX_K2_SYM_IMP { println(" FAIL: not =>" as *u8); return 1 }
32 let v4: nx_int = nx_k2_mark_theorem(ch4)
33 if v4 != NX_K2_OK { println(" FAIL: mark_theorem rejected closed theorem" as *u8); return 1 }
34 println(" T4 PASS (closed theorem A => A produced by discharge)" as *u8)
35
36 // ---- T5: NOT_INTRO -- assume A, derive false, conclude NOT A ----
37 // Setup: axioms (A => B), (~B); under assumption A derive B via MP,
38 // then contradiction with (~B) gives false, then NOT_INTRO discharges
39 // A to give NOT A.
40 println("[T5] NOT_INTRO: from (A=>B), (~B), assume A; derive false; discharge to NOT A:" as *u8)
41 let ch5: *K2Chain = nx_k2_chain_new(16)
42 let ta5: *Term = nx_term_const(SYM_A)
43 let tb5: *Term = nx_term_const(SYM_B)
44 let imp_ab: *Term = nx_k2_imp(ta5, tb5)
45 let not_b: *Term = nx_k2_not(tb5)
46 let j0: nx_int = nx_k2_axiom(ch5, imp_ab) // 0 : A=>B
47 let j1: nx_int = nx_k2_axiom(ch5, not_b) // 1 : ~B
48 let j2: nx_int = nx_k2_assume(ch5, ta5) // 2 : A (open hyp)
49 let j3: nx_int = nx_k2_modus_ponens(ch5, j0, j2) // 3 : B (open hyp A)
50 if j3 < 0 { println(" FAIL: MP failed" as *u8); return 1 }
51 let j4: nx_int = nx_k2_contradiction(ch5, j3, j1) // 4 : false (open hyp A)
52 if j4 < 0 { println(" FAIL: contradiction failed" as *u8); return 1 }
53 let n4: *K2Thm = nx_k2_at(ch5, j4)
54 if n4.n_hyps != 1 { println(" FAIL: contradiction did not inherit hyp A" as *u8); return 1 }
55 let j5: nx_int = nx_k2_not_intro(ch5, j2, j4) // 5 : NOT A (closed)
56 if j5 < 0 { println(" FAIL: NOT_INTRO returned error" as *u8); return 1 }
57 let n5: *K2Thm = nx_k2_at(ch5, j5)
58 if n5.n_hyps != 0 { println(" FAIL: NOT_INTRO did not close" as *u8); return 1 }
59 if n5.stmt.kind != NX_TERM_APP { println(" FAIL: not a negation" as *u8); return 1 }
60 if n5.stmt.sym != NX_K2_SYM_NOT { println(" FAIL: not ~" as *u8); return 1 }
61 let v5: nx_int = nx_k2_mark_theorem(ch5)
62 if v5 != NX_K2_OK { println(" FAIL: mark_theorem rejected" as *u8); return 1 }
63 println(" T5 PASS (closed theorem NOT A produced via assumption discharge)" as *u8)
64
65 // ---- T6: LCF DISCH semantics -- discharge of unused assumption ----
66 // Standard HOL Light DISCH: discharging an assumption that the
67 // sub-proof didn't actually use is SOUND -- the result is just
68 // weakened (the conclusion holds regardless of the discharged
69 // assumption). Engine relies on this to compose K combinator etc.
70 println("[T6] LCF DISCH: discharge of unused assumption -- standard HOL semantics:" as *u8)
71 let ch6: *K2Chain = nx_k2_chain_new(8)
72 let ta6: *Term = nx_term_const(SYM_A)
73 let tb6: *Term = nx_term_const(SYM_B)
74 let assume_b: nx_int = nx_k2_assume(ch6, tb6)
75 let assume_a: nx_int = nx_k2_assume(ch6, ta6)
76 let imp_ba: *Term = nx_k2_imp(tb6, ta6)
77 let ax_imp: nx_int = nx_k2_axiom(ch6, imp_ba)
78 let mp_a: nx_int = nx_k2_modus_ponens(ch6, ax_imp, assume_b)
79 // mp_a has hyps={B} only. imp_intro discharging A produces
80 // (A => mp_a.stmt) with hyps still = {B} (A wasn't used).
81 let lift: nx_int = nx_k2_imp_intro(ch6, assume_a, mp_a)
82 if lift < 0 { println(" FAIL: LCF DISCH rejected unused-assumption discharge" as *u8); return 1 }
83 let lift_thm: *K2Thm = nx_k2_at(ch6, lift)
84 if lift_thm.stmt.kind != NX_TERM_APP { println(" FAIL: not an implication" as *u8); return 1 }
85 if lift_thm.stmt.sym != NX_K2_SYM_IMP { println(" FAIL: not =>" as *u8); return 1 }
86 if lift_thm.n_hyps != 1 { println(" FAIL: hyps not preserved" as *u8); return 1 }
87 println(" T6 PASS (LCF DISCH -- unused-assumption discharge is sound)" as *u8)
88
89 // ---- T7: OR_INTRO_L ----
90 println("[T7] OR_INTRO_L: from A, conclude A | B:" as *u8)
91 let ch7: *K2Chain = nx_k2_chain_new(8)
92 let a7: *Term = nx_term_const(SYM_A)
93 let b7: *Term = nx_term_const(SYM_B)
94 let _k0: nx_int = nx_k2_axiom(ch7, a7)
95 let k1: nx_int = nx_k2_or_intro_l(ch7, 0, b7)
96 if k1 < 0 { println(" FAIL: OR_INTRO_L error" as *u8); return 1 }
97 let n7: *K2Thm = nx_k2_at(ch7, k1)
98 if n7.stmt.sym != NX_K2_SYM_OR { println(" FAIL: not OR" as *u8); return 1 }
99 println(" T7 PASS (OR_INTRO_L produced A | B)" as *u8)
100
101 // ---- T8: EQ_SYM (a==b) |- (b==a) ----
102 println("[T8] EQ_SYM: from a==b, conclude b==a:" as *u8)
103 let ch8: *K2Chain = nx_k2_chain_new(8)
104 let ta8: *Term = nx_term_const(SYM_A)
105 let tb8: *Term = nx_term_const(SYM_B)
106 let eq_ab: *Term = nx_k2_eq(ta8, tb8)
107 let _l0: nx_int = nx_k2_axiom(ch8, eq_ab)
108 let l1: nx_int = nx_k2_eq_sym(ch8, 0)
109 if l1 < 0 { println(" FAIL: EQ_SYM error" as *u8); return 1 }
110 let n8: *K2Thm = nx_k2_at(ch8, l1)
111 let lhs: *Term = nx_term_arg(n8.stmt, 0)
112 let rhs: *Term = nx_term_arg(n8.stmt, 1)
113 if lhs.sym != SYM_B { println(" FAIL: lhs not B" as *u8); return 1 }
114 if rhs.sym != SYM_A { println(" FAIL: rhs not A" as *u8); return 1 }
115 println(" T8 PASS (EQ_SYM swaps sides correctly)" as *u8)
116
117 // ---- T9: EQ_TRANS (a==b, b==c) |- (a==c) ----
118 println("[T9] EQ_TRANS: from a==b and b==c, conclude a==c:" as *u8)
119 let ch9: *K2Chain = nx_k2_chain_new(8)
120 let ta9: *Term = nx_term_const(SYM_A)
121 let tb9: *Term = nx_term_const(SYM_B)
122 let tc9: *Term = nx_term_const(SYM_C)
123 let _m0: nx_int = nx_k2_axiom(ch9, nx_k2_eq(ta9, tb9))
124 let _m1: nx_int = nx_k2_axiom(ch9, nx_k2_eq(tb9, tc9))
125 let m2: nx_int = nx_k2_eq_trans(ch9, 0, 1)
126 if m2 < 0 { println(" FAIL: EQ_TRANS error" as *u8); return 1 }
127 let n9: *K2Thm = nx_k2_at(ch9, m2)
128 let l9: *Term = nx_term_arg(n9.stmt, 0)
129 let r9: *Term = nx_term_arg(n9.stmt, 1)
130 if l9.sym != SYM_A { println(" FAIL: trans lhs wrong" as *u8); return 1 }
131 if r9.sym != SYM_C { println(" FAIL: trans rhs wrong" as *u8); return 1 }
132 println(" T9 PASS (EQ_TRANS chains correctly)" as *u8)
133
134 // ---- T10: kernel REJECTS bad EQ_TRANS (mismatched middle) ----
135 println("[T10] BAD EQ_TRANS: (a==b) + (c==a) ?- (a==a) -- middle mismatch must reject:" as *u8)
136 let cha: *K2Chain = nx_k2_chain_new(8)
137 let _q0: nx_int = nx_k2_axiom(cha, nx_k2_eq(nx_term_const(SYM_A), nx_term_const(SYM_B)))
138 let _q1: nx_int = nx_k2_axiom(cha, nx_k2_eq(nx_term_const(SYM_C), nx_term_const(SYM_A)))
139 let q2: nx_int = nx_k2_eq_trans(cha, 0, 1)
140 if q2 >= 0 { println(" FAIL: kernel accepted bad EQ_TRANS" as *u8); return 1 }
141 if q2 != (0 - NX_K2_ERR_MISMATCH) { println(" WARN: rejected with unexpected code" as *u8) }
142 println(" T10 PASS (kernel REJECTED middle-term mismatch)" as *u8)
143
144 println("" as *u8)
145 println("=== ALL DISCHARGE + OR + EQ TESTS PASSED ===" as *u8)
146 println("nx_kernel_v2 now ships:" as *u8)
147 println(" AXIOM, ASSUMPTION, MODUS_PONENS, AND_INTRO, AND_ELIM_L," as *u8)
148 println(" AND_ELIM_R, IMP_INTRO, REFL, CONTRADICTION, NOT_INTRO," as *u8)
149 println(" OR_INTRO_L, OR_INTRO_R, EQ_SYM, EQ_TRANS" as *u8)
150 println("All with Term-level semantic verification + LCF-style rejection." as *u8)
151 return 0
152}