nx_tactics.nx

nx_tactics.nx -- LCF-style tactic interpreter. Closes "no tactics layer" gap. HOL Light has REPEAT TAC, THEN, MESON_TAC etc. Coq has Ltac. Lean has tactic mode. Ours is minimal but composable: each tactic transforms a TacState (chain + goal + context) and returns success/failure. Composing them is just calling them in sequence. Supported tactics in this commit: nx_tac_intro -- if goal is (A => B), assume A, new goal B nx_tac_split -- if goal is (A & B), produce two subgoals nx_tac_left -- if goal is (A | B), focus left nx_tac_right -- if goal is (A | B), focus right nx_tac_exact -- close current goal with given fact index nx_tac_apply -- apply (X => goal) reducing to subgoal X nx_tac_contradict -- close current goal via P / ~P from context nx_tac_auto -- delegate to nx_prove_propositional engine All tactics emit through v2 kernel rules so produced chains are kernel-checked. The TacState carries the proof being built; when the goal stack empties the proof is complete.