nx_prover_a1_test.nx source
↩ module page · 89 lines · 3914 B
1// nx_prover_a1_test.nx -- Phase A1 extended-rule prover smoke.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_prover.nx"
6import "nx_prover_a1.nx"
7
8func main() -> i64 {
9 // === Case 1: Substitution. Given a=b (stmt 10), P(a) (stmt 20),
10 // target P(b) (stmt 21).
11 let s1: *ProofState = nx_prover_state_alloc(21)
12 nx_prover_add_axiom(s1, 10, NX_AX_LOGIC_IDENTITY) // a=b
13 nx_prover_add_axiom(s1, 20, NX_AX_PEANO_PA1_ZERO_EXISTS) // P(a)
14 let subst: *i64 = (sys_mmap(24)) as *i64
15 subst[0] = 10; subst[1] = 20; subst[2] = 21
16 let empty: *i64 = (sys_mmap(8)) as *i64
17 let v1: i64 = nx_prover_a1_search(s1, empty, 0, subst, 1, empty, 0, empty, 0, 10)
18 if v1 != NX_PROVER_PROVED { return 10 }
19
20 // === Case 2: Conjunction introduction. Given A (stmt 1), B (stmt 2),
21 // target A^B (stmt 3).
22 let s2: *ProofState = nx_prover_state_alloc(3)
23 nx_prover_add_axiom(s2, 1, NX_AX_LOGIC_IDENTITY)
24 nx_prover_add_axiom(s2, 2, NX_AX_LOGIC_IDENTITY)
25 let conj: *i64 = (sys_mmap(24)) as *i64
26 conj[0] = 1; conj[1] = 2; conj[2] = 3
27 let v2: i64 = nx_prover_a1_search(s2, empty, 0, empty, 0, conj, 1, empty, 0, 10)
28 if v2 != NX_PROVER_PROVED { return 20 }
29
30 // === Case 3: Conjunction elimination. Given A^B (stmt 5),
31 // target A (stmt 1).
32 let s3: *ProofState = nx_prover_state_alloc(1)
33 nx_prover_add_axiom(s3, 5, NX_AX_LOGIC_IDENTITY)
34 let conj3: *i64 = (sys_mmap(24)) as *i64
35 conj3[0] = 1; conj3[1] = 2; conj3[2] = 5
36 let v3: i64 = nx_prover_a1_search(s3, empty, 0, empty, 0, conj3, 1, empty, 0, 10)
37 if v3 != NX_PROVER_PROVED { return 30 }
38
39 // === Case 4: Disjunction introduction. Given A (stmt 1),
40 // target A v B (stmt 7).
41 let s4: *ProofState = nx_prover_state_alloc(7)
42 nx_prover_add_axiom(s4, 1, NX_AX_LOGIC_IDENTITY)
43 let disj: *i64 = (sys_mmap(16)) as *i64
44 disj[0] = 1; disj[1] = 7
45 let v4: i64 = nx_prover_a1_search(s4, empty, 0, empty, 0, empty, 0, disj, 1, 10)
46 if v4 != NX_PROVER_PROVED { return 40 }
47
48 // === Case 5: COMBINED rules. Build a chain that mixes MP +
49 // substitution + conjunction intro.
50 //
51 // Axioms: stmt 1 (A), stmt 2 (B)
52 // Impls: 2 -> 4 (B implies D)
53 // Conj: A^D (stmt 1, 4, 100)
54 // Target: A^D = stmt 100
55 let s5: *ProofState = nx_prover_state_alloc(100)
56 nx_prover_add_axiom(s5, 1, NX_AX_LOGIC_IDENTITY)
57 nx_prover_add_axiom(s5, 2, NX_AX_LOGIC_IDENTITY)
58 let impls5: *i64 = (sys_mmap(8)) as *i64
59 impls5[0] = 2; impls5[1] = 4
60 let conj5: *i64 = (sys_mmap(24)) as *i64
61 conj5[0] = 1; conj5[1] = 4; conj5[2] = 100
62 let v5: i64 = nx_prover_a1_search(s5, impls5, 1, empty, 0, conj5, 1, empty, 0, 10)
63 if v5 != NX_PROVER_PROVED { return 50 }
64
65 // === Case 6: Chain substitution + MP.
66 //
67 // Axioms: stmt 10 (a=b), stmt 20 (P(a))
68 // Subst : a=b + P(a) -> P(b) (stmts 10, 20, 21)
69 // Impls : 21 -> 30
70 // Target: 30
71 let s6: *ProofState = nx_prover_state_alloc(30)
72 nx_prover_add_axiom(s6, 10, NX_AX_LOGIC_IDENTITY)
73 nx_prover_add_axiom(s6, 20, NX_AX_LOGIC_IDENTITY)
74 let subst6: *i64 = (sys_mmap(24)) as *i64
75 subst6[0] = 10; subst6[1] = 20; subst6[2] = 21
76 let impls6: *i64 = (sys_mmap(8)) as *i64
77 impls6[0] = 21; impls6[1] = 30
78 let v6: i64 = nx_prover_a1_search(s6, impls6, 1, subst6, 1, empty, 0, empty, 0, 10)
79 if v6 != NX_PROVER_PROVED { return 60 }
80
81 // === Case 7: Negative -- conjunction premise missing.
82 let s7: *ProofState = nx_prover_state_alloc(3)
83 nx_prover_add_axiom(s7, 1, NX_AX_LOGIC_IDENTITY)
84 // Note: stmt 2 NOT in axioms.
85 let v7: i64 = nx_prover_a1_search(s7, empty, 0, empty, 0, conj, 1, empty, 0, 10)
86 if v7 != NX_PROVER_NO_RULES_APPLY { return 70 }
87
88 return 0
89}