summaryrefslogtreecommitdiff
path: root/AvlVerification.lean
diff options
context:
space:
mode:
authorRaito Bezarius2024-04-17 15:08:07 +0200
committerRaito Bezarius2024-04-17 15:08:07 +0200
commit945c630ec18e282bd0db731fb3f0b521e99de059 (patch)
tree5eefbf30b7a41612d61a5fe26223a59398af4fa2 /AvlVerification.lean
parent117cd1c0afbc50ffc5a90473cb4c01185188711e (diff)
feat: add functional correctness of elements contained in the resulting tree
We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to '')
-rw-r--r--AvlVerification.lean20
1 files changed, 6 insertions, 14 deletions
diff --git a/AvlVerification.lean b/AvlVerification.lean
index b90680c..f9e6830 100644
--- a/AvlVerification.lean
+++ b/AvlVerification.lean
@@ -32,16 +32,8 @@ structure AVLTreeSet (T : Type) where
def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) :=
Result.ok { root := none }
-/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]:
- Source: 'src/main.rs', lines 30:4-30:39 -/
-def AVLTreeSet.find
- (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
- Result Bool
- :=
- sorry
-
/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0:
- Source: 'src/main.rs', lines 63:4-81:5 -/
+ Source: 'src/main.rs', lines 43:4-61:5 -/
divergent def AVLTreeSet.insert_loop
(T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T))
:
@@ -69,17 +61,17 @@ divergent def AVLTreeSet.insert_loop
Result.ok (b, some (AVLNode.mk t current_tree3 current_tree2))
/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]:
- Source: 'src/main.rs', lines 63:4-63:46 -/
+ Source: 'src/main.rs', lines 43:4-43:46 -/
def AVLTreeSet.insert
(T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
Result (Bool × (AVLTreeSet T))
:=
do
- let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root
- Result.ok (b, { root := as })
+ let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root
+ Result.ok (b, { root := u })
/- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
- Source: 'src/main.rs', lines 85:4-85:43 -/
+ Source: 'src/main.rs', lines 65:4-65:43 -/
def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
if self < other
then Result.ok Ordering.Less
@@ -89,7 +81,7 @@ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
else Result.ok Ordering.Greater
/- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}]
- Source: 'src/main.rs', lines 84:0-84:16 -/
+ Source: 'src/main.rs', lines 64:0-64:16 -/
def OrdU32 : Ord U32 := {
cmp := OrdU32.cmp
}