diff options
| -rw-r--r-- | AvlVerification.lean | 18 | ||||
| -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 | ||||
| -rw-r--r-- | Main.lean | 122 | ||||
| -rw-r--r-- | notes.md | 11 |
7 files changed, 433 insertions, 116 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 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 @@ -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. |