Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]

abbrev Nat.Internal.Linear.Var : Type

@[reducible, inline]

abbrev Nat.Internal.Linear.Context : Type

@[reducible, inline]

abbrev Nat.Internal.Linear.fixedVar : Nat

When encoding polynomials. We use fixedVar for encoding numerals. The denotation of fixedVar is always 1.

@[reducible, inline]

noncomputable abbrev Nat.Internal.Linear.Var.denote (ctx : Context) (v : Var) : Nat

inductive Nat.Internal.Linear.Expr : Type

• num (v : Nat) : Expr
• var (i : Var) : Expr
• add (a b : Expr) : Expr
• mulL (k : Nat) (a : Expr) : Expr
• mulR (a : Expr) (k : Nat) : Expr

@[instance_reducible]

instance Nat.Internal.Linear.instInhabitedExpr : Inhabited Expr

@[instance_reducible]

instance Nat.Internal.Linear.instBEqExpr : BEq Expr

def Nat.Internal.Linear.instBEqExpr.beq : Expr → Expr → Bool

@[reducible, inline]

noncomputable abbrev Nat.Internal.Linear.Expr.denote (ctx : Context) : Expr → Nat

@[reducible, inline]

abbrev Nat.Internal.Linear.Poly : Type

@[reducible, inline]

noncomputable abbrev Nat.Internal.Linear.Poly.denote (ctx : Context) (p : Poly) : Nat

def Nat.Internal.Linear.Poly.insert (k : Nat) (v : Var) (p : Poly) : Poly

def Nat.Internal.Linear.Poly.norm (p : Poly) : Poly

def Nat.Internal.Linear.Poly.norm.go (p r : Poly) : Poly

def Nat.Internal.Linear.Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) : Poly × Poly

def Nat.Internal.Linear.hugeFuel : Nat

def Nat.Internal.Linear.Poly.cancel (p₁ p₂ : Poly) : Poly × Poly

def Nat.Internal.Linear.Poly.isNum? (p : Poly) : Option Nat

def Nat.Internal.Linear.Poly.isZero (p : Poly) : Bool

def Nat.Internal.Linear.Poly.isNonZero (p : Poly) : Bool

@[inline]

abbrev Nat.Internal.Linear.Poly.denote_eq (ctx : Context) (mp : Poly × Poly) : Prop

@[inline]

abbrev Nat.Internal.Linear.Poly.denote_le (ctx : Context) (mp : Poly × Poly) : Prop

def Nat.Internal.Linear.Expr.toPoly (e : Expr) : Poly

def Nat.Internal.Linear.Expr.toPoly.go (coeff : Nat) : Expr → Poly → Poly

def Nat.Internal.Linear.Expr.toNormPoly (e : Expr) : Poly

def Nat.Internal.Linear.Expr.inc (e : Expr) : Expr

structure Nat.Internal.Linear.PolyCnstr : Type

• eq : Bool
• lhs : Poly
• rhs : Poly

@[instance_reducible]

instance Nat.Internal.Linear.instBEqPolyCnstr : BEq PolyCnstr

def Nat.Internal.Linear.instBEqPolyCnstr.beq : PolyCnstr → PolyCnstr → Bool

instance Nat.Internal.Linear.instReflBEqPolyCnstr : ReflBEq PolyCnstr

instance Nat.Internal.Linear.instLawfulBEqPolyCnstr : LawfulBEq PolyCnstr

structure Nat.Internal.Linear.ExprCnstr : Type

• eq : Bool
• lhs : Expr
• rhs : Expr

@[reducible, inline]

abbrev Nat.Internal.Linear.PolyCnstr.denote (ctx : Context) (c : PolyCnstr) : Prop

def Nat.Internal.Linear.PolyCnstr.norm (c : PolyCnstr) : PolyCnstr

def Nat.Internal.Linear.PolyCnstr.isUnsat (c : PolyCnstr) : Bool

def Nat.Internal.Linear.PolyCnstr.isValid (c : PolyCnstr) : Bool

@[reducible, inline]

abbrev Nat.Internal.Linear.ExprCnstr.denote (ctx : Context) (c : ExprCnstr) : Prop

def Nat.Internal.Linear.ExprCnstr.toPoly (c : ExprCnstr) : PolyCnstr

def Nat.Internal.Linear.ExprCnstr.toNormPoly (c : ExprCnstr) : PolyCnstr

def Nat.Internal.Linear.monomialToExpr (k : Nat) (v : Var) : Expr

def Nat.Internal.Linear.Poly.toExpr (p : Poly) : Expr

def Nat.Internal.Linear.Poly.toExpr.go (e : Expr) (p : Poly) : Expr

def Nat.Internal.Linear.PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr

theorem Nat.Internal.Linear.Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote ctx (insert k v p) = denote ctx p + k * Var.denote ctx v

theorem Nat.Internal.Linear.Poly.denote_norm_go (ctx : Context) (p r : Poly) : denote ctx (norm.go p r) = denote ctx p + denote ctx r

theorem Nat.Internal.Linear.Poly.denote_sort (ctx : Context) (m : Poly) : denote ctx m.norm = denote ctx m

theorem Nat.Internal.Linear.Poly.denote_append (ctx : Context) (p q : Poly) : denote ctx (p ++ q) = denote ctx p + denote ctx q

theorem Nat.Internal.Linear.Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote ctx ((k, v) :: p) = k * Var.denote ctx v + denote ctx p

theorem Nat.Internal.Linear.Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.reverse p) = denote ctx p

theorem Nat.Internal.Linear.Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) : denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)

theorem Nat.Internal.Linear.Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)) : denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

theorem Nat.Internal.Linear.Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) : denote_eq ctx (m₁.cancel m₂)

theorem Nat.Internal.Linear.Poly.of_denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁.cancel m₂)) : denote_eq ctx (m₁, m₂)

theorem Nat.Internal.Linear.Poly.denote_eq_cancel_eq (ctx : Context) (m₁ m₂ : Poly) : denote_eq ctx (m₁.cancel m₂) = denote_eq ctx (m₁, m₂)

theorem Nat.Internal.Linear.Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)) : denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)

theorem Nat.Internal.Linear.Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) (h : denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)) : denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

theorem Nat.Internal.Linear.Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) : denote_le ctx (m₁.cancel m₂)

theorem Nat.Internal.Linear.Poly.of_denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁.cancel m₂)) : denote_le ctx (m₁, m₂)

theorem Nat.Internal.Linear.Poly.denote_le_cancel_eq (ctx : Context) (m₁ m₂ : Poly) : denote_le ctx (m₁.cancel m₂) = denote_le ctx (m₁, m₂)

theorem Nat.Internal.Linear.Expr.denote_toPoly_go {k : Nat} {p : Poly} (ctx : Context) (e : Expr) : Poly.denote ctx (toPoly.go k e p) = k * denote ctx e + Poly.denote ctx p

theorem Nat.Internal.Linear.Expr.denote_toPoly (ctx : Context) (e : Expr) : Poly.denote ctx e.toPoly = denote ctx e

theorem Nat.Internal.Linear.Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) : denote ctx a = denote ctx b

theorem Nat.Internal.Linear.Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) : (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)

theorem Nat.Internal.Linear.Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) : (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

theorem Nat.Internal.Linear.Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (denote ctx a < denote ctx b) = (denote ctx c < denote ctx d)

theorem Nat.Internal.Linear.ExprCnstr.toPoly_norm_eq (c : ExprCnstr) : c.toPoly.norm = c.toNormPoly

theorem Nat.Internal.Linear.ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : PolyCnstr.denote ctx c.toPoly = denote ctx c

theorem Nat.Internal.Linear.ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : PolyCnstr.denote ctx c.toNormPoly = denote ctx c

theorem Nat.Internal.Linear.Poly.of_isZero (ctx : Context) {p : Poly} (h : p.isZero = true) : denote ctx p = 0

theorem Nat.Internal.Linear.Poly.of_isNonZero (ctx : Context) {p : Poly} (h : p.isNonZero = true) : denote ctx p > 0

theorem Nat.Internal.Linear.PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat = true → denote ctx c = False

theorem Nat.Internal.Linear.PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid = true → denote ctx c = True

theorem Nat.Internal.Linear.ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat = true) : denote ctx c = False

theorem Nat.Internal.Linear.ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid = true) : denote ctx c = True

theorem Nat.Internal.Linear.ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : (c.toNormPoly == d.toPoly) = true) : denote ctx c = denote ctx d

theorem Nat.Internal.Linear.Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : (e.toNormPoly == e'.toPoly) = true) : denote ctx e = denote ctx e'

def Nat.Internal.elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α