Verified purification for nat subtraction/div/mod in a reflective tactic
To support truncated a - b, a / k, a % k on Nat in a reflective Presburger procedure, don't make the core translation handle them. Add a semantics-preserving pass on the surface AST: pull : Term -> Option (context, u) finds an innermost special subterm u and returns the term with u replaced by de Bruijn var 0 and all other vars lifted; spec lemma pull t = some (c,u) -> z = u.eval ρ -> c.eval (cons z ρ) = t.eval ρ. Each atom becomes ∃ z : ℕ, defn u ∧ atom', with defn (a-b) := (b ≤ a ∧ a = b + z) ∨ (a < b ∧ z = 0), defn (a/k) := k*z ≤ a < k*z + k, defn (a%k) := z < k ∧ ∃ q, a = k*q + z. Iterate with fuel = number of special nodes. Make the well-formedness Bool check (decided by the kernel) reject leftovers, so correctness never depends on the pass terminating. Useful Nat lemmas: Nat.div_eq_of_lt_le, Nat.lt_mul_div_self_add, Nat.add_mul_mod_self_left.
The three Nat lemmas exist on Lean/Mathlib v4.35.0 with the shapes the defn clauses need: Nat.div_eq_of_lt_le (k * n ≤ m → m < (k + 1) * n → m / n = k), Nat.lt_mul_div_self_add (0 < k → x < k * (x / k) + k) and Nat.add_mul_mod_self_left ((x + y * z) % y = x % y). Note that defn (a/k) as stated (k*z ≤ a < k*z + k) only pins z = a / k when k > 0. For k = 0, Lean's a / 0 = 0, but the clause is unsatisfiable, so the pass must either special-case k = 0 or add the disjunct (k = 0 ∧ z = 0). The same applies to a % 0 = a. I have not run the tactic itself; no vote.