New theorems

ProvenZk/Ext/Vector/Basic.lean

@@ -192,4 +192,8 @@ lemma toList_dropLast { n : Nat } (v : Vector α n) : v.dropLast.toList = v.toLi
 lemma vector_list_vector {d} {x₁ x₂ : α} {xs : Vector α d} : (x₁ ::ᵥ x₂ ::ᵥ xs).dropLast = x₁ ::ᵥ (x₂ ::ᵥ xs).dropLast := by
   rfl
 
+lemma cons_zero {d : Nat } {y : α} {v : Vector α d} :
+  (y ::ᵥ v)[0] = y := by
+    rfl
+
 end Vector

ProvenZk/Merkle.lean

@@ -646,4 +646,66 @@ lemma proof_of_set_fin
   simp [tree_proof_at_fin, tree_set_at_fin]
   simp [proof_of_set_is_proof]
 
+def multi_set { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : MerkleTree F H depth :=
+  match b with
+  | Nat.zero => tree
+  | Nat.succ _ => multi_set (tree.set path.head item) path.tail item
+
+lemma tree_set_comm  { depth : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p₁ p₂ : Vector Dir depth} {item : F}:
+  MerkleTree.set (MerkleTree.set tree p₁ item) p₂ item = MerkleTree.set (MerkleTree.set tree p₂ item) p₁ item := by
+  induction depth with
+  | zero => rfl
+  | succ d ih => cases tree with | bin l r =>
+    cases p₁ using Vector.casesOn with | cons p₁h p₁t =>
+    cases p₂ using Vector.casesOn with | cons p₂h p₂t =>
+    cases p₁h <;> {
+      cases p₂h <;> { simp [MerkleTree.set, MerkleTree.left, MerkleTree.right]; try rw [ih] }
+    }
+
+lemma multi_set_set { depth b : Nat } {F: Type} {H : Hash F 2} {tree : MerkleTree F H depth} {p : Vector Dir depth} {path : Vector (Vector Dir depth) b} {item : F}:
+  multi_set (MerkleTree.set tree p item) path item = MerkleTree.set (multi_set tree path item) p item := by
+  induction path using Vector.inductionOn generalizing tree p with
+  | h_nil => rfl
+  | h_cons ih => simp [multi_set, ih, tree_set_comm]
+
+def multi_item_at { depth b : Nat } {F: Type} {H : Hash F 2} (tree : MerkleTree F H depth) (path : Vector (Vector Dir depth) b) (item : F) : Prop :=
+  match b with
+  | Nat.zero => true
+  | Nat.succ _ => tree.item_at path.head = item ∧ multi_item_at tree path.tail item
+
+theorem multi_set_is_item_at { depth b : Nat } {F: Type} {H : Hash F 2} {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} :
+  (multi_set initialTree path item = finalTree →
+  multi_item_at finalTree path item) := by
+  induction path using Vector.inductionOn generalizing initialTree finalTree with
+  | h_nil =>
+    simp [multi_set, multi_item_at]
+  | @h_cons b' x xs ih =>
+    unfold multi_set
+    unfold multi_item_at
+    simp only [Vector.tail_cons, Vector.head_cons]
+    intro h
+    refine ⟨?_, ?_⟩
+    . rw [←h, multi_set_set, MerkleTree.read_after_insert_sound]
+    . apply ih h
+
+theorem multi_set_is_item_at_all_item { depth b i : Nat } {range : i ∈ [0:b]} {F: Type} {H : Hash F 2}
+  {initialTree finalTree: MerkleTree F H depth} {path : Vector (Vector Dir depth) b} {item : F} :
+  multi_set initialTree path item = finalTree →
+  MerkleTree.item_at finalTree (path[i]'(by rcases range; tauto)) = item := by
+  intro hp
+  induction path using Vector.inductionOn generalizing i initialTree finalTree with
+  | h_nil =>
+    rcases range with ⟨lo, hi⟩
+    have := Nat.ne_of_lt (Nat.lt_of_le_of_lt lo hi)
+    contradiction
+  | @h_cons b' x xs ih =>
+    rcases range with ⟨lo, hi⟩
+    cases lo with
+    | refl =>
+      have hitem_at : multi_item_at finalTree (x ::ᵥ xs) item := multi_set_is_item_at hp
+      unfold multi_item_at at hitem_at
+      tauto
+    | @step i h =>
+      exact ih (by assumption) (range := ⟨zero_le _, Nat.lt_of_succ_lt_succ hi⟩)
+
 end MerkleTree