Update the Lean library to 4.11.0-rc2 (#316)

* Make minor updates

* Start updating Lean to v4.11.0-rc2

* Fix Diverge/Elab.lean

* Make minor modifications

* Update the Lean tests and fix the proofs

* Add a model for clone::clone::Clone::clone_from to the Lean library

* Revert some modifications

* Revert more modifications

backends/lean/Base/Diverge/Elab.lean

@@ -10,9 +10,6 @@ namespace Diverge
 /- Automating the generation of the encoding and the proofs so as to use nice
    syntactic sugar. -/
 
-syntax (name := divergentDef)
-  declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command
-
 open Lean Elab Term Meta Primitives Lean.Meta
 open Utils
 
@@ -1389,17 +1386,43 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
         else return ()
       catch _ => s.restore
 
--- The following two functions are copy-pasted from Lean.Elab.MutualDef
-
+-- The following three functions are copy-pasted from Lean.Elab.MutualDef.lean
 open private elabHeaders levelMVarToParamHeaders getAllUserLevelNames withFunLocalDecls elabFunValues
   instantiateMVarsAtHeader instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes withUsed from Lean.Elab.MutualDef
 
+-- Copy/pasted from Lean.Elab.Term.withHeaderSecVars (because the definition is private)
+private def Term.withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader)
+    (k : Array Expr → TermElabM α) : TermElabM α := do
+  let (_, used) ← collectUsed.run {}
+  let (lctx, localInsts, vars) ← removeUnused vars used
+  withLCtx lctx localInsts <| k vars
+where
+  collectUsed : StateRefT CollectFVars.State MetaM Unit := do
+    -- directly referenced in headers
+    headers.forM (·.type.collectFVars)
+    -- included by `include`
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      if includedVars.contains ldecl.userName then
+        modify (·.add ldecl.fvarId)
+    -- transitively referenced
+    get >>= (·.addDependencies) >>= set
+    -- instances (`addDependencies` unnecessary as by definition they may only reference variables
+    -- already included)
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      let st ← get
+      if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then
+        modify (·.add ldecl.fvarId)
+  getFVars (e : Expr) : MetaM (Array FVarId) :=
+    (·.2.fvarIds) <$> e.collectFVars.run {}
+
 -- 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 :=
+def Term.elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -1418,7 +1441,7 @@ where
       withFunLocalDecls headers fun funFVars => do
         for view in views, funFVar in funFVars do
           addLocalVarInfo view.declId funFVar
-          -- Modification 1:
+          -- 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
@@ -1428,7 +1451,7 @@ where
           addTermInfo' view.declId funFVar
         let values ←
           try
-            let values ← elabFunValues headers
+            let values ← elabFunValues headers vars includedVars
             Term.synthesizeSyntheticMVarsNoPostponing
             values.mapM (instantiateMVars ·)
           catch ex =>
@@ -1438,18 +1461,23 @@ where
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
         checkLetRecsToLiftTypes funFVars letRecsToLift
-        withUsed vars headers values letRecsToLift fun vars => do
+        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else 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 ← shareCommonPreDefs 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
+          addPreDefinitions preDefs -- MODIFICATION 2: we use our custom function here
           processDeriving headers
+      for view in views, header in headers do
+        -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
+        -- that depends only on a part of the ref
+        addDeclarationRanges header.declName view.ref
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
@@ -1460,22 +1488,61 @@ where
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"
 
+#check Command.elabMutualDef
+
+-- Copy/pasted from Lean.Elab.MutualDef
 open Command in
+open Language in
 def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
-  let views ← ds.mapM fun d => do
-    let `($mods:declModifiers divergent def $id:declId $sig:optDeclSig $val:declVal) := d
-      | throwUnsupportedSyntax
-    let modifiers ← elabModifiers mods
-    let (binders, type) := expandOptDeclSig sig
-    let deriving? := none
-    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
+  let opts ← getOptions
+  withAlwaysResolvedPromises ds.size fun headerPromises => do
+    let snap? := (← read).snap?
+    let mut views := #[]
+    let mut defs := #[]
+    let mut reusedAllHeaders := true
+    for h : i in [0:ds.size], headerPromise in headerPromises do
+      let d := ds[i]
+      let modifiers ← elabModifiers d[0]
+      if ds.size > 1 && modifiers.isNonrec then
+        throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
+      let mut view ← mkDefView modifiers d[2] -- MODIFICATION: changed the index to 2
+      let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
+      if let some snap := snap? then
+        view := { view with headerSnap? := some {
+          old? := do
+            -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the
+            -- elaboration context and state are unchanged, and the syntax of this as well as all
+            -- previous headers is unchanged, then the elaboration result for this header (which
+            -- includes state from elaboration of previous headers!) should be unchanged.
+            guard reusedAllHeaders
+            let old ← snap.old?
+            -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
+            let old ← old.val.get.toTyped? DefsParsedSnapshot
+            let oldParsed ← old.defs[i]?
+            guard <| fullHeaderRef.eqWithInfoAndTraceReuse opts oldParsed.fullHeaderRef
+            -- no syntax guard to store, we already did the necessary checks
+            return ⟨.missing, oldParsed.headerProcessedSnap⟩
+          new := headerPromise
+        } }
+        defs := defs.push {
+          fullHeaderRef
+          headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
+        }
+        reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
+      views := views.push view
+    if let some snap := snap? then
+      -- no non-fatal diagnostics at this point
+      snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
+    let includedVars := (← getScope).includedVars
+    runTermElabM fun vars => Term.elabMutualDef vars includedVars views
+
+syntax (name := divergentDef)
+  declModifiers "divergent" Lean.Parser.Command.definition : command
 
 -- Special command so that we don't fall back to the built-in mutual when we produce an error.
 local syntax "_divergent" Parser.Command.mutual : command
-elab_rules : command | `(_divergent mutual $decls* end) => Command.elabMutualDef decls
+elab_rules : command
+  | `(_divergent mutual $decls* end) => Command.elabMutualDef decls
 
 macro_rules
   | `(mutual $decls* end) => do
@@ -1501,6 +1568,8 @@ namespace Tests
 
   /- Some examples of partial functions -/
 
+  -- set_option trace.Diverge true
+  -- set_option pp.rawOnError true
   --set_option trace.Diverge.def true
   --set_option trace.Diverge.def.genBody true
   --set_option trace.Diverge.def.valid true

backends/lean/Base/Primitives/Core.lean

@@ -74,3 +74,10 @@ end core
 
 /- [core::option::Option::is_none] -/
 @[simp] def core.option.Option.is_none (T: Type) (self: Option T): Bool := self.isNone
+
+/- [core::clone::Clone::clone_from]:
+   Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43
+   Name pattern: core::clone::Clone::clone_from -/
+@[simp] def core.clone.Clone.clone_from
+  {Self : Type} (cloneInst : core.clone.Clone Self) (_self : Self) (source : Self) : Result Self :=
+  cloneInst.clone source

backends/lean/Base/Utils.lean

@@ -869,7 +869,7 @@ def evalAesopSaturate (options : Aesop.Options') (ruleSets : Array Name) : Tacti
   let rss ← Aesop.Frontend.getGlobalRuleSets ruleSets
   let rs ← Aesop.mkLocalRuleSet rss options
     |> Aesop.ElabM.runForwardElab (← getMainGoal)
-  tryLiftMetaTactic1 (Aesop.saturate rs · |>.run { options }) "Aesop.saturate failed"
+  tryLiftMetaTactic1 (Aesop.saturate rs · options) "Aesop.saturate failed"
 
 /-- Normalize the let-bindings by inlining them -/
 def normalizeLetBindings (e : Expr) : MetaM Expr :=

backends/lean/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e242f1edcacf917f40fae9b81f57f4bd0a4e45ac",
+   "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

backends/lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.11.0-rc2

compiler/ExtractBuiltin.ml

@@ -508,6 +508,7 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
            ~extract_name:
              (Some (backend_choice "" "core::option::Option::is_none"))
            ~can_fail:false ();
+         mk_fun "core::clone::Clone::clone_from" ();
        ]
       @ List.map
           (fun ty ->

tests/lean/Avl/Properties.lean

@@ -799,7 +799,6 @@ theorem Tree.insert_in_opt_node_spec
     split_conjs
     . simp [Node.invAux, Node.balanceFactor]
     . simp [Subtree.inv]
-    . apply Set.ext; simp
   . -- tree = some
     rename Node T => node
     have hNodeInv : Node.inv node := by simp_all (config := {maxDischargeDepth := 1})

tests/lean/External/FunsExternal_Template.lean

@@ -24,10 +24,3 @@ axiom core.cell.Cell.get_mut
   core.cell.Cell T → State → Result (State × (T × (T → State → Result
     (State × (core.cell.Cell T)))))
 
-/- [core::clone::Clone::clone_from]:
-   Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43
-   Name pattern: core::clone::Clone::clone_from -/
-axiom core.clone.Clone.clone_from
-  {Self : Type} (self_clause : core.clone.Clone Self) :
-  Self → Self → State → Result (State × Self)
-

tests/lean/Tutorial/Exercises.lean

@@ -165,7 +165,7 @@ theorem even_spec (n : U32) :
   . progress as ⟨ n' ⟩
     progress as ⟨ b ⟩
     simp [*]
-    simp [Int.even_sub]
+    simp [Int.odd_sub]
 termination_by n.toNat
 decreasing_by scalar_decr_tac
 
@@ -437,10 +437,9 @@ divergent def add_no_overflow_loop
     - `scalar_eq_nf`: similar, but tuned to prove goals of the shape: `... = ...`
     You can try both tactics and see their effect.
  -/
--- Here, we're using ring_nf
 @[simp]
-theorem toInt_aux_append (l0 l1 : List U32) :
-  toInt_aux (l0 ++ l1) = toInt_aux l0 + 2 ^ (32 * l0.length) * toInt_aux l1 := by
+theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
+  toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
   sorry
 
 /-- You will need this lemma for the proof of `add_no_overflow_loop_spec`.
@@ -461,16 +460,11 @@ theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length)
   toInt_aux (l.update i x) = toInt_aux l + 2 ^ (32 * i) * (x - l.index i) := by
   sorry
 
-/-- You will need this lemma for the proof of `add_no_overflow_loop_spec`.
+/-- The proof about `add_no_overflow_loop`.
 
-    Advice: do the proof of `add_no_overflow_loop_spec` first, then come back to prove this lemma.
+    Hint: you will need to reason about non-linear arithmetic with `scalar_nf` and
+    `scalar_eq_nf`` (see above).
  -/
-@[simp]
-theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) :
-  toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by
-  sorry
-
-/-- The proof about `add_no_overflow_loop` -/
 @[pspec]
 theorem add_no_overflow_loop_spec
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize)