inductive Lean.Data.AC.Expr : Type

• var (x : Nat) : Expr
• op (lhs rhs : Expr) : Expr

instance Lean.Data.AC.instInhabitedExpr : Inhabited Expr

Equations

• Lean.Data.AC.instInhabitedExpr = { default := Lean.Data.AC.Expr.var default }

instance Lean.Data.AC.instReprExpr : Repr Expr

Equations

• Lean.Data.AC.instReprExpr = { reprPrec := Lean.Data.AC.reprExpr✝ }

instance Lean.Data.AC.instBEqExpr : BEq Expr

Equations

• Lean.Data.AC.instBEqExpr = { beq := Lean.Data.AC.beqExpr✝ }

structure Lean.Data.AC.Variable {α : Sort u} (op : α → α → α) : Type u

• value : α
• neutral : Option (PLift (Std.LawfulIdentity op self.value))

structure Lean.Data.AC.Context (α : Sort u) : Type u

• op : α → α → α
• assoc : Std.Associative self.op
• comm : Option (PLift (Std.Commutative self.op))
• idem : Option (PLift (Std.IdempotentOp self.op))
• vars : List (Variable self.op)
• arbitrary : α

class Lean.Data.AC.ContextInformation (α : Sort u) : Sort (max 1 u)

• isNeutral : α → Nat → Bool
• isComm : α → Bool
• isIdem : α → Bool

class Lean.Data.AC.EvalInformation (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

• arbitrary : α → β
• evalOp : α → β → β → β
• evalVar : α → Nat → β

def Lean.Data.AC.Context.var {α : Sort u_1} (ctx : Context α) (idx : Nat) : Variable ctx.op

Equations

• ctx.var idx = ctx.vars.getD idx { value := ctx.arbitrary, neutral := none }

instance Lean.Data.AC.instContextInformationContext {α : Sort u_1} : ContextInformation (Context α)

Equations

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

instance Lean.Data.AC.instEvalInformationContext {α : Sort u_1} : EvalInformation (Context α) α

Equations

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

def Lean.Data.AC.eval {α : Sort u_1} (β : Sort u) [EvalInformation α β] (ctx : α) (ex : Expr) : β

Equations

• Lean.Data.AC.eval β ctx (Lean.Data.AC.Expr.var a) = Lean.Data.AC.EvalInformation.evalVar ctx a
• Lean.Data.AC.eval β ctx (a.op a_1) = Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.eval β ctx a) (Lean.Data.AC.eval β ctx a_1)

def Lean.Data.AC.Expr.toList : Expr → List Nat

Equations

• (Lean.Data.AC.Expr.var a).toList = [a]
• (a.op a_1).toList = a.toList.append a_1.toList

def Lean.Data.AC.evalList {α : Sort u_1} (β : Sort u) [EvalInformation α β] (ctx : α) : List Nat → β

Equations

• Lean.Data.AC.evalList β ctx [] = Lean.Data.AC.EvalInformation.arbitrary ctx
• Lean.Data.AC.evalList β ctx [x_1] = Lean.Data.AC.EvalInformation.evalVar ctx x_1
• Lean.Data.AC.evalList β ctx (x_1 :: xs) = Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.EvalInformation.evalVar ctx x_1) (Lean.Data.AC.evalList β ctx xs)

def Lean.Data.AC.insert (x : Nat) : List Nat → List Nat

Equations

• Lean.Data.AC.insert x [] = [x]
• Lean.Data.AC.insert x (a :: as) = if x < a then x :: a :: as else a :: Lean.Data.AC.insert x as

def Lean.Data.AC.sort (xs : List Nat) : List Nat

Equations

• Lean.Data.AC.sort xs = Lean.Data.AC.sort.loop [] xs

def Lean.Data.AC.sort.loop : List Nat → List Nat → List Nat

Equations

• Lean.Data.AC.sort.loop x✝ [] = x✝
• Lean.Data.AC.sort.loop x✝ (x_2 :: xs) = Lean.Data.AC.sort.loop (Lean.Data.AC.insert x_2 x✝) xs

def Lean.Data.AC.mergeIdem (xs : List Nat) : List Nat

Equations

• Lean.Data.AC.mergeIdem [] = []
• Lean.Data.AC.mergeIdem (a :: as) = Lean.Data.AC.mergeIdem.loop a as

def Lean.Data.AC.mergeIdem.loop : Nat → List Nat → List Nat

Equations

• Lean.Data.AC.mergeIdem.loop x✝ (next :: rest) = if x✝ = next then Lean.Data.AC.mergeIdem.loop x✝ rest else x✝ :: Lean.Data.AC.mergeIdem.loop next rest
• Lean.Data.AC.mergeIdem.loop x✝ [] = [x✝]

def Lean.Data.AC.removeNeutrals {α : Sort u_1} [info : ContextInformation α] (ctx : α) : List Nat → List Nat

Equations

• Lean.Data.AC.removeNeutrals ctx (x_1 :: xs) = match Lean.Data.AC.removeNeutrals.loop ctx (x_1 :: xs) with | [] => [x_1] | ys => ys
• Lean.Data.AC.removeNeutrals ctx [] = []

def Lean.Data.AC.removeNeutrals.loop {α : Sort u_1} [info : ContextInformation α] (ctx : α) : List Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Lean.Data.AC.removeNeutrals.loop ctx [] = []

def Lean.Data.AC.norm {α : Sort u_1} [info : ContextInformation α] (ctx : α) (e : Expr) : List Nat

Equations

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

noncomputable def Lean.Data.AC.List.two_step_induction {motive : List Nat → Sort u} (l : List Nat) (empty : motive []) (single : (a : Nat) → motive [a]) (step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)) : motive l

Equations

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

theorem Lean.Data.AC.Context.mergeIdem_nonEmpty (e : List Nat) (h : e ≠ []) : mergeIdem e ≠ []

theorem Lean.Data.AC.Context.mergeIdem_head {x : Nat} {xs : List Nat} : mergeIdem (x :: x :: xs) = mergeIdem (x :: xs)

theorem Lean.Data.AC.Context.mergeIdem_head2 {x y : Nat} {ys : List Nat} (h : x ≠ y) : mergeIdem (x :: y :: ys) = x :: mergeIdem (y :: ys)

theorem Lean.Data.AC.Context.evalList_mergeIdem {α : Sort u_1} (ctx : Context α) (h : ContextInformation.isIdem ctx = true) (e : List Nat) : evalList α ctx (mergeIdem e) = evalList α ctx e

theorem Lean.Data.AC.insert_nonEmpty {x : Nat} {xs : List Nat} : insert x xs ≠ []

theorem Lean.Data.AC.Context.sort_loop_nonEmpty {ys : List Nat} (xs : List Nat) (h : xs ≠ []) : sort.loop xs ys ≠ []

theorem Lean.Data.AC.Context.evalList_insert {α : Sort u_1} (ctx : Context α) (h : Std.Commutative ctx.op) (x : Nat) (xs : List Nat) : evalList α ctx (insert x xs) = evalList α ctx (x :: xs)

theorem Lean.Data.AC.Context.evalList_sort_congr {α : Sort u_1} {a b c : List Nat} (ctx : Context α) (h : Std.Commutative ctx.op) (h₂ : evalList α ctx a = evalList α ctx b) (h₃ : a ≠ []) (h₄ : b ≠ []) : evalList α ctx (sort.loop a c) = evalList α ctx (sort.loop b c)

theorem Lean.Data.AC.Context.evalList_sort_loop_swap {α : Sort u_1} {y : Nat} (ctx : Context α) (h : Std.Commutative ctx.op) (xs ys : List Nat) : evalList α ctx (sort.loop xs (y :: ys)) = evalList α ctx (sort.loop (y :: xs) ys)

theorem Lean.Data.AC.Context.evalList_sort_cons {α : Sort u_1} (ctx : Context α) (h : Std.Commutative ctx.op) (x : Nat) (xs : List Nat) : evalList α ctx (sort (x :: xs)) = evalList α ctx (x :: sort xs)

theorem Lean.Data.AC.Context.evalList_sort {α : Sort u_1} (ctx : Context α) (h : ContextInformation.isComm ctx = true) (e : List Nat) : evalList α ctx (sort e) = evalList α ctx e

theorem Lean.Data.AC.Context.toList_nonEmpty (e : Expr) : e.toList ≠ []

theorem Lean.Data.AC.Context.unwrap_isNeutral {α : Sort u_1} {ctx : Context α} {x : Nat} : ContextInformation.isNeutral ctx x = true → Std.LawfulIdentity (EvalInformation.evalOp ctx) (EvalInformation.evalVar ctx x)

theorem Lean.Data.AC.Context.evalList_removeNeutrals {α : Sort u_1} (ctx : Context α) (e : List Nat) : evalList α ctx (removeNeutrals ctx e) = evalList α ctx e

theorem Lean.Data.AC.Context.evalList_append {α : Sort u_1} (ctx : Context α) (l r : List Nat) (h₁ : l ≠ []) (h₂ : r ≠ []) : evalList α ctx (l.append r) = ctx.op (evalList α ctx l) (evalList α ctx r)

theorem Lean.Data.AC.Context.eval_toList {α : Sort u_1} (ctx : Context α) (e : Expr) : evalList α ctx e.toList = eval α ctx e

theorem Lean.Data.AC.Context.eval_norm {α : Sort u_1} (ctx : Context α) (e : Expr) : evalList α ctx (norm ctx e) = eval α ctx e

theorem Lean.Data.AC.Context.eq_of_norm {α : Sort u_1} (ctx : Context α) (a b : Expr) (h : (norm ctx a == norm ctx b) = true) : eval α ctx a = eval α ctx b