Update Lean to v4.9.0-rc1

2 files changed, 95 insertions, 55 deletions

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