update to 4.7.0-rc2

Author: kovach

Etch/StreamFusion/Examples/Basic.lean

@@ -43,14 +43,10 @@ def d2 : ℕ :=
 
 -- With stream combinators
 example : ℕ := eval $ Σ i => (f $[i] predicate(i) * locations(i)) * counts(i)
+
 --example : ℕ := eval $ Σ i => predicate(i) * (f $[i] locations(i)) * counts(i)
 def d3 : ℕ := eval $ Σ i => (f $[i] predicate(i) * (ArraySet.toSeqStream locations)(i)) * counts(i)
 
---def d2 : ℕ :=
---  (locations.filter predicate).foldl
---    (init := 0) (fun result key =>
---    result + counts.findD (f key) 0)
-
 #eval d1
   (locations := #["Hi", "There"])
   (HashMap.ofList [("HI", 10), ("THERE", 3)])

Etch/StreamFusion/Proofs/Imap.lean

@@ -54,8 +54,7 @@ theorem IsLawful.imap {s : Stream ι α} [AddZeroClass α] [IsLawful s] {f : ι
   rintro q ⟨j₁, b⟩ j₂ hj
   dsimp only [imap_general_seek, imap_general_σ, imap_general_valid]
   dsimp at q
-  suffices : ∀ i, f i = j₂ → s.eval (s.seek q (g (s.index q) j₁, b)) i = s.eval q i
-  · sorry
+  suffices ∀ i, f i = j₂ → s.eval (s.seek q (g (s.index q) j₁, b)) i = s.eval q i by sorry
   rintro i rfl
   by_cases le : s.index q ≤ i
   · apply ‹IsLawful s›.seek_spec
@@ -68,6 +67,4 @@ theorem IsLawful.imap {s : Stream ι α} [AddZeroClass α] [IsLawful s] {f : ι
     · refine lt_of_lt_of_le ?_ (s.mono q _)
       simpa using le
 
-
-
 end Etch.Verification.Stream

Etch/StreamFusion/Proofs/StreamProof.lean

@@ -1,4 +1,5 @@
 import Mathlib.Tactic.Linarith
+import Mathlib.Order.Basic
 
 import Etch.StreamFusion.Stream
 import Etch.Verification.FinsuppLemmas
@@ -261,7 +262,7 @@ noncomputable def Stream.eval [AddZeroClass α] (s : Stream ι α) [IsBounded s]
       have : (s.advance q) ≺ q := s.next_wf ⟨q, h⟩
       s.eval₀ ⟨q, h⟩ + s.eval (s.advance q)
     else 0
-termination_by _ x => s.wf.wrap x
+termination_by x => s.wf.wrap x
 
 @[simp] lemma Stream.eval_zero [AddZeroClass α] : (0 : Stream ι α).eval = 0 := by
   ext; rw [Stream.eval]; simp
@@ -283,10 +284,10 @@ end well_founded
           let acc' := if hr : hr then f acc i (value q hv hr) else acc
           go f valid ready index value next h acc' q'
         else acc
+    termination_by s.wf.wrap q
+    decreasing_by exact h q hv
   go f s.valid (fun q h => s.ready ⟨q,h⟩) (fun q h => s.index ⟨q,h⟩) (fun q v r => s.value ⟨⟨q,v⟩,r⟩) s.next
     (fun q hv => s.progress rfl.le) acc q
-termination_by _ => s.wf.wrap q
-decreasing_by exact h q hv
 
 theorem Stream.fold_wf_spec [Preorder ι] (f : β → ι → α → β) (s : Stream ι α) [IsBounded s]
     (q : {q // s.valid q}) (acc : β) :
@@ -446,6 +447,10 @@ theorem Stream.IsStrictMono.eval_seek_eq_zero [AddZeroClass α] {s : Stream ι 
     refine lt_of_lt_of_le ?_ (hs.1 _ _)
     simpa using fst_lt_of_lt_of_lt h₁ h₂
 
+-- not sure why these are needed now
+instance instDecidableLT (x y : ι × Bool) [Decidable (x.1 < y.1)] [Decidable (x.2 < y.2)] : Decidable (x < y) := And.decidable
+instance (x y : ι × Bool) [Decidable (x.1 < y.1)] [Decidable (x.2 < y.2)] : Decidable (x <ₗ y) := inferInstance
+
 theorem Stream.IsStrictMono.eval₀_eq_eval_filter [AddCommMonoid α] {s : Stream ι α} [IsBounded s]
     (hs : s.IsStrictMono) (q : {q // s.valid q}) :
     s.eval₀ q = (s.eval q).filter fun i => (i, false) <ₗ s.toOrder q := by

Etch/Util/ExpressionTree.lean

@@ -1,6 +1,5 @@
 import Lean
 import Std.Lean.Expr
-import Std.Data.Option.Basic
 import Etch.Util.Labels
 
 open Lean Elab Term Meta

Etch/Util/Labels.lean

@@ -52,7 +52,7 @@ def LabelIdx.compareAux (x y : Nat) : Ordering :=
     | .eq => compareAux (x / 2) (y / 2)
     | .lt => .lt
     | .gt => .gt
-termination_by _ x y => x + y
+termination_by x + y
 
 instance : Ord LabelIdx := ⟨fun x y => LabelIdx.compareAux x.data y.data⟩
 instance : LT LabelIdx := ⟨fun x y => compare x y == .lt⟩
@@ -81,7 +81,7 @@ def LabelIdx.freshBeforeAux (x y : Nat) : Nat :=
       2 * freshAfterAux (xb / 2)
     else
       panic! "x < y not true in freshBeforeAux"
-termination_by _ x y => y
+termination_by y
 
 /-- Gives a label that is between `x` and `y`, assuming that `x < y`. -/
 def LabelIdx.freshBefore (x y : LabelIdx) : LabelIdx :=

Etch/Verification/FinsuppLemmas.lean

@@ -1,5 +1,6 @@
 import Mathlib.Data.Finsupp.Basic
 import Mathlib.Data.Finsupp.Indicator
+import Mathlib.Data.Finsupp.Notation
 
 variable {α β γ : Type _} [AddCommMonoid β]
 

Etch/Verification/Misc.lean

@@ -7,7 +7,6 @@ import Mathlib.Data.List.FinRange
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.PFun
 import Mathlib.Data.Prod.Lex
-import Mathlib.Init.IteSimp
 
 /-!
 This is a collection of miscellaneous lemmas. Not all of these are used;
@@ -328,19 +327,21 @@ theorem Finsupp.mul_single_eq_zero {ι β : Type _} [MulZeroClass β] (i₁ i₂
   exact hi
 #align finsupp.mul_single_eq_zero Finsupp.mul_single_eq_zero
 
-theorem Finsupp.mul_filter {ι β : Type _} [MulZeroClass β] (P Q : ι → Prop) (f g : ι →₀ β) :
+variable {ι : Type _} (P Q : ι → Prop) [DecidablePred P] [DecidablePred Q]
+
+theorem Finsupp.mul_filter {β : Type _} [MulZeroClass β] (f g : ι →₀ β) :
     f.filter P * g.filter Q = (f * g).filter fun i => P i ∧ Q i := by
   ext i
   by_cases h₁ : P i <;> by_cases h₂ : Q i <;> simp [h₁, h₂]
 #align finsupp.mul_filter Finsupp.mul_filter
 
-theorem Finsupp.mul_filter' {ι β : Type _} [MulZeroClass β] (P : ι → Prop) (f g : ι →₀ β) :
+theorem Finsupp.mul_filter' {β : Type _} [MulZeroClass β] (f g : ι →₀ β) :
     (f * g).filter P = f.filter P * g.filter P := by simp [Finsupp.mul_filter]
 #align finsupp.mul_filter' Finsupp.mul_filter'
 
-theorem Finsupp.filter_ext_iff {ι β : Type _} [AddZeroClass β] (P : ι → Prop) (f g : ι →₀ β) :
+theorem Finsupp.filter_ext_iff {β : Type _} [AddZeroClass β] (f g : ι →₀ β) :
     f.filter P = g.filter P ↔ ∀ a, P a → f a = g a := by classical
-  simp [FunLike.ext_iff, Finsupp.filter_apply, apply_ite₂ (· = ·), ← imp_iff_not_or]
+  simp [DFunLike.ext_iff, Finsupp.filter_apply, apply_ite₂ (· = ·), ← imp_iff_not_or]
 #align finsupp.filter_ext_iff Finsupp.filter_ext_iff
 
 theorem mul_eq_zero_of {α : Type _} [MulZeroClass α] {x y : α} : x = 0 ∨ y = 0 → x * y = 0

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "c1a3cdf748424810985b479d2712998921c7c797",
+   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "6f42d2822aba47eb690ed98c508a23e6f0becce2",
+   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4/",
    "type": "git",
    "subDir": null,
-   "rev": "702f3fe16c773ae1e34fbf179342d0877f8cb4f1",
+   "rev": "35909eaa5b71d0bd5a6e259b5cc9732132d977c7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "702f3fe16c773ae1e34fbf179342d0877f8cb4f1",
+   "inputRev": "35909eaa5b71d0bd5a6e259b5cc9732132d977c7",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "etch",

lakefile.lean

@@ -51,4 +51,4 @@ lean_exe seq {
 lean_lib Etch.Verification.Semantics.Example
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4/"@"702f3fe16c773ae1e34fbf179342d0877f8cb4f1"
+  "https://github.com/leanprover-community/mathlib4/"@"35909eaa5b71d0bd5a6e259b5cc9732132d977c7"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.7.0-rc2