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 tactic (and, in future, also the linear_combination tactic).

Inequalities

inductive Mathlib.Ineq : Type

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

• eq: Mathlib.Ineq
• le: Mathlib.Ineq
• lt: Mathlib.Ineq

instance Mathlib.instDecidableEqIneq : DecidableEq Mathlib.Ineq

Equations

• Mathlib.instDecidableEqIneq x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Mathlib.instInhabitedIneq : Inhabited Mathlib.Ineq

Equations

• Mathlib.instInhabitedIneq = { default := Mathlib.Ineq.eq }

instance Mathlib.instReprIneq : Repr Mathlib.Ineq

Equations

• Mathlib.instReprIneq = { reprPrec := Mathlib.reprIneq✝ }

def Mathlib.Ineq.max : Mathlib.Ineq → Mathlib.Ineq → Mathlib.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.

Equations

• Mathlib.Ineq.lt.max x = Mathlib.Ineq.lt
• x.max Mathlib.Ineq.lt = Mathlib.Ineq.lt
• Mathlib.Ineq.le.max x = Mathlib.Ineq.le
• x.max Mathlib.Ineq.le = Mathlib.Ineq.le
• Mathlib.Ineq.eq.max Mathlib.Ineq.eq = Mathlib.Ineq.eq

def Mathlib.Ineq.cmp : Mathlib.Ineq → Mathlib.Ineq → Ordering

Ineq is ordered eq < le < lt.

Equations

• Mathlib.Ineq.eq.cmp Mathlib.Ineq.eq = Ordering.eq
• Mathlib.Ineq.eq.cmp x = Ordering.lt
• Mathlib.Ineq.le.cmp Mathlib.Ineq.le = Ordering.eq
• Mathlib.Ineq.le.cmp Mathlib.Ineq.lt = Ordering.lt
• Mathlib.Ineq.lt.cmp Mathlib.Ineq.lt = Ordering.eq
• x✝.cmp x = Ordering.gt

def Mathlib.Ineq.toString : Mathlib.Ineq → String

Prints an Ineq as the corresponding infix symbol.

Equations

• Mathlib.Ineq.eq.toString = "="
• Mathlib.Ineq.le.toString = "≤"
• Mathlib.Ineq.lt.toString = "<"

instance Mathlib.Ineq.instToString : ToString Mathlib.Ineq

Equations

• Mathlib.Ineq.instToString = { toString := Mathlib.Ineq.toString }

instance Mathlib.Ineq.instToFormat : Lean.ToFormat Mathlib.Ineq

Equations

• Mathlib.Ineq.instToFormat = { format := fun (i : Mathlib.Ineq) => Std.Format.text i.toString }

Parsing inequalities

def Lean.Expr.ineq? (e : Lean.Expr) : Lean.MetaM (Mathlib.Ineq × Lean.Expr × Lean.Expr × Lean.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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Expr.ineqOrNotIneq? (e : Lean.Expr) : Lean.MetaM (Bool × Mathlib.Ineq × Lean.Expr × Lean.Expr × Lean.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.

Equations

• One or more equations did not get rendered due to their size.