Updated to lean 4.2.0

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 /.cache
+*.olean

ProvenZk/Binary.lean

@@ -1,3 +1,4 @@
+import Mathlib.Data.ZMod.Defs
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.Bitvec.Defs
 
@@ -412,7 +413,6 @@ theorem zmod_to_bit_coe {n : Nat} [Fact (n > 1)] {w : Vector Bit d} :
           apply absurd this
           simp
         | succ =>
-          simp
           rfl
     }
 
@@ -507,7 +507,6 @@ theorem fin_to_bits_le_to_recover_binary_zmod' {n d : Nat} [Fact (n > 1)] {v : Z
     linarith
     assumption
     assumption
-    simp [recover_binary_nat_to_bits_le]
     simp [fin_to_bits_le]
     split
     rename_i h

ProvenZk/Ext/Fin.lean

@@ -18,7 +18,7 @@ theorem castSucc_def {i : Fin n} :
   Fin.mk (n := Nat.succ n) (i.val) (by cases i; linarith) = i.castSucc := by
   rfl
 
-theorem cast_last {n : Nat} : ↑n = Fin.last n := by
+theorem nat_cast_last {n : Nat} : ↑n = Fin.last n := by
   conv => lhs; whnf
   conv => rhs; whnf
   simp

ProvenZk/Ext/List.lean

@@ -1,3 +1,6 @@
+-- import Mathlib.Data.List.Basic
+-- import Mathlib.Data.List.Indexes
+import Std.Data.List.Basic
 import Mathlib.Data.List.Basic
 import Mathlib.Data.List.Indexes
 
@@ -39,4 +42,4 @@ theorem dropLast_cons {head₁ head₂ : α} {tail : List α} : List.dropLast (h
   | nil => simp
   | cons _ _ _ => simp [List.dropLast]
 
-end List
+end List

ProvenZk/Ext/Vector/Basic.lean

@@ -1,6 +1,11 @@
+--import Mathlib.Data.Vector.Snoc
+--import Mathlib.Data.Matrix.Basic
+--import Mathlib.Data.List.Defs
+import Mathlib.Data.Vector
+import Mathlib.Data.Vector.Basic
 import Mathlib.Data.Vector.Snoc
 import Mathlib.Data.Matrix.Basic
-import Mathlib.Data.List.Defs
+import Std.Data.Fin.Lemmas
 
 import ProvenZk.Ext.Fin
 import ProvenZk.Ext.Range
@@ -220,13 +225,13 @@ lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = v
   induction n with
   | zero =>
     cases i using Fin.cases with
-    | H0 => cases vs using Vector.casesOn with | cons hd tl => simp
-    | Hs i => cases i using finZeroElim
+    | zero => cases vs using Vector.casesOn with | cons hd tl => simp
+    | succ i => cases i using finZeroElim
   | succ n ih =>
     cases vs using Vector.casesOn with | cons hd tl =>
     cases i using Fin.cases with
-    | H0 => simp
-    | Hs i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih]
+    | zero => simp
+    | succ i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih]
 
 theorem vector_get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by
   rfl

ProvenZk/Ext/Vector/SetLoop.lean

@@ -1,6 +1,5 @@
 import ProvenZk.Ext.Vector.Basic
 
-
 namespace Vector
 
 private lemma set_at_len (l1 l2 : List α) (it new : α):
@@ -133,4 +132,4 @@ theorem setLoop_mapIdx {v : Vector α n} {f : ℕ -> α -> α }:
   apply Vector.eq
   simp [listMapIdx_setLoop, toList_setLoop]
 
-end Vector
+end Vector

ProvenZk/Gates.lean

@@ -1,4 +1,4 @@
-import Mathlib.Data.ZMod.Basic
+import Mathlib.Data.ZMod.Defs
 
 import ProvenZk.Binary
 

ProvenZk/Subvector.lean

@@ -10,8 +10,8 @@ def snoc (vs: SubVector α n prop) (v : Subtype prop): SubVector α n.succ prop
   ⟨vs.val.snoc v.val, by
     intro i
     cases i using Fin.lastCases with
-    | hlast => simp [GetElem.getElem, Fin.last_def, Subtype.property]
-    | hcast i =>
+    | last => simp [GetElem.getElem, Fin.last_def, Subtype.property]
+    | cast i =>
       have := vs.prop i
       simp at this
       simp [*]
@@ -56,6 +56,6 @@ theorem snoc_lower {vs : SubVector α n prop} {v : Subtype prop}:
     cases n with
     | zero => cases i using finZeroElim
     | _ => simp [GetElem.getElem, snoc]
-  . simp [GetElem.getElem, snoc, Fin.cast_last]
+  . simp [GetElem.getElem, snoc, Fin.nat_cast_last]
 
 end SubVector

lake-manifest.json

@@ -1,39 +1,52 @@
-{"version": 4,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
-    "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "name": "Cli",
-    "inputRev?": "nightly"}},
-  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9",
+    "rev": "753159252c585df6b6aa7c48d2b8828d58388b79",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}},
+    "inputRev?": "v4.2.0",
+    "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
-    "name": "aesop",
-    "inputRev?": "master"}},
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "6747f41f28627bed83e6d5891683538211caa2c1",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}}],
+ "name": "«proven-zk»"}

lakefile.lean

@@ -6,7 +6,7 @@ package «proven-zk» {
 }
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9"
+  "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
 
 @[default_target]
 lean_lib «ProvenZk» {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:v4.2.0