Int certificates for the Sym.Arith normalizer

Over Int, a linear relation k * q + c = 0 with k > 0 forces k ∣ c, and k * q + c ≤ 0 ↔ q + ⌈c / k⌉ ≤ 0. These theorems let the normalizer divide the coefficients of an Int relation by their gcd, close an equation whose constant is not divisible by the gcd, tighten an inequality, and normalize a divisibility constraint k ∣ e by the gcd of k and the coefficients of e, as simp +arith does with Int.Linear. The polynomial q and the constant c are computed by the normalizer; the kernel checks p = k * q + c by evaluation (split_cert).

noncomputable def Lean.Grind.CommRing.split_cert (p q : Poly) (k c : Int) : Bool

p = k * q + c with k > 0.

theorem Lean.Grind.CommRing.denote_of_split_cert (ctx : Context Int) {p q : Poly} {k c : Int} (h : split_cert p q k c = true) : 0 < k ∧ Poly.denote ctx p = k * Poly.denote ctx q + c

noncomputable def Lean.Grind.CommRing.eq_div_cert (lhs rhs lhs' rhs' : Expr) (k : Int) : Bool

theorem Lean.Grind.CommRing.eq_norm_div_expr (ctx : Context Int) (lhs rhs lhs' rhs' : Expr) (k : Int) : eq_div_cert lhs rhs lhs' rhs' k = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

noncomputable def Lean.Grind.CommRing.eq_unsat_cert (lhs rhs : Expr) (q : Poly) (k c : Int) : Bool

theorem Lean.Grind.CommRing.eq_norm_unsat_expr (ctx : Context Int) (lhs rhs : Expr) (q : Poly) (k c : Int) : eq_unsat_cert lhs rhs q k c = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = False

noncomputable def Lean.Grind.CommRing.le_tight_cert (lhs rhs lhs' rhs' : Expr) (q : Poly) (k c : Int) : Bool

theorem Lean.Grind.CommRing.le_norm_tight_expr (ctx : Context Int) (lhs rhs lhs' rhs' : Expr) (q : Poly) (k c : Int) : le_tight_cert lhs rhs lhs' rhs' q k c = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')

noncomputable def Lean.Grind.CommRing.dvd_cert (k : Int) (e e' : Expr) (k' : Int) (q : Poly) (g c : Int) : Bool

theorem Lean.Grind.CommRing.dvd_norm_expr (ctx : Context Int) (k : Int) (e e' : Expr) (k' : Int) (q : Poly) (g c : Int) : dvd_cert k e e' k' q g c = true → (k ∣ Expr.denote ctx e) = (k' ∣ Expr.denote ctx e')

noncomputable def Lean.Grind.CommRing.dvd_unsat_cert (k : Int) (e : Expr) (q : Poly) (g c : Int) : Bool

theorem Lean.Grind.CommRing.dvd_norm_unsat_expr (ctx : Context Int) (k : Int) (e : Expr) (q : Poly) (g c : Int) : dvd_unsat_cert k e q g c = true → (k ∣ Expr.denote ctx e) = False