From 33a92dac2635ead90cb84c16023355a7d679d434 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Tue, 26 Mar 2024 14:25:07 +0100
Subject: feat: first property "set of values post = {a} \cup set of values
 pre"

This is a first property which is generic of all BSTs.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 Main.lean | 87 +++++++++++++++++++++++++++++++++++++++++++++------------------
 1 file changed, 62 insertions(+), 25 deletions(-)

diff --git a/Main.lean b/Main.lean
index dea47e5..c96af67 100644
--- a/Main.lean
+++ b/Main.lean
@@ -33,59 +33,96 @@ def AVL.height (tree: AVLTree T): Nat := match tree with
 end
 
 
-def AVLTree.mem (tree: AVLTree T) (x: T): Prop :=
+@[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 y
+  | 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.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... ?
-
-#check (AVL.nil.insert _ _ 0#u32)
-
-
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root))
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root))
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun (added, tree)  => Result.ret (added, AVLTree.setOf tree.root))
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root))
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun (added, tree)  => Result.ret (added, AVLTree.setOf tree.root))
-#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root))
-
-def AVLTreeSet.setOfInsert {H: avl_verification.Ord T} (a: T) (t: AVLTreeSet T) := Primitives.bind (t.insert _ H a) (fun (_, tree) => Result.ret (AVLTree.setOf tree.root))
-
 -- TODO: derive from Ord an Lean Order instance.
 -- TODO: oh no, H.cmp returns a Result!
 
 @[pspec]
-def AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} 
+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' := by
-  match t with
-  | none => simp [AVLTreeSet.insert_loop]
+  ∃ 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 as ⟨ ordering ⟩
+    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
-      simp
+      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 x = Result.ret t' ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) := by
+  ∃ 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; simp
+  progress keep h as ⟨ t', Hset ⟩; simp
+  rw [Hset]
 
 end Avl
-- 
cgit v1.2.3