diff options
| -rw-r--r-- | AvlVerification/BinarySearchTree.lean | 37 | ||||
| -rw-r--r-- | AvlVerification/Insert.lean | 87 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 55 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 81 | ||||
| -rw-r--r-- | Main.lean | 122 | ||||
| -rw-r--r-- | notes.md | 11 |
6 files changed, 286 insertions, 107 deletions
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean new file mode 100644 index 0000000..130fd73 --- /dev/null +++ b/AvlVerification/BinarySearchTree.lean @@ -0,0 +1,37 @@ +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)) + +-- This is the binary search invariant. +inductive BST [LT T]: AVLTree T -> Prop +| none : BST 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)) + +@[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 left [LT T] {t: AVLTree T}: BST t -> BST t.left := by + intro H + induction H with + | none => exact BST.none + | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption + +theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by + intro H + induction H with + | none => exact BST.none + | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption + +end BST diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean new file mode 100644 index 0000000..870e9c2 --- /dev/null +++ b/AvlVerification/Insert.lean @@ -0,0 +1,87 @@ +import AvlVerification.Tree +import AvlVerification.BinarySearchTree +import AvlVerification.Specifications + +namespace Implementation + +open Primitives +open avl_verification +open Tree (AVLTree) + +variable {T: Type} + +@[pspec] +theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} + (a: T) (t: Option (AVLNode T)) + [LT T] + (Hbs_search: BST.BST t) + (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o): + ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩ +-- ∧ AVLTree.set t'.2 = insert a (AVLTree.set t) + ∧ BST.BST t_new + := by match t with + | none => + simp [AVLTreeSet.insert_loop, AVLTree.set, setOf, BST.BST] + | some (AVLNode.mk b left right) => + rw [AVLTreeSet.insert_loop] + simp only [] + progress keep Hordering as ⟨ ordering ⟩ + cases ordering + all_goals simp only [] + have Hbs_search_right: BST.BST right := BST.right Hbs_search + have Hbs_search_left: BST.BST left := BST.left Hbs_search + { + progress keep Htree as ⟨ added₁, right₁, Hbst ⟩ + refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩ + simp only [true_and] + refine' (BST.BST.some b left right₁ _ _ Hbs_search_left Hbst) + cases' Hbs_search; assumption + induction right with + | none => + simp [AVLTreeSet.insert_loop] at Htree + rw [← Htree.2] + refine' (BST.ForallNode.some _ _ _ BST.ForallNode.none _ BST.ForallNode.none) + sorry + | some node => + -- clef: ∀ x ∈ node.right, b < x + -- de plus: b < a + -- or, right₁ = insert a node.right moralement + -- donc, il suffit de prouver que: ∀ x ∈ insert a node.right, b < x <-> b < a /\ ∀ x ∈ node.right, b < x + sorry + } + { + simp [Hbs_search] + } + { + -- Symmetric case of left. + sorry + } + +@[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) + -- 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) + := 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) + +end Implementation + diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean new file mode 100644 index 0000000..0bf9ffb --- /dev/null +++ b/AvlVerification/Specifications.lean @@ -0,0 +1,55 @@ +import «AvlVerification» + +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) +| .fail e => .fail e +| .div => .div + +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 + +end avl_verification + +namespace Specifications + +open Primitives +open Result + +variable {T: Type} + +class OrdSpec (U: Type) where + cmp: U -> U -> Result Ordering + infallible: ∀ a b, ∃ o, cmp a b = .ret o + +instance: Coe (avl_verification.Ordering) (_root_.Ordering) where + coe a := a.toLeanOrdering + +def ordSpecOfInfaillible + (H: avl_verification.Ord T) + (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ret o) + : OrdSpec T where + cmp x y := (H.cmp x y).map (fun z => z.toLeanOrdering) + infallible := by + intros a b + -- TODO: transform the "raw" hypothesis into the "nice" hypothesis. + sorry + +instance [OrdSpec T]: Ord T where + compare x y := match (OrdSpec.cmp x y) with + | .ret z => z + | .fail _ => by sorry + | .div => by sorry + +end Specifications diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean new file mode 100644 index 0000000..3316e9e --- /dev/null +++ b/AvlVerification/Tree.lean @@ -0,0 +1,81 @@ +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) + +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 @@ -10,119 +10,27 @@ namespace Avl open avl_verification variable {T: Type} -def AVL.nil: AVLTreeSet T := { root := none } +-- instance {H: avl_verification.Ord T}: LT T := { +-- lt := λ x y => H.cmp x y = Result.ret Ordering.Less +-- } +-- This is the binary search invariant. +def BSTree.searchInvariant {H: avl_verification.Ord T} (t: AVLTree T) := match t with +| none => True +| some (AVLNode.mk y u v) => ∀ x ∈ AVLTree.setOf (u : AVLTree T), H.cmp y x = Result.ret Ordering.Less ∧ ∀ x ∈ AVLTree.setOf (v : AVLTree T), H.cmp y x = Result.ret Ordering.Greater --- TODO: AVLTree T ou AVLNode T? -noncomputable def AVL.height' (tree: AVLNode T): Nat := AVLNode.rec tree - (mk := fun _ _ _ ihl ihr => 1 + ihl + ihr) - (none := 0) - (some := fun _ ih => 1 + ih) +-- Prove that: +-- searchInvariant t <-> searchInvariant t.left /\ searchInvariant t.right /\ something about t.val +-- searchInvariant t -> searchInvariant t.left /\ searchInvariant t.right by weakening. --- Otherwise, Lean cannot prove termination by itself. -@[reducible] -def AVLTree (U: Type) := Option (AVLNode U) +def BSTree.nil_has_searchInvariant {H: avl_verification.Ord T}: @BSTree.searchInvariant _ H AVL.nil.root := by trivial -mutual -def AVL.height'' (tree: AVLNode T): Nat := match tree with -| AVLNode.mk y left right => 1 + AVL.height left + AVL.height right +theorem BSTree.searchInvariant_children {H: avl_verification.Ord T} (t: AVLTree T): @searchInvariant _ H t -> @searchInvariant _ H t.left ∧ @searchInvariant _ H t.right := sorry -def AVL.height (tree: AVLTree T): Nat := match tree with -| none => 0 -| some node => 1 + AVL.height'' node -end - - -@[reducible] -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 - --- TODO: why the explicit type annotation is required here? --- TODO(reinforcement): ∪ is actually disjoint. -@[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] - - -def AVLTree.setOf: AVLTree T -> Set T := AVLTree.mem -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 AVLTree.height (t: AVLTree T) := AVL.height t +def AVLTree.balanceFactor (t: AVLTree T): Int := t.right.height - t.left.height +def AVLTree.balanceInvariant (t: AVLTree T) := t.balanceFactor = -1 ∨ t.balanceFactor = 0 ∨ t.balanceFactor = 1 def AVLTree.mem_eq_setOf (t: AVLTree T): AVLTree.mem t = t.setOf := rfl --- TODO: {t.val} = {} if t.val is none else {t.val.get!} otherwise. --- @[simp] --- def AVLTree.setOf_eq_union (t: AVLTree T): t.setOf = {t.val} ∪ t.left.setOf ∪ t.right.setOf := sorry - --- Note: we would like to have a theorem that says something like --- t.setOf = {t.val} ∪ t.left.setOf ∪ t.right.setOf --- but it's not doable because Aeneas does not generate a `structure` but an inductive type with one constructor. - -#check AVL.nil -#check U32.ofInt 0 -#check 0#u32 --- TODO: créer une instance OfNat pour les Uxyz. --- TODO: générer {} adéquatement... ? --- TODO: derive from Ord an Lean Order instance. --- TODO: oh no, H.cmp returns a Result! - -@[pspec] -theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} - (a: T) (t: Option (AVLNode T)) - (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): - ∃ t', AVLTreeSet.insert_loop T H a t = Result.ret t' - ∧ AVLTree.setOf t'.2 = insert a (AVLTree.setOf t) := by match t with - | none => - simp [AVLTreeSet.insert_loop, AVLTree.setOf] - | some (AVLNode.mk b left right) => - rw [AVLTreeSet.insert_loop] - simp only [] - progress keep Hordering as ⟨ ordering ⟩ - cases ordering - all_goals { - -- TODO: oof. - -- We are trying to tackle all goals at the same time. - -- Refactor this to make it only one simp ideally without even `try`. - simp only [] - try progress keep H as ⟨ t'', Hset ⟩ - simp [AVLTree.setOf] - try simp [AVLTree.setOf] at Hset - try simp [Hset] - try rw [Set.insert_comm, Set.insert_union] - try simp [Hcmp_eq _ _ Hordering] - } - -@[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) - (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) - -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root) - := by - rw [AVLTreeSet.insert] - progress keep h as ⟨ t', Hset ⟩; simp - rw [Hset] - end Avl diff --git a/notes.md b/notes.md new file mode 100644 index 0000000..cd82dd3 --- /dev/null +++ b/notes.md @@ -0,0 +1,11 @@ +# Formalization notes + +- Inhabited is not synthesized systematically for any type. +- Synthesize type aliases (?): requires to obtain this information before MIR. + +## Bundle of specifications + +Most of the time, we have naked types which does not exhibit their "expected" specification, +e.g. an `Ord` trait which does not prove that it's an order. + +Ideally, we need to be able to build trait specifications and find a way to unbundle them and use them in the different tactics. |