Binary meet and finite join basis

This basis has one binary meet operation and a finite-arity join operation for every arity. Nullary join supplies the bottom element. It is convenient for cyclic discrete constructions, where joins are free and only binary meets are counted; finite joins can subsequently be expanded into binary joins without changing meet cost.

inductive Algebraic.JoinMeet.Op : Type

Binary meet or a join with a specified finite arity.

• meet : Op
• join (arity : ℕ) : Op

def Algebraic.JoinMeet.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.JoinMeet.instDecidableEqOp.decEq Algebraic.JoinMeet.Op.meet Algebraic.JoinMeet.Op.meet = isTrue ⋯
• Algebraic.JoinMeet.instDecidableEqOp.decEq Algebraic.JoinMeet.Op.meet (Algebraic.JoinMeet.Op.join arity) = isFalse ⋯
• Algebraic.JoinMeet.instDecidableEqOp.decEq (Algebraic.JoinMeet.Op.join arity) Algebraic.JoinMeet.Op.meet = isFalse ⋯
• Algebraic.JoinMeet.instDecidableEqOp.decEq (Algebraic.JoinMeet.Op.join a) (Algebraic.JoinMeet.Op.join b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.JoinMeet.instDecidableEqOp : DecidableEq Op

Equations

• Algebraic.JoinMeet.instDecidableEqOp = Algebraic.JoinMeet.instDecidableEqOp.decEq

@[reducible]

def Algebraic.JoinMeet.arity : Op → ℕ

Arity of a meet/join operation.

Equations

• Algebraic.JoinMeet.arity Algebraic.JoinMeet.Op.meet = 2
• Algebraic.JoinMeet.arity (Algebraic.JoinMeet.Op.join count) = count

@[simp]

theorem Algebraic.JoinMeet.arity_meet : arity Op.meet = 2

theorem Algebraic.JoinMeet.arity_join (count : ℕ) : arity (Op.join count) = count

@[reducible, inline]

abbrev Algebraic.JoinMeet.signature : Signature

Signature with binary meet and every finite join.

Equations

• Algebraic.JoinMeet.signature = { Op := Algebraic.JoinMeet.Op, Arity := Algebraic.JoinMeet.arity }

def Algebraic.JoinMeet.setInterpretation (Γ : Type u) : Interpretation signature (Set Γ)

Interpret meet as intersection and finite join as indexed union.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.JoinMeet.setInterpretation Γ Algebraic.JoinMeet.Op.meet input = input 0 ∩ input 1

def Algebraic.JoinMeet.meetCost : OperationCost signature

Charge meets and treat all finite joins as free.

Equations

• Algebraic.JoinMeet.meetCost Algebraic.JoinMeet.Op.meet = 1
• Algebraic.JoinMeet.meetCost (Algebraic.JoinMeet.Op.join arity) = 0

@[simp]

theorem Algebraic.JoinMeet.meetCost_meet : meetCost Op.meet = 1

@[simp]

theorem Algebraic.JoinMeet.meetCost_join (count : ℕ) : meetCost (Op.join count) = 0