Skip to content

Update Lean to v4.33.0-rc2 #34

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
abentkamp wants to merge 2 commits into
base: dev
Choose a base branch
from
Draft

Update Lean to v4.33.0-rc2 #34

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
95048d6
Update Lean to v4.33.0-rc2
abentkamp Aug 4, 2026
48f6fb4
Fix `lake build --iofail` under Lean v4.33
abentkamp Aug 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 3 additions & 7 deletions backends/lean/Aeneas/Data/Array.lean
View file
Open in desktop

@clementblaudeau clementblaudeau Aug 4, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could be upstreamed regardless of the lean version bump right ?

Original file line number Diff line number Diff line change
Expand Up @@ -108,13 +108,9 @@ theorem getElem_set! {α : Type u}
simp only [set!_eq_setIfInBounds, ← getElem_toList, toList_setIfInBounds]
simp_lists

@[simp, simp_lists_safe]
theorem getElem!_set!_ne {α : Type u}
[Inhabited α] {i j : ℕ} {x : α} {xs : Array α}
(h : i ≠ j) :
(xs.set! i x)[j]! = xs[j]! := by
simp only [set!_eq_setIfInBounds, ← getElem!_toList, toList_setIfInBounds]
simp_lists
-- `Array.getElem!_set!_ne` is now provided by the core library; just register the
-- Aeneas simp attributes on it.
attribute [simp, simp_lists_safe] _root_.Array.getElem!_set!_ne

@[simp, simp_lists_safe]
theorem getElem_set!_ne {α : Type u}
Expand Down
23 changes: 6 additions & 17 deletions backends/lean/Aeneas/Data/Vector.lean
View file
Open in desktop

@clementblaudeau clementblaudeau Aug 4, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same for this one

Original file line number Diff line number Diff line change
Expand Up @@ -108,16 +108,9 @@ theorem getElem!_set! {α : Type u}
← Array.getElem!_toList, Array.toList_setIfInBounds]
simp_lists

@[simp, simp_lists_safe]
theorem getElem_set! {α : Type u}
[Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
(hi : i < n ∧ j = i) :
(xs.set! i x)[j] = x := by
have : i < xs.toArray.size := by scalar_tac
simp only [getElem_eq_toArray_getElem, toArray_set!, Array.set!_eq_setIfInBounds,
Array.size_setIfInBounds, size_toArray, Array.Inhabited_getElem_eq_getElem!,
← Array.getElem!_toList, Array.toList_setIfInBounds, hi]
grind
-- `Vector.getElem_set!_self` is now provided by the core library; register the
-- Aeneas simp attribute on it.
attribute [simp_lists_safe] getElem_set!_self

@[simp, simp_lists_safe]
theorem getElem!_set!_ne {α : Type u}
Expand All @@ -127,13 +120,9 @@ theorem getElem!_set!_ne {α : Type u}
simp only [getElem!_eq_toArray_getElem!, toArray_set!]
simp_lists

@[simp, simp_lists_safe]
theorem getElem_set!_ne {α : Type u}
[Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
(h : i ≠ j ∧ j < n) :
(xs.set! i x)[j] = xs[j] := by
simp only [getElem_eq_toArray_getElem, toArray_set!]
simp_lists
-- `Vector.getElem_set!_ne` is now provided by the core library; register the
-- Aeneas simp attribute on it.
attribute [simp_lists_safe] getElem_set!_ne

@[simp, simp_lists_safe]
theorem getElem!_replicate {α : Type u} [Inhabited α] {i n : ℕ} {a : α} (h : i < n) :
Expand Down
33 changes: 22 additions & 11 deletions backends/lean/Aeneas/Do/Tests.lean
View file
Open in desktop

@clementblaudeau clementblaudeau Aug 4, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are those specific to the lean bump ? They seem like reasonable changes anyway

Original file line number Diff line number Diff line change
Expand Up @@ -625,13 +625,15 @@ def do_match_cross_arm_used (t : Two) : Result Nat := do

/-- warning: Variable name `n` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _n

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `n` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _n

Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
#guard_msgs in
Expand All @@ -647,7 +649,8 @@ def do_let_arrow_id_used : Result Nat := do

/-- warning: Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _x

Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
#guard_msgs in
Expand All @@ -668,25 +671,29 @@ def do_let_arrow_pat_used : Result Nat := do
/--
warning: Variable name `a` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `b` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `c` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `d` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-/
Expand All @@ -699,25 +706,29 @@ def do_let_arrow_pat_unused : Result Nat := do
/--
warning: Variable name `a` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `b` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `c` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _c

Note: This linter can be disabled with `set_option linter.unusedVariables false`
---
warning: Variable name `d` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _d

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-/
Expand Down
53 changes: 33 additions & 20 deletions backends/lean/Aeneas/Std/Array/Array.lean
View file
Open in desktop

@clementblaudeau clementblaudeau Aug 4, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Proof changes like those seem fine to me.

Original file line number Diff line number Diff line change
Expand Up @@ -225,6 +225,7 @@ theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (
:= by
simp only [partialSpec, update, set]
cases hopt : v[i]? <;> simp_all
rfl

def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
Result (α × (α -> Array α n)) := do
Expand All @@ -244,8 +245,8 @@ theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i:
@[simp]
theorem Array.set_getElem!_eq {α} {n : Usize} [Inhabited α] (x : Array α n) (i : Usize) :
x.set i (x.val[i.val]!) = x := by
have := @List.set_getElem_self _ x.val i.val
simp only [Array, Subtype.ext_iff, set_val_eq, List.set_getElem!]
apply Subtype.ext
simp only [set_val_eq, List.set_getElem!]

@[simp]
theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h : i.val < x.length) :
Expand All @@ -254,15 +255,14 @@ theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h :
simpa using h
have hself : x.val.set i.val x.val[i.val] = x.val :=
List.set_getElem_self (as := x.val) (i := i.val) (h := h')
simp only [Array, Subtype.ext_iff, set_val_eq] at hself ⊢
apply Subtype.ext
simp only [set_val_eq]
exact hself

@[simp↓, simp_lists_safe↓]
theorem Array.getElem_set_eq {α} {n : Usize} (v : Array α n) (i : Usize) (x : α) (h : i.val < (v.set i x).length) :
(v.set i x)[i]'h = x := by
cases v
unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
simp only [List.getElem_set_self]
simp only [Array.getElem_Usize_eq, Array.set_val_eq, List.getElem_set_self]

@[simp↓, simp_lists_safe↓]
theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α) (h : j.val < (v.set i x).length)
Expand All @@ -274,9 +274,8 @@ theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x
theorem Array.getElem_set_neq {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α)
(h : j.val < (v.set i x).length) (h' : i ≠ j) :
(v.set i x)[j]'h = v[j] := by
cases v
unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
simp only [ne_eq, UScalar.neq_to_neq_val] at *
simp only [ne_eq, UScalar.neq_to_neq_val] at h'
simp only [Array.getElem_Usize_eq, Array.set_val_eq]
simp_lists [List.getElem_set_ne]

/-- Small helper (this function doesn't model a specific Rust function) -/
Expand All @@ -289,13 +288,19 @@ theorem Array.clone_length {α : Type u} {n : Usize} (clone : α → Result α)
simp [Array.clone] at h
simp [List.clone] at h
split at h <;> simp_all
rename_i heq
have := List.mapM_Result_length heq
cases s'; simp_all
cases h; simp_all

@[step]
theorem Array.clone_spec {α : Type u} {n : Usize} {clone : α → Result α} {s : Array α n} (h : ∀ x ∈ s.val, clone x = ok x) :
Array.clone clone s ⦃ s' => s' = s ⦄ := by
simp only [Array.clone]
have ⟨ l', h ⟩ := spec_imp_exists (List.clone_spec h)
simp [h]
simp only [h.1, bind_tc_ok]
apply (spec_ok _).mpr
exact Subtype.ext h.2.1

@[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone"]
def core.array.CloneArray.clone
Expand All @@ -307,8 +312,9 @@ theorem core.array.CloneArray.clone_spec {T : Type} {N : Usize} (cloneInst : cor
(h : ∀ x ∈ a.val, cloneInst.clone x = ok x) :
core.array.CloneArray.clone cloneInst a ⦃ a' => a = a' ⦄:= by
unfold clone
have := spec_imp_exists (Array.clone_spec h)
grind
have ⟨a', h'⟩ := spec_imp_exists (Array.clone_spec h)
rw [h'.1]
exact (spec_ok _).mpr h'.2.symm

@[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone_from"]
def core.array.CloneArray.clone_from {T : Type} {N : Usize} (cloneInst : core.clone.Clone T)
Expand All @@ -320,8 +326,9 @@ theorem core.array.CloneArray.clone_from_spec {T : Type} {N : Usize} (cloneInst
(self source : Array T N) (h : ∀ x ∈ source.val, cloneInst.clone x = ok x) :
core.array.CloneArray.clone_from cloneInst self source ⦃ source' => source = source' ⦄ := by
unfold clone_from
have := spec_imp_exists (Array.clone_spec h)
grind
have ⟨source', h'⟩ := spec_imp_exists (Array.clone_spec h)
rw [h'.1]
exact (spec_ok _).mpr h'.2.symm

@[reducible, rust_trait_impl "core::clone::Clone<[@T; @N]>"]
def core.clone.CloneArray {T : Type} (N : Usize)
Expand All @@ -337,7 +344,8 @@ def Array.setSlice! {α : Type u} {n} (s : Array α n) (i : ℕ) (s' : List α)
theorem Array.setSlice!_getElem!_prefix {α} {n} [Inhabited α]
(s : Array α n) (s' : List α) (i j : ℕ) (h : j < i) :
(s.setSlice! i s')[j]! = s[j]! := by
simp only [Array.setSlice!, Array.getElem!_Nat_eq]
simp only [Array.getElem!_Nat_eq]
simp only [Array.setSlice!]
simp_lists

@[simp_lists_safe]
Expand All @@ -346,7 +354,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
(s.setSlice! i s')[j] = s[j] := by
have hj' : j < (s.setSlice! i s').length := by scalar_tac
have h1 : (s.setSlice! i s')[j]? = s[j]? := by
simp only [Array.getElem?_Nat_eq, Array.setSlice!]
simp only [Array.getElem?_Nat_eq]
simp only [Array.setSlice!]
simp_lists [List.setSlice!_getElem?_prefix]
simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
Option.some.injEq] at h1
Expand All @@ -356,7 +365,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
theorem Array.setSlice!_getElem!_middle {α} {n} [Inhabited α]
(s : Array α n) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
(s.setSlice! i s')[j]! = s'[j - i]! := by
simp only [Array.setSlice!, Array.getElem!_Nat_eq]
simp only [Array.getElem!_Nat_eq]
simp only [Array.setSlice!]
simp_lists

@[simp_lists_safe]
Expand All @@ -367,7 +377,8 @@ theorem Array.setSlice!_getElem_middle {α} {n}
scalar_tac
have hji : j - i < s'.length := h.2.1
have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
simp only [Array.getElem?_Nat_eq, Array.setSlice!]
simp only [Array.getElem?_Nat_eq]
simp only [Array.setSlice!]
simp_lists [List.setSlice!_getElem?_middle]
simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji,
Option.some.injEq] at h1
Expand All @@ -376,15 +387,17 @@ theorem Array.setSlice!_getElem_middle {α} {n}
theorem Array.setSlice!_getElem!_suffix {α} {n} [Inhabited α]
(s : Array α n) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
(s.setSlice! i s')[j]! = s[j]! := by
simp only [Array.setSlice!, Array.getElem!_Nat_eq]
simp only [Array.getElem!_Nat_eq]
simp only [Array.setSlice!]
simp_lists

theorem Array.setSlice!_getElem_suffix {α} {n}
(s : Array α n) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j ∧ j < s.length) :
(s.setSlice! i s')[j] = s[j] := by
have hj' : j < (s.setSlice! i s').length := by scalar_tac
have h1 : (s.setSlice! i s')[j]? = s[j]? := by
simp only [Array.getElem?_Nat_eq, Array.setSlice!]
simp only [Array.getElem?_Nat_eq]
simp only [Array.setSlice!]
simp_lists [List.setSlice!_getElem?_suffix]
simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
Option.some.injEq] at h1
Expand Down
Loading
Loading