Documentation

Init.Data.AC

inductive Lean.Data.AC.Expr :

Type

var: Nat → Lean.Data.AC.Expr
op: Lean.Data.AC.Expr → Lean.Data.AC.Expr → Lean.Data.AC.Expr

instance Lean.Data.AC.instInhabitedExpr :

Inhabited Lean.Data.AC.Expr

Equations

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

instance Lean.Data.AC.instReprExpr :

Repr Lean.Data.AC.Expr

Equations

Lean.Data.AC.instReprExpr = { reprPrec := [anonymous] }

instance Lean.Data.AC.instBEqExpr :

BEq Lean.Data.AC.Expr

Equations

Lean.Data.AC.instBEqExpr = { beq := [anonymous] }

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

Type u

value : α
neutral : Option (Lean.IsNeutral op value)

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

Type u

op : α → α → α
assoc : Lean.IsAssociative op
comm : Option (Lean.IsCommutative op)
idem : Option (Lean.IsIdempotent op)
vars : List (Lean.Data.AC.Variable op)
arbitrary : α

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

Sort (max 1 u)

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

Instances

Lean.Data.AC.instContextInformationContext

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

Sort (max (max 1 u) v)

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

Instances

Lean.Data.AC.instEvalInformationContext

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

Lean.Data.AC.Variable ctx.op

Equations

Lean.Data.AC.Context.var ctx idx = List.getD ctx.vars idx { value := ctx.arbitrary, neutral := none }

instance Lean.Data.AC.instContextInformationContext {α : Sort u_1} :

Lean.Data.AC.ContextInformation (Lean.Data.AC.Context α)

Equations

Lean.Data.AC.instContextInformationContext = { isNeutral := fun ctx x => Option.isSome (Lean.Data.AC.Context.var ctx x).neutral, isComm := fun ctx => Option.isSome ctx.comm, isIdem := fun ctx => Option.isSome ctx.idem }

instance Lean.Data.AC.instEvalInformationContext {α : Sort u_1} :

Lean.Data.AC.EvalInformation (Lean.Data.AC.Context α) α

Equations

Lean.Data.AC.instEvalInformationContext = { arbitrary := fun ctx => ctx.arbitrary, evalOp := fun ctx => ctx.op, evalVar := fun ctx idx => (Lean.Data.AC.Context.var ctx idx).value }

def Lean.Data.AC.eval {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (ex : Lean.Data.AC.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 (Lean.Data.AC.Expr.op a 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 :

Lean.Data.AC.Expr → List Nat

Equations

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

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

List Nat → β

Equations

Lean.Data.AC.evalList β ctx [] = Lean.Data.AC.EvalInformation.arbitrary ctx
Lean.Data.AC.evalList β ctx [x] = Lean.Data.AC.EvalInformation.evalVar ctx x
Lean.Data.AC.evalList β ctx (x :: xs) = Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.EvalInformation.evalVar ctx x) (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) :

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 _fun_discr [] = _fun_discr
Lean.Data.AC.sort.loop _fun_discr (x :: xs) = Lean.Data.AC.sort.loop (Lean.Data.AC.insert x _fun_discr) xs

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

Equations

Lean.Data.AC.mergeIdem xs = match xs with | [] => [] | x :: xs => Lean.Data.AC.mergeIdem.loop x xs

def Lean.Data.AC.mergeIdem.loop :

Nat → List Nat → List Nat

Equations

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

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

List Nat → List Nat

Equations

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

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

List Nat → List Nat

Equations

Lean.Data.AC.removeNeutrals.loop ctx (x :: xs) = match Lean.Data.AC.ContextInformation.isNeutral ctx x with | true => Lean.Data.AC.removeNeutrals.loop ctx xs | false => x :: Lean.Data.AC.removeNeutrals.loop ctx xs
Lean.Data.AC.removeNeutrals.loop ctx [] = []

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

Equations

Lean.Data.AC.norm ctx e = let xs := Lean.Data.AC.Expr.toList e; let xs := Lean.Data.AC.removeNeutrals ctx xs; let xs := if Lean.Data.AC.ContextInformation.isComm ctx = true then Lean.Data.AC.sort xs else xs; if Lean.Data.AC.ContextInformation.isIdem ctx = true then Lean.Data.AC.mergeIdem xs else xs

theorem 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

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

Lean.Data.AC.mergeIdem e ≠ []

theorem Lean.Data.AC.Context.mergeIdem_head {x : Nat} {xs : List Nat} :

Lean.Data.AC.mergeIdem (x :: x :: xs) = Lean.Data.AC.mergeIdem (x :: xs)

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

Lean.Data.AC.mergeIdem (x :: y :: ys) = x :: Lean.Data.AC.mergeIdem (y :: ys)

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.mergeIdem e) = Lean.Data.AC.evalList α ctx e

theorem Lean.Data.AC.insert_nonEmpty {x : Nat} {xs : List Nat} :

Lean.Data.AC.insert x xs ≠ []

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

Lean.Data.AC.sort.loop xs ys ≠ []

theorem Lean.Data.AC.Context.evalList_insert {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (h : Lean.IsCommutative ctx.op) (x : Nat) (xs : List Nat) :

Lean.Data.AC.evalList α ctx (Lean.Data.AC.insert x xs) = Lean.Data.AC.evalList α ctx (x :: xs)

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop a c) = Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop b c)

theorem Lean.Data.AC.Context.evalList_sort_loop_swap {α : Sort u_1} {y : Nat} (ctx : Lean.Data.AC.Context α) (h : Lean.IsCommutative ctx.op) (xs : List Nat) (ys : List Nat) :

Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop xs (y :: ys)) = Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop (y :: xs) ys)

theorem Lean.Data.AC.Context.evalList_sort_cons {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (h : Lean.IsCommutative ctx.op) (x : Nat) (xs : List Nat) :

Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort (x :: xs)) = Lean.Data.AC.evalList α ctx (x :: Lean.Data.AC.sort xs)

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort e) = Lean.Data.AC.evalList α ctx e

theorem Lean.Data.AC.Context.toList_nonEmpty (e : Lean.Data.AC.Expr) :

Lean.Data.AC.Expr.toList e ≠ []

theorem Lean.Data.AC.Context.unwrap_isNeutral {α : Sort u_1} {ctx : Lean.Data.AC.Context α} {x : Nat} :

Lean.Data.AC.ContextInformation.isNeutral ctx x = true → Lean.IsNeutral (Lean.Data.AC.EvalInformation.evalOp ctx) (Lean.Data.AC.EvalInformation.evalVar ctx x)

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.removeNeutrals ctx e) = Lean.Data.AC.evalList α ctx e

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

Lean.Data.AC.evalList α ctx (List.append l r) = Lean.Data.AC.Context.op ctx (Lean.Data.AC.evalList α ctx l) (Lean.Data.AC.evalList α ctx r)

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.Expr.toList e) = Lean.Data.AC.eval α ctx e

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

Lean.Data.AC.evalList α ctx (Lean.Data.AC.norm ctx e) = Lean.Data.AC.eval α ctx e

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

Lean.Data.AC.eval α ctx a = Lean.Data.AC.eval α ctx b