@[reducible, inline]

abbrev Lean.Grind.AC.Var : Type

Equations

• Lean.Grind.AC.Var = Nat

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

• vars : RArray (PLift α)
• op : α → α → α

inductive Lean.Grind.AC.Expr : Type

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

instance Lean.Grind.AC.instInhabitedExpr : Inhabited Expr

Equations

• Lean.Grind.AC.instInhabitedExpr = { default := Lean.Grind.AC.instInhabitedExpr.default }

def Lean.Grind.AC.instInhabitedExpr.default : Expr

Equations

• Lean.Grind.AC.instInhabitedExpr.default = Lean.Grind.AC.Expr.var default

instance Lean.Grind.AC.instReprExpr : Repr Expr

Equations

• Lean.Grind.AC.instReprExpr = { reprPrec := Lean.Grind.AC.instReprExpr.repr }

def Lean.Grind.AC.instReprExpr.repr : Expr → Nat → Std.Format

Equations

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

instance Lean.Grind.AC.instBEqExpr : BEq Expr

Equations

• Lean.Grind.AC.instBEqExpr = { beq := Lean.Grind.AC.instBEqExpr.beq }

def Lean.Grind.AC.instBEqExpr.beq : Expr → Expr → Bool

Equations

• Lean.Grind.AC.instBEqExpr.beq (Lean.Grind.AC.Expr.var a) (Lean.Grind.AC.Expr.var b) = (a == b)
• Lean.Grind.AC.instBEqExpr.beq (a.op a_1) (b.op b_1) = (Lean.Grind.AC.instBEqExpr.beq a b && Lean.Grind.AC.instBEqExpr.beq a_1 b_1)
• Lean.Grind.AC.instBEqExpr.beq x✝¹ x✝ = false

noncomputable def Lean.Grind.AC.Var.denote {α : Sort u} (ctx : Context α) (x : Var) : α

Equations

• Lean.Grind.AC.Var.denote ctx x = PLift.rec (fun (x : α) => x) (ctx.vars.get x)

noncomputable def Lean.Grind.AC.Expr.denote {α : Sort u_1} (ctx : Context α) (e : Expr) : α

Equations

• Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Expr.rec (fun (x : Lean.Grind.AC.Var) => Lean.Grind.AC.Var.denote ctx x) (fun (x x : Lean.Grind.AC.Expr) (ih₁ ih₂ : α) => ctx.op ih₁ ih₂) e

theorem Lean.Grind.AC.Expr.denote_var {α : Sort u_1} (ctx : Context α) (x : Var) : denote ctx (var x) = Var.denote ctx x

theorem Lean.Grind.AC.Expr.denote_op {α : Sort u_1} (ctx : Context α) (a b : Expr) : denote ctx (a.op b) = ctx.op (denote ctx a) (denote ctx b)

inductive Lean.Grind.AC.Seq : Type

• var (x : Var) : Seq
• cons (x : Var) (s : Seq) : Seq

def Lean.Grind.AC.instInhabitedSeq.default : Seq

Equations

• Lean.Grind.AC.instInhabitedSeq.default = Lean.Grind.AC.Seq.var default

instance Lean.Grind.AC.instInhabitedSeq : Inhabited Seq

Equations

• Lean.Grind.AC.instInhabitedSeq = { default := Lean.Grind.AC.instInhabitedSeq.default }

instance Lean.Grind.AC.instReprSeq : Repr Seq

Equations

• Lean.Grind.AC.instReprSeq = { reprPrec := Lean.Grind.AC.instReprSeq.repr }

def Lean.Grind.AC.instReprSeq.repr : Seq → Nat → Std.Format

Equations

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

instance Lean.Grind.AC.instBEqSeq : BEq Seq

Equations

• Lean.Grind.AC.instBEqSeq = { beq := Lean.Grind.AC.instBEqSeq.beq }

def Lean.Grind.AC.instBEqSeq.beq : Seq → Seq → Bool

Equations

• Lean.Grind.AC.instBEqSeq.beq (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b) = (a == b)
• Lean.Grind.AC.instBEqSeq.beq (Lean.Grind.AC.Seq.cons a a_1) (Lean.Grind.AC.Seq.cons b b_1) = (a == b && Lean.Grind.AC.instBEqSeq.beq a_1 b_1)
• Lean.Grind.AC.instBEqSeq.beq x✝¹ x✝ = false

noncomputable def Lean.Grind.AC.Seq.beq' (s₁ : Seq) : Seq → Bool

Equations

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

theorem Lean.Grind.AC.Seq.beq'_eq (s₁ s₂ : Seq) : (s₁.beq' s₂ = true) = (s₁ = s₂)

instance Lean.Grind.AC.instLawfulBEqSeq : LawfulBEq Seq

noncomputable def Lean.Grind.AC.Seq.denote {α : Sort u_1} (ctx : Context α) (s : Seq) : α

Equations

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

theorem Lean.Grind.AC.Seq.denote_var {α : Sort u_1} (ctx : Context α) (x : Var) : denote ctx (var x) = Var.denote ctx x

theorem Lean.Grind.AC.Seq.denote_op {α : Sort u_1} (ctx : Context α) (x : Var) (s : Seq) : denote ctx (cons x s) = ctx.op (Var.denote ctx x) (denote ctx s)

def Lean.Grind.AC.Expr.toSeq' (e : Expr) (s : Seq) : Seq

Equations

• (Lean.Grind.AC.Expr.var x).toSeq' s = Lean.Grind.AC.Seq.cons x s
• (a.op b).toSeq' s = a.toSeq' (b.toSeq' s)

noncomputable def Lean.Grind.AC.Expr.toSeq'_k (e : Expr) : Seq → Seq

Equations

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

theorem Lean.Grind.AC.Expr.toSeq'_k_eq_toSeq' (e : Expr) (s : Seq) : e.toSeq'_k s = e.toSeq' s

def Lean.Grind.AC.Expr.toSeq (e : Expr) : Seq

Equations

• (Lean.Grind.AC.Expr.var x).toSeq = Lean.Grind.AC.Seq.var x
• (a.op b).toSeq = a.toSeq' b.toSeq

noncomputable def Lean.Grind.AC.Expr.toSeq_k (e : Expr) : Seq

Equations

• e.toSeq_k = Lean.Grind.AC.Expr.rec Lean.Grind.AC.Seq.var (fun (a x : Lean.Grind.AC.Expr) (x ihb : Lean.Grind.AC.Seq) => a.toSeq'_k ihb) e

theorem Lean.Grind.AC.Expr.toSeq_k_eq_toSeq (e : Expr) : e.toSeq_k = e.toSeq

theorem Lean.Grind.AC.Expr.denote_toSeq' {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr) (s : Seq), Seq.denote ctx (e.toSeq' s) = ctx.op (denote ctx e) (Seq.denote ctx s)

theorem Lean.Grind.AC.Expr.denote_toSeq {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr), Seq.denote ctx e.toSeq = denote ctx e

def Lean.Grind.AC.Seq.erase0 (s : Seq) : Seq

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.AC.Seq.var x).erase0 = Lean.Grind.AC.Seq.var x

noncomputable def Lean.Grind.AC.Seq.erase0_k (s : Seq) : Seq

Equations

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

theorem Lean.Grind.AC.Seq.erase0_k_var (x : Var) : (var x).erase0_k = var x

theorem Lean.Grind.AC.Seq.erase0_k_cons (x : Var) (s : Seq) : (cons x s).erase0_k = Bool.rec (Bool.rec (cons x s.erase0_k) (var x) (s.erase0_k.beq' (var 0))) s.erase0_k (Nat.beq x 0)

theorem Lean.Grind.AC.Seq.erase0_k_eq_erase0 (s : Seq) : s.erase0_k = s.erase0

theorem Lean.Grind.AC.Seq.denote_erase0 {α : Sort u_1} (ctx : Context α) {inst : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (s : Seq) : denote ctx s.erase0 = denote ctx s

def Lean.Grind.AC.Seq.insert (x : Var) (s : Seq) : Seq

Equations

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

noncomputable def Lean.Grind.AC.Seq.insert_k (x : Var) (s : Seq) : Seq

Equations

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

theorem Lean.Grind.AC.Seq.insert_k_eq_insert (x : Var) (s : Seq) : insert_k x s = insert x s

theorem Lean.Grind.AC.Seq.denote_insert {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (x : Var) (s : Seq) : denote ctx (insert x s) = ctx.op (Var.denote ctx x) (denote ctx s)

def Lean.Grind.AC.Seq.sort' (s acc : Seq) : Seq

Equations

• (Lean.Grind.AC.Seq.var x).sort' acc = Lean.Grind.AC.Seq.insert x acc
• (Lean.Grind.AC.Seq.cons x s_2).sort' acc = s_2.sort' (Lean.Grind.AC.Seq.insert x acc)

noncomputable def Lean.Grind.AC.Seq.sort'_k (s : Seq) : Seq → Seq

Equations

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

theorem Lean.Grind.AC.Seq.sort'_k_eq_sort' (s acc : Seq) : s.sort'_k acc = s.sort' acc

theorem Lean.Grind.AC.Seq.denote_sort' {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s acc : Seq) : denote ctx (s.sort' acc) = ctx.op (denote ctx s) (denote ctx acc)

def Lean.Grind.AC.Seq.sort (s : Seq) : Seq

Equations

• (Lean.Grind.AC.Seq.var x).sort = Lean.Grind.AC.Seq.var x
• (Lean.Grind.AC.Seq.cons x s_2).sort = s_2.sort' (Lean.Grind.AC.Seq.var x)

noncomputable def Lean.Grind.AC.Seq.sort_k (s : Seq) : Seq

Equations

• s.sort_k = Lean.Grind.AC.Seq.rec (fun (x : Lean.Grind.AC.Var) => Lean.Grind.AC.Seq.var x) (fun (x : Lean.Grind.AC.Var) (s x_1 : Lean.Grind.AC.Seq) => s.sort' (Lean.Grind.AC.Seq.var x)) s

theorem Lean.Grind.AC.Seq.sort_k_eq_sort (s : Seq) : s.sort_k = s.sort

theorem Lean.Grind.AC.Seq.denote_sort {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s : Seq) : denote ctx s.sort = denote ctx s

def Lean.Grind.AC.Seq.eraseDup (s : Seq) : Seq

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.AC.Seq.var x).eraseDup = Lean.Grind.AC.Seq.var x

noncomputable def Lean.Grind.AC.Seq.eraseDup_k (s : Seq) : Seq

Equations

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

theorem Lean.Grind.AC.Seq.eraseDup_k_cons (x : Var) (s : Seq) : (cons x s).eraseDup_k = rec (fun (y : Var) => Bool.rec (cons x (var y)) (var x) (Nat.beq x y)) (fun (y : Var) (s' x_1 : Seq) => Bool.rec (cons x (cons y s')) (cons y s') (Nat.beq x y)) s.eraseDup_k

theorem Lean.Grind.AC.Seq.eraseDup_k_eq_eraseDup (s : Seq) : s.eraseDup_k = s.eraseDup

theorem Lean.Grind.AC.Seq.denote_eraseDup {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (s : Seq) : denote ctx s.eraseDup = denote ctx s

def Lean.Grind.AC.Seq.concat (s₁ s₂ : Seq) : Seq

Equations

• (Lean.Grind.AC.Seq.var x).concat s₂ = Lean.Grind.AC.Seq.cons x s₂
• (Lean.Grind.AC.Seq.cons x s_1).concat s₂ = Lean.Grind.AC.Seq.cons x (s_1.concat s₂)

noncomputable def Lean.Grind.AC.Seq.concat_k (s₁ : Seq) : Seq → Seq

Equations

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

theorem Lean.Grind.AC.Seq.concat_k_eq_concat (s₁ s₂ : Seq) : s₁.concat_k s₂ = s₁.concat s₂

theorem Lean.Grind.AC.Seq.denote_concat {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} (s₁ s₂ : Seq) : denote ctx (s₁.concat s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

theorem Lean.Grind.AC.eq_orient {α : Sort u_1} (ctx : Context α) (lhs rhs : Seq) : Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx rhs = Seq.denote ctx lhs

theorem Lean.Grind.AC.eq_simp_lhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₂ → Seq.denote ctx rhs₁ = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx lhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₁

theorem Lean.Grind.AC.diseq_simp_lhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx rhs₁ ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_exact {α : Sort u_1} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq) : Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx lhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₁

noncomputable def Lean.Grind.AC.simp_prefix_cert (lhs rhs tail s s' : Seq) : Bool

Equations

• Lean.Grind.AC.simp_prefix_cert lhs rhs tail s s' = (s.beq' (lhs.concat_k tail)).and' (s'.beq' (rhs.concat_k tail))

theorem Lean.Grind.AC.eq_simp_lhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_prefix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq), simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.simp_suffix_cert (lhs rhs head s s' : Seq) : Bool

Equations

• Lean.Grind.AC.simp_suffix_cert lhs rhs head s s' = (s.beq' (head.concat_k lhs)).and' (s'.beq' (head.concat_k rhs))

theorem Lean.Grind.AC.eq_simp_lhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_suffix {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq), simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.simp_middle_cert (lhs rhs head tail s s' : Seq) : Bool

Equations

• Lean.Grind.AC.simp_middle_cert lhs rhs head tail s s' = (s.beq' (head.concat_k (lhs.concat_k tail))).and' (s'.beq' (head.concat_k (rhs.concat_k tail)))

theorem Lean.Grind.AC.eq_simp_lhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_middle {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq), simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.superpose_cert (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool

Equations

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

theorem Lean.Grind.AC.superpose {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : superpose_cert p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs = Seq.denote ctx rhs

Given lhs₁ = rhs₁ and lhs₂ = rhs₂ where lhs₁ := p * c and lhs₂ := c * s, lhs = rhs where lhs := rhs₁ * s and rhs := p * rhs₂

def Lean.Grind.AC.Seq.unionFuel (fuel : Nat) (s₁ s₂ : Seq) : Seq

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.AC.Seq.unionFuel 0 s₁ s₂ = s₁.concat s₂
• Lean.Grind.AC.Seq.unionFuel fuel_2.succ (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s) = Lean.Grind.AC.Seq.insert x₁ (Lean.Grind.AC.Seq.cons x s)
• Lean.Grind.AC.Seq.unionFuel fuel_2.succ (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂) = Lean.Grind.AC.Seq.insert x₂ (Lean.Grind.AC.Seq.cons x s)

noncomputable def Lean.Grind.AC.Seq.unionFuel_k (fuel : Nat) : Seq → Seq → Seq

Equations

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

theorem Lean.Grind.AC.Seq.unionFuel_k_eq_unionFuel (fuel : Nat) (s₁ s₂ : Seq) : unionFuel_k fuel s₁ s₂ = unionFuel fuel s₁ s₂

theorem Lean.Grind.AC.Seq.denote_unionFuel {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (fuel : Nat) (s₁ s₂ : Seq) : denote ctx (unionFuel fuel s₁ s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

def Lean.Grind.AC.hugeFuel : Nat

Equations

• Lean.Grind.AC.hugeFuel = 1000000

def Lean.Grind.AC.Seq.union (s₁ s₂ : Seq) : Seq

Equations

• s₁.union s₂ = Lean.Grind.AC.Seq.unionFuel Lean.Grind.AC.hugeFuel s₁ s₂

noncomputable def Lean.Grind.AC.Seq.union_k (s₁ s₂ : Seq) : Seq

Equations

• s₁.union_k s₂ = Lean.Grind.AC.Seq.unionFuel_k Lean.Grind.AC.hugeFuel s₁ s₂

theorem Lean.Grind.AC.Seq.union_k_eq_union (s₁ s₂ : Seq) : s₁.union_k s₂ = s₁.union s₂

theorem Lean.Grind.AC.Seq.denote_union {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (s₁ s₂ : Seq) : denote ctx (s₁.union s₂) = ctx.op (denote ctx s₁) (denote ctx s₂)

noncomputable def Lean.Grind.AC.simp_ac_cert (c lhs rhs s s' : Seq) : Bool

Equations

• Lean.Grind.AC.simp_ac_cert c lhs rhs s s' = (s.beq' (c.union_k lhs)).and' (s'.beq' (c.union_k rhs))

theorem Lean.Grind.AC.simp_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs rhs s s' : Seq) : simp_ac_cert c lhs rhs s s' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx s = Seq.denote ctx s'

Given lhs = rhs, and a term s := union a lhs, rewrite it to s' := union a rhs

theorem Lean.Grind.AC.eq_simp_lhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' = Seq.denote ctx rhs₂

theorem Lean.Grind.AC.eq_simp_rhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂'

theorem Lean.Grind.AC.diseq_simp_lhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂' ≠ Seq.denote ctx rhs₂

theorem Lean.Grind.AC.diseq_simp_rhs_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq) : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂ → Seq.denote ctx lhs₂ ≠ Seq.denote ctx rhs₂'

noncomputable def Lean.Grind.AC.superpose_ac_cert (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool

Equations

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

theorem Lean.Grind.AC.superpose_ac {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₂ = Seq.denote ctx rhs₂ → Seq.denote ctx lhs = Seq.denote ctx rhs

Given lhs₁ = rhs₁ and lhs₂ = rhs₂ where lhs₁ := union c r₁ and lhs₂ := union c r₂, lhs = rhs where lhs := union r₂ rhs₁ and rhs := union r₁ rhs₂

noncomputable def Lean.Grind.AC.Seq.contains_k (s : Seq) (x : Var) : Bool

Equations

• s.contains_k x = Lean.Grind.AC.Seq.rec (fun (y : Lean.Grind.AC.Var) => Nat.beq x y) (fun (y : Lean.Grind.AC.Var) (x_1 : Lean.Grind.AC.Seq) (ih : Bool) => (Nat.beq x y).or' ih) s

theorem Lean.Grind.AC.Seq.contains_k_var (y x : Var) : (var y).contains_k x = (x == y)

theorem Lean.Grind.AC.Seq.contains_k_cons (y x : Var) (s : Seq) : (cons y s).contains_k x = (x == y || s.contains_k x)

theorem Lean.Grind.AC.Seq.denote_insert_of_contains {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.Commutative ctx.op] [inst₃ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.contains_k x = true → denote ctx (insert x s) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_ac_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

Equations

• Lean.Grind.AC.superpose_ac_idempotent_cert x lhs₁ rhs₁ rhs = (lhs₁.contains_k x).and' (rhs.beq' (Lean.Grind.AC.Seq.insert x rhs₁))

Remark: see Section 4.1 of the paper "MODULARITY, COMBINATION, AC CONGRUENCE CLOSURE" to understand why superpose_ac_idempotent is needed.

theorem Lean.Grind.AC.superpose_ac_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} {inst₃ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_ac_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

noncomputable def Lean.Grind.AC.Seq.startsWithVar_k (s : Seq) (x : Var) : Bool

Equations

• s.startsWithVar_k x = Lean.Grind.AC.Seq.rec (fun (y : Lean.Grind.AC.Var) => Nat.beq x y) (fun (y : Lean.Grind.AC.Var) (x_1 : Lean.Grind.AC.Seq) (x_2 : Bool) => Nat.beq x y) s

theorem Lean.Grind.AC.Seq.startsWithVar_k_var (y x : Var) : (var y).startsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.startsWithVar_k_cons (y x : Var) (s : Seq) : (cons y s).startsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.denote_concat_of_startsWithVar {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.startsWithVar_k x = true → denote ctx ((var x).concat_k s) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_head_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

Equations

• Lean.Grind.AC.superpose_head_idempotent_cert x lhs₁ rhs₁ rhs = (lhs₁.startsWithVar_k x).and' (rhs.beq' ((Lean.Grind.AC.Seq.var x).concat rhs₁))

theorem Lean.Grind.AC.superpose_head_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_head_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

superpose_ac_idempotent for the non-commutative case. This is the "head"-case

noncomputable def Lean.Grind.AC.Seq.endsWithVar_k (s : Seq) (x : Var) : Bool

Equations

• s.endsWithVar_k x = Lean.Grind.AC.Seq.rec (fun (y : Lean.Grind.AC.Var) => Nat.beq x y) (fun (x : Lean.Grind.AC.Var) (x : Lean.Grind.AC.Seq) (ih : Bool) => ih) s

theorem Lean.Grind.AC.Seq.endsWithVar_k_var (y x : Var) : (var y).endsWithVar_k x = (x == y)

theorem Lean.Grind.AC.Seq.endsWithVar_k_cons (y x : Var) (s : Seq) : (cons y s).endsWithVar_k x = s.endsWithVar_k x

theorem Lean.Grind.AC.Seq.denote_concat_of_endsWithVar {α : Sort u_1} (ctx : Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op] (s : Seq) (x : Var) : s.endsWithVar_k x = true → denote ctx (s.concat_k (var x)) = denote ctx s

noncomputable def Lean.Grind.AC.superpose_tail_idempotent_cert (x : Var) (lhs₁ rhs₁ rhs : Seq) : Bool

Equations

• Lean.Grind.AC.superpose_tail_idempotent_cert x lhs₁ rhs₁ rhs = (lhs₁.endsWithVar_k x).and' (rhs.beq' (rhs₁.concat (Lean.Grind.AC.Seq.var x)))

theorem Lean.Grind.AC.superpose_tail_idempotent {α : Sort u_1} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op} (x : Var) (lhs₁ rhs₁ rhs : Seq) : superpose_tail_idempotent_cert x lhs₁ rhs₁ rhs = true → Seq.denote ctx lhs₁ = Seq.denote ctx rhs₁ → Seq.denote ctx lhs₁ = Seq.denote ctx rhs

superpose_ac_idempotent for the non-commutative case. It is similar to superpose_head_idempotent but for the "tail"-case

noncomputable def Lean.Grind.AC.eq_norm_a_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_norm_a_cert lhs rhs lhs' rhs' = (lhs.toSeq.beq' lhs').and' (rhs.toSeq.beq' rhs')

theorem Lean.Grind.AC.eq_norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_a_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_ac_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_norm_ac_cert lhs rhs lhs' rhs' = (lhs.toSeq.sort.beq' lhs').and' (rhs.toSeq.sort.beq' rhs')

theorem Lean.Grind.AC.eq_norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ac_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_ai_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_norm_ai_cert lhs rhs lhs' rhs' = (lhs.toSeq.erase0.beq' lhs').and' (rhs.toSeq.erase0.beq' rhs')

theorem Lean.Grind.AC.eq_norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ai_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_norm_aci_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_norm_aci_cert lhs rhs lhs' rhs' = (lhs.toSeq.erase0.sort.beq' lhs').and' (rhs.toSeq.erase0.sort.beq' rhs')

theorem Lean.Grind.AC.eq_norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_aci_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_erase_dup_cert (lhs rhs lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_erase_dup_cert lhs rhs lhs' rhs' = (lhs.eraseDup.beq' lhs').and' (rhs.eraseDup.beq' rhs')

theorem Lean.Grind.AC.eq_erase_dup {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs lhs' rhs' : Seq), eq_erase_dup_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.eq_erase0_cert (lhs rhs lhs' rhs' : Seq) : Bool

Equations

• Lean.Grind.AC.eq_erase0_cert lhs rhs lhs' rhs' = (lhs.erase0.beq' lhs').and' (rhs.erase0.beq' rhs')

theorem Lean.Grind.AC.eq_erase0 {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs lhs' rhs' : Seq), eq_erase0_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs' = Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_a_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ac_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_ai_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs : Expr) (lhs' rhs' : Seq), eq_norm_aci_cert lhs rhs lhs' rhs' = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_erase_dup {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs lhs' rhs' : Seq), eq_erase_dup_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

theorem Lean.Grind.AC.diseq_erase0 {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs lhs' rhs' : Seq), eq_erase0_cert lhs rhs lhs' rhs' = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → Seq.denote ctx lhs' ≠ Seq.denote ctx rhs'

noncomputable def Lean.Grind.AC.diseq_unsat_cert (lhs rhs : Seq) : Bool

Equations

• Lean.Grind.AC.diseq_unsat_cert lhs rhs = lhs.beq' rhs

theorem Lean.Grind.AC.diseq_unsat {α : Sort u_1} (ctx : Context α) (lhs rhs : Seq) : diseq_unsat_cert lhs rhs = true → Seq.denote ctx lhs ≠ Seq.denote ctx rhs → False

theorem Lean.Grind.AC.norm_a {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} (e : Expr) (s : Seq), e.toSeq.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_ac {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} (e : Expr) (s : Seq), e.toSeq.sort.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_ai {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (e : Expr) (s : Seq), e.toSeq.erase0.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.norm_aci {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.Commutative ctx.op} {x✝¹ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (e : Expr) (s : Seq), e.toSeq.erase0.sort.beq' s = true → Expr.denote ctx e = Seq.denote ctx s

theorem Lean.Grind.AC.eq_erase0_rhs {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)} (lhs rhs rhs' : Seq), rhs.erase0.beq' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs = Seq.denote ctx rhs'

theorem Lean.Grind.AC.eq_erase_dup_rhs {α : Sort u_1} (ctx : Context α) : ∀ {x : Std.Associative ctx.op} {x✝ : Std.IdempotentOp ctx.op} (lhs rhs rhs' : Seq), rhs.eraseDup.beq' rhs' = true → Seq.denote ctx lhs = Seq.denote ctx rhs → Seq.denote ctx lhs = Seq.denote ctx rhs'

theorem Lean.Grind.AC.eq_expr_seq_seq {α : Sort u_1} (ctx : Context α) (e : Expr) (s₁ s₂ : Seq) : Expr.denote ctx e = Seq.denote ctx s₁ → Seq.denote ctx s₁ = Seq.denote ctx s₂ → Expr.denote ctx e = Seq.denote ctx s₂

theorem Lean.Grind.AC.imp_eq {α : Sort u_1} (ctx : Context α) (lhs rhs : Expr) (s : Seq) : Expr.denote ctx lhs = Seq.denote ctx s → Expr.denote ctx rhs = Seq.denote ctx s → Expr.denote ctx lhs = Expr.denote ctx rhs

theorem Lean.Grind.AC.refl {α : Sort u_1} (ctx : Context α) (s : Seq) : Seq.denote ctx s = Seq.denote ctx s