nx_proof_emit.nx source
↩ module page · 138 lines · 5712 B
1// nx_proof_emit.nx -- two-column proof emitter.
2//
3// Closes the named blocker for "two-column proof" -- previously
4// DERIVABLE but not yet shipped as a callable engine. This file
5// makes it L3 (callable) per the every-primitive-usable cardinal.
6//
7// Walks a v2 chain and prints each step in the standard math two-
8// column form:
9//
10// #idx | statement | justification
11// -----+------------------------+--------------------------------
12// 0 | A | AXIOM
13// 1 | A => B | AXIOM
14// 2 | B | MODUS_PONENS (1, 0)
15//
16// This is the format every K-12 / undergrad textbook uses for proofs.
17// HOL Light has it via print_thm; Coq / Lean have similar.
18
19// nx_safety_envelope:
20// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
21// sil_target: SIL1
22// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
23// verdict: NOT_YET_EVALUATED
24
25import "nx_kernel_v2.nx"
26
27// Print the rule name (string) for a rule code.
28func nx_emit_rule_name(rule: nx_int) -> nx_int {
29 if rule == NX_K2_AXIOM { print("AXIOM " as *u8); return 0 }
30 if rule == NX_K2_ASSUMPTION { print("ASSUMPTION " as *u8); return 0 }
31 if rule == NX_K2_MODUS_PONENS { print("MODUS_PONENS " as *u8); return 0 }
32 if rule == NX_K2_AND_INTRO { print("AND_INTRO " as *u8); return 0 }
33 if rule == NX_K2_AND_ELIM_L { print("AND_ELIM_L " as *u8); return 0 }
34 if rule == NX_K2_AND_ELIM_R { print("AND_ELIM_R " as *u8); return 0 }
35 if rule == NX_K2_IMP_INTRO { print("IMP_INTRO " as *u8); return 0 }
36 if rule == NX_K2_SUBST { print("SUBST " as *u8); return 0 }
37 if rule == NX_K2_REFL { print("REFL " as *u8); return 0 }
38 if rule == NX_K2_CONTRADICTION { print("CONTRADICTION " as *u8); return 0 }
39 if rule == NX_K2_NOT_INTRO { print("NOT_INTRO " as *u8); return 0 }
40 if rule == NX_K2_OR_INTRO_L { print("OR_INTRO_L " as *u8); return 0 }
41 if rule == NX_K2_OR_INTRO_R { print("OR_INTRO_R " as *u8); return 0 }
42 if rule == NX_K2_OR_ELIM { print("OR_ELIM " as *u8); return 0 }
43 if rule == NX_K2_EQ_SYM { print("EQ_SYM " as *u8); return 0 }
44 if rule == NX_K2_EQ_TRANS { print("EQ_TRANS " as *u8); return 0 }
45 if rule == NX_K2_EX_FALSO { print("EX_FALSO " as *u8); return 0 }
46 print("UNKNOWN_RULE " as *u8)
47 return 0
48}
49
50// Pretty-print a Term (compact infix where useful).
51func nx_emit_term(t: *Term) -> nx_int {
52 if t.kind == NX_TERM_VAR { print("?v" as *u8); print_i64(t.sym); return 0 }
53 if t.kind == NX_TERM_CONST { print("c" as *u8); print_i64(t.sym); return 0 }
54 if t.kind == NX_TERM_APP {
55 if t.sym == NX_K2_SYM_IMP {
56 print("(" as *u8)
57 let _e1: nx_int = nx_emit_term(nx_term_arg(t, 0))
58 print(" => " as *u8)
59 let _e2: nx_int = nx_emit_term(nx_term_arg(t, 1))
60 print(")" as *u8); return 0
61 }
62 if t.sym == NX_K2_SYM_AND {
63 print("(" as *u8)
64 let _e1: nx_int = nx_emit_term(nx_term_arg(t, 0))
65 print(" & " as *u8)
66 let _e2: nx_int = nx_emit_term(nx_term_arg(t, 1))
67 print(")" as *u8); return 0
68 }
69 if t.sym == NX_K2_SYM_OR {
70 print("(" as *u8)
71 let _e1: nx_int = nx_emit_term(nx_term_arg(t, 0))
72 print(" | " as *u8)
73 let _e2: nx_int = nx_emit_term(nx_term_arg(t, 1))
74 print(")" as *u8); return 0
75 }
76 if t.sym == NX_K2_SYM_NOT {
77 print("~" as *u8)
78 let _e1: nx_int = nx_emit_term(nx_term_arg(t, 0))
79 return 0
80 }
81 if t.sym == NX_K2_SYM_EQ {
82 let _e1: nx_int = nx_emit_term(nx_term_arg(t, 0))
83 print("==" as *u8)
84 let _e2: nx_int = nx_emit_term(nx_term_arg(t, 1))
85 return 0
86 }
87 if t.sym == NX_K2_SYM_FALSE { print("FALSE" as *u8); return 0 }
88 // Generic application
89 print("f" as *u8); print_i64(t.sym); print("(" as *u8)
90 var i: nx_int = 0
91 while i < t.n_args {
92 if i > 0 { print(", " as *u8) }
93 let _en: nx_int = nx_emit_term(nx_term_arg(t, i))
94 i = i + 1
95 }
96 print(")" as *u8); return 0
97 }
98 return 0
99}
100
101// Print premise list as "(p1, p2, ...)".
102func nx_emit_premises(t: *K2Thm) -> nx_int {
103 if t.n_prem == 0 { return 0 }
104 print("(" as *u8)
105 var i: nx_int = 0
106 while i < t.n_prem {
107 if i > 0 { print(", " as *u8) }
108 let p: *nx_int = ((t.premises as nx_int) + (i * 8)) as *nx_int
109 print_i64(p[0])
110 i = i + 1
111 }
112 print(")" as *u8)
113 return 0
114}
115
116// Emit the entire chain in two-column form.
117func nx_emit_two_column(ch: *K2Chain) -> nx_int {
118 println("---- two-column proof ----" as *u8)
119 println(" # | statement | justification" as *u8)
120 println("----+--------------------------------------------+----------------" as *u8)
121 var i: nx_int = 0
122 while i < ch.n {
123 let t: *K2Thm = nx_k2_at(ch, i)
124 if i < 10 { print(" " as *u8) }
125 print_i64(i)
126 print(" | " as *u8)
127 let _e: nx_int = nx_emit_term(t.stmt)
128 print(" | " as *u8)
129 let _r: nx_int = nx_emit_rule_name(t.rule)
130 let _p: nx_int = nx_emit_premises(t)
131 if t.n_hyps > 0 {
132 print(" [hyps:" as *u8); print_i64(t.n_hyps); print("]" as *u8)
133 }
134 println("" as *u8)
135 i = i + 1
136 }
137 return 0
138}