Documentation

Init.Data.Nat.Linear

Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]
Equations
@[reducible, inline]
Equations

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

Equations
Instances For
@[reducible, inline]
Equations
Equations
def Nat.Linear.Poly.insert (k : Nat) (v : Var) (p : Poly) :
Equations
def Nat.Linear.Poly.mul (k : Nat) (p : Poly) :
Equations
Equations
def Nat.Linear.Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) :
Equations
Equations
def Nat.Linear.Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) :
Equations
def Nat.Linear.Poly.combine (p₁ p₂ : Poly) :
Equations
def Nat.Linear.Expr.toPoly.go (coeff : Nat) :
ExprPolyPoly
Equations
Equations
  • e.toNormPoly = e.toPoly.norm
Equations
Equations
Equations
  • c₁.combine c₂ = match (c₁.lhs.combine c₂.lhs).cancel (c₁.rhs.combine c₂.rhs) with | (lhs, rhs) => { eq := c₁.eq && c₂.eq, lhs := lhs, rhs := rhs }
Equations
Equations
  • c.norm = match c.lhs.norm.cancel c.rhs.norm with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
Equations
  • c.isUnsat = bif c.eq then c.lhs.isZero && c.rhs.isNonZero || c.lhs.isNonZero && c.rhs.isZero else c.lhs.isNonZero && c.rhs.isZero
Equations
  • c.isValid = bif c.eq then c.lhs.isZero && c.rhs.isZero else c.lhs.isZero
Equations
  • c.toPoly = { eq := c.eq, lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }
Equations
  • c.toNormPoly = match c.lhs.toNormPoly.cancel c.rhs.toNormPoly with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
Equations
  • c.toExpr = { eq := c.eq, lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
theorem Nat.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.Linear.Poly.denote_norm_go (ctx : Context) (p r : Poly) :
denote ctx (norm.go p r) = denote ctx p + denote ctx r
theorem Nat.Linear.Poly.denote_sort (ctx : Context) (m : Poly) :
denote ctx m.norm = denote ctx m
theorem Nat.Linear.Poly.denote_append (ctx : Context) (p q : Poly) :
denote ctx (p ++ q) = denote ctx p + denote ctx q
theorem Nat.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.Linear.Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) :
denote ctx (mul k p) = k * denote ctx p
theorem Nat.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.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.Linear.Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) :
denote_eq ctx (m₁.cancel m₂)
theorem Nat.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.Linear.Poly.denote_eq_cancel_eq (ctx : Context) (m₁ m₂ : Poly) :
denote_eq ctx (m₁.cancel m₂) = denote_eq ctx (m₁, m₂)
theorem Nat.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.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.Linear.Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) :
denote_le ctx (m₁.cancel m₂)
theorem Nat.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.Linear.Poly.denote_le_cancel_eq (ctx : Context) (m₁ m₂ : Poly) :
denote_le ctx (m₁.cancel m₂) = denote_le ctx (m₁, m₂)
theorem Nat.Linear.Poly.denote_combineAux (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) :
denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
theorem Nat.Linear.Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) :
denote ctx (p₁.combine p₂) = denote ctx p₁ + denote ctx p₂
theorem Nat.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.Linear.Expr.denote_toPoly (ctx : Context) (e : Expr) :
Poly.denote ctx e.toPoly = denote ctx e
theorem Nat.Linear.Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) :
denote ctx a = denote ctx b
theorem Nat.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.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.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.Linear.ExprCnstr.toPoly_norm_eq (c : ExprCnstr) :
c.toPoly.norm = c.toNormPoly
theorem Nat.Linear.Poly.mul.go_denote (ctx : Context) (k : Nat) (p : Poly) :
denote ctx (go k p) = k * denote ctx p
theorem Nat.Linear.PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) :
denote ctx (mul (k + 1) c) = denote ctx c
theorem Nat.Linear.PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ : denote ctx c₁) (h₂ : denote ctx c₂) :
denote ctx (c₁.combine c₂)
theorem Nat.Linear.Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} :
p.isNum? = some kdenote ctx p = k
theorem Nat.Linear.Poly.of_isZero (ctx : Context) {p : Poly} (h : p.isZero = true) :
denote ctx p = 0
theorem Nat.Linear.Poly.of_isNonZero (ctx : Context) {p : Poly} (h : p.isNonZero = true) :
denote ctx p > 0
theorem Nat.Linear.ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat = true) :
denote ctx c = False
theorem Nat.Linear.ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid = true) :
denote ctx c = True
theorem Nat.Linear.Certificate.of_combine (ctx : Context) (cs : Certificate) (h : PolyCnstr.denote ctx cs.combineFalse) :
denote ctx cs
theorem Nat.Linear.Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : cs.combine.isUnsat = true) :
denote ctx cs
theorem Nat.Linear.Poly.denote_toExpr (ctx : Context) (p : Poly) :
Expr.denote ctx p.toExpr = denote ctx p
theorem Nat.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.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.elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = bα) :
α
Equations
  • a.elimOffset b k h₁ h₂ = h₂