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
        @[reducible, inline]
        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
                            Equations
                            Instances For
                              Equations
                              Instances For
                                Equations
                                • p.norm = p.sort.fuse
                                Instances For
                                  Equations
                                  • e.toNormPoly = e.toPoly.norm
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        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 }
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            • c.norm = match c.lhs.sort.fuse.cancel c.rhs.sort.fuse with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
                                            Instances For
                                              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
                                              Instances For
                                                Equations
                                                • c.isValid = bif c.eq then c.lhs.isZero && c.rhs.isZero else c.lhs.isZero
                                                Instances For
                                                  Equations
                                                  • c.toPoly = { eq := c.eq, lhs := c.lhs.toPoly, rhs := c.rhs.toPoly }
                                                  Instances For
                                                    Equations
                                                    • c.toNormPoly = match c.lhs.toNormPoly.cancel c.rhs.toNormPoly with | (lhs, rhs) => { eq := c.eq, lhs := lhs, rhs := rhs }
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • c.toExpr = { eq := c.eq, lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
                                                            Instances For
                                                              theorem Nat.Linear.Expr.of_cancel_eq (ctx : Nat.Linear.Context) (a : Nat.Linear.Expr) (b : Nat.Linear.Expr) (c : Nat.Linear.Expr) (d : Nat.Linear.Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
                                                              theorem Nat.Linear.Expr.of_cancel_le (ctx : Nat.Linear.Context) (a : Nat.Linear.Expr) (b : Nat.Linear.Expr) (c : Nat.Linear.Expr) (d : Nat.Linear.Expr) (h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)) :
                                                              theorem Nat.Linear.Expr.of_cancel_lt (ctx : Nat.Linear.Context) (a : Nat.Linear.Expr) (b : Nat.Linear.Expr) (c : Nat.Linear.Expr) (d : Nat.Linear.Expr) (h : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)) :
                                                              theorem Nat.Linear.ExprCnstr.toPoly_norm_eq (c : Nat.Linear.ExprCnstr) :
                                                              c.toPoly.norm = c.toNormPoly
                                                              def Nat.elimOffset {α : Sort u} (a : Nat) (b : Nat) (k : Nat) (h₁ : a + k = b + k) (h₂ : a = bα) :
                                                              α
                                                              Equations
                                                              • a.elimOffset b k h₁ h₂ = h₂
                                                              Instances For