@[irreducible]

def Auto.Bin.inductionOn {motive : Nat → Sort u} (x : Nat) (ind : (x : Nat) → motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) : motive x

Equations

• Auto.Bin.inductionOn 0 ind base₀ base₁ = base₀
• Auto.Bin.inductionOn 1 ind base₀ base₁ = base₁
• Auto.Bin.inductionOn x'.succ.succ ind base₀ base₁ = ind x' (Auto.Bin.inductionOn ((x' + 2) / 2) ind base₀ base₁)

@[irreducible]

def Auto.Bin.induction {motive : Nat → Sort u} (ind : (x : Nat) → motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) (x : Nat) : motive x

Equations

• Auto.Bin.induction ind base₀ base₁ x = Auto.Bin.inductionOn x ind base₀ base₁

inductive Auto.BinTree (α : Type u) : Type u

• leaf {α : Type u} : BinTree α
• node {α : Type u} : BinTree α → Option α → BinTree α → BinTree α

def Auto.instReprBinTree.repr {α✝ : Type u_1} [Repr α✝] : BinTree α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Auto.instReprBinTree.repr Auto.BinTree.leaf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Auto.BinTree.leaf")).group prec✝

instance Auto.instReprBinTree {α✝ : Type u_1} [Repr α✝] : Repr (BinTree α✝)

Equations

• Auto.instReprBinTree = { reprPrec := Auto.instReprBinTree.repr }

instance Auto.instToExprBinTreeOfToLevel {α✝ : Type u} [Lean.ToExpr α✝] [ToLevel] : Lean.ToExpr (BinTree α✝)

Equations

• Auto.instToExprBinTreeOfToLevel = { toExpr := Auto.instToExprBinTree.toExpr✝, toTypeExpr := (Lean.Expr.const `Auto.BinTree [Auto.toLevel]).app (Lean.toTypeExpr α✝) }

instance Auto.BinTree.instInhabited {α : Type u_1} : Inhabited (BinTree α)

Equations

• Auto.BinTree.instInhabited = { default := Auto.BinTree.leaf }

def Auto.BinTree.beq {α : Type u_1} [BEq α] (a b : BinTree α) : Bool

Equations

• Auto.BinTree.leaf.beq Auto.BinTree.leaf = true
• (la.node xa ra).beq (lb.node xb rb) = (la.beq lb && xa == xb && ra.beq rb)
• a.beq b = false

instance Auto.BinTree.instBEq {α : Type u_1} [BEq α] : BEq (BinTree α)

Equations

• Auto.BinTree.instBEq = { beq := Auto.BinTree.beq }

theorem Auto.BinTree.beq_def {α : Type u_1} [BEq α] {x y : BinTree α} : (x == y) = x.beq y

theorem Auto.BinTree.beq_refl {α : Type u_1} [BEq α] (α_beq_refl : ∀ (x : α), (x == x) = true) {a : BinTree α} : (a == a) = true

def Auto.BinTree.toString {α : Type u_1} [ToString α] : BinTree α → String

Equations

• Auto.BinTree.leaf.toString = ""
• (a.node (some x_2) a_2).toString = "{" ++ a.toString ++ ("|" ++ toString x_2 ++ "|") ++ a_2.toString ++ "}"
• (a.node none a_2).toString = "{" ++ a.toString ++ "" ++ a_2.toString ++ "}"

def Auto.BinTree.toStringDisplay {α : Type u_1} [ToString α] (bt : BinTree α) : String

Equations

• bt.toStringDisplay = Auto.BinTree.toStringDisplayAux✝ "R" bt

theorem Auto.BinTree.eq_of_beq_eq_true {α : Type u_1} [BEq α] (α_eq_of_beq_eq_true : ∀ (x y : α), (x == y) = true → x = y) {a b : BinTree α} (H : (a == b) = true) : a = b

instance Auto.BinTree.instLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] : LawfulBEq (BinTree α)

def Auto.BinTree.val? {α : Type u_1} (bt : BinTree α) : Option α

Equations

• Auto.BinTree.leaf.val? = none
• (a.node a_1 a_2).val? = a_1

def Auto.BinTree.valD {α : Type u_1} (bt : BinTree α) (default : α) : α

Equations

• bt.valD default = bt.val?.getD default

def Auto.BinTree.left! {α : Type u_1} (bt : BinTree α) : BinTree α

Equations

• Auto.BinTree.leaf.left! = Auto.BinTree.leaf
• (a.node a_1 a_2).left! = a

def Auto.BinTree.right! {α : Type u_1} (bt : BinTree α) : BinTree α

Equations

• Auto.BinTree.leaf.right! = Auto.BinTree.leaf
• (a.node a_1 a_2).right! = a_2

@[irreducible]

def Auto.BinTree.get?'WF {α : Type u_1} (bt : BinTree α) (n : Nat) : Option α

Equations

• bt.get?'WF 0 = none
• bt.get?'WF 1 = bt.val?
• bt.get?'WF n_2.succ.succ = match n_2.succ.succ.mod 2 with | 0 => bt.left!.get?'WF (n_2.succ.succ.div 2) | n.succ => bt.right!.get?'WF (n_2.succ.succ.div 2)

theorem Auto.BinTree.get?'WF.succSucc {α : Type u_1} (bt : BinTree α) (n : Nat) : bt.get?'WF (n + 2) = match (n + 2).mod 2 with | 0 => bt.left!.get?'WF ((n + 2).div 2) | n_1.succ => bt.right!.get?'WF ((n + 2).div 2)

def Auto.BinTree.get?'Aux {α : Type u_1} (bt : BinTree α) (n rd : Nat) : Option α

Equations

• bt.get?'Aux n 0 = none
• bt.get?'Aux 0 n_1.succ = none
• bt.get?'Aux 1 n_1.succ = bt.val?
• bt.get?'Aux x'.succ.succ n_1.succ = match x'.succ.succ.mod 2 with | 0 => bt.left!.get?'Aux (x'.succ.succ.div 2) n_1 | n.succ => bt.right!.get?'Aux (x'.succ.succ.div 2) n_1

theorem Auto.BinTree.get?'Aux.equiv {α : Type u_1} (bt : BinTree α) (n rd : Nat) : rd ≥ n → bt.get?'Aux n rd = bt.get?'WF n

def Auto.BinTree.get?' {α : Type u_1} (bt : BinTree α) (n : Nat) : Option α

Equations

• bt.get?' n = bt.get?'Aux n n

def Auto.BinTree.get? {α : Type u_1} (bt : BinTree α) (n : Nat) : Option α

Equations

• bt.get? n = bt.get?' n.succ

theorem Auto.BinTree.get?'.equiv {α : Type u_1} (bt : BinTree α) (n : Nat) : bt.get?' n = bt.get?'WF n

theorem Auto.BinTree.get?'_succSucc {α : Type u_1} (bt : BinTree α) (n : Nat) : bt.get?' (n + 2) = match (n + 2) % 2 with | 0 => bt.left!.get?' ((n + 2) / 2) | n_1.succ => bt.right!.get?' ((n + 2) / 2)

theorem Auto.BinTree.get?'_leaf {α : Type u_1} (n : Nat) : leaf.get?' n = none

@[irreducible]

def Auto.BinTree.insert'WF {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : BinTree α

Equations

• One or more equations did not get rendered due to their size.
• bt.insert'WF 0 x = bt
• Auto.BinTree.leaf.insert'WF 1 x = Auto.BinTree.leaf.node (some x) Auto.BinTree.leaf
• (a.node a_1 a_2).insert'WF 1 x = a.node (some x) a_2

theorem Auto.BinTree.insert'WF.succSucc {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : bt.insert'WF (n + 2) x = match (n + 2).mod 2 with | 0 => match bt with | leaf => (leaf.insert'WF ((n + 2).div 2) x).node none leaf | l.node v r => (l.insert'WF ((n + 2).div 2) x).node v r | n_1.succ => match bt with | leaf => leaf.node none (leaf.insert'WF ((n + 2).div 2) x) | l.node v r => l.node v (r.insert'WF ((n + 2).div 2) x)

def Auto.BinTree.insert'Aux {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) (rd : Nat) : BinTree α

Equations

• One or more equations did not get rendered due to their size.
• bt.insert'Aux n x 0 = bt
• bt.insert'Aux 0 x n_1.succ = bt
• Auto.BinTree.leaf.insert'Aux 1 x n_1.succ = Auto.BinTree.leaf.node (some x) Auto.BinTree.leaf
• (a.node a_1 a_2).insert'Aux 1 x n_1.succ = a.node (some x) a_2

theorem Auto.BinTree.insert'Aux.equiv {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) (rd : Nat) : rd ≥ n → bt.insert'Aux n x rd = bt.insert'WF n x

def Auto.BinTree.insert' {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : BinTree α

Equations

• bt.insert' n x = bt.insert'Aux n x n

def Auto.BinTree.insert {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : BinTree α

Equations

• bt.insert n x = bt.insert' n.succ x

theorem Auto.BinTree.insert'.equiv {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : bt.insert' n x = bt.insert'WF n x

theorem Auto.BinTree.insert'.succSucc {α : Type u_1} (bt : BinTree α) (n : Nat) (x : α) : bt.insert' (n + 2) x = match (n + 2) % 2 with | 0 => match bt with | leaf => (leaf.insert' ((n + 2) / 2) x).node none leaf | l.node v r => (l.insert' ((n + 2) / 2) x).node v r | n_1.succ => match bt with | leaf => leaf.node none (leaf.insert' ((n + 2) / 2) x) | l.node v r => l.node v (r.insert' ((n + 2) / 2) x)

theorem Auto.BinTree.insert'.correct₁ {β : Type u_1} (bt : BinTree β) (n : Nat) (x : β) : n ≠ 0 → (bt.insert' n x).get?' n = some x

theorem Auto.BinTree.insert.correct₁ {β : Type u_1} (bt : BinTree β) (n : Nat) (x : β) : (bt.insert n x).get? n = some x

theorem Auto.BinTree.insert'.correct₂ {β : Type u_1} (bt : BinTree β) (n₁ n₂ : Nat) (x : β) : n₁ ≠ n₂ → (bt.insert' n₁ x).get?' n₂ = bt.get?' n₂

theorem Auto.BinTree.insert.correct₂ {β : Type u_1} (bt : BinTree β) (n₁ n₂ : Nat) (x : β) (H : n₁ ≠ n₂) : (bt.insert n₁ x).get? n₂ = bt.get? n₂

def Auto.BinTree.foldl {α : Sort u_1} {β : Type u_2} (f : α → β → α) (init : α) : BinTree β → α

Depth-first preorder traversal of the BinTree

Equations

• Auto.BinTree.foldl f init Auto.BinTree.leaf = init
• Auto.BinTree.foldl f init (a.node (some x_2) a_2) = Auto.BinTree.foldl f (f (Auto.BinTree.foldl f init a) x_2) a_2
• Auto.BinTree.foldl f init (a.node none a_2) = Auto.BinTree.foldl f (Auto.BinTree.foldl f init a) a_2

theorem Auto.BinTree.foldl_inv {α : Sort u_1} {β : Type u_2} {f : α → β → α} {init : α} {bt : BinTree β} (inv : α → Prop) (zero : inv init) (ind : ∀ (a : α) (b : β), inv a → inv (f a b)) : inv (foldl f init bt)

def Auto.BinTree.allp' {α : Type u_1} (p : α → Prop) (bt : BinTree α) : Prop

Equations

• Auto.BinTree.allp' p bt = ∀ (n : Nat), Auto.Option.allp p (bt.get?' n)

def Auto.BinTree.allp {α : Type u_1} (p : α → Prop) (bt : BinTree α) : Prop

Equations

• Auto.BinTree.allp p bt = ∀ (n : Nat), Auto.Option.allp p (bt.get? n)

theorem Auto.BinTree.allp_equiv {α✝ : Type u_1} {p : α✝ → Prop} {bt : BinTree α✝} : allp' p bt ↔ allp p bt

theorem Auto.BinTree.allp'_leaf {α : Type u_1} (p : α → Prop) : allp' p leaf ↔ True

theorem Auto.BinTree.allp'_node {α : Type u_1} {l : BinTree α} {x : Option α} {r : BinTree α} (p : α → Prop) : allp' p (l.node x r) ↔ allp' p l ∧ Option.allp p x ∧ allp' p r

theorem Auto.BinTree.allp'_insert' {α : Type u_1} (p : α → Prop) (bt : BinTree α) (n : Nat) (x : α) : allp' p (bt.insert' n x) ↔ (n ≠ 0 → p x) ∧ ∀ (n' : Nat), n' ≠ n → Option.allp p (bt.get?' n')

theorem Auto.BinTree.allp_insert {α : Type u_1} (p : α → Prop) (bt : BinTree α) (n : Nat) (x : α) : allp p (bt.insert n x) ↔ p x ∧ ∀ (n' : Nat), n' ≠ n → Option.allp p (bt.get? n')

def Auto.BinTree.all {α : Type u_1} (p : α → Bool) : BinTree α → Bool

Equations

• Auto.BinTree.all p = Auto.BinTree.foldl (fun (i : Bool) (x : α) => i && p x) true

theorem Auto.BinTree.all_with_init {α : Type u_1} (p : α → Bool) (bt : BinTree α) (init : Bool) : foldl (fun (i : Bool) (x : α) => i && p x) init bt = (all p bt && init)

theorem Auto.BinTree.all_node {α : Type u_1} {l : BinTree α} {x : Option α} {r : BinTree α} (p : α → Bool) : all p (l.node x r) = (all p l && Option.all p x && all p r)

theorem Auto.BinTree.all_allp' {α : Type u_1} (p : α → Bool) (bt : BinTree α) : all p bt = true ↔ allp' (fun (x : α) => p x = true) bt

theorem Auto.BinTree.all_allp {α : Type u_1} (p : α → Bool) (bt : BinTree α) : all p bt = true ↔ allp (fun (x : α) => p x = true) bt

theorem Auto.BinTree.all_spec' {α : Type u_1} (p : α → Bool) (bt : BinTree α) : all p bt = true ↔ ∀ (n : Nat), Option.all p (bt.get?' n) = true

theorem Auto.BinTree.all_spec {α : Type u_1} (p : α → Bool) (bt : BinTree α) : all p bt = true ↔ ∀ (n : Nat), Option.all p (bt.get? n) = true

theorem Auto.BinTree.all_insert' {α : Type u_1} (p : α → Bool) (bt : BinTree α) (n : Nat) (x : α) : all p (bt.insert' n x) = true ↔ (n ≠ 0 → p x = true) ∧ ∀ (n' : Nat), n' ≠ n → Option.all p (bt.get?' n') = true

theorem Auto.BinTree.all_insert {α : Type u_1} (p : α → Bool) (bt : BinTree α) (n : Nat) (x : α) : all p (bt.insert n x) = true ↔ p x = true ∧ ∀ (n' : Nat), n' ≠ n → Option.all p (bt.get? n') = true

def Auto.BinTree.mapOpt {α : Type u_1} {β : Type u_2} (f : α → Option β) : BinTree α → BinTree β

Equations

• Auto.BinTree.mapOpt f Auto.BinTree.leaf = Auto.BinTree.leaf
• Auto.BinTree.mapOpt f (a.node a_1 a_2) = (Auto.BinTree.mapOpt f a).node (a_1.bind f) (Auto.BinTree.mapOpt f a_2)

theorem Auto.BinTree.mapOpt_allp' {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Prop) (bt : BinTree α) : allp' p (mapOpt f bt) ↔ allp' (fun (x : α) => Option.allp p (f x)) bt

theorem Auto.BinTree.mapOpt_allp {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Prop) (bt : BinTree α) : allp p (mapOpt f bt) ↔ allp (fun (x : α) => Option.allp p (f x)) bt

theorem Auto.BinTree.get?'_mapOpt {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → Option β) (bt : BinTree α) : (mapOpt f bt).get?' n = (bt.get?' n).bind f

theorem Auto.BinTree.get?_mapOpt {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → Option β) (bt : BinTree α) : (mapOpt f bt).get? n = (bt.get? n).bind f

def Auto.BinTree.ofListGet {α : Type u_1} (xs : List α) : BinTree α

Equations

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

partial def Auto.BinTree.ofListFoldl {α : Type u_1} (xs : List α) : BinTree α

Property : xs.foldl f init = (ofListFoldl xs).foldl f init

def Auto.BinTree.toLCtx {α : Type u} [ToLevel] [Lean.ToExpr α] (bl : BinTree α) (default : α) : Lean.Expr

Given a bl : BinTree α, return Lean.toExpr (fun n => (BinTree.get? bl n).getD default)

Equations

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

def Auto.BinTree.get?Pos {α : Type u_1} (bt : BinTree α) (p : Pos) : Option α

Equations

• bt.get?Pos Auto.Pos.xH = bt.val?
• bt.get?Pos p'.xO = bt.left!.get?Pos p'
• bt.get?Pos p'.xI = bt.right!.get?Pos p'

theorem Auto.BinTree.get?Pos_leaf {α : Type u_1} (p : Pos) : leaf.get?Pos p = none

def Auto.BinTree.insertPos {α : Type u_1} (bt : BinTree α) (p : Pos) (x : α) : BinTree α

Equations

• Auto.BinTree.leaf.insertPos Auto.Pos.xH x = Auto.BinTree.leaf.node (some x) Auto.BinTree.leaf
• (a.node a_1 a_2).insertPos Auto.Pos.xH x = a.node (some x) a_2
• Auto.BinTree.leaf.insertPos p'.xO x = (Auto.BinTree.leaf.insertPos p' x).node none Auto.BinTree.leaf
• (a.node a_1 a_2).insertPos p'.xO x = (a.insertPos p' x).node a_1 a_2
• Auto.BinTree.leaf.insertPos p'.xI x = Auto.BinTree.leaf.node none (Auto.BinTree.leaf.insertPos p' x)
• (a.node a_1 a_2).insertPos p'.xI x = a.node a_1 (a_2.insertPos p' x)

theorem Auto.BinTree.insertPos.correct₁ {β : Type u_1} (bt : BinTree β) (p : Pos) (x : β) : (bt.insertPos p x).get?Pos p = some x

theorem Auto.BinTree.insertPos.correct₂ {β : Type u_1} (bt : BinTree β) (p₁ p₂ : Pos) (x : β) : p₁ ≠ p₂ → (bt.insertPos p₁ x).get?Pos p₂ = bt.get?Pos p₂

def Auto.BinTree.allpPos {α : Type u_1} (p : α → Prop) (bt : BinTree α) : Prop

Equations

• Auto.BinTree.allpPos p bt = ∀ (q : Auto.Pos), Auto.Option.allp p (bt.get?Pos q)

theorem Auto.BinTree.allpPos_leaf {α : Type u_1} (p : α → Prop) : allpPos p leaf ↔ True

theorem Auto.BinTree.allpPos_node {α : Type u_1} {l : BinTree α} {x : Option α} {r : BinTree α} (p : α → Prop) : allpPos p (l.node x r) ↔ allpPos p l ∧ Option.allp p x ∧ allpPos p r

theorem Auto.BinTree.allpPos_insert {α : Type u_1} (p : α → Prop) (bt : BinTree α) (q : Pos) (x : α) : allpPos p (bt.insertPos q x) ↔ p x ∧ ∀ (q' : Pos), q ≠ q' → Option.allp p (bt.get?Pos q')

theorem Auto.BinTree.mapOpt_allpPos {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Prop) (bt : BinTree α) : allpPos p (mapOpt f bt) ↔ allpPos (fun (x : α) => Option.allp p (f x)) bt

def Auto.BinTree.toLCtxPos {α : Type u} [ToLevel] [Lean.ToExpr α] (bl : BinTree α) (default : α) : Lean.Expr

Given a bl : BinTree α, return Lean.toExpr (fun n => (BinTree.get?Pos bl n).getD default)

Equations

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