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.

Equations

• Lean.Grind.CommRing.split_cert p q k c = (Int.blt' 0 k && p.beq' ((Lean.Grind.CommRing.Poly.mulConst_k k q).addConst_k c))

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

Equations

• Lean.Grind.CommRing.eq_div_cert lhs rhs lhs' rhs' k = (!k.beq' 0 && (lhs.sub rhs).toPoly_k.beq' (Lean.Grind.CommRing.Poly.mulConst_k k (lhs'.sub rhs').toPoly_k))

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

Equations

• Lean.Grind.CommRing.eq_unsat_cert lhs rhs q k c = (Lean.Grind.CommRing.split_cert (lhs.sub rhs).toPoly_k q k c && !(c % k).beq' 0)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Grind.CommRing.dvd_cert k e e' k' q g c = (Lean.Grind.CommRing.split_cert e.toPoly_k q g c && k.beq' (k' * g) && (c % g).beq' 0 && e'.toPoly_k.beq' (q.addConst_k (c / g)))

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

Equations

• Lean.Grind.CommRing.dvd_unsat_cert k e q g c = (Lean.Grind.CommRing.split_cert e.toPoly_k q g c && (k % g).beq' 0 && !(c % g).beq' 0)

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