structure Data.Dual (α : Type u) : Type u

Dual α reverses the Append (semigroup) operation:

$$\text{Dual}(a) \mathbin{++} \text{Dual}(b) = \text{Dual}(b \mathbin{++} a)$$

If $(S, \diamond)$ is a semigroup, then $(\text{Dual}\;S,\, \diamond^{\text{op}})$ is the opposite semigroup where $a \diamond^{\text{op}} b = b \diamond a$.

• getDual : α

def Data.instBEqDual.beq {α✝ : Type u_1} [BEq α✝] : Dual α✝ → Dual α✝ → Bool

Equations

• Data.instBEqDual.beq { getDual := a } { getDual := b } = (a == b)
• Data.instBEqDual.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqDual {α✝ : Type u_1} [BEq α✝] : BEq (Dual α✝)

Equations

• Data.instBEqDual = { beq := Data.instBEqDual.beq }

def Data.instOrdDual.ord {α✝ : Type u_1} [Ord α✝] : Dual α✝ → Dual α✝ → Ordering

Equations

• Data.instOrdDual.ord { getDual := a } { getDual := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instOrdDual {α✝ : Type u_1} [Ord α✝] : Ord (Dual α✝)

Equations

• Data.instOrdDual = { compare := Data.instOrdDual.ord }

@[implicit_reducible]

instance Data.instReprDual {α✝ : Type u_1} [Repr α✝] : Repr (Dual α✝)

Equations

• Data.instReprDual = { reprPrec := Data.instReprDual.repr }

def Data.instReprDual.repr {α✝ : Type u_1} [Repr α✝] : Dual α✝ → Nat → Std.Format

Equations

• Data.instReprDual.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getDual" ++ Std.Format.text " := " ++ (Std.Format.nest 11 (repr x✝.getDual)).group) " }"

def Data.instHashableDual.hash {α✝ : Type u_1} [Hashable α✝] : Dual α✝ → UInt64

Equations

• Data.instHashableDual.hash { getDual := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instHashableDual {α✝ : Type u_1} [Hashable α✝] : Hashable (Dual α✝)

Equations

• Data.instHashableDual = { hash := Data.instHashableDual.hash }

@[implicit_reducible]

instance Data.instToStringDual {α : Type u_1} [ToString α] : ToString (Dual α)

ToString instance for Dual α, displaying as Dual(...).

Equations

• Data.instToStringDual = { toString := fun (d : Data.Dual α) => toString "Dual(" ++ toString d.getDual ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendDual {α : Type u_1} [Append α] : Append (Dual α)

Append instance for Dual α — reverses the underlying operation: $\text{Dual}(a) \mathbin{++} \text{Dual}(b) = \text{Dual}(b \mathbin{++} a)$.

Equations

• Data.instAppendDual = { append := fun (a b : Data.Dual α) => { getDual := b.getDual ++ a.getDual } }

theorem Data.Dual.append_assoc {α : Type u_1} [Append α] [h : Std.Associative fun (x1 x2 : α) => x1 ++ x2] (a b c : Dual α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of the dual semigroup. Given associativity of $(++)$ on $\alpha$:

$$(\text{Dual}\;a \mathbin{++} \text{Dual}\;b) \mathbin{++} \text{Dual}\;c = \text{Dual}\;a \mathbin{++} (\text{Dual}\;b \mathbin{++} \text{Dual}\;c)$$

structure Data.Endo (α : Type u) : Type u

Endo α wraps endomorphisms $\alpha \to \alpha$. Forms a monoid under function composition:

• Operation: $\text{Endo}(f) \mathbin{++} \text{Endo}(g) = \text{Endo}(f \circ g)$
• Identity: $\text{Endo}(\text{id})$

$$(\text{Endo}\;f \mathbin{++} \text{Endo}\;g)(x) = f(g(x))$$

• appEndo : α → α

@[implicit_reducible]

instance Data.instAppendEndo {α : Type u_1} : Append (Endo α)

Append instance for Endo α via function composition: $\text{Endo}(f) \mathbin{++} \text{Endo}(g) = \text{Endo}(f \circ g)$.

Equations

• Data.instAppendEndo = { append := fun (f g : Data.Endo α) => { appEndo := f.appEndo ∘ g.appEndo } }

theorem Data.Endo.append_assoc {α : Type u_1} (a b c : Endo α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of endomorphism composition. Since $(f \circ g) \circ h = f \circ (g \circ h)$ holds definitionally, this is rfl.

structure Data.First (α : Type u) : Type u

First α keeps the leftmost some value under Append:

$$\text{First}(x) \mathbin{++} \text{First}(y) = \text{First}(x \mathbin{<|>} y)$$

• $\text{First}(\text{some}\;a) \mathbin{++} \_ = \text{First}(\text{some}\;a)$
• $\text{First}(\text{none}) \mathbin{++} y = y$

Identity element: $\text{First}(\text{none})$.

• getFirst : Option α

def Data.instBEqFirst.beq {α✝ : Type u_1} [BEq α✝] : First α✝ → First α✝ → Bool

Equations

• Data.instBEqFirst.beq { getFirst := a } { getFirst := b } = (a == b)
• Data.instBEqFirst.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqFirst {α✝ : Type u_1} [BEq α✝] : BEq (First α✝)

Equations

• Data.instBEqFirst = { beq := Data.instBEqFirst.beq }

@[implicit_reducible]

instance Data.instReprFirst {α✝ : Type u_1} [Repr α✝] : Repr (First α✝)

Equations

• Data.instReprFirst = { reprPrec := Data.instReprFirst.repr }

def Data.instReprFirst.repr {α✝ : Type u_1} [Repr α✝] : First α✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.instToStringFirst {α : Type u_1} [ToString α] : ToString (First α)

ToString instance for First α, displaying as First(...).

Equations

• Data.instToStringFirst = { toString := fun (f : Data.First α) => toString "First(" ++ toString f.getFirst ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendFirst {α : Type u_1} : Append (First α)

Append instance for First α — keeps the leftmost some.

Equations

• Data.instAppendFirst = { append := fun (a b : Data.First α) => { getFirst := a.getFirst <|> b.getFirst } }

theorem Data.First.append_assoc {α : Type u_1} (a b c : First α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of First: $((a \mathbin{++} b) \mathbin{++} c) = (a \mathbin{++} (b \mathbin{++} c))$.

Follows from the associativity of Option's <|> (left-biased choice).

structure Data.Last (α : Type u) : Type u

Last α keeps the rightmost some value under Append:

$$\text{Last}(x) \mathbin{++} \text{Last}(y) = \text{Last}(y \mathbin{<|>} x)$$

• $\_ \mathbin{++} \text{Last}(\text{some}\;b) = \text{Last}(\text{some}\;b)$
• $x \mathbin{++} \text{Last}(\text{none}) = x$

Identity element: $\text{Last}(\text{none})$.

• getLast : Option α

@[implicit_reducible]

instance Data.instBEqLast {α✝ : Type u_1} [BEq α✝] : BEq (Last α✝)

Equations

• Data.instBEqLast = { beq := Data.instBEqLast.beq }

def Data.instBEqLast.beq {α✝ : Type u_1} [BEq α✝] : Last α✝ → Last α✝ → Bool

Equations

• Data.instBEqLast.beq { getLast := a } { getLast := b } = (a == b)
• Data.instBEqLast.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instReprLast {α✝ : Type u_1} [Repr α✝] : Repr (Last α✝)

Equations

• Data.instReprLast = { reprPrec := Data.instReprLast.repr }

def Data.instReprLast.repr {α✝ : Type u_1} [Repr α✝] : Last α✝ → Nat → Std.Format

Equations

• Data.instReprLast.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getLast" ++ Std.Format.text " := " ++ (Std.Format.nest 11 (repr x✝.getLast)).group) " }"

@[implicit_reducible]

instance Data.instToStringLast {α : Type u_1} [ToString α] : ToString (Last α)

ToString instance for Last α, displaying as Last(...).

Equations

• Data.instToStringLast = { toString := fun (l : Data.Last α) => toString "Last(" ++ toString l.getLast ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendLast {α : Type u_1} : Append (Last α)

Append instance for Last α — keeps the rightmost some.

Equations

• Data.instAppendLast = { append := fun (a b : Data.Last α) => { getLast := b.getLast <|> a.getLast } }

theorem Data.Last.append_assoc {α : Type u_1} (a b c : Last α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of Last: $((a \mathbin{++} b) \mathbin{++} c) = (a \mathbin{++} (b \mathbin{++} c))$.

Follows from the associativity of right-biased <|> on Option.

structure Data.Sum (α : Type u) : Type u

Sum α is a monoid wrapper under addition:

• Operation: $\text{Sum}(a) \mathbin{++} \text{Sum}(b) = \text{Sum}(a + b)$
• Identity: $\text{Sum}(0)$

$$\text{Sum}(a) \mathbin{++} \text{Sum}(b) = \text{Sum}(a + b)$$

• getSum : α

def Data.instBEqSum.beq {α✝ : Type u_1} [BEq α✝] : Sum α✝ → Sum α✝ → Bool

Equations

• Data.instBEqSum.beq { getSum := a } { getSum := b } = (a == b)
• Data.instBEqSum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqSum {α✝ : Type u_1} [BEq α✝] : BEq (Sum α✝)

Equations

• Data.instBEqSum = { beq := Data.instBEqSum.beq }

def Data.instOrdSum.ord {α✝ : Type u_1} [Ord α✝] : Sum α✝ → Sum α✝ → Ordering

Equations

• Data.instOrdSum.ord { getSum := a } { getSum := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instOrdSum {α✝ : Type u_1} [Ord α✝] : Ord (Sum α✝)

Equations

• Data.instOrdSum = { compare := Data.instOrdSum.ord }

@[implicit_reducible]

instance Data.instReprSum {α✝ : Type u_1} [Repr α✝] : Repr (Sum α✝)

Equations

• Data.instReprSum = { reprPrec := Data.instReprSum.repr }

def Data.instReprSum.repr {α✝ : Type u_1} [Repr α✝] : Sum α✝ → Nat → Std.Format

Equations

• Data.instReprSum.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getSum" ++ Std.Format.text " := " ++ (Std.Format.nest 10 (repr x✝.getSum)).group) " }"

@[implicit_reducible]

instance Data.instHashableSum {α✝ : Type u_1} [Hashable α✝] : Hashable (Sum α✝)

Equations

• Data.instHashableSum = { hash := Data.instHashableSum.hash }

def Data.instHashableSum.hash {α✝ : Type u_1} [Hashable α✝] : Sum α✝ → UInt64

Equations

• Data.instHashableSum.hash { getSum := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instToStringSum {α : Type u_1} [ToString α] : ToString (Sum α)

ToString instance for Sum α, displaying as Sum(...).

Equations

• Data.instToStringSum = { toString := fun (s : Data.Sum α) => toString "Sum(" ++ toString s.getSum ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendSumOfAdd {α : Type u_1} [Add α] : Append (Sum α)

Append instance for Sum α — delegates to Add: $\text{Sum}(a) \mathbin{++} \text{Sum}(b) = \text{Sum}(a + b)$.

Equations

• Data.instAppendSumOfAdd = { append := fun (a b : Data.Sum α) => { getSum := a.getSum + b.getSum } }

theorem Data.Sum.append_assoc {α : Type u_1} [Add α] [h : Std.Associative fun (x1 x2 : α) => x1 + x2] (a b c : Sum α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of Sum, given associativity of $(+)$ on $\alpha$:

$$(a + b) + c = a + (b + c) \;\implies\; \text{Sum}(a) \mathbin{++} \text{Sum}(b) \mathbin{++} \text{Sum}(c) = \text{Sum}(a) \mathbin{++} (\text{Sum}(b) \mathbin{++} \text{Sum}(c))$$

structure Data.Product (α : Type u) : Type u

Product α is a monoid wrapper under multiplication:

• Operation: $\text{Product}(a) \mathbin{++} \text{Product}(b) = \text{Product}(a \times b)$
• Identity: $\text{Product}(1)$

$$\text{Product}(a) \mathbin{++} \text{Product}(b) = \text{Product}(a \times b)$$

• getProduct : α

def Data.instBEqProduct.beq {α✝ : Type u_1} [BEq α✝] : Product α✝ → Product α✝ → Bool

Equations

• Data.instBEqProduct.beq { getProduct := a } { getProduct := b } = (a == b)
• Data.instBEqProduct.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqProduct {α✝ : Type u_1} [BEq α✝] : BEq (Product α✝)

Equations

• Data.instBEqProduct = { beq := Data.instBEqProduct.beq }

def Data.instOrdProduct.ord {α✝ : Type u_1} [Ord α✝] : Product α✝ → Product α✝ → Ordering

Equations

• Data.instOrdProduct.ord { getProduct := a } { getProduct := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instOrdProduct {α✝ : Type u_1} [Ord α✝] : Ord (Product α✝)

Equations

• Data.instOrdProduct = { compare := Data.instOrdProduct.ord }

def Data.instReprProduct.repr {α✝ : Type u_1} [Repr α✝] : Product α✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.instReprProduct {α✝ : Type u_1} [Repr α✝] : Repr (Product α✝)

Equations

• Data.instReprProduct = { reprPrec := Data.instReprProduct.repr }

@[implicit_reducible]

instance Data.instHashableProduct {α✝ : Type u_1} [Hashable α✝] : Hashable (Product α✝)

Equations

• Data.instHashableProduct = { hash := Data.instHashableProduct.hash }

def Data.instHashableProduct.hash {α✝ : Type u_1} [Hashable α✝] : Product α✝ → UInt64

Equations

• Data.instHashableProduct.hash { getProduct := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instToStringProduct {α : Type u_1} [ToString α] : ToString (Product α)

ToString instance for Product α, displaying as Product(...).

Equations

• Data.instToStringProduct = { toString := fun (p : Data.Product α) => toString "Product(" ++ toString p.getProduct ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendProductOfMul {α : Type u_1} [Mul α] : Append (Product α)

Append instance for Product α — delegates to Mul: $\text{Product}(a) \mathbin{++} \text{Product}(b) = \text{Product}(a \times b)$.

Equations

• Data.instAppendProductOfMul = { append := fun (a b : Data.Product α) => { getProduct := a.getProduct * b.getProduct } }

theorem Data.Product.append_assoc {α : Type u_1} [Mul α] [h : Std.Associative fun (x1 x2 : α) => x1 * x2] (a b c : Product α) : a ++ b ++ c = a ++ (b ++ c)

Associativity of Product, given associativity of $(\times)$ on $\alpha$:

$$(a \times b) \times c = a \times (b \times c) \;\implies\; \text{Product}(a) \mathbin{++} \text{Product}(b) \mathbin{++} \text{Product}(c) = \text{Product}(a) \mathbin{++} (\text{Product}(b) \mathbin{++} \text{Product}(c))$$

structure Data.All : Type

All is the boolean monoid under conjunction $(\wedge)$:

• Operation: $\text{All}(a) \mathbin{++} \text{All}(b) = \text{All}(a \wedge b)$
• Identity: $\text{All}(\text{true})$

$$\text{All}(a) \mathbin{++} \text{All}(b) = \text{All}(a \mathbin{\&\&} b)$$

• getAll : Bool

def Data.instBEqAll.beq : All → All → Bool

Equations

• Data.instBEqAll.beq { getAll := a } { getAll := b } = (a == b)
• Data.instBEqAll.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqAll : BEq All

Equations

• Data.instBEqAll = { beq := Data.instBEqAll.beq }

@[implicit_reducible]

instance Data.instOrdAll : Ord All

Equations

• Data.instOrdAll = { compare := Data.instOrdAll.ord }

def Data.instOrdAll.ord : All → All → Ordering

Equations

• Data.instOrdAll.ord { getAll := a } { getAll := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instReprAll : Repr All

Equations

• Data.instReprAll = { reprPrec := Data.instReprAll.repr }

def Data.instReprAll.repr : All → Nat → Std.Format

Equations

• Data.instReprAll.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getAll" ++ Std.Format.text " := " ++ (Std.Format.nest 10 (repr x✝.getAll)).group) " }"

def Data.instHashableAll.hash : All → UInt64

Equations

• Data.instHashableAll.hash { getAll := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instHashableAll : Hashable All

Equations

• Data.instHashableAll = { hash := Data.instHashableAll.hash }

@[implicit_reducible]

instance Data.instToStringAll : ToString All

ToString instance for All, displaying as All(...).

Equations

• Data.instToStringAll = { toString := fun (a : Data.All) => toString "All(" ++ toString a.getAll ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendAll : Append All

Append instance for All — boolean conjunction: $\text{All}(a) \mathbin{++} \text{All}(b) = \text{All}(a \mathbin{\&\&} b)$.

Equations

• Data.instAppendAll = { append := fun (a b : Data.All) => { getAll := a.getAll && b.getAll } }

theorem Data.All.append_assoc (a b c : All) : a ++ b ++ c = a ++ (b ++ c)

Associativity of All:

$$(a \mathbin{\&\&} b) \mathbin{\&\&} c = a \mathbin{\&\&} (b \mathbin{\&\&} c)$$

Proved by case analysis on $a$.

structure Data.Any : Type

Any is the boolean monoid under disjunction $(\vee)$:

• Operation: $\text{Any}(a) \mathbin{++} \text{Any}(b) = \text{Any}(a \vee b)$
• Identity: $\text{Any}(\text{false})$

$$\text{Any}(a) \mathbin{++} \text{Any}(b) = \text{Any}(a \mathbin{||} b)$$

• getAny : Bool

@[implicit_reducible]

instance Data.instBEqAny : BEq Any

Equations

• Data.instBEqAny = { beq := Data.instBEqAny.beq }

def Data.instBEqAny.beq : Any → Any → Bool

Equations

• Data.instBEqAny.beq { getAny := a } { getAny := b } = (a == b)
• Data.instBEqAny.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instOrdAny : Ord Any

Equations

• Data.instOrdAny = { compare := Data.instOrdAny.ord }

def Data.instOrdAny.ord : Any → Any → Ordering

Equations

• Data.instOrdAny.ord { getAny := a } { getAny := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instReprAny : Repr Any

Equations

• Data.instReprAny = { reprPrec := Data.instReprAny.repr }

def Data.instReprAny.repr : Any → Nat → Std.Format

Equations

• Data.instReprAny.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "getAny" ++ Std.Format.text " := " ++ (Std.Format.nest 10 (repr x✝.getAny)).group) " }"

@[implicit_reducible]

instance Data.instHashableAny : Hashable Any

Equations

• Data.instHashableAny = { hash := Data.instHashableAny.hash }

def Data.instHashableAny.hash : Any → UInt64

Equations

• Data.instHashableAny.hash { getAny := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instToStringAny : ToString Any

ToString instance for Any, displaying as Any(...).

Equations

• Data.instToStringAny = { toString := fun (a : Data.Any) => toString "Any(" ++ toString a.getAny ++ toString ")" }

@[implicit_reducible]

instance Data.instAppendAny : Append Any

Append instance for Any — boolean disjunction: $\text{Any}(a) \mathbin{++} \text{Any}(b) = \text{Any}(a \mathbin{||} b)$.

Equations

• Data.instAppendAny = { append := fun (a b : Data.Any) => { getAny := a.getAny || b.getAny } }

theorem Data.Any.append_assoc (a b c : Any) : a ++ b ++ c = a ++ (b ++ c)

Associativity of Any:

$$(a \mathbin{||} b) \mathbin{||} c = a \mathbin{||} (b \mathbin{||} c)$$

Proved by case analysis on $a$.