diff options
Diffstat (limited to 'AvlVerification')
| -rw-r--r-- | AvlVerification/BinarySearchTree.lean | 54 | ||||
| -rw-r--r-- | AvlVerification/Insert.lean | 173 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 98 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 81 |
4 files changed, 0 insertions, 406 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean deleted file mode 100644 index 2b17d52..0000000 --- a/AvlVerification/BinarySearchTree.lean +++ /dev/null @@ -1,54 +0,0 @@ -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 deleted file mode 100644 index f5b7958..0000000 --- a/AvlVerification/Insert.lean +++ /dev/null @@ -1,173 +0,0 @@ -import AvlVerification.Tree -import AvlVerification.BinarySearchTree -import AvlVerification.Specifications - -namespace Implementation - -open Primitives -open avl_verification -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) - -variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H) - -@[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)) - : - BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩ - ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by - intro Hbst - match t with - | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf] - | 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, 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 - apply Hnode; exact H_forall_right - exact (ltOfRustOrder H b a Hordering) - exact H_bst_left - convert H_bst - exact H_result.2 - simp [AVLTree.set_some] - rewrite [H_result.2, H_set] - simp - } - { - simp; split_conjs - . tauto - . simp [Ospec.equivalence _ _ Hordering] - } - { - 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 - exact (gtOfRustOrder H b a Hordering) - exact H_forall_right - 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): - 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 - ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set 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 deleted file mode 100644 index ac2d056..0000000 --- a/AvlVerification/Specifications.lean +++ /dev/null @@ -1,98 +0,0 @@ -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: outParam (avl_verification.Ord T)) - --- TODO: reason about raw bundling vs. refined bundling. --- 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 - -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, OrdSpecRel H Eq - -instance: Coe (avl_verification.Ordering) (_root_.Ordering) where - coe a := a.toLeanOrdering - -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 - ) - -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 - 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: 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 - intro Hcmp - apply ltOfRustOrder - exact (Spec.duality _ _ Hcmp) - - -end Specifications diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean deleted file mode 100644 index 8a043a1..0000000 --- a/AvlVerification/Tree.lean +++ /dev/null @@ -1,81 +0,0 @@ -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) - -@[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 |