Skip to content
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.

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

chore: bump lean and mathlib to 4.15.0 #32

Merged
merged 1 commit into from
Jan 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
16 changes: 8 additions & 8 deletions Lampe/Lampe.lean
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ nr_def simple_if<>(x : Field, y : Field) -> Field {
example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y])
fun v => v = y := by
simp only [simple_if]
steps <;> tauto
steps <;> try tauto
. sl
. sl
simp_all
Expand All @@ -91,10 +91,10 @@ example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body
fun v => v = x := by
simp only [simple_if_else]
steps
. simp only [decide_True, exists_const]
. simp only [decide_true, exists_const]
sl
contradiction
. simp_all [decide_True, exists_const]
. simp_all [decide_true, exists_const]

nr_def simple_lambda<>(x : Field, y : Field) -> Field {
let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field };
Expand Down Expand Up @@ -155,7 +155,7 @@ example {p} {arg : Tp.denote p Tp.field} :
sl
tauto
try_impls_all [] simpleTraitEnv
all_goals tauto
all_goals try tauto
simp only
steps
simp_all only [exists_const, SLP.true_star]
Expand Down Expand Up @@ -255,7 +255,7 @@ example : STHoare p ⟨[(add_two_fields.name, add_two_fields.fn)], []⟩ ⟦⟧
. sl
tauto
on_goal 3 => exact add_two_fields.fn
all_goals tauto
all_goals try tauto
on_goal 3 => exact fun v => v = 3
. simp only [add_two_fields]
steps
Expand Down Expand Up @@ -296,7 +296,7 @@ nr_def simple_array<>() -> Field {
example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![])
fun (v : Tp.denote p .field) => v = 2 := by
simp only [simple_array, Expr.mkArray]
steps <;> tauto
steps <;> try tauto
aesop

nr_def tuple_lens<>() -> Field {
Expand Down Expand Up @@ -380,12 +380,12 @@ example : STHoare p ⟨[(simple_func.name, simple_func.fn), (call.name, call.fn)
steps
. apply STHoare.callDecl_intro
sl
all_goals tauto
all_goals try tauto
simp only [call]
steps
. apply STHoare.callDecl_intro
sl
all_goals tauto
all_goals try tauto
simp only [simple_func]
steps
on_goal 2 => exact fun v => v = 10
Expand Down
22 changes: 11 additions & 11 deletions Lampe/Lampe/Builtin/Array.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ lemma Fin.n_is_non_zero {h : Fin n} : n ≠ 0 := by
contradiction
simp

lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h₁ h₂ h₃} :
(Mathlib.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = Mathlib.Vector.get vec ⟨idx + 1, h₃⟩ := by
unfold Mathlib.Vector.get Mathlib.Vector.eraseIdx
lemma List.Vector.get_after_erase {idx : Nat} {vec : List.Vector α n} {h₁ h₂ h₃} :
(List.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = List.Vector.get vec ⟨idx + 1, h₃⟩ := by
unfold List.Vector.get List.Vector.eraseIdx
cases vec
simp_all only [Fin.cast_mk, List.get_eq_getElem]
rename List _ => l
Expand All @@ -41,20 +41,20 @@ lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h
. aesop

@[simp]
lemma Mathlib.Vector.get_after_insert {idx : Nat} {vec : Mathlib.Vector α n} {h} :
(Mathlib.Vector.insertNth v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
unfold Mathlib.Vector.insertNth Mathlib.Vector.get
lemma List.Vector.get_after_insert {idx : Nat} {vec : List.Vector α n} {h} :
(List.Vector.insertIdx v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
unfold List.Vector.insertIdx List.Vector.get
cases vec
simp_all only [List.get_eq_getElem, Fin.coe_cast]
apply List.get_insertNth_self
apply List.get_insertIdx_self
subst_vars
linarith

namespace Lampe.Builtin

@[reducible]
def replaceArray' (arr : Tp.denote p (.array tp n)) (idx : Fin n.toNat) (v : Tp.denote p tp) : Tp.denote p (.array tp n) :=
let arr' := (arr.insertNth v ⟨idx.val + 1, by aesop⟩)
let arr' := (arr.insertIdx v ⟨idx.val + 1, by aesop⟩)
arr'.eraseIdx ⟨idx.val, by cases idx; tauto⟩

example {p} : (replaceArray' (p := p) (n := ⟨3, by aesop⟩) (tp := .bool) ⟨[false, false, false], (by rfl)⟩ ⟨1, by tauto⟩ true).get ⟨1, by tauto⟩ = true := by rfl
Expand All @@ -65,10 +65,10 @@ theorem index_replaced_arr {n : U 32} {idx : Fin n.toNat} {arr} :
unfold replaceArray'
cases em (n.toNat > 0)
. simp_all only [gt_iff_lt, eq_mp_eq_cast]
generalize h₁ : (Mathlib.Vector.insertNth _ _ _) = arr₁
generalize h₁ : (List.Vector.insertIdx _ _ _) = arr₁
cases idx
rw [Mathlib.Vector.get_after_erase, ←h₁]
apply Mathlib.Vector.get_after_insert
rw [List.Vector.get_after_erase, ←h₁]
apply List.Vector.get_after_insert
. simp_all only [gt_iff_lt, not_lt, nonpos_iff_eq_zero, lt_self_iff_false, dite_false]
rename_i h
rw [h] at idx
Expand Down
2 changes: 1 addition & 1 deletion Lampe/Lampe/Builtin/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ lemma HList.toList_length_is_n (h_same : tps = List.replicate n tp) :
rfl

@[reducible]
def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : Mathlib.Vector (rep tp) n :=
def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : List.Vector (rep tp) n :=
⟨HList.toList l h_same, by apply HList.toList_length_is_n⟩

@[reducible]
Expand Down
2 changes: 1 addition & 1 deletion Lampe/Lampe/Builtin/BigInt.lean
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ Converts a list `l` to a vector of size `n`s.
- If `n < l.length`, then the output is truncated from the end.
- If `n > l.length`, then the higher indices are populated with `zero`.
-/
def listToVec (l : List α) (zero : α) : Mathlib.Vector α n :=
def listToVec (l : List α) (zero : α) : List.Vector α n :=
⟨l.takeD n zero, List.takeD_length _ _ _⟩

/--
Expand Down
1 change: 1 addition & 0 deletions Lampe/Lampe/Builtin/Helpers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ namespace Lampe
def extList (lst : List α) (len : Nat) (default : α) : List α
:= lst ++ (List.replicate (len - lst.length) default)

@[reducible]
def decomposeToRadix (r : Nat) (v : Nat) (h : r > 1) : List Nat := match v with
| .zero => List.nil
| v' + 1 => List.cons ((v' + 1) % r) (decomposeToRadix r ((v' + 1) / r) h)
Expand Down
18 changes: 9 additions & 9 deletions Lampe/Lampe/Builtin/Lens.lean
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,12 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
unfold omni_frame
intros
cases_type readLensOmni
. constructor <;> tauto
rw [Finmap.lookup_union_left] <;> tauto
. constructor <;> try tauto
rw [Finmap.lookup_union_left] <;> try tauto
apply Finmap.mem_of_lookup_eq_some <;> tauto
repeat apply Exists.intro <;> tauto
. apply readLensOmni.err <;> tauto
rw [Finmap.lookup_union_left] <;> tauto
. apply readLensOmni.err <;> try tauto
rw [Finmap.lookup_union_left] <;> try tauto
apply Finmap.mem_of_lookup_eq_some <;> tauto
}

Expand Down Expand Up @@ -69,7 +69,7 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
rename_i p st₁ st₂ hd outTp args Q _ hd
cases_type modifyLensOmni
. constructor
rw [Finmap.lookup_union_left] <;> tauto
rw [Finmap.lookup_union_left] <;> try tauto
apply Finmap.mem_of_lookup_eq_some <;> tauto
tauto
simp only
Expand All @@ -82,14 +82,14 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
rw [←hst]
apply And.intro
. rw [←Finmap.insert_eq_singleton_union]
apply Finmap.insert_mem_disjoint <;> tauto
apply Finmap.insert_mem_disjoint <;> try tauto
apply Finmap.mem_of_lookup_eq_some <;> tauto
. apply And.intro
. simp [Finmap.union_assoc, Finmap.insert_eq_singleton_union]
. apply And.intro ?_ (by rfl)
simp_all [Finmap.insert_union, Finmap.insert_eq_singleton_union]
. apply modifyLensOmni.err <;> tauto
rw [Finmap.lookup_union_left] <;> tauto
. apply modifyLensOmni.err <;> try tauto
rw [Finmap.lookup_union_left] <;> try tauto
apply Finmap.mem_of_lookup_eq_some <;> tauto
}

Expand All @@ -115,7 +115,7 @@ def getLens (lens : Lens rep tp₁ tp₂) : Builtin := {
unfold omni_frame
intros
cases_type getLensOmni
. constructor <;> tauto
. constructor <;> try tauto
repeat apply Exists.intro <;> tauto
. apply getLensOmni.err <;> tauto
}
Expand Down
8 changes: 4 additions & 4 deletions Lampe/Lampe/Builtin/Slice.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,17 @@ namespace Lampe.Builtin

@[reducible]
def replaceSlice' (s : Tp.denote p $ .slice tp) (i : Fin s.length) (v : Tp.denote p tp) : Tp.denote p $ .slice tp :=
List.modifyNth (fun _ => v) i s
List.modify (fun _ => v) i s

@[simp]
theorem replaceSlice_length_eq_length :
(replaceSlice' s i v).length = s.length := by
simp_all [List.length_modifyNth]
simp_all [List.length_modify]

@[simp]
theorem index_replaced_slice :
(replaceSlice' s idx v).get ⟨idx.val, h⟩ = v := by
simp_all [List.modifyNth_eq_set_get?, List.getElem_eq_iff]
simp_all [List.modify_eq_set_get?, List.getElem_eq_iff]

/--
Defines the builtin slice constructor.
Expand Down Expand Up @@ -85,7 +85,7 @@ In Noir, this builtin corresponds to `fn insert(self, index: u32, elem: T) -> Se
def sliceInsert := newGenericPureBuiltin
(fun tp => ⟨[.slice tp, .u 32, tp], .slice tp⟩)
(fun _ h![l, i, e] => ⟨i.toNat < l.length,
fun _ => l.insertNth i.toNat e⟩)
fun _ => l.insertIdx i.toNat e⟩)


/--
Expand Down
Loading
Loading