summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--AvlVerification.lean18
-rw-r--r--AvlVerification/BinarySearchTree.lean54
-rw-r--r--AvlVerification/Insert.lean172
-rw-r--r--AvlVerification/Specifications.lean94
-rw-r--r--AvlVerification/Tree.lean78
-rw-r--r--Main.lean122
-rw-r--r--notes.md11
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
diff --git a/Main.lean b/Main.lean
index c96af67..6010d26 100644
--- a/Main.lean
+++ b/Main.lean
@@ -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.