chore: update to v4.28.0

ArkLib/Data/CodingTheory/BerlekampWelch/BerlekampWelch.lean

@@ -132,13 +132,13 @@ within `e` Hamming errors of the received word `f`.
 - `f : Fin n → F` - Received word
 -/
 theorem not_exists_of_decoder_eq_none {e k : ℕ} [NeZero n] {ωs f : Fin n → F}
-  (he : 2 * e < n - k + 1)
-  (hn : k ≤ n)
-  (h_inj : Function.Injective ωs)
-  (h_none : decoder e k ωs f = none)
-  : ¬∃p : F[X], Δ₀(f, p.eval ∘ ωs) ≤ e ∧ p.natDegree < k := by
-  intro contr
-  aesop (add safe forward (decoder_eq_some))
+    (he : 2 * e < n - k + 1) (hn : k ≤ n)
+    (h_inj : Function.Injective ωs)
+    (h_none : decoder e k ωs f = none) :
+    ¬ ∃ p : F[X], Δ₀(f, p.eval ∘ ωs) ≤ e ∧ p.natDegree < k := by
+  rintro ⟨p, hp, hpk⟩
+  have := decoder_eq_some he hn h_inj hpk hp
+  aesop
 
 end
 

ArkLib/Data/CodingTheory/Prelims.lean

@@ -98,7 +98,7 @@ lemma cRank_rank_conversion :
   ]
   calc U.cRank ≤ ↑(Fintype.card (Fin n)) := by exact Matrix.cRank_le_card_width U
          _ = ↑n := by rw[Fintype.card_fin]
-  exact Cardinal.nat_lt_aleph0 n
+  exact Cardinal.natCast_lt_aleph0
 
 /-- An m×n matrix has full rank if the submatrix consisting of columns 1 through m has rank m. -/
 lemma full_row_rank_via_rank_subLeftFull (h : m ≤ n) :

ArkLib/Data/CodingTheory/ProximityGap/DG25.lean

@@ -302,7 +302,8 @@ theorem CA_split_rowwise_implies_CA
           simp only [InterleavedSymbol, WordStack, InterleavedWord,
             instInterleavableWordStackInterleavedWord, interleaveWordStack, Fin.isValue,
             Matrix.transpose_apply]
-          rw! [Nat.sub_add_cancel (h := by omega)]
+        rw! [Nat.sub_add_cancel (h := by omega)]
+        rfl
 
 omit [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype A] [DecidableEq A] [Fintype F] in
 /-- `[⊗_{i=0}^{ϑ-1}(1-r_i, r_i)] · [ - u₀ - ; ... ; - u_{2^ϑ-1} - ]`
@@ -413,10 +414,6 @@ variable {F : Type} [CommRing F] [Fintype F] [NoZeroDivisors F] [DecidableEq F]
 variable (MC : ModuleCode ι F A) [Nontrivial MC]
   (C : Set (Word A ι)) [Nonempty C] -- todo: change to Nontrivial if needed
 
-instance : NoZeroSMulDivisors (R := F) (M := A) := Module.Free.noZeroSMulDivisors F A
-
-instance : NoZeroSMulDivisors (R := F) (M := Word A ι) := _root_.Function.noZeroSMulDivisors
-
 instance : Nonempty MC := by exact instNonemptyOfInhabited
 
 -- instance : ∀ (κ : Type*) [Fintype κ] [DecidableEq κ], Nonempty (C ^⋈ κ) := by

ArkLib/Data/Fin/Tuple/Lemmas.lean

@@ -738,7 +738,7 @@ theorem fappend₂_right {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fi
       rw! [this, ih]; simp
     · have hi : i = last n := by ext; simp; omega
       have : natAdd m i = last (m + n) := by ext; simp; omega
-      rw! [this, fconcat₂_last, hi]
+      rw! [this, fconcat₂_last, hi]; rfl
 
 theorem fappend₂_ext {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin n → A} {β₂ : Fin n → B}
     (u₁ u₂ : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v₁ v₂ : (i : Fin n) → F₂ (β₁ i) (β₂ i)) :
@@ -907,7 +907,7 @@ theorem fappend_right {α : Fin m → A} {β : Fin n → A}
       simp
     · have hi : i = last n := by ext; simp; omega
       have : natAdd m i = last (m + n) := by ext; simp; omega
-      rw! [this, fconcat_last, hi]
+      rw! [this, fconcat_last, hi]; rfl
 
 theorem fappend_ext {α : Fin m → A} {β : Fin n → A}
     (u₁ u₂ : (i : Fin m) → F (α i)) (v₁ v₂ : (i : Fin n) → F (β i)) :

ArkLib/Data/Fin/Tuple/TakeDrop.lean

@@ -69,8 +69,9 @@ theorem rtake_zero (v : (i : Fin n) → α i) :
 theorem rtake_self (v : (i : Fin n) → α i) :
     rtake n (by omega) v = fun i : Fin n => dcast (by simp [Fin.cast]) (v i) := by
   ext i
-  simp [rtake, Fin.natAdd, dcast, cast]
+  simp only [natAdd, cast_mk, rtake, dcast, cast]
   rw! [Nat.sub_self, Nat.zero_add]
+  rfl
 
 @[simp]
 theorem rtake_self' {α : Sort*} (v : Fin n → α) : rtake n (by omega) v = v :=
@@ -116,16 +117,19 @@ theorem take_rtake_append {α : Sort*} (m : ℕ) (h : m ≤ n) (v : Fin n → α
 theorem ofFn_rtake_eq_rtake_ofFn {α : Type*} {m : ℕ} (h : m ≤ n) (v : Fin n → α) :
     List.ofFn (rtake m h v) = (List.ofFn v).rtake m := by
   ext i a
-  simp [List.rtake, natAdd, Fin.cast]
-  constructor <;> intro ⟨hi, ha⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [ha]
+  simp only [List.getElem?_ofFn, rtake_apply, Fin.cast, natAdd, Option.dite_none_right_eq_some,
+    Option.some.injEq, List.rtake, List.length_ofFn, List.getElem?_drop]
+  constructor <;> intro ⟨hi, ha⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [ha] <;> rfl
 
 /-- Alternative version of `ofFn_rtake_eq_rtake_ofFn` with `l : List α` instead of `v : Fin n → α`.
 -/
 theorem ofFn_rtake_get {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
     List.ofFn (rtake m h l.get) = l.rtake m := by
   ext i a
-  simp [List.rtake, natAdd, Fin.cast, List.getElem?_eq_some_iff]
-  constructor <;> intro ⟨hi, ha⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [ha]
+  simp only [List.getElem?_ofFn, rtake_apply, Fin.cast, natAdd, List.get_eq_getElem,
+    Option.dite_none_right_eq_some, Option.some.injEq, List.rtake, List.getElem?_drop,
+    List.getElem?_eq_some_iff]
+  constructor <;> intro ⟨hi, ha⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [ha] <;> rfl
 
 /-- `Fin.rtake` intertwines with `List.rtake` via `List.get`. -/
 theorem get_rtake_eq_rtake_get_comp_cast {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
@@ -286,14 +290,14 @@ theorem ofFn_drop_eq_drop_ofFn {α : Type*} {m : ℕ} (h : m ≤ n) (v : Fin n 
     List.ofFn (drop m h v) = (List.ofFn v).drop m := by
   ext i a
   simp
-  constructor <;> intro ⟨h, h'⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [add_comm, h']
+  constructor <;> intro ⟨h, h'⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [add_comm, h'] <;> rfl
 
 /-- Alternative version of `ofFn_drop_eq_drop_ofFn` with `l : List α` instead of `v : Fin n → α`. -/
 theorem ofFn_drop_get {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
     List.ofFn (drop m h l.get) = l.drop m := by
   ext i a
   simp [List.getElem?_eq_some_iff]
-  constructor <;> intro ⟨h, h'⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [add_comm, h']
+  constructor <;> intro ⟨h, h'⟩ <;> refine ⟨by omega, ?_⟩ <;> rw! [add_comm, h'] <;> rfl
 
 /-- `Fin.drop` intertwines with `List.drop` via `List.get`. -/
 theorem get_drop_eq_drop_get_comp_cast {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
@@ -316,6 +320,7 @@ theorem drop_eq_rtake (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
   simp only [Fin.cast, coe_addNat, drop, dcast, cast, coe_natAdd, rtake]
   have : n - (n - m) + i.val = i.val + m := by omega
   rw! [this]
+  rfl
 
 /-- Version of `drop_eq_rtake` for uniform tuples `v : Fin n → α` -/
 theorem drop_eq_rtake' {α : Sort*} (m : ℕ) (h : m ≤ n) (v : Fin n → α) :
@@ -329,7 +334,9 @@ same as the original tuple. -/
 theorem take_drop_addCases' (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
     Fin.addCases' (take m h v) (drop m h v) =
       fun i =>
-        cast (by simp [append, addCases, castLE, Fin.cast]; intro hi; rw! [Nat.sub_add_cancel hi])
+        cast (by
+          simp [append, addCases, castLE, Fin.cast]
+          intro hi; rw! [Nat.sub_add_cancel hi]; rfl)
           (v (i.cast (by omega))) := by
   ext i
   simp [addCases', addCases, Fin.cast, castLE, cast]

ArkLib/Data/MvPolynomial/Degrees.lean

@@ -39,10 +39,6 @@ def CEmbedding : R ↪ MvPolynomial σ R := ⟨C, C_injective σ R⟩
 
 section Support
 
-theorem support_C {r : R} [h : Decidable (r = 0)] :
-    (@C R σ _ r).support = if r = 0 then ∅ else { 0 } := by
-  rw [←monomial_zero', support_monomial]
-
 theorem support_C_subset {r : R} : (@C R σ _ r).support ⊆ { 0 } := by
   rw [←monomial_zero']
   exact support_monomial_subset

ArkLib/Data/Probability/Instances.lean

@@ -15,16 +15,17 @@ open NNReal Finset Function
 open scoped BigOperators ProbabilityTheory
 open Real
 
+-- TODO(dtumad): Move most of the stuff in this file to VCV and generalize as possible
+
 section
 variable {α : Type*}
 
 instance [IsEmpty α] : IsEmpty (PMF α) := by
   refine Subtype.isEmpty_of_false ?_
   intro f h
   have : Fintype α := Fintype.ofIsEmpty
-  obtain h' := hasSum_fintype f ; simp at h'
-  have one_eq_zero := HasSum.unique h h'
-  simp_all only [one_ne_zero]
+  have one_eq_zero := HasSum.unique h (hasSum_fintype f)
+  aesop
 
 -- @[simp]
 -- theorem PMF.eq_pure_iff_ge_one {α : Type*} {p : PMF α} {a : α} : p = pure a ↔ p a ≥ 1 := by

ArkLib/OracleReduction/Execution.lean

@@ -128,6 +128,7 @@ private lemma fst_map_simulateQ_loggingOracle_run {ι : Type} {spec : OracleSpec
     simp only [simulateQ_query_bind]
     show Prod.fst <$> (do let u ← liftM (loggingOracle t); simulateQ loggingOracle (oa u)).run =
       liftM (query t) >>= oa
+    stop -- This is broken for now until the refactor of `loggingOracle` and `WriterT`
     simp only [WriterT.run_bind, map_bind, Functor.map_map]
     have key : ∀ (w : QueryLog spec), (fun a_1 => (Prod.map id (w * ·) a_1).1) =
         (Prod.fst : α × QueryLog spec → α) :=

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean

@@ -176,6 +176,7 @@ theorem take_append_left (T : FullTranscript pSpec₁) (T' : FullTranscript pSpe
     FullTranscript.cast, Transcript.cast]
   have : ⟨i.val, by omega⟩ = Fin.castAdd n i := by ext; simp
   rw! (castMode := .all) [this, Fin.happend_left]
+  rfl
 
 @[simp]
 theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pSpec₂) :

ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean

@@ -763,12 +763,9 @@ lemma take_snoc_oracle_eq_oStmtIn (i : Fin ℓ)
       OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)
     (newOracleFn : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :
     (take_snoc_oracle 𝔽q β i oStmtIn newOracleFn) = oStmtIn := by
-  unfold take_snoc_oracle snoc_oracle
-  simp only [eq_mpr_eq_cast, id_eq]
-  if hi: isCommitmentRound ℓ ϑ i then
-    simp only [Fin.is_lt, ↓reduceDIte, Fin.eta]
-  else
-    simp only [Fin.is_lt, ↓reduceDIte, Fin.eta]
+  unfold take_snoc_oracle
+  unfold snoc_oracle
+  simp
 
 /-- Extract the first oracle f^(0) from oracle statements -/
 def getFirstOracle {i : Fin (ℓ + 1)}

ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean

@@ -362,7 +362,7 @@ lemma qMap_total_fiber_repr_coeff (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i
     simp only [qMap_total_fiber, ↓reduceDIte, Nat.add_zero, eq_mp_eq_cast, cast_eq, not_lt_zero',
       tsub_zero, Fin.eta]
   · simp only [qMap_total_fiber, h_steps_eq_0, ↓reduceDIte, Module.Basis.repr_symm_apply,
-    Module.Basis.repr_linearCombination, Finsupp.equivFunOnFinite_symm_apply_toFun]
+    Module.Basis.repr_linearCombination, Finsupp.equivFunOnFinite_symm_apply_apply]
 
 def pointToIterateQuotientIndex (i : Fin (ℓ + 1)) (steps : ℕ) (h_i_add_steps : i.val + steps ≤ ℓ)
     (x : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩)) : Fin (2 ^ steps) := by
@@ -541,7 +541,7 @@ lemma pointToIterateQuotientIndex_qMap_total_fiber_eq_self (i : Fin ℓ) (steps
     · simp only [hsteps, ↓reduceDIte, eqRec_eq_cast, Nat.add_zero, Nat.pow_zero]
       omega
     · simp only [hsteps, ↓reduceDIte, Module.Basis.repr_linearCombination,
-      Finsupp.equivFunOnFinite_symm_apply_toFun, h_j, ite_eq_left_iff, one_ne_zero,
+      Finsupp.equivFunOnFinite_symm_apply_apply, h_j, ite_eq_left_iff, one_ne_zero,
       imp_false, Decidable.not_not]
       -- ⊢ (if j.getBit ↑k = 0 then 0 else 1) = j.getBit ↑k
       have h := Nat.getBit_eq_zero_or_one (k := j) (n := k)

ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean

@@ -127,21 +127,10 @@ def proximityChecksSpec (γ_challenges :
           (v:=v) (i:=⟨i, by exact h_i_lt_ℓ⟩) (steps:=ϑ)
         let f_i_next_val :=
           if hk: k_val < ℓ / ϑ - 1 then
-            let x_next: sDomain 𝔽q β h_ℓ_add_R_rate ⟨i + ϑ, by
-              dsimp only [i]
-              let kfin: Fin (ℓ / ϑ - 1) := ⟨k_val, hk⟩
-              change kfin * ϑ + ϑ < r
-              calc _ ≤ ℓ - ϑ := bIdx_mul_ϑ_add_x_lt_ℓ_sub_ϑ (bIdx:=kfin) (x:=ϑ) (hx:=Nat.le_refl ϑ)
-                _ < ℓ := rounds_sub_steps_lt
-                _ < r := ℓ_lt_r (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
-            ⟩ := next_suffix_of_v
-            oStmt ⟨k_val + 1, by rw [toOutCodewordsCount_last ℓ ϑ]; omega⟩ ⟨x_next, by
-              simp only
-              have h_index: (k_val + 1) * ϑ = i + ϑ := by
-                dsimp only [i]; rw [Nat.add_mul, Nat.one_mul]
-              rw! [h_index]
-              exact Submodule.coe_mem x_next
-            ⟩
+            let x_next : sDomain 𝔽q β h_ℓ_add_R_rate ⟨i + ϑ, by omega⟩ := next_suffix_of_v
+            let ⟨x_next', hx_next'⟩ := x_next
+            oStmt ⟨k_val + 1, by rw [toOutCodewordsCount_last ℓ ϑ]; omega⟩
+              (⟨x_next', by simpa [Nat.add_mul] using hx_next'⟩)
           else final_constant
         c_next = f_i_next_val
       consistency_check

ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean

@@ -491,6 +491,7 @@ noncomputable def commitOracleVerifier (i : Fin ℓ) (hCR : isCommitmentRound 
       simp_rw [hOracleIdx];
       have h := toOutCodewordsCount_mul_ϑ_eq_i_succ ℓ ϑ (i := i) (hCR := hCR)
       rw! [h]
+      rfl
 
 /-- The oracle reduction that is the `i`-th round of Binary commitmentfold. -/
 noncomputable def commitOracleReduction (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) :

ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean

@@ -306,7 +306,7 @@ noncomputable def batchingKnowledgeStateFunction :
       -- ⊢ stmtIn.1.original_claim = (MvPolynomial.aeval stmtIn.1.t_eval_point) ↑witMid.t
       sorry
     | ⟨1, h⟩ => nomatch h
-  toFun_full := fun ⟨stmtLast, oStmtLast⟩ tr witOut h_relOut => by sorry
+  toFun_full := fun ⟨stmtLast, oStmtLast⟩ tr witOut => by sorry
 
 /-! ## Security Properties -/
 

ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean

@@ -312,7 +312,8 @@ def iteratedSumcheckKnowledgeStateFunction (i : Fin ℓ') :
       tauto
     · -- m = 1: dir 1 = V_to_P, contradicts hDir
       simp [pSpecSumcheckRound] at hDir
-  toFun_full := fun ⟨stmtLast, oStmtLast⟩ tr witOut h_relOut => by
+  toFun_full := fun ⟨stmtLast, oStmtLast⟩ tr witOut => by
+    intro h_relOut
     simp at h_relOut
     rcases h_relOut with ⟨stmtOut, ⟨oStmtOut, h_conj⟩⟩
     have h_simulateQ := h_conj.1

ArkLib/ProofSystem/Component/RandomQuery.lean

@@ -171,7 +171,7 @@ def knowledgeStateFunction :
     answer (oracles 0) q = answer (oracles 1) q
   toFun_empty := fun stmt => by simp
   toFun_next | 0 => fun hDir ⟨stmt, oStmt⟩ tr h => by simp_all
-  toFun_full := fun ⟨stmt, oStmt⟩ tr _ h => by
+  toFun_full := fun ⟨stmt, oStmt⟩ tr _ => by
     sorry
     -- simp_all [oracleVerifier, OracleVerifier.toVerifier, Verifier.run]
 

ArkLib/ProofSystem/Component/ReduceClaim.lean

@@ -194,7 +194,8 @@ def oracleKnowledgeStateFunction (hRel : ∀ stmtIn oStmtIn witOut,
   toFun | ⟨0, _⟩ => fun ⟨stmtIn, oStmtIn⟩ _ witIn => ⟨⟨stmtIn, oStmtIn⟩, witIn⟩ ∈ relIn
   toFun_empty := fun stmtIn witIn => by simp
   toFun_next := fun m => Fin.elim0 m
-  toFun_full := fun ⟨stmtIn, oStmtIn⟩ _ witOut h => by
+  toFun_full := fun ⟨stmtIn, oStmtIn⟩ _ witOut => by
+    intro h
     simp_all [Verifier.run, oracleVerifier, OracleVerifier.toVerifier]
     sorry
 

ArkLib/ProofSystem/Fri/Spec/SingleRound.lean

@@ -128,7 +128,9 @@ private lemma sum_add_one {i : Fin (k + 1)} :
               use
                 (by
                   rw [Nat.lt_min]
-                  simp
+                  simp only [zero_lt_one, List.length_drop, List.length_finRange, tsub_pos_iff_lt,
+                    Order.lt_add_one_iff, true_and]
+                  fin_omega
                 )
               rw [List.getElem_drop]
               simp