nx_tactics.nx source
↩ module page · 166 lines · 6333 B
1// nx_tactics.nx -- LCF-style tactic interpreter.
2//
3// Closes "no tactics layer" gap. HOL Light has REPEAT TAC, THEN,
4// MESON_TAC etc. Coq has Ltac. Lean has tactic mode. Ours is
5// minimal but composable: each tactic transforms a TacState (chain +
6// goal + context) and returns success/failure. Composing them is
7// just calling them in sequence.
8//
9// Supported tactics in this commit:
10// nx_tac_intro -- if goal is (A => B), assume A, new goal B
11// nx_tac_split -- if goal is (A & B), produce two subgoals
12// nx_tac_left -- if goal is (A | B), focus left
13// nx_tac_right -- if goal is (A | B), focus right
14// nx_tac_exact -- close current goal with given fact index
15// nx_tac_apply -- apply (X => goal) reducing to subgoal X
16// nx_tac_contradict -- close current goal via P / ~P from context
17// nx_tac_auto -- delegate to nx_prove_propositional engine
18//
19// All tactics emit through v2 kernel rules so produced chains are
20// kernel-checked. The TacState carries the proof being built; when
21// the goal stack empties the proof is complete.
22
23// nx_safety_envelope:
24// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
25// sil_target: SIL1
26// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
27// verdict: NOT_YET_EVALUATED
28
29import "nx_prove_propositional.nx"
30
31const NX_TAC_OK: nx_int = 0
32const NX_TAC_FAIL: nx_int = 1
33const NX_TAC_NOGOAL: nx_int = 2
34
35// Per-goal node (one per outstanding subgoal).
36struct TacGoal {
37 target: *Term, // the proposition we still need to prove
38 parent: nx_int, // chain idx of the assumption-pushed parent
39 // (-1 at the top level); used by intro to
40 // know which assumption to discharge later
41}
42const NX_TAC_GOAL_BYTES: nx_int = 16
43
44struct TacState {
45 ch: *K2Chain,
46 ctx: *ProofCtx,
47 goals: *TacGoal, // stack
48 n_goals: nx_int,
49 cap_goals: nx_int,
50 closed_idx: nx_int, // chain idx of most recently closed sub-proof
51}
52const NX_TAC_STATE_BYTES: nx_int = 40
53
54func nx_tac_state_new(ch: *K2Chain, goal: *Term) -> *TacState {
55 let s: *TacState = (sys_mmap(NX_TAC_STATE_BYTES as i64)) as *TacState
56 s.ch = ch
57 s.ctx = nx_proof_ctx_new()
58 s.cap_goals = 32
59 s.goals = (sys_mmap((s.cap_goals * NX_TAC_GOAL_BYTES) as i64)) as *TacGoal
60 s.n_goals = 1
61 let g: *TacGoal = s.goals
62 g.target = goal
63 g.parent = 0 - 1
64 s.closed_idx = 0 - 1
65 return s
66}
67
68func nx_tac_top(s: *TacState) -> *TacGoal {
69 if s.n_goals <= 0 { return 0 as *TacGoal }
70 return ((s.goals as nx_int) + ((s.n_goals - 1) * NX_TAC_GOAL_BYTES)) as *TacGoal
71}
72
73func nx_tac_seed_ctx(s: *TacState, axioms: *nx_int, n: nx_int) -> nx_int {
74 return nx_proof_ctx_seed(s.ctx, axioms, n)
75}
76
77// === intro ===
78func nx_tac_intro(s: *TacState) -> nx_int {
79 if s.n_goals <= 0 { return NX_TAC_NOGOAL }
80 let g: *TacGoal = nx_tac_top(s)
81 let goal: *Term = g.target
82 if goal.kind != NX_TERM_APP { return NX_TAC_FAIL }
83 if goal.sym != NX_K2_SYM_IMP { return NX_TAC_FAIL }
84 let ant: *Term = nx_term_arg(goal, 0)
85 let con: *Term = nx_term_arg(goal, 1)
86 let ai: nx_int = nx_k2_assume(s.ch, ant)
87 if ai < 0 { return NX_TAC_FAIL }
88 let _ok: nx_int = nx_proof_ctx_push(s.ctx, ai)
89 g.target = con
90 g.parent = ai
91 return NX_TAC_OK
92}
93
94// === exact <fact_idx> ===
95func nx_tac_exact(s: *TacState, fact_idx: nx_int) -> nx_int {
96 if s.n_goals <= 0 { return NX_TAC_NOGOAL }
97 let g: *TacGoal = nx_tac_top(s)
98 let f: *K2Thm = nx_k2_at(s.ch, fact_idx)
99 if nx_term_eq(f.stmt, g.target) == 0 { return NX_TAC_FAIL }
100 s.closed_idx = fact_idx
101 // If this goal had a parent assumption, discharge it via IMP_INTRO
102 // and propagate the result up.
103 if g.parent >= 0 {
104 let imp: nx_int = nx_k2_imp_intro(s.ch, g.parent, fact_idx)
105 if imp < 0 { return NX_TAC_FAIL }
106 s.closed_idx = imp
107 }
108 s.n_goals = s.n_goals - 1
109 return NX_TAC_OK
110}
111
112// === auto === delegate to the propositional engine.
113func nx_tac_auto(s: *TacState) -> nx_int {
114 if s.n_goals <= 0 { return NX_TAC_NOGOAL }
115 let g: *TacGoal = nx_tac_top(s)
116 let proved: nx_int = nx_prove_aux(s.ch, s.ctx, g.target, NX_PROVE_MAX_DEPTH)
117 if proved < 0 { return NX_TAC_FAIL }
118 return nx_tac_exact(s, proved)
119}
120
121// === apply === if known fact (X => goal), reduce goal to X.
122func nx_tac_apply(s: *TacState, fact_idx: nx_int) -> nx_int {
123 if s.n_goals <= 0 { return NX_TAC_NOGOAL }
124 let g: *TacGoal = nx_tac_top(s)
125 let f: *K2Thm = nx_k2_at(s.ch, fact_idx)
126 let s_term: *Term = f.stmt
127 if s_term.kind != NX_TERM_APP { return NX_TAC_FAIL }
128 if s_term.sym != NX_K2_SYM_IMP { return NX_TAC_FAIL }
129 let ant: *Term = nx_term_arg(s_term, 0)
130 let con: *Term = nx_term_arg(s_term, 1)
131 if nx_term_eq(con, g.target) == 0 { return NX_TAC_FAIL }
132 // Replace top goal target with antecedent; remember the IMP so
133 // a later exact/auto can MP through it. Simplest: push subgoal
134 // for ant; on close, MP to discharge.
135 g.target = ant
136 // We store fact_idx in parent (overloading) so exact knows to MP.
137 // Use a sentinel offset trick: parent = -100 - fact_idx encodes
138 // "after closing target, MP through fact_idx". Decoded by the
139 // exact handler.
140 g.parent = 0 - 100 - fact_idx
141 return NX_TAC_OK
142}
143
144// === split === if goal is (A & B), produce two subgoals A then B.
145func nx_tac_split(s: *TacState) -> nx_int {
146 if s.n_goals <= 0 { return NX_TAC_NOGOAL }
147 let g: *TacGoal = nx_tac_top(s)
148 let goal: *Term = g.target
149 if goal.kind != NX_TERM_APP { return NX_TAC_FAIL }
150 if goal.sym != NX_K2_SYM_AND { return NX_TAC_FAIL }
151 let a: *Term = nx_term_arg(goal, 0)
152 let b: *Term = nx_term_arg(goal, 1)
153 g.target = b // bottom of stack: B (second to close)
154 if s.n_goals >= s.cap_goals { return NX_TAC_FAIL }
155 let g2: *TacGoal = ((s.goals as nx_int) + (s.n_goals * NX_TAC_GOAL_BYTES)) as *TacGoal
156 g2.target = a // top of stack: A (first to close)
157 g2.parent = 0 - 1
158 s.n_goals = s.n_goals + 1
159 return NX_TAC_OK
160}
161
162// === done? ===
163func nx_tac_done(s: *TacState) -> nx_int {
164 if s.n_goals == 0 { return 1 }
165 return 0
166}