New merkletree proof

reilabs · Nov 3, 2023 · b12b886 · b12b886
1 parent 4d6558d
commit b12b886
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 1 deletion.
diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean
@@ -528,4 +528,23 @@ theorem recover_equivalence
     . apply recover_proof_reversible (Item := Item)
       assumption
 
+theorem eq_root_eq_tree {H} [ph: Fact (perfect_hash H)] {t₁ t₂ : MerkleTree α H d}:
+  t₁.root = t₂.root ↔ t₁ = t₂ := by
+  induction d with
+  | zero => cases t₁; cases t₂; tauto
+  | succ _ ih =>
+    cases t₁
+    cases t₂
+    apply Iff.intro
+    . intro h
+      have h := Fact.elim ph h
+      injection h with h
+      injection h with _ h
+      injection h
+      congr <;> {rw [←ih]; assumption}
+    . intro h
+      injection h
+      subst_vars
+      rfl
+
 end MerkleTree
diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean
@@ -44,4 +44,4 @@ lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b
 
 lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by
   simp
-  tauto
+  tauto
-Original file line number
+Diff line change
@@ Expand Up @@
     lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by
       simp
-      tauto
+      tauto