Auto.Lib.BinTree

@[irreducible]

def Auto.Bin.inductionOn {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.inductionOn ind base₀ base₁ 0 = base₀
Auto.Bin.inductionOn ind base₀ base₁ 1 = base₁
Auto.Bin.inductionOn ind base₀ base₁ x'.succ.succ = ind x' (Auto.Bin.inductionOn ind base₀ base₁ ((x' + 2) / 2))

Instances For

source

@[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 ind base₀ base₁ x

Instances For

source

inductive Auto.BinTree (α : Type u) :

Type u

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

Instances For

source

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

Repr (BinTree α✝)

Equations

Auto.instReprBinTree = { reprPrec := Auto.reprBinTree✝ }

source

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

Lean.ToExpr (BinTree α✝)

Equations

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

source

instance Auto.BinTree.instInhabited {α : Type u_1} :

Inhabited (BinTree α)

Equations

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

source

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

Instances For

source

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

BEq (BinTree α)

Equations

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

source

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

(x == y) = x.beq y

source

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

(a == a) = true

source

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 ++ "}"

Instances For

source

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

String

Equations

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

Instances For

source

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

source

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

LawfulBEq (BinTree α)

source

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

Instances For

source

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

Equations

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

Instances For

source

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

Instances For

source

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

Instances For

source

@[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 x'.succ.succ = match x'.succ.succ.mod 2 with | 0 => bt.left!.get?'WF (x'.succ.succ.div 2) | n.succ => bt.right!.get?'WF (x'.succ.succ.div 2)

Instances For

source

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)

source

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 n_3.succ.succ n_1.succ = match n_3.succ.succ.mod 2 with | 0 => bt.left!.get?'Aux (n_3.succ.succ.div 2) n_1 | n.succ => bt.right!.get?'Aux (n_3.succ.succ.div 2) n_1

Instances For

source

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

source

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

Option α

Equations

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

Instances For

source

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

Option α

Equations

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

Instances For

source

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

bt.get?' n = bt.get?'WF n

source

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)

source

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

leaf.get?' n = none

source

@[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
(a.node a_1 a_2).insert'WF x'.succ.succ x = match x'.succ.succ.mod 2 with | 0 => (a.insert'WF (x'.succ.succ.div 2) x).node a_1 a_2 | n.succ => a.node a_1 (a_2.insert'WF (x'.succ.succ.div 2) x)

Instances For

source

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)

source

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

Instances For

source

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

source

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

BinTree α

Equations

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

Instances For

source

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

BinTree α

Equations

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

Instances For

source

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

bt.insert' n x = bt.insert'WF n x

source

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)

source

theorem Auto.BinTree.insert'.correct₁ {β : Type u_1} (bt : BinTree β) (n : Nat) (x : β) :

n ≠ 0 → (bt.insert' n x).get?' n = some x

source

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

(bt.insert n x).get? n = some x

source

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₂

source

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₂

source

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

Instances For

source

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)

source

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)

Instances For

source

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)

Instances For

source

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

allp' p bt ↔ allp p bt

source

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

allp' p leaf ↔ True

source

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

source

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')

source

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')

source

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

Instances For

source

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)

source

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)

source

theorem Auto.BinTree.all_allp' {α : Type u_1} (p : α → Bool) (bt : BinTree α) :

all p bt = true ↔ allp' (fun (x : α) => p x = true) bt

source

theorem Auto.BinTree.all_allp {α : Type u_1} (p : α → Bool) (bt : BinTree α) :

all p bt = true ↔ allp (fun (x : α) => p x = true) bt

source

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

source

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

source

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

source

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

source

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)

Instances For

source

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

source

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

source

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

source

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

source

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

BinTree α

Equations

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

Instances For

source

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

BinTree α

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

source

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.

Instances For

source

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

Option α

Equations

Instances For

source

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

leaf.get?Pos p = none

source

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)

Instances For

source

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

(bt.insertPos p x).get?Pos p = some x

source

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₂

source

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)

Instances For

source

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

allpPos p leaf ↔ True

source

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

source

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')

source

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

source

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.

Instances For