Documentation

Init.Data.Nat.Linear

Helper definitions and theorems for constructing linear arithmetic proofs.

@[reducible, inline]
Equations
    Instances For
      @[reducible, inline]
      Equations
        Instances For

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

          Equations
            Instances For
              Equations
                Instances For
                  Instances For
                    Equations
                      Instances For
                        @[reducible, inline]
                        Equations
                          Instances For
                            Equations
                              Instances For
                                def Nat.Linear.Poly.insert (k : Nat) (v : Var) (p : Poly) :
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For
                                            def Nat.Linear.Poly.cancelAux (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly) :
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Instances For
                                                                        Equations
                                                                          Instances For
                                                                            Equations
                                                                              Instances For
                                                                                def Nat.Linear.Expr.toPoly.go (coeff : Nat) :
                                                                                ExprPolyPoly
                                                                                Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Instances For
                                                                                              Instances For
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        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_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.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.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.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.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
                                                                                                                                          Instances For