diff options
Diffstat (limited to 'AvlVerification')
| -rw-r--r-- | AvlVerification/BinarySearchTree.lean | 54 | ||||
| -rw-r--r-- | AvlVerification/Insert.lean | 172 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 94 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 78 |
4 files changed, 398 insertions, 0 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean new file mode 100644 index 0000000..2b17d52 --- /dev/null +++ b/AvlVerification/BinarySearchTree.lean @@ -0,0 +1,54 @@ +import AvlVerification.Tree + +namespace BST + +open Primitives (Result) +open avl_verification (AVLNode Ordering) +open Tree (AVLTree AVLNode.left AVLNode.right AVLNode.val) + +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 := 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 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 + -> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right)) + +@[simp] +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}: Invariant t -> Invariant t.left := by + intro H + induction H with + | none => exact Invariant.none + | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption + +theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by + intro H + induction H with + | none => exact Invariant.none + | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption + +end BST diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean new file mode 100644 index 0000000..baf3441 --- /dev/null +++ b/AvlVerification/Insert.lean @@ -0,0 +1,172 @@ +import AvlVerification.Tree +import AvlVerification.BinarySearchTree +import AvlVerification.Specifications + +namespace Implementation + +open Primitives +open avl_verification +open Tree (AVLTree) +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) + +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 + +@[pspec] +theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) + (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.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 + | none => + simp [AVLTreeSet.insert_loop, AVLTree.set, setOf] + intros _ Hpa + constructor; all_goals try simp [BST.ForallNode.none] + exact Hpa + | some (AVLNode.mk b left right) => + rw [AVLTreeSet.insert_loop] + simp only [] + progress keep Hordering as ⟨ ordering ⟩ + cases ordering + all_goals simp only [] + { + progress keep Htree as ⟨ added₁, right₁, Hnode ⟩ + refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩ + simp only [true_and] + intros Hptree Hpa + constructor + exact Hptree.left + exact Hptree.label + exact Hnode Hptree.right Hpa + } + { + simp; tauto + } + { + -- TODO: investigate wlog. + -- Symmetric case of left. + progress keep Htree as ⟨ added₁, left₁, Hnode ⟩ + refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩ + simp only [true_and] + intros Hptree Hpa + constructor + exact Hnode Hptree.left Hpa + exact Hptree.label + exact Hptree.right + } + +@[pspec] +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 + intro Hbst + letI instOrd : _root_.Ord T := (rustOrder Ospec) + letI instLt : LT T := (rustLt Ospec) + match t with + | none => simp [AVLTreeSet.insert_loop] + | some (AVLNode.mk b left right) => + rw [AVLTreeSet.insert_loop] + simp only [] + have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible + progress keep Hordering as ⟨ ordering ⟩ + cases ordering + all_goals simp only [] + { + have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := 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] + cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right + constructor + exact H_forall_left + apply Hnode; exact H_forall_right + exact (ltOfRustOrder H b a Hordering) + exact H_bst_left + convert H_bst + exact H_result.2 + } + { + simp; tauto + } + { + 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 + (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) + := by + 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 new file mode 100644 index 0000000..958a3e7 --- /dev/null +++ b/AvlVerification/Specifications.lean @@ -0,0 +1,94 @@ +import «AvlVerification» + +namespace Primitives + +namespace Result + +def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with +| .ok y => .ok (f y) +| .fail e => .fail e +| .div => .div + +@[inline] +def isok {A: Type} : Result A -> Bool +| .ok _ => true +| .fail _ => false +| .div => false + +@[inline] +def get? {A: Type}: (r: Result A) -> isok r -> A +| .ok x, _ => x + +end Result + +end Primitives + +namespace avl_verification + +def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := match o with +| .Less => .lt +| .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 + +open Primitives +open Result + +variable {T: Type} (H: avl_verification.Ord T) + +-- TODO: reason about raw bundling vs. refined bundling. +class OrdSpec where + 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 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 + 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}: + haveI O := ordOfOrdSpec H Spec + haveI := @ltOfOrd _ O + ∀ a b, H.cmp a b = .ok .Less -> a < b := by + intros a b + intro Hcmp + 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 new file mode 100644 index 0000000..fdd4b78 --- /dev/null +++ b/AvlVerification/Tree.lean @@ -0,0 +1,78 @@ +import «AvlVerification» + +namespace Tree + +variable {T: Type} + +open avl_verification + +-- Otherwise, Lean cannot prove termination by itself. +@[reducible] +def AVLTree (U: Type) := Option (AVLNode U) +def AVLTree.nil: AVLTree T := none + +def AVLTree.val (t: AVLTree T): Option T := match t with +| none => none +| some (AVLNode.mk x _ _) => some x + +def AVLTree.left (t: AVLTree T): AVLTree T := match t with +| none => none +| some (AVLNode.mk _ left _) => left + +def AVLTree.right (t: AVLTree T): AVLTree T := match t with +| none => none +| some (AVLNode.mk _ _ right) => right + +def AVLNode.left (t: AVLNode T): AVLTree T := match t with +| AVLNode.mk _ left _ => left + +def AVLNode.right (t: AVLNode T): AVLTree T := match t with +| AVLNode.mk _ _ right => right + +def AVLNode.val (t: AVLNode T): T := match t with +| AVLNode.mk x _ _ => x + +mutual +def AVLTree.height_node (tree: AVLNode T): Nat := match tree with +| AVLNode.mk y left right => 1 + AVLTree.height left + AVLTree.height right + +def AVLTree.height (tree: AVLTree T): Nat := match tree with +| none => 0 +| some n => 1 + AVLTree.height_node n +end + +def AVLTreeSet.nil: AVLTreeSet T := { root := AVLTree.nil } + +-- Automatic synthesization of this seems possible at the Lean level? +instance: Inhabited (AVLTree T) where + default := AVLTree.nil + +instance: Inhabited (AVLTreeSet T) where + default := AVLTreeSet.nil + +instance: Coe (Option (AVLNode T)) (AVLTree T) where + coe x := x + +-- TODO: ideally, it would be nice if we could generalize +-- this to any `BinaryTree` typeclass. + +def AVLTree.mem (tree: AVLTree T) (x: T) := + match tree with + | none => False + | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x + +@[simp] +def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl + +@[simp] +def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by + ext y + rw [AVLTree.mem] + simp [Set.insert_union] + simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def] + +-- TODO(reinforcement): ∪ is actually disjoint if we prove this is a binary search tree. + +def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t) + +end Tree |