diff options
| -rw-r--r-- | AvlVerification.lean | 18 | ||||
| -rw-r--r-- | AvlVerification/BinarySearchTree.lean | 41 | ||||
| -rw-r--r-- | AvlVerification/Insert.lean | 95 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 62 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 3 |
5 files changed, 138 insertions, 81 deletions
diff --git a/AvlVerification.lean b/AvlVerification.lean index e0516b4..828b2aa 100644 --- a/AvlVerification.lean +++ b/AvlVerification.lean @@ -30,7 +30,7 @@ structure AVLTreeSet (T : Type) where /- [avl_verification::{avl_verification::AVLTreeSet<T>}::new]: Source: 'src/main.rs', lines 24:4-24:24 -/ def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) := - Result.ret { root := none } + Result.ok { root := none } /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0: Source: 'src/main.rs', lines 28:4-46:5 -/ @@ -41,7 +41,7 @@ divergent def AVLTreeSet.insert_loop := match current_tree with | none => let a := AVLNode.mk value none none - Result.ret (true, some a) + Result.ok (true, some a) | some current_node => do let ⟨ t, current_tree1, current_tree2 ⟩ := current_node @@ -50,13 +50,13 @@ divergent def AVLTreeSet.insert_loop | Ordering.Less => do let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree2 - Result.ret (b, some (AVLNode.mk t current_tree1 back)) + Result.ok (b, some (AVLNode.mk t current_tree1 back)) | Ordering.Equal => - Result.ret (false, some (AVLNode.mk t current_tree1 current_tree2)) + Result.ok (false, some (AVLNode.mk t current_tree1 current_tree2)) | Ordering.Greater => do let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree1 - Result.ret (b, some (AVLNode.mk t back current_tree2)) + Result.ok (b, some (AVLNode.mk t back current_tree2)) /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: Source: 'src/main.rs', lines 28:4-28:46 -/ @@ -66,17 +66,17 @@ def AVLTreeSet.insert := do let (b, back) ← AVLTreeSet.insert_loop T OrdInst value self.root - Result.ret (b, { root := back }) + Result.ok (b, { root := back }) /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]: Source: 'src/main.rs', lines 50:4-50:43 -/ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := if self < other - then Result.ret Ordering.Less + then Result.ok Ordering.Less else if self = other - then Result.ret Ordering.Equal - else Result.ret Ordering.Greater + then Result.ok Ordering.Equal + else Result.ok Ordering.Greater /- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}] Source: 'src/main.rs', lines 49:0-49:16 -/ diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean index 954f21f..2b17d52 100644 --- a/AvlVerification/BinarySearchTree.lean +++ b/AvlVerification/BinarySearchTree.lean @@ -10,34 +10,45 @@ inductive ForallNode (p: T -> Prop): AVLTree T -> Prop | none : ForallNode p none | some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right)) -theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := sorry - -theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := sorry - -theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := sorry +theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := by + intro Hpt + cases Hpt with + | none => simp [AVLTree.left, ForallNode.none] + | some a left right f_pleft f_pa f_pright => simp [AVLTree.left, f_pleft] + +theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := by + intro Hpt + cases Hpt with + | none => simp [AVLTree.right, ForallNode.none] + | some a left right f_pleft f_pa f_pright => simp [AVLTree.right, f_pright] + +theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := by + intro Hpt + cases Hpt with + | some a left right f_pleft f_pa f_pright => exact f_pa -- This is the binary search invariant. -inductive BST [LT T]: AVLTree T -> Prop -| none : BST none +inductive Invariant [LT T]: AVLTree T -> Prop +| none : Invariant none | some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right - -> BST left -> BST right -> BST (some (AVLNode.mk a left right)) + -> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right)) @[simp] -theorem singleton_bst [LT T] {a: T}: BST (some (AVLNode.mk a none none)) := by - apply BST.some - all_goals simp [ForallNode.none, BST.none] +theorem singleton_bst [LT T] {a: T}: Invariant (some (AVLNode.mk a none none)) := by + apply Invariant.some + all_goals simp [ForallNode.none, Invariant.none] -theorem left [LT T] {t: AVLTree T}: BST t -> BST t.left := by +theorem left [LT T] {t: AVLTree T}: Invariant t -> Invariant t.left := by intro H induction H with - | none => exact BST.none + | none => exact Invariant.none | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption -theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by +theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by intro H induction H with - | none => exact BST.none + | none => exact Invariant.none | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption end BST diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean index 3c2b8b3..baf3441 100644 --- a/AvlVerification/Insert.lean +++ b/AvlVerification/Insert.lean @@ -7,9 +7,47 @@ namespace Implementation open Primitives open avl_verification open Tree (AVLTree) -open Specifications (OrdSpec ordSpecOfInfaillible ordOfOrdSpec ltOfRustOrder) +open Specifications (OrdSpec ordSpecOfTotalityAndDuality 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) --- TODO: OSpec should be proven. 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 @@ -20,9 +58,9 @@ instance rustLt' : LT T := rustLt Ospec @[pspec] theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) - (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o) + (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ok o) (a: T) (t: Option (AVLNode T)): - ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩ + ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩ -- ∧ AVLTree.set t'.2 = insert a (AVLTree.set t) ∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new) := by match t with @@ -68,8 +106,8 @@ lemma AVLTreeSet.insert_loop_spec_global (a: T) (t: Option (AVLNode T)) : haveI : LT T := (rustLt Ospec) - BST.BST t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩ - ∧ BST.BST t_new := by + BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩ + ∧ BST.Invariant t_new := by intro Hbst letI instOrd : _root_.Ord T := (rustOrder Ospec) letI instLt : LT T := (rustLt Ospec) @@ -78,9 +116,7 @@ lemma AVLTreeSet.insert_loop_spec_global | some (AVLNode.mk b left right) => rw [AVLTreeSet.insert_loop] simp only [] - have := Ospec.infallible; simp at this - -- TODO: unbundle `this`... - have : ∀ a b, ∃ o, H.cmp a b = .ret o := sorry + have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible progress keep Hordering as ⟨ ordering ⟩ cases ordering all_goals simp only [] @@ -104,34 +140,33 @@ lemma AVLTreeSet.insert_loop_spec_global simp; tauto } { - sorry + have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := 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] + cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right + constructor + apply Hnode; exact H_forall_left + exact (gtOfRustOrder H b a Hordering) + exact H_forall_right + convert H_bst + exact H_result.2 + exact H_bst_right } @[pspec] def AVLTreeSet.insert_spec - {H: avl_verification.Ord T} - -- TODO: this can be generalized into `H.cmp` must be an equivalence relation. - -- and insert works no longer on Sets but on set quotiented by this equivalence relation. - (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b) - (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o) - (Hbs_search: @BSTree.searchInvariant _ H t) (a: T) (t: AVLTreeSet T): - ∃ t', t.insert _ H a = Result.ret t' - -- set of values *POST* insertion is {a} \cup set of values of the *PRE* tree. - ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) + 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. - ∧ @BSTree.searchInvariant _ H t'.2.root - -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root) + ∧ BST.Invariant t'.root) := by - rw [AVLTreeSet.insert] - progress keep h as ⟨ t', Hset ⟩; simp - rw [Hset] - sorry - - --- insert is infaillible, right? --- instance [LT T] (o: avl_verification.Ord T): Insert T (AVLTreeSet T) where --- insert x tree := (AVLTreeSet.insert T o tree x).map (fun (added, tree) => tree) + rw [AVLTreeSet.insert]; intro Hbst + progress keep h as ⟨ t', Hset ⟩; + simp; assumption end Implementation diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean index 247fd00..958a3e7 100644 --- a/AvlVerification/Specifications.lean +++ b/AvlVerification/Specifications.lean @@ -5,19 +5,19 @@ namespace Primitives namespace Result def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with -| .ret y => .ret (f y) +| .ok y => .ok (f y) | .fail e => .fail e | .div => .div @[inline] -def isRet {A: Type} : Result A -> Bool -| .ret _ => true +def isok {A: Type} : Result A -> Bool +| .ok _ => true | .fail _ => false | .div => false @[inline] -def get? {A: Type}: (r: Result A) -> isRet r -> A -| .ret x, _ => x +def get? {A: Type}: (r: Result A) -> isok r -> A +| .ok x, _ => x end Result @@ -30,6 +30,11 @@ def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := m | .Equal => .eq | .Greater => .gt +def Ordering.ofLeanOrdering (o: _root_.Ordering): avl_verification.Ordering := match o with +| .lt => .Less +| .eq => .Equal +| .gt => .Greater + end avl_verification namespace Specifications @@ -39,42 +44,51 @@ open Result variable {T: Type} (H: avl_verification.Ord T) +-- TODO: reason about raw bundling vs. refined bundling. class OrdSpec where - cmp: T -> T -> Result Ordering := fun x y => (H.cmp x y).map (fun z => z.toLeanOrdering) - infallible: ∀ a b, ∃ (o: Ordering), cmp a b = .ret o - -@[simp] -theorem OrdSpec.cmpEq {Spec: OrdSpec H}: ∀ x y, Spec.cmp x y = (H.cmp x y).map (fun z => z.toLeanOrdering) := sorry - -@[simp] -theorem OrdSpec.infallibleEq {Spec: OrdSpec H}: ∀ a b, ∃ (o: Ordering), Spec.cmp a b = .ret o <-> ∀ a b, ∃ (o: Ordering), (H.cmp a b).map (fun z => z.toLeanOrdering) = .ret o := sorry + infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o + duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less instance: Coe (avl_verification.Ordering) (_root_.Ordering) where coe a := a.toLeanOrdering -def ordSpecOfInfaillible +def ordSpecOfTotalityAndDuality (H: avl_verification.Ord T) - (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ret o) + (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 := by - intros a b; cases' (Hresult a b) with o Hcmp; refine' ⟨ o.toLeanOrdering, _ ⟩ - simp [Result.map, Hcmp] + infallible := Hresult + duality := Hduality def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where - compare x y := (spec.cmp x y).get? (by + compare x y := (H.cmp x y).get? (by cases' (spec.infallible x y) with o Hcmp - rewrite [isRet, Hcmp] + rewrite [isok, Hcmp] simp only ) theorem ltOfRustOrder {Spec: OrdSpec H}: haveI O := ordOfOrdSpec H Spec haveI := @ltOfOrd _ O - ∀ a b, H.cmp a b = .ret .Less -> a < b := by + ∀ a b, H.cmp a b = .ok .Less -> a < b := by intros a b intro Hcmp - change ((Spec.cmp a b).get? _ == .lt) - simp [Hcmp, map, avl_verification.Ordering.toLeanOrdering] - simp [get?] + rw [LT.lt] + simp [ltOfOrd] + rw [compare] + simp [ordOfOrdSpec] + -- https://proofassistants.stackexchange.com/questions/1062/what-does-the-motive-is-not-type-correct-error-mean-in-lean + simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering] rfl + +theorem gtOfRustOrder {Spec: OrdSpec H}: + haveI O := ordOfOrdSpec H Spec + haveI := @ltOfOrd _ O + ∀ a b, H.cmp a b = .ok .Greater -> b < a := by + intros a b + intro Hcmp + apply ltOfRustOrder + exact (Spec.duality _ _ Hcmp) + + end Specifications diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean index 3316e9e..fdd4b78 100644 --- a/AvlVerification/Tree.lean +++ b/AvlVerification/Tree.lean @@ -75,7 +75,4 @@ 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) -def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry -def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry - end Tree |