From b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:04:13 +0200
Subject: Update Lean to v4.9.0-rc1
---
backends/lean/Base/Arith/Base.lean | 11 +--
backends/lean/Base/Arith/Int.lean | 8 +-
backends/lean/Base/Arith/Scalar.lean | 2 +
backends/lean/Base/Diverge/Base.lean | 21 +++--
backends/lean/Base/Diverge/Elab.lean | 129 ++++++++++++++++----------
backends/lean/Base/Extensions.lean | 1 -
backends/lean/Base/IList/IList.lean | 12 +--
backends/lean/Base/Primitives/ArraySlice.lean | 3 +-
backends/lean/Base/Primitives/Scalar.lean | 24 ++---
backends/lean/Base/Primitives/Vec.lean | 3 +-
backends/lean/Base/Progress/Base.lean | 3 +-
backends/lean/Base/Progress/Progress.lean | 11 +--
backends/lean/Base/Utils.lean | 55 ++++++-----
backends/lean/lake-manifest.json | 26 +++---
backends/lean/lean-toolchain | 2 +-
15 files changed, 172 insertions(+), 139 deletions(-)
(limited to 'backends/lean')
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index 8ada4171..fb6b12e5 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -1,6 +1,5 @@
import Lean
-import Std.Data.Int.Lemmas
-import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Linarith -- Introduces a lot of useful lemmas
namespace Arith
@@ -21,12 +20,12 @@ theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by
have hne : x - y ≠ 0 := by
simp
intro h
- have: x = y := by linarith
+ have: x = y := by omega
simp_all
have h := ne_zero_is_lt_or_gt hne
match h with
- | .inl _ => left; linarith
- | .inr _ => right; linarith
+ | .inl _ => left; omega
+ | .inr _ => right; omega
-- TODO: move?
theorem add_one_le_iff_le_ne (n m : Nat) (h1 : m ≤ n) (h2 : m ≠ n) : m + 1 ≤ n := by
@@ -66,7 +65,7 @@ theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
(h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) :
↑(x.toNat - x') < y := by
- have : 0 ≤ x := by linarith
+ have : 0 ≤ x := by omega
simp [Int.toNat_sub_of_le, *]
end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 6d27a35e..1d3e82be 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -180,7 +180,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
-- Add a declaration
let nval ← Utils.addDeclTac name e type (asLet := false)
-- Simplify to unfold the declaration to unfold (i.e., the projector)
- Utils.simpAt true {} [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
+ Utils.simpAt true {} #[] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
-- Return the new value
pure nval
@@ -214,7 +214,7 @@ def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM U
extraPreprocess
-- Reduce all the terms in the goal - note that the extra preprocessing step
-- might have proven the goal, hence the `Tactic.allGoals`
- Tactic.allGoals do tryTac (dsimpAt false {} [] [] [] Tactic.Location.wildcard)
+ Tactic.allGoals do tryTac (dsimpAt false {} #[] [] [] [] Tactic.Location.wildcard)
elab "int_tac_preprocess" : tactic =>
intTacPreprocess (do pure ())
@@ -231,10 +231,10 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess : Tactic
-- the goal. I think before leads to a smaller proof term?
Tactic.allGoals (intTacPreprocess extraPreprocess)
-- More preprocessing
- Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} [] [``nat_zero_eq_int_zero] [] .wildcard))
+ Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} #[] [] [``nat_zero_eq_int_zero] [] .wildcard))
-- Split the conjunctions in the goal
if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
- -- Call linarith
+ -- Call omega
Tactic.allGoals do
try do Tactic.Omega.omegaTactic {}
catch _ =>
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 8793713b..ecc5acaf 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -18,6 +18,8 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-- Reveal the concrete bounds, simplify calls to [ofInt]
Utils.simpAt true {}
+ -- Simprocs
+ #[]
-- Unfoldings
[``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 0f20125f..aab4db8f 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,7 +1,6 @@
import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
-import Mathlib.Tactic.Linarith
import Base.Primitives.Base
import Base.Arith.Base
import Base.Diverge.ElabBase
@@ -36,20 +35,19 @@ namespace Lemmas
revert m
induction k -- TODO: induction h rather?
case zero =>
- simp_all
intro m h1 h2
have h: n = m := by omega
unfold for_all_fin_aux; simp_all
simp_all
-- There is no i s.t. m ≤ i
intro i h3; cases i; simp_all
- linarith
+ omega
case succ k hi =>
intro m hk hmn
intro hf i hmi
have hne: m ≠ n := by
have hineq := Nat.lt_of_sub_eq_succ hk
- linarith
+ omega
-- m = i?
if heq: m = i then
-- Yes: simply use the `for_all_fin_aux` hyp
@@ -64,7 +62,7 @@ namespace Lemmas
have heq1: n - (m + 1) = k := by
-- TODO: very annoying arithmetic proof
simp [Nat.sub_eq_iff_eq_add hineq]
- have hineq1: m ≤ n := by linarith
+ have hineq1: m ≤ n := by omega
simp [Nat.sub_eq_iff_eq_add hineq1] at hk
simp_arith [hk]
have hi := hi (m + 1) heq1 hineq
@@ -199,7 +197,7 @@ namespace Fix
| 0 =>
exfalso
zify at *
- linarith
+ omega
| Nat.succ m1 =>
simp_arith at Hle
simp [fix_fuel]
@@ -407,7 +405,7 @@ namespace Fix
. simp at Hl
-- Make a case disjunction on `h y (fix_fuel m k)`: if it is not equal
-- to div, use the monotonicity of `h y`
- have Hle : m ≤ n := by linarith
+ have Hle : m ≤ n := by omega
have Hffmono := fix_fuel_mono Hkmono Hle
have Hmono := Hhmono y Hffmono
simp [result_rel] at Hmono
@@ -568,6 +566,7 @@ namespace FixI
have Heq := Fix.is_valid_fix_fixed_eq Hvalid'
simp [fix]
conv => lhs; rw [Heq]
+ rfl
/- Some utilities to define the mutually recursive functions -/
@@ -778,6 +777,7 @@ namespace FixII
have Heq := Fix.is_valid_fix_fixed_eq Hvalid'
simp [fix]
conv => lhs; rw [Heq]
+ rfl
/- Some utilities to define the mutually recursive functions -/
@@ -966,6 +966,7 @@ namespace Ex1
have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
simp [list_nth]
conv => lhs; rw [Heq]
+ rfl
end Ex1
@@ -1011,6 +1012,7 @@ namespace Ex2
have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
simp [list_nth]
conv => lhs; rw [Heq]
+ rfl
end Ex2
@@ -1183,6 +1185,7 @@ namespace Ex4
.ok b) := by
simp [is_even, is_odd];
conv => lhs; rw [body_fix_eq]
+ rfl
theorem is_odd_eq (i : Int) : is_odd i =
(if i = 0
@@ -1192,6 +1195,7 @@ namespace Ex4
.ok b) := by
simp [is_even, is_odd];
conv => lhs; rw [body_fix_eq]
+ rfl
end Ex4
namespace Ex5
@@ -1263,6 +1267,7 @@ namespace Ex5
have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a)
simp [id]
conv => lhs; rw [Heq]; simp; rw [id_body]
+ rfl
end Ex5
@@ -1336,6 +1341,7 @@ namespace Ex6
have Heq := is_valid_fix_fixed_eq body_is_valid
simp [list_nth]
conv => lhs; rw [Heq]
+ rfl
-- Write the proof term explicitly: the generation of the proof term (without tactics)
-- is automatable, and the proof term is actually a lot simpler and smaller when we
@@ -1429,6 +1435,7 @@ namespace Ex7
have Heq := is_valid_fix_fixed_eq body_is_valid
simp [list_nth]
conv => lhs; rw [Heq]
+ rfl
-- Write the proof term explicitly: the generation of the proof term (without tactics)
-- is automatable, and the proof term is actually a lot simpler and smaller when we
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 5db8ffed..60955051 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -22,6 +22,10 @@ def normalize_let_bindings := true
open WF in
+-- Small utility - it seems that `Name.append` doesn't do what we want
+def appendToName (n : Name) (s : String) : Name :=
+ Name.str n s
+
-- TODO: use those
def UnitType := Expr.const ``PUnit [Level.succ .zero]
def UnitValue := Expr.const ``PUnit.unit [Level.succ .zero]
@@ -548,7 +552,7 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr)
-- Add the declaration
let value ← mkLambdaFVars #[kk_var] body
trace[Diverge.def.genBody] "Body after abstracting kk: {value}"
- let name := preDef.declName.append "body"
+ let name := appendToName preDef.declName "body"
let levelParams := grLvlParams
let decl := Declaration.defnDecl {
name := name
@@ -603,7 +607,7 @@ def mkDeclareMutRecBody (grName : Name) (grLvlParams : List Name)
let body ← mkLambdaFVars #[kk_var, i_var] body
trace[Diverge.def] "mkDeclareMutRecBody: body: {body}"
-- Add the declaration
- let name := grName.append "mut_rec_body"
+ let name := appendToName grName "mut_rec_body"
let levelParams := grLvlParams
let decl := Declaration.defnDecl {
name := name
@@ -1047,7 +1051,7 @@ partial def proveSingleBodyIsValid
mkForallFVars #[k_var, t_var, x_var] ty
trace[Diverge.def.valid] "proveSingleBodyIsValid: thmTy\n{thmTy}:\n{← inferType thmTy}"
-- Save the theorem
- let name := preDef.declName ++ "body_is_valid"
+ let name := appendToName preDef.declName "body_is_valid"
let decl := Declaration.thmDecl {
name
levelParams := preDef.levelParams
@@ -1107,7 +1111,7 @@ def proveMutRecIsValid
trace[Diverge.def.valid] "Generated the term: {isValid}"
-- Save the theorem
let thmTy ← mkAppM ``FixII.is_valid #[mutRecBodyConst]
- let name := grName ++ "mut_rec_body_is_valid"
+ let name := appendToName grName "mut_rec_body_is_valid"
let decl := Declaration.thmDecl {
name
levelParams := grLvlParams
@@ -1196,7 +1200,7 @@ partial def proveUnfoldingThms (isValidThm : Expr)
let proof ← mkLambdaFVars xs proof
trace[Diverge.def.unfold] "proveUnfoldingThms: proof: {proof}:\n{← inferType proof}"
-- Declare the theorem
- let name := preDef.declName ++ "unfold"
+ let name := appendToName preDef.declName "unfold"
let decl := Declaration.thmDecl {
name
levelParams := preDef.levelParams
@@ -1282,7 +1286,7 @@ def divRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
-- Add an auxiliary definition for `param_in_out_ty` (this is a potentially big term)
let param_in_out_ty ← do
let value ← mkLambdaFVars #[i_var] param_in_out_ty
- let name := grName.append "param_in_out_ty"
+ let name := appendToName grName "param_in_out_ty"
let levelParams := grLvlParams
let decl := Declaration.defnDecl {
name := name
@@ -1392,44 +1396,71 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
open private elabHeaders levelMVarToParamHeaders getAllUserLevelNames withFunLocalDecls elabFunValues
instantiateMVarsAtHeader instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes withUsed from Lean.Elab.MutualDef
-def Term.elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
- let scopeLevelNames ← getLevelNames
- let headers ← elabHeaders views
- let headers ← levelMVarToParamHeaders views headers
- let allUserLevelNames := getAllUserLevelNames headers
- withFunLocalDecls headers fun funFVars => do
- for view in views, funFVar in funFVars do
- addLocalVarInfo view.declId funFVar
- -- Add fake use site to prevent "unused variable" warning (if the
- -- function is actually not recursive, Lean would print this warning).
- -- Remark: we could detect this case and encode the function without
- -- using the fixed-point. In practice it shouldn't happen however:
- -- we define non-recursive functions with the `divergent` keyword
- -- only for testing purposes.
- addTermInfo' view.declId funFVar
- let values ←
- try
- let values ← elabFunValues headers
- Term.synthesizeSyntheticMVarsNoPostponing
- values.mapM (instantiateMVars ·)
- catch ex =>
- logException ex
- headers.mapM fun header => mkSorry header.type (synthetic := true)
- let headers ← headers.mapM instantiateMVarsAtHeader
- let letRecsToLift ← getLetRecsToLift
- let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
- checkLetRecsToLiftTypes funFVars letRecsToLift
- withUsed vars headers values letRecsToLift fun vars => do
- let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
- for preDef in preDefs do
- trace[Diverge.elab] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
- let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
- let preDefs ← instantiateMVarsAtPreDecls preDefs
- let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
- for preDef in preDefs do
- trace[Diverge.elab] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
- checkForHiddenUnivLevels allUserLevelNames preDefs
- addPreDefinitions preDefs
+-- Comes from Term.isExample
+def isExample (views : Array DefView) : Bool :=
+ views.any (·.kind.isExample)
+
+open Language in
+def Term.elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
+ if isExample views then
+ withoutModifyingEnv do
+ -- save correct environment in info tree
+ withSaveInfoContext do
+ go
+ else
+ go
+where
+ go :=
+ withAlwaysResolvedPromises views.size fun bodyPromises =>
+ withAlwaysResolvedPromises views.size fun tacPromises => do
+ let scopeLevelNames ← getLevelNames
+ let headers ← elabHeaders views bodyPromises tacPromises
+ let headers ← levelMVarToParamHeaders views headers
+ let allUserLevelNames := getAllUserLevelNames headers
+ withFunLocalDecls headers fun funFVars => do
+ for view in views, funFVar in funFVars do
+ addLocalVarInfo view.declId funFVar
+ -- Modification 1:
+ -- Add fake use site to prevent "unused variable" warning (if the
+ -- function is actually not recursive, Lean would print this warning).
+ -- Remark: we could detect this case and encode the function without
+ -- using the fixed-point. In practice it shouldn't happen however:
+ -- we define non-recursive functions with the `divergent` keyword
+ -- only for testing purposes.
+ addTermInfo' view.declId funFVar
+ let values ←
+ try
+ let values ← elabFunValues headers
+ Term.synthesizeSyntheticMVarsNoPostponing
+ values.mapM (instantiateMVars ·)
+ catch ex =>
+ logException ex
+ headers.mapM fun header => mkSorry header.type (synthetic := true)
+ let headers ← headers.mapM instantiateMVarsAtHeader
+ let letRecsToLift ← getLetRecsToLift
+ let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+ checkLetRecsToLiftTypes funFVars letRecsToLift
+ withUsed vars headers values letRecsToLift fun vars => do
+ let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+ for preDef in preDefs do
+ trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+ let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
+ let preDefs ← instantiateMVarsAtPreDecls preDefs
+ let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+ for preDef in preDefs do
+ trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
+ checkForHiddenUnivLevels allUserLevelNames preDefs
+ addPreDefinitions preDefs -- Modification 2: we use our custom function here
+ processDeriving headers
+
+ processDeriving (headers : Array DefViewElabHeader) := do
+ for header in headers, view in views do
+ if let some classNamesStx := view.deriving? then
+ for classNameStx in classNamesStx do
+ let className ← realizeGlobalConstNoOverload classNameStx
+ withRef classNameStx do
+ unless (← processDefDeriving className header.declName) do
+ throwError "failed to synthesize instance '{className}' for '{header.declName}'"
open Command in
def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
@@ -1439,7 +1470,8 @@ def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
let modifiers ← elabModifiers mods
let (binders, type) := expandOptDeclSig sig
let deriving? := none
- pure { ref := d, kind := DefKind.def, modifiers,
+ let headerRef := Syntax.missing -- Not sure what to put here
+ pure { ref := d, kind := DefKind.def, headerRef, modifiers,
declId := id, binders, type? := type, value := val, deriving? }
runTermElabM fun vars => Term.elabMutualDef vars views
@@ -1460,7 +1492,7 @@ elab_rules : command
if (`_root_).isPrefixOf name then throwUnsupportedSyntax
let view := extractMacroScopes name
let .str ns shortName := view.name | throwUnsupportedSyntax
- let shortName' := { view with name := shortName }.review
+ let shortName' := { view with name := Name.mkSimple shortName }.review
let cmd ← `(mutual $mods:declModifiers divergent%$tk def $(⟨setDeclIdName id shortName'⟩):declId $sig:optDeclSig $val:declVal end)
if ns matches .anonymous then
Command.elabCommand cmd
@@ -1475,6 +1507,7 @@ namespace Tests
--set_option trace.Diverge.def.genBody true
--set_option trace.Diverge.def.valid true
--set_option trace.Diverge.def.genBody.visit true
+ --set_option trace.Diverge.def.unfold true
divergent def list_nth {a: Type u} (ls : List a) (i : Int) : Result a :=
match ls with
@@ -1492,7 +1525,7 @@ namespace Tests
0 ≤ i → i < ls.length →
∃ x, list_nth ls i = .ok x := by
induction ls
- . intro i hpos h; simp at h; linarith
+ . intro i hpos h; simp at h; omega
. rename_i hd tl ih
intro i hpos h
-- We can directly use `rw [list_nth]`
@@ -1502,7 +1535,7 @@ namespace Tests
. -- We don't have to do this if we use scalar_tac
have hneq : 0 < i := by cases i <;> rename_i a _ <;> simp_all; cases a <;> simp_all
simp at h
- have ⟨ x, ih ⟩ := ih (i - 1) (by linarith) (by linarith)
+ have ⟨ x, ih ⟩ := ih (i - 1) (by omega) (by omega)
simp [ih]
tauto
diff --git a/backends/lean/Base/Extensions.lean b/backends/lean/Base/Extensions.lean
index c0e80861..b491f81b 100644
--- a/backends/lean/Base/Extensions.lean
+++ b/backends/lean/Base/Extensions.lean
@@ -1,5 +1,4 @@
import Lean
-import Std.Lean.HashSet
import Base.Utils
import Base.Primitives.Base
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index ca5ee266..a1897191 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -1,7 +1,6 @@
/- Complementary list functions and lemmas which operate on integers rather
than natural numbers. -/
-import Std.Data.Int.Lemmas
import Base.Arith
import Base.Utils
@@ -17,7 +16,7 @@ def len (ls : List α) : Int :=
theorem len_pos : 0 ≤ (ls : List α).len := by
induction ls <;> simp [*]
- linarith
+ omega
instance (a : Type u) : Arith.HasIntProp (List a) where
prop_ty := λ ls => 0 ≤ ls.len
@@ -169,6 +168,7 @@ theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
have hl : l.toNat = .succ (l.toNat - 1) := by
cases hl: l.toNat <;> simp_all
conv => rhs; rw[hl]
+ rfl
termination_by l.toNat
decreasing_by int_decr_tac
@@ -277,12 +277,12 @@ open Arith in
if heq: i = 0 then
simp [*] at *
have := tl.len_pos
- linarith
+ omega
else
have : 0 < i := by int_tac
simp [*]
apply hi
- linarith
+ omega
theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len :=
match ls with
@@ -291,13 +291,13 @@ theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len :=
if h: i = 0 then by simp [*]
else
have := idrop_len_le (i - 1) tl
- by simp [*]; linarith
+ by simp [*]; omega
@[simp]
theorem idrop_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) :
(ls.idrop i).len = ls.len - i :=
match ls with
- | [] => by simp_all; linarith
+ | [] => by simp_all; omega
| hd :: tl =>
if h: i = 0 then by simp [*]
else
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 17ee626f..be460987 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -325,8 +325,7 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran
have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
simp [*]
-attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
-set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
+set_option pp.fieldNotation.generalized true
def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
-- TODO: not completely sure here
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index f4264b9b..9f809ead 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1,6 +1,5 @@
import Lean
import Lean.Meta.Tactic.Simp
-import Mathlib.Tactic.Linarith
import Base.Primitives.Base
import Base.Primitives.Core
import Base.Diverge.Base
@@ -9,6 +8,9 @@ import Base.Arith.Int
namespace Primitives
+-- Deactivate the warnings which appear when we use `#assert`
+set_option linter.hashCommand false
+
----------------------
-- MACHINE INTEGERS --
----------------------
@@ -279,11 +281,11 @@ theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by
theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by
have := Scalar.cMin_bound ty
- linarith
+ omega
theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by
have := Scalar.cMax_bound ty
- linarith
+ omega
/-- The scalar type.
@@ -310,7 +312,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
:=
λ h => by
- apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
+ apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> omega
def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
(h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
@@ -345,7 +347,7 @@ theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
have ⟨ hmin, hmax ⟩ := h
have hbmin := Scalar.cMin_bound ty
have hbmax := Scalar.cMax_bound ty
- cases hmin <;> cases hmax <;> apply And.intro <;> linarith
+ cases hmin <;> cases hmax <;> apply And.intro <;> omega
theorem Scalar.check_bounds_eq_in_bounds (ty : ScalarTy) (x : Int) :
Scalar.check_bounds ty x ↔ Scalar.in_bounds ty x := by
@@ -730,7 +732,6 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
(∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
have h := @add_equiv ty x y
split at h <;> simp_all
- apply h
theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
@@ -738,7 +739,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
have hmin : Scalar.min ty ≤ ↑x + ↑y := by
have hx := x.hmin
have hy := y.hmin
- cases ty <;> simp [min, ScalarTy.isSigned] at * <;> linarith
+ cases ty <;> simp [min, ScalarTy.isSigned] at * <;> omega
apply add_spec <;> assumption
/- Fine-grained theorems -/
@@ -825,7 +826,6 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
have h := @sub_equiv ty x y
split at h <;> simp_all
- apply h
theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
{x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
@@ -834,7 +834,7 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
have hx := x.hmin
have hxm := x.hmax
have hy := y.hmin
- cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> linarith
+ cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> omega
intros
apply sub_spec <;> assumption
@@ -1030,11 +1030,11 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
have hx := x.hmin
have hy := y.hmin
simp [h] at hx hy
- have hmin : 0 ≤ ↑x / ↑y := Int.ediv_nonneg hx hy
+ have hmin : 0 ≤ x.val / y.val := Int.ediv_nonneg hx hy
have hmax : ↑x / ↑y ≤ Scalar.max ty := by
have := Int.ediv_le_self ↑y hx
have := x.hmax
- linarith
+ omega
have hs := @div_spec ty x y hnz
simp [*] at hs
apply hs
@@ -1151,7 +1151,7 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
have h : (0 : Int) < y := by int_tac
have h := Int.emod_lt_of_pos ↑x h
have := y.hmax
- linarith
+ omega
have hs := @rem_spec ty x y hnz
simp [*] at hs
simp [*]
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index d144fcb8..0b010944 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
-import Mathlib.Tactic.Linarith
import Base.IList
import Base.Primitives.Scalar
import Base.Primitives.ArraySlice
@@ -59,7 +58,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
have h : nlen ≤ Usize.max := by
simp [Usize.max] at *
have hm := Usize.refined_max.property
- cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
+ cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try omega
ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
else
fail maximumSizeExceeded
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 03c80a42..0e46737f 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,5 +1,4 @@
import Lean
-import Std.Lean.HashSet
import Base.Utils
import Base.Primitives.Base
import Base.Extensions
@@ -111,7 +110,7 @@ section Methods
-- Collect all the free variables in the arguments
let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
-- Check if they intersect the fvars we introduced for the existentially quantified variables
- let evarsSet : HashSet FVarId := HashSet.ofArray (evars.map (fun (x : Expr) => x.fvarId!))
+ let evarsSet : HashSet FVarId := HashSet.empty.insertMany (evars.map (fun (x : Expr) => x.fvarId!))
let filtArgsFVars := allArgsFVars.toArray.filter (fun var => evarsSet.contains var)
if filtArgsFVars.isEmpty then pure ()
else
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 03d464d7..da601b73 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -131,7 +131,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
Tactic.focus do
let _ ←
tryTac
- (simpAt true {} []
+ (simpAt true {} #[] []
[``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
-- It may happen that at this point the goal is already solved (though this is rare)
@@ -140,7 +140,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
else
trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
-- TODO: remove this (some types get unfolded too much: we "fold" them back)
- let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep)
+ let _ ← tryTac (simpAt true {} #[] [] scalar_eqs [] .wildcard_dep)
trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
@@ -346,11 +346,8 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
-- Not a local declaration: should be a theorem
trace[Progress] "With arg: theorem"
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
- let cs ← resolveGlobalConstWithInfos id
- match cs with
- | [] => throwError "Could not find theorem {id}"
- | id :: _ =>
- pure (some (.Theorem id))
+ let some (.const name _) ← Term.resolveId? id | throwError m!"Could not find theorem: {id}"
+ pure (some (.Theorem name))
else pure none
let ids :=
let args := asArgs.getArgs
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 4be46400..7225d8a3 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -7,7 +7,6 @@ Mathlib tactics:
- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
-- should we use linarith or omega?
- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
-/
@@ -133,8 +132,9 @@ open Lean.Elab.Command
liftTermElabM do
let id := stx[1]
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
- let cs ← resolveGlobalConstWithInfos id
- explore_decl cs[0]!
+ let some cs ← Term.resolveId? id | throwError m!"Unknown id: {id}"
+ let name := cs.constName!
+ explore_decl name
private def test1 : Nat := 0
private def test2 (x : Nat) : Nat := x
@@ -704,49 +704,48 @@ inductive Location where
/-- Same as Tactic.Location -/
| targets (hypotheses : Array Syntax) (type : Bool)
--- Comes from Tactic.simpLocation
-def customSimpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
- (loc : Location) : TacticM Simp.UsedSimps := do
+#check Tactic.simpLocation
+#check Tactic.Location
+#check MVarId.getNondepPropHyps
+#check simpLocation
+
+-- Adapted from Tactic.simpLocation
+def customSimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none)
+ (loc : Location) : TacticM Simp.Stats := do
match loc with
| Location.targets hyps simplifyTarget =>
- withMainContext do
- let fvarIds ← Lean.Elab.Tactic.getFVarIds hyps
- go fvarIds simplifyTarget
+ -- Simply call the regular simpLocation
+ simpLocation ctx simprocs discharge? (Tactic.Location.targets hyps simplifyTarget)
| Location.wildcard =>
- withMainContext do
- go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
+ -- Simply call the regular simpLocation
+ simpLocation ctx simprocs discharge? Tactic.Location.wildcard
| Location.wildcard_dep =>
+ -- Custom behavior
withMainContext do
- let ctx ← Lean.MonadLCtx.getLCtx
- let decls ← ctx.getDecls
+ -- Lookup *all* the declarations
+ let lctx ← Lean.MonadLCtx.getLCtx
+ let decls ← lctx.getDecls
let tgts := (decls.map (fun d => d.fvarId)).toArray
- go tgts (simplifyTarget := true)
-where
- go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
- let mvarId ← getMainGoal
- let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
- match result? with
- | none => replaceMainGoal []
- | some (_, mvarId) => replaceMainGoal [mvarId]
- return usedSimps
+ -- Call the regular simpLocation.go
+ simpLocation.go ctx simprocs discharge? tgts (simplifyTarget := true)
/- Call the simp tactic. -/
-def simpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
- (loc : Location) :
+def simpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : Simp.SimprocsArray)
+ (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Location) :
Tactic.TacticM Unit := do
-- Initialize the simp context
let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
-- Apply the simplifier
- let _ ← customSimpLocation ctx (discharge? := .none) loc
+ let _ ← customSimpLocation ctx simprocs (discharge? := .none) loc
/- Call the dsimp tactic. -/
-def dsimpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
- (loc : Tactic.Location) :
+def dsimpAt (simpOnly : Bool) (config : Simp.Config) (simprocs : Simp.SimprocsArray)
+ (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Tactic.Location) :
Tactic.TacticM Unit := do
-- Initialize the simp context
let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
-- Apply the simplifier
- dsimpLocation ctx loc
+ dsimpLocation ctx simprocs loc
-- Call the simpAll tactic
def simpAll (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 99ec856e..de2e22cd 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": 7,
+{"version": "1.0.0",
"packagesDir": ".lake/packages",
"packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
- "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
- "name": "std",
+ "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981",
+ "name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
@@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
- "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+ "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@@ -22,25 +22,25 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
- "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+ "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
- "configFile": "lakefile.lean"},
+ "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
- "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+ "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
- "inputRev": "v0.0.30",
+ "inputRev": "v0.0.36",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
- "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+ "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@@ -49,16 +49,16 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
- "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+ "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
- "configFile": "lakefile.lean"},
+ "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
- "rev": "3e99b48baf21ffdd202d5c2e39990fc23f4c6d32",
+ "rev": "659d35143a857ceb5ba7c02a0e1530a1c7aec70c",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 9ad30404..0ba3faf8 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.9.0-rc1
--
cgit v1.2.3
From d5cf75a0f8209298ad85f46249f14d5c3a24faf6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:37:18 +0200
Subject: Update the tests
---
backends/lean/Base/Utils.lean | 5 -----
1 file changed, 5 deletions(-)
(limited to 'backends/lean')
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 7225d8a3..5954f048 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -704,11 +704,6 @@ inductive Location where
/-- Same as Tactic.Location -/
| targets (hypotheses : Array Syntax) (type : Bool)
-#check Tactic.simpLocation
-#check Tactic.Location
-#check MVarId.getNondepPropHyps
-#check simpLocation
-
-- Adapted from Tactic.simpLocation
def customSimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none)
(loc : Location) : TacticM Simp.Stats := do
--
cgit v1.2.3