Documentation Verification Report

WF

📁 Source: Batteries/Data/RBMap/WF.lean

Statistics

Metric	Count
Definitions `WF`, `WF`, `WF`, `WF`, `mapSnd`, `mapVal`, `DelProp`, `IsMonotone`, `RedRed`, `WF`, `mapMonotone`	11
Theorems `instIsMonotoneProdByKeyFstMapSnd`, `append`, `balLeft`, `balRight`, `del`, `ins`, `map`, `reverse`, `setRed`, `trivial`, `All_and`, `append`, `balLeft`, `balRight`, `del`, `erase`, `ins`, `insert`, `map`, `reverse`, `setBlack`, `redred`, `lt_mono`, `append`, `balLeft`, `balRight`, `balance1`, `balance2`, `del`, `erase`, `ins`, `insert`, `map`, `reverse`, `setBlack`, `setRed`, `balance1`, `balance2`, `imp`, `of_false`, `of_red`, `reverse`, `setBlack`, `out`, `WF_iff`, `balance1_All`, `balance1_eq`, `balance2_All`, `balance2_eq`, `lt_congr_left`, `lt_congr_right`, `flip`, `trans_l`, `trans_r`, `insert_setBlack`, `isRed_reverse`, `reverse_balLeft`, `reverse_balRight`, `reverse_balance1`, `reverse_balance2`, `reverse_eq_iff`, `reverse_ins`, `reverse_insert`, `reverse_reverse`, `reverse_setBlack`, `reverse_setRed`, `setBlack_idem`	67
Total	78

Batteries.BinomialHeap.Imp.FindMin

Definitions

Name	Category	Theorems
`WF` 📖	CompData	—

Batteries.BinomialHeap.Imp.Heap

Definitions

Name	Category	Theorems
`WF` 📖	MathDef	4 math math: `Batteries.BinomialHeap.Imp.FindMin.WF.next`, `Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap`, `WF.nil`, `WF.singleton`

Batteries.BinomialHeap.Imp.HeapNode

Definitions

Name	Category	Theorems
`WF` 📖	MathDef	1 math math: `Batteries.BinomialHeap.Imp.FindMin.WF.node`

Batteries.PairingHeapImp.Heap

Definitions

Name	Category	Theorems
`WF` 📖	CompData	3 math math: `WF.combine`, `WF.merge_node`, `WF.singleton`

Batteries.RBMap

Definitions

Name	Category	Theorems
`mapVal` 📖	CompOp	—

Batteries.RBMap.Imp

Definitions

Name	Category	Theorems
`mapSnd` 📖	CompOp	1 math math: `instIsMonotoneProdByKeyFstMapSnd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonotoneProdByKeyFstMapSnd` 📖	mathematical	—	`Batteries.RBNode.IsMonotone` `Ordering.byKey` `mapSnd`	—	—

Batteries.RBNode

Definitions

Name	Category	Theorems
`DelProp` 📖	MathDef	1 math math: `Balanced.del`
`IsMonotone` 📖	CompData	1 math math: `Batteries.RBMap.Imp.instIsMonotoneProdByKeyFstMapSnd`
`RedRed` 📖	CompData	3 math math: `DelProp.redred`, `Balanced.append`, `Balanced.ins`
`WF` 📖	CompData	9 math math: `Batteries.RBSet.AlterWF.wf`, `WF_iff`, `Batteries.RBSet.toStream_eq`, `Batteries.RBMap.toStream_eq`, `Batteries.RBSet.mem_toList`, `Batteries.RBSet.val_toList`, `Batteries.RBSet.ModifyWF.wf`, `Batteries.RBMap.mem_toList`, `Batteries.RBMap.val_toList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`All_and` 📖	mathematical	—	`All`	—	—
`WF_iff` 📖	mathematical	—	`WF` `Ordered` `Balanced`	—	`WF.out`
`balance1_All` 📖	mathematical	—	`All` `balance1`	—	—
`balance1_eq` 📖	mathematical	`Balanced`	`balance1` `node` `Batteries.RBColor.black`	—	—
`balance2_All` 📖	mathematical	—	`All` `balance2`	—	—
`balance2_eq` 📖	mathematical	`Balanced`	`balance2` `node` `Batteries.RBColor.black`	—	`reverse_reverse` `reverse_balance2` `balance1_eq` `Balanced.reverse`
`insert_setBlack` 📖	mathematical	—	`setBlack` `insert` `ins`	—	`setBlack_idem`
`isRed_reverse` 📖	mathematical	—	`isRed` `reverse`	—	—
`reverse_balLeft` 📖	mathematical	—	`reverse` `balLeft` `balRight`	—	`balLeft.fun_cases_unfolding` `balRight.fun_cases_unfolding`
`reverse_balRight` 📖	mathematical	—	`reverse` `balRight` `balLeft`	—	`reverse_reverse` `reverse_balLeft`
`reverse_balance1` 📖	mathematical	—	`reverse` `balance1` `balance2`	—	—
`reverse_balance2` 📖	mathematical	—	`reverse` `balance2` `balance1`	—	`reverse_balance1` `reverse_reverse`
`reverse_eq_iff` 📖	mathematical	—	`reverse`	—	`reverse_reverse`
`reverse_ins` 📖	mathematical	—	`reverse` `ins`	—	`reverse_balance1` `reverse_balance2`
`reverse_insert` 📖	mathematical	—	`reverse` `insert`	—	`isRed_reverse` `reverse_setBlack` `reverse_ins`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	—
`reverse_setBlack` 📖	mathematical	—	`reverse` `setBlack`	—	—
`reverse_setRed` 📖	mathematical	—	`reverse` `setRed`	—	—
`setBlack_idem` 📖	mathematical	—	`setBlack`	—	—

Batteries.RBNode.All

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.append`	—	—
`balLeft` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.balLeft`	—	—
`balRight` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.balRight`	—	`reverse` `balLeft` `Batteries.RBNode.reverse_balRight`
`del` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.del`	—	`Batteries.RBNode.del.eq_def` `balLeft` `balRight` `append`
`ins` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.ins`	—	`Batteries.RBNode.ins.eq_def`
`map` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.map`	—	—
`reverse` 📖	mathematical	—	`Batteries.RBNode.All` `Batteries.RBNode.reverse`	—	—
`setRed` 📖	mathematical	`Batteries.RBNode.All`	`Batteries.RBNode.setRed`	—	—
`trivial` 📖	mathematical	—	`Batteries.RBNode.All`	—	—

Batteries.RBNode.Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.RedRed` `Batteries.RBNode.append`	—	—
`balLeft` 📖	mathematical	`Batteries.RBNode.RedRed` `Batteries.RBNode.Balanced`	`Batteries.RBColor` `Batteries.RBColor.red` `Batteries.RBNode.balLeft`	—	`Batteries.RBNode.RedRed.of_red` `Batteries.RBNode.RedRed.balance2`
`balRight` 📖	mathematical	`Batteries.RBNode.Balanced` `Batteries.RBNode.RedRed`	`Batteries.RBColor` `Batteries.RBColor.red` `Batteries.RBNode.balRight`	—	`Batteries.RBNode.reverse_reverse` `Batteries.RBNode.reverse_balRight` `Batteries.RBNode.RedRed.reverse` `balLeft` `reverse`
`del` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.DelProp` `Batteries.RBNode.isBlack` `Batteries.RBNode.del`	—	`Batteries.RBNode.del.eq_def` `Batteries.RBNode.RedRed.of_false` `balLeft` `balRight` `append` `Batteries.RBNode.RedRed.imp`
`erase` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.erase` `Batteries.RBColor.black`	—	`Batteries.RBNode.DelProp.redred` `del` `Batteries.RBNode.RedRed.setBlack`
`ins` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.RedRed` `Batteries.RBColor` `Batteries.RBNode.isRed` `Batteries.RBColor.red` `Batteries.RBNode.ins`	—	`Batteries.RBNode.ins.eq_def` `Batteries.RBNode.RedRed.balance1` `Batteries.RBNode.RedRed.balance2`
`insert` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.insert`	—	`ins` `setBlack`
`map` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.map`	—	—
`reverse` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.reverse`	—	—
`setBlack` 📖	mathematical	`Batteries.RBNode.Balanced`	`Batteries.RBNode.setBlack` `Batteries.RBColor.black`	—	—

Batteries.RBNode.DelProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`redred` 📖	mathematical	`Batteries.RBNode.DelProp`	`Batteries.RBNode.RedRed` `Batteries.RBColor` `Batteries.RBColor.black`	—	`Batteries.RBNode.RedRed.imp`

Batteries.RBNode.IsMonotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_mono` 📖	mathematical	—	`Batteries.RBNode.cmpLT`	—	—

Batteries.RBNode.Ordered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append` 📖	mathematical	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT` `Batteries.RBNode.Ordered`	`Batteries.RBNode.append`	—	—
`balLeft` 📖	mathematical	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT` `Batteries.RBNode.Ordered`	`Batteries.RBNode.balLeft`	—	`balance2` `Batteries.RBNode.cmpLT.trans_r` `Batteries.RBNode.balance2_All` `Batteries.RBNode.All.setRed` `Batteries.RBNode.cmpLT.trans_l` `setRed`
`balRight` 📖	mathematical	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT` `Batteries.RBNode.Ordered`	`Batteries.RBNode.balRight`	—	`Batteries.RBNode.reverse_reverse` `Batteries.RBNode.reverse_balRight` `reverse` `balLeft` `Batteries.RBNode.All.imp` `Batteries.RBNode.cmpLT.flip` `Batteries.RBNode.All.reverse`
`balance1` 📖	mathematical	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT` `Batteries.RBNode.Ordered`	`Batteries.RBNode.balance1`	—	`Batteries.RBNode.cmpLT.trans_l` `Batteries.RBNode.cmpLT.trans_r`
`balance2` 📖	mathematical	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT` `Batteries.RBNode.Ordered`	`Batteries.RBNode.balance2`	—	`Batteries.RBNode.reverse_reverse` `Batteries.RBNode.reverse_balance2` `reverse` `balance1` `Batteries.RBNode.All.imp` `Batteries.RBNode.cmpLT.flip` `Batteries.RBNode.All.reverse`
`del` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.del`	—	`Batteries.RBNode.del.eq_def` `balLeft` `Batteries.RBNode.All.del` `balRight` `append`
`erase` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.erase`	—	`setBlack` `del`
`ins` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.ins`	—	`Batteries.RBNode.ins.eq_def` `Batteries.RBNode.All.ins` `Batteries.RBNode.All.imp` `balance1` `balance2`
`insert` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.insert`	—	`ins`
`map` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.map`	—	`Batteries.RBNode.All.map` `Batteries.RBNode.IsMonotone.lt_mono`
`reverse` 📖	mathematical	`Batteries.RBNode.Ordered`	`Batteries.RBNode.reverse`	—	`Batteries.RBNode.All.imp` `Batteries.RBNode.cmpLT.flip` `Batteries.RBNode.All.reverse`
`setBlack` 📖	mathematical	—	`Batteries.RBNode.Ordered` `Batteries.RBNode.setBlack`	—	—
`setRed` 📖	mathematical	—	`Batteries.RBNode.Ordered` `Batteries.RBNode.setRed`	—	—

Batteries.RBNode.RedRed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`balance1` 📖	mathematical	`Batteries.RBNode.RedRed` `Batteries.RBNode.Balanced`	`Batteries.RBNode.balance1`	—	—
`balance2` 📖	mathematical	`Batteries.RBNode.Balanced` `Batteries.RBNode.RedRed`	`Batteries.RBNode.balance2`	—	`Batteries.RBNode.reverse_balance1` `Batteries.RBNode.reverse_reverse` `Batteries.RBNode.Balanced.reverse` `balance1` `reverse`
`imp` 📖	—	`Batteries.RBNode.RedRed`	—	—	—
`of_false` 📖	mathematical	`Batteries.RBNode.RedRed`	`Batteries.RBNode.Balanced`	—	—
`of_red` 📖	mathematical	`Batteries.RBNode.RedRed` `Batteries.RBNode.node` `Batteries.RBColor.red`	`Batteries.RBNode.Balanced`	—	—
`reverse` 📖	mathematical	`Batteries.RBNode.RedRed`	`Batteries.RBNode.reverse`	—	`Batteries.RBNode.Balanced.reverse`
`setBlack` 📖	mathematical	`Batteries.RBNode.RedRed`	`Batteries.RBNode.Balanced` `Batteries.RBNode.setBlack` `Batteries.RBColor.black`	—	`Batteries.RBNode.Balanced.setBlack`

Batteries.RBNode.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	`Batteries.RBNode.WF`	`Batteries.RBNode.Ordered` `Batteries.RBNode.Balanced`	—	`Batteries.RBNode.Ordered.insert` `Batteries.RBNode.Balanced.insert` `Batteries.RBNode.Ordered.erase` `Batteries.RBNode.Balanced.erase`

Batteries.RBNode.cmpEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_congr_left` 📖	mathematical	—	`Batteries.RBNode.cmpLT`	—	—
`lt_congr_right` 📖	mathematical	—	`Batteries.RBNode.cmpLT`	—	—

Batteries.RBNode.cmpLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	mathematical	—	`Batteries.RBNode.cmpLT`	—	`Std.instTransCmpFlipOrdering_batteries`
`trans_l` 📖	—	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT`	—	—	`Batteries.RBNode.All.imp` `trans`
`trans_r` 📖	—	`Batteries.RBNode.All` `Batteries.RBNode.cmpLT`	—	—	`Batteries.RBNode.All.imp` `trans`

Batteries.RBSet

Definitions

Name	Category	Theorems
`mapMonotone` 📖	CompOp	—

---

← Back to Index