feat: when Lean cannot prove termination, then report error and add definition as partial, and if it fails add as axiom

src/Lean/Elab/PreDefinition/Main.lean

@@ -75,6 +75,20 @@ private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array
         return TransformStep.visit e
     return { preDef with value }
 
+private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
+  for preDef in preDefs do
+    let decl := Declaration.axiomDecl {
+      name        := preDef.declName,
+      levelParams := preDef.levelParams,
+      type        := preDef.type,
+      isUnsafe    := preDef.modifiers.isUnsafe
+    }
+    addDecl decl
+    withSaveInfoContext do  -- save new env
+      addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
+    applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
+    applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+
 def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -83,6 +97,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   let cliques := partitionPreDefs preDefs
   let mut terminationBy ← liftMacroM <| WF.expandTerminationBy hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
   let mut decreasingBy  ← liftMacroM <| WF.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
+  let mut hasErrors := false
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0] then
@@ -99,26 +114,43 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
           withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
       addAndCompilePartial preDefs
     else
-      let mut wf? := none
-      let mut decrTactic? := none
-      if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
-        wf? := some wf
-        terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
-      if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
-        decrTactic? := some (← withRef ref `(by $decrTactic))
-        decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
-      if wf?.isSome || decrTactic?.isSome then
-        wfRecursion preDefs wf? decrTactic?
-      else
-        withRef (preDefs[0].ref) <| mapError
-          (orelseMergeErrors
-            (structuralRecursion preDefs)
-            (wfRecursion preDefs none none))
-          (fun msg =>
-            let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
-            m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
-  liftMacroM <| terminationBy.ensureAllUsed
-  liftMacroM <| decreasingBy.ensureAllUsed
+      try
+        let mut wf? := none
+        let mut decrTactic? := none
+        if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
+          wf? := some wf
+          terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
+        if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
+          decrTactic? := some (← withRef ref `(by $decrTactic))
+          decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
+        if wf?.isSome || decrTactic?.isSome then
+          wfRecursion preDefs wf? decrTactic?
+        else
+          withRef (preDefs[0].ref) <| mapError
+            (orelseMergeErrors
+              (structuralRecursion preDefs)
+              (wfRecursion preDefs none none))
+            (fun msg =>
+              let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
+              m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
+      catch ex =>
+        hasErrors := true
+        logException ex
+        let s ← saveState
+        try
+          if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
+            -- try to add as partial definition
+            try
+              addAndCompilePartial preDefs
+            catch _ =>
+              s.restore
+              addAsAxioms preDefs
+          else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
+            addAsAxioms preDefs
+        catch _ => s.restore
+  unless hasErrors do
+    liftMacroM <| terminationBy.ensureAllUsed
+    liftMacroM <| decreasingBy.ensureAllUsed
 
 builtin_initialize
   registerTraceClass `Elab.definition.body

tests/lean/sanitychecks.lean

@@ -1,16 +1,16 @@
 theorem unsound : False := -- Error
   unsound
 
-partial theorem unsound : False := -- Error
-  unsound
+partial theorem unsound2 : False := -- Error
+  unsound2
 
-unsafe theorem unsound : False := -- Error
-  unsound
+unsafe theorem unsound3 : False := -- Error
+  unsound3
 
-constant unsound : False  -- Error
+constant unsound4 : False  -- Error
 
 axiom magic : False -- OK
-
+namespace Foo
 partial def foo (x : Nat) : Nat := foo x  -- OK
 
 unsafe def unsound2 : False := unsound  -- OK

tests/lean/sanitychecks.lean.expected.out

@@ -4,12 +4,12 @@ with errors
 structural recursion cannot be used
 
 well-founded recursion cannot be used, 'unsound' does not take any arguments
-sanitychecks.lean:4:8-5:9: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
-sanitychecks.lean:7:7-8:9: error: 'unsafe' theorems are not allowed
-sanitychecks.lean:10:0-10:24: error: failed to synthesize
+sanitychecks.lean:4:8-5:10: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
+sanitychecks.lean:7:7-8:10: error: 'unsafe' theorems are not allowed
+sanitychecks.lean:10:0-10:25: error: failed to synthesize
   Inhabited False
-sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'unsound3' is not a function
+sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
-sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'unsound4', failed to show that type is inhabited and non empty
+sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty
 sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
 sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'

tests/lean/terminationFailure.lean

@@ -0,0 +1,23 @@
+def f (x : Nat) : Nat :=
+  if h : x > 0 then
+    g x + 2
+  else
+    1
+where
+  g : Nat → Nat
+  | 0 => 2
+  | x => f x * 2
+
+#check f
+#check f.g
+
+inductive Foo where
+  | a | b | c
+
+def h (x : Nat) : Foo :=
+  match x with
+  | 0 => Foo.a
+  | 1 => Foo.b
+  | x => h x
+
+#check h

tests/lean/terminationFailure.lean.expected.out

@@ -0,0 +1,20 @@
+terminationFailure.lean:7:2-7:3: error: fail to show termination for
+  f.g
+  f
+with errors
+structural recursion does not handle mutually recursive functions
+
+'termination_by' modifier missing
+f : Nat → Nat
+f.g : Nat → Nat
+terminationFailure.lean:17:4-17:5: error: fail to show termination for
+  h
+with errors
+argument #1 was not used for structural recursion
+  failed to eliminate recursive application
+    h x
+
+structural recursion cannot be used
+
+'termination_by' modifier missing
+h : Nat → Foo