Documentation

Mathlib.Data.Ineq

Ineq datatype #

This file contains an enum Ineq (whose constructors are eq, le, lt), and operations involving it. The type Ineq is one of the fundamental objects manipulated by the linarith and linear_combination tactics.

Inequalities #

source
🔶 coverage
inductive Mathlib.Ineq :
Type

The three-element type Ineq is used to represent the strength of a comparison between terms.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance Mathlib.instDecidableEqIneq :
    DecidableEq Ineq
    source
    🔸 coverage
    @[implicit_reducible]
    instance Mathlib.instInhabitedIneq :
    Inhabited Ineq
    source
    🔸 coverage
    def Mathlib.instInhabitedIneq.default :
    Ineq
    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance Mathlib.instReprIneq :
      Repr Ineq
      source
      🔸 coverage
      def Mathlib.instReprIneq.repr :
      Ineq → ℕ → Std.Format
      Instances For
        source
        🔸 coverage
        def Mathlib.Ineq.max :
        Ineq → Ineq → Ineq

        max R1 R2 computes the strength of the sum of two inequalities. If t1 R1 0 and t2 R2 0, then t1 + t2 (max R1 R2) 0.

        Instances For
          source
          🔸 coverage
          def Mathlib.Ineq.cmp :
          Ineq → Ineq → Ordering

          Ineq is ordered eq < le < lt.

          Instances For
            source
            🔸 coverage
            def Mathlib.Ineq.toString :
            Ineq → String

            Prints an Ineq as the corresponding infix symbol.

            Instances For
              source
              🔸 coverage
              @[implicit_reducible]
              instance Mathlib.Ineq.instToString :
              ToString Ineq
              source
              🔸 coverage
              @[implicit_reducible]
              instance Mathlib.Ineq.instToFormat :
              Std.ToFormat Ineq

              Parsing inequalities #

              source
              🔸 coverage
              def Lean.Expr.ineq? (e : Expr) :
              MetaM (Mathlib.Ineq × Expr × Expr × Expr)

              Given an expression e, parse it as a =, ≤ or <, and return this relation (as a Linarith.Ineq) together with the type in which the (in)equality occurs and the two sides of the (in)equality.

              This function is more naturally in the Option monad, but it is convenient to put in MetaM for compositionality.

              Instances For
                source
                🔸 coverage
                def Lean.Expr.ineqOrNotIneq? (e : Expr) :
                MetaM (Bool × Mathlib.Ineq × Expr × Expr × Expr)

                Given an expression e, parse it as a =, ≤ or <, or the negation of such, and return this relation (as a Linarith.Ineq) together with the type in which the (in)equality occurs, the two sides of the (in)equality, and a Boolean flag indicating the presence or absence of the ¬.

                This function is more naturally in the Option monad, but it is convenient to put in MetaM for compositionality.

                Instances For