summaryrefslogtreecommitdiff
path: root/AvlVerification
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--AvlVerification.lean20
-rw-r--r--AvlVerification/Insert.lean115
-rw-r--r--AvlVerification/Specifications.lean36
-rw-r--r--AvlVerification/Tree.lean3
4 files changed, 89 insertions, 85 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
}
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index baf3441..16e740f 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -6,55 +6,49 @@ namespace Implementation
open Primitives
open avl_verification
-open Tree (AVLTree)
-open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+open Tree (AVLTree AVLTree.set)
+open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
-example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _
- (by
- -- Totality
- intro a b
- unfold Ord.cmp
- unfold OrdU32
- unfold OrdU32.cmp
- if hlt : a < b then
- use .Less
- simp [hlt]
- else
- if heq: a = b
- then
- use .Equal
- simp [hlt]
- rw [heq]
- -- TODO: simp [hlt, heq] breaks everything???
- else
- use .Greater
- simp [hlt, heq]
- ) (by
- -- Duality
- intro a b Hgt
- if hlt : b < a then
- unfold Ord.cmp
- unfold OrdU32
- unfold OrdU32.cmp
- simp [hlt]
- else
- unfold Ord.cmp at Hgt
- unfold OrdU32 at Hgt
- unfold OrdU32.cmp at Hgt
- have hnlt : ¬ (a < b) := sorry
- have hneq : ¬ (a = b) := sorry
- exfalso
- apply hlt
- -- I need a Preorder on U32 now.
- sorry)
+-- example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _
+-- (by
+-- -- Totality
+-- intro a b
+-- unfold Ord.cmp
+-- unfold OrdU32
+-- unfold OrdU32.cmp
+-- if hlt : a < b then
+-- use .Less
+-- simp [hlt]
+-- else
+-- if heq: a = b
+-- then
+-- use .Equal
+-- simp [hlt]
+-- rw [heq]
+-- -- TODO: simp [hlt, heq] breaks everything???
+-- else
+-- use .Greater
+-- simp [hlt, heq]
+-- ) (by
+-- -- Duality
+-- intro a b Hgt
+-- if hlt : b < a then
+-- unfold Ord.cmp
+-- unfold OrdU32
+-- unfold OrdU32.cmp
+-- simp [hlt]
+-- else
+-- unfold Ord.cmp at Hgt
+-- unfold OrdU32 at Hgt
+-- unfold OrdU32.cmp at Hgt
+-- have hnlt : ¬ (a < b) := sorry
+-- have hneq : ¬ (a = b) := sorry
+-- exfalso
+-- apply hlt
+-- -- I need a Preorder on U32 now.
+-- sorry)
-variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpec T H)
-
-instance rustOrder {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): _root_.Ord U := ordOfOrdSpec O OSpec
--- Why the TC fails if I don't specify the previous instance explicitly?
-instance rustLt {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): LT U := @ltOfOrd _ (ordOfOrdSpec O OSpec)
-
-instance rustLt' : LT T := rustLt Ospec
+variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
@[pspec]
theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
@@ -105,14 +99,11 @@ theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
lemma AVLTreeSet.insert_loop_spec_global
(a: T) (t: Option (AVLNode T))
:
- haveI : LT T := (rustLt Ospec)
BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
- ∧ BST.Invariant t_new := by
+ ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by
intro Hbst
- letI instOrd : _root_.Ord T := (rustOrder Ospec)
- letI instLt : LT T := (rustLt Ospec)
match t with
- | none => simp [AVLTreeSet.insert_loop]
+ | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
| some (AVLNode.mk b left right) =>
rw [AVLTreeSet.insert_loop]
simp only []
@@ -121,12 +112,13 @@ lemma AVLTreeSet.insert_loop_spec_global
cases ordering
all_goals simp only []
{
- have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
+ have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩
exact (fun x => b < x)
rewrite [Htree] at H_result; simp at H_result
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
simp only [true_and]
+ split_conjs
cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
constructor
exact H_forall_left
@@ -135,17 +127,23 @@ lemma AVLTreeSet.insert_loop_spec_global
exact H_bst_left
convert H_bst
exact H_result.2
+ simp [AVLTree.set_some]
+ rewrite [H_result.2, H_set]
+ simp
}
{
- simp; tauto
+ simp; split_conjs
+ . tauto
+ . simp [Ospec.equality _ _ Hordering]
}
{
- have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
+ have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩
exact (fun x => x < b)
rewrite [Htree] at H_result; simp at H_result
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
simp only [true_and]
+ split_conjs
cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
constructor
apply Hnode; exact H_forall_left
@@ -154,15 +152,18 @@ lemma AVLTreeSet.insert_loop_spec_global
convert H_bst
exact H_result.2
exact H_bst_right
+ simp [AVLTree.set_some]
+ rewrite [H_result.2, H_set]
+ simp [Set.singleton_union, Set.insert_comm, Set.insert_union]
}
@[pspec]
def AVLTreeSet.insert_spec
(a: T) (t: AVLTreeSet T):
- haveI : LT T := (rustLt Ospec)
BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t')
-- it's still a binary search tree.
- ∧ BST.Invariant t'.root)
+ ∧ BST.Invariant t'.root
+ ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root)
:= by
rw [AVLTreeSet.insert]; intro Hbst
progress keep h as ⟨ t', Hset ⟩;
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 958a3e7..0694df3 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -42,32 +42,40 @@ namespace Specifications
open Primitives
open Result
-variable {T: Type} (H: avl_verification.Ord T)
+variable {T: Type} (H: outParam (avl_verification.Ord T))
-- TODO: reason about raw bundling vs. refined bundling.
-class OrdSpec where
+-- raw bundling: hypothesis with Rust extracted objects.
+-- refined bundling: lifted hypothesis with Lean native objects.
+class OrdSpecInfaillible where
infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o
+
+class OrdSpecDuality extends OrdSpecInfaillible H where
duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
+-- TODO: OrdSpecEq := OrdSpecRel (R := Eq).
+class OrdSpecEq extends OrdSpecInfaillible H where
+ equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b
+
+class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where
+ equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
+
+class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H
+
instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
coe a := a.toLeanOrdering
-def ordSpecOfTotalityAndDuality
- (H: avl_verification.Ord T)
- (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ok o)
- (Hduality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less)
- : OrdSpec H where
- infallible := Hresult
- duality := Hduality
-
-def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
+def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpecInfaillible H): Ord T where
compare x y := (H.cmp x y).get? (by
cases' (spec.infallible x y) with o Hcmp
rewrite [isok, Hcmp]
simp only
)
-theorem ltOfRustOrder {Spec: OrdSpec H}:
+instance [spec: OrdSpecInfaillible H]: Ord T := ordOfOrdSpec H spec
+instance [OrdSpecInfaillible H]: LT T := ltOfOrd
+
+theorem ltOfRustOrder {Spec: OrdSpecInfaillible H}:
haveI O := ordOfOrdSpec H Spec
haveI := @ltOfOrd _ O
∀ a b, H.cmp a b = .ok .Less -> a < b := by
@@ -81,8 +89,8 @@ theorem ltOfRustOrder {Spec: OrdSpec H}:
simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering]
rfl
-theorem gtOfRustOrder {Spec: OrdSpec H}:
- haveI O := ordOfOrdSpec H Spec
+theorem gtOfRustOrder {Spec: OrdSpecDuality H}:
+ haveI O := ordOfOrdSpec H Spec.toOrdSpecInfaillible
haveI := @ltOfOrd _ O
∀ a b, H.cmp a b = .ok .Greater -> b < a := by
intros a b
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
index fdd4b78..8a043a1 100644
--- a/AvlVerification/Tree.lean
+++ b/AvlVerification/Tree.lean
@@ -75,4 +75,7 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.
def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
+@[simp]
+def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry
+
end Tree
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 04:35:23 +0000