Typeclasses for algebraic operations

Notation typeclass for Inv, the multiplicative analogue of Neg.

We also introduce notation classes SMul and VAdd for multiplicative and additive actions.

SMul is typically, but not exclusively, used for scalar multiplication-like operators. See the module Algebra.AddTorsor for a motivating example for the name VAdd (vector addition).

Note Zero has already been defined in core Lean.

Notation

• a • b is used as notation for HSMul.hSMul a b.
• a +ᵥ b is used as notation for HVAdd.hVAdd a b.

class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) : Type (max (max u v) w)

The notation typeclass for heterogeneous additive actions. This enables the notation a +ᵥ b : γ where a : α, b : β.

• hVAdd : α → β → γ

  a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent.

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) : Type (max (max u v) w)

The notation typeclass for heterogeneous scalar multiplication. This enables the notation a • b : γ where a : α, b : β.

It is assumed to represent a left action in some sense. The notation a • b is augmented with a macro (below) to have it elaborate as a left action. Only the b argument participates in the elaboration algorithm: the algorithm uses the type of b when calculating the type of the surrounding arithmetic expression and it tries to insert coercions into b to get some b' such that a • b' has the same type as b'. See the module documentation near the macro for more details.

• hSMul : α → β → γ

  a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

class VAdd (G : Type u) (P : Type v) : Type (max u v)

Type class for the +ᵥ notation.

• vadd : G → P → P

  a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

class VSub (G : outParam (Type u_1)) (P : Type u_2) : Type (max u_1 u_2)

Type class for the -ᵥ notation.

• vsub : P → P → G

  a -ᵥ b computes the difference of a and b. The meaning of this notation is type-dependent, but it is intended to be used for additive torsors.

class SMul (M : Type u) (α : Type v) : Type (max u v)

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

• smul : M → α → α

  a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

theorem SMul.ext {M : Type u} {α : Type v} {x y : SMul M α} (smul : smul = smul) : x = y

theorem VAdd.ext {G : Type u} {P : Type v} {x y : VAdd G P} (vadd : vadd = vadd) : x = y

def «term_+ᵥ_» : Lean.TrailingParserDescr

a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent.

Equations

• «term_+ᵥ_» = Lean.ParserDescr.trailingNode `«term_+ᵥ_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ ") (Lean.ParserDescr.cat `term 65))

def «term_-ᵥ_» : Lean.TrailingParserDescr

a -ᵥ b computes the difference of a and b. The meaning of this notation is type-dependent, but it is intended to be used for additive torsors.

Equations

• «term_-ᵥ_» = Lean.ParserDescr.trailingNode `«term_-ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ᵥ ") (Lean.ParserDescr.cat `term 66))

def «term_•_» : Lean.TrailingParserDescr

a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

Equations

• «term_•_» = Lean.ParserDescr.trailingNode `«term_•_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 73))

We have a macro to make x • y notation participate in the expression tree elaborator, like other arithmetic expressions such as +, *, /, ^, =, inequalities, etc. The macro is using the leftact% elaborator introduced in this RFC.

As a concrete example of the effect of this macro, consider

variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
#check m + r • n

Without the macro, the expression would elaborate as m + ↑(r • n : ↑N) : M. With the macro, the expression elaborates as m + r • (↑n : M) : M. To get the first interpretation, one can write m + (r • n :).

Here is a quick review of the expression tree elaborator:

1. It builds up an expression tree of all the immediately accessible operations that are marked with binop%, unop%, leftact%, rightact%, binrel%, etc.
2. It elaborates every leaf term of this tree (without an expected type, so as if it were temporarily wrapped in (... :)).
3. Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists.
4. It inserts coercions around leaf terms wherever needed.

The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.

Note(kmill): If we were to remove HSMul and switch to using SMul directly, then the expression tree elaborator would not be able to insert coercions within the right operand; they would likely appear as ↑(x • y) rather than x • ↑y, unlike other arithmetic operations.

@[defaultInstance 1000]

instance instHSMul {α : Type u_1} {β : Type u_2} [SMul α β] : HSMul α β β

Equations

• instHSMul = { hSMul := SMul.smul }

@[defaultInstance 1000]

instance instHVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] : HVAdd α β β

Equations

• instHVAdd = { hVAdd := VAdd.vadd }

theorem SMul.smul_eq_hSMul {α : Type u_1} {β : Type u_2} [SMul α β] : smul = HSMul.hSMul

theorem VAdd.vadd_eq_hVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] : vadd = HVAdd.hVAdd

class Inv (α : Type u) : Type u

Class of types that have an inversion operation.

• inv : α → α

  Invert an element of α, denoted by a⁻¹.

def «term_⁻¹» : Lean.TrailingParserDescr

Invert an element of α, denoted by a⁻¹.

Equations

• «term_⁻¹» = Lean.ParserDescr.trailingNode `«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

@[simp]

theorem mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : α) (b : P → α) (c : ¬P → α) : (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

theorem add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : α) (b : P → α) (c : ¬P → α) : (a + if h : P then b h else c h) = if h : P then a + b h else a + c h

@[simp]

theorem mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c : α) : (a * if P then b else c) = if P then a * b else a * c

theorem add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c : α) : (a + if P then b else c) = if P then a + b else a + c

@[simp]

theorem dite_mul {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

theorem dite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) + c = if h : P then a h + c else b h + c

@[simp]

theorem ite_mul {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c : α) : (if P then a else b) * c = if P then a * c else b * c

theorem ite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c : α) : (if P then a else b) + c = if P then a + c else b + c

theorem dite_mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) : ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

theorem dite_add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) : ((if h : P then a h else b h) + if h : P then c h else d h) = if h : P then a h + c h else b h + d h

theorem ite_mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a b c d : α) : ((if P then a else b) * if P then c else d) = if P then a * c else b * d

theorem ite_add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a b c d : α) : ((if P then a else b) + if P then c else d) = if P then a + c else b + d

theorem div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : α) (b : P → α) (c : ¬P → α) : (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

theorem sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : α) (b : P → α) (c : ¬P → α) : (a - if h : P then b h else c h) = if h : P then a - b h else a - c h

theorem div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c : α) : (a / if P then b else c) = if P then a / b else a / c

theorem sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c : α) : (a - if P then b else c) = if P then a - b else a - c

theorem dite_div {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

theorem dite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : P → α) (b : ¬P → α) (c : α) : (if h : P then a h else b h) - c = if h : P then a h - c else b h - c

theorem ite_div {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c : α) : (if P then a else b) / c = if P then a / c else b / c

theorem ite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c : α) : (if P then a else b) - c = if P then a - c else b - c

theorem dite_div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) : ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

theorem dite_sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α) : ((if h : P then a h else b h) - if h : P then c h else d h) = if h : P then a h - c h else b h - d h

theorem ite_div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a b c d : α) : ((if P then a else b) / if P then c else d) = if P then a / c else b / d

theorem ite_sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a b c d : α) : ((if P then a else b) - if P then c else d) = if P then a - c else b - d

class One (α : Type u) : Type u

• one : α

@[instance 300]

instance One.toOfNat1 {α : Type u_2} [One α] : OfNat α 1

Equations

• One.toOfNat1 = { ofNat := One.one }

@[instance 200]

instance One.ofOfNat1 {α : Type u_2} [OfNat α 1] : One α

Equations

• One.ofOfNat1 = { one := 1 }

@[instance 20]

instance Zero.instNonempty {α : Type u} [Zero α] : Nonempty α

@[instance 20]

instance One.instNonempty {α : Type u} [One α] : Nonempty α

theorem Subsingleton.eq_one {α : Type u} [One α] [Subsingleton α] (a : α) : a = 1

theorem Subsingleton.eq_zero {α : Type u} [Zero α] [Subsingleton α] (a : α) : a = 0