feat: elaborate temination_by term

src/Lean/Elab/PreDefinition/Main.lean

@@ -75,11 +75,14 @@ def addPreDefinitions (preDefs : Array PreDefinition) (terminationBy? : Option S
       addAndCompileUnsafe preDefs
     else if preDefs.any (·.modifiers.isPartial) then
       addAndCompilePartial preDefs
+    else if let some wfStx := terminationBy.find? (preDefs.map (·.declName)) then
+      terminationBy := terminationBy.erase (preDefs.map (·.declName))
+      wfRecursion preDefs wfStx
     else
-      terminationBy ← withRef (preDefs[0].ref) <| mapError
+      withRef (preDefs[0].ref) <| mapError
         (orelseMergeErrors
-          (structuralRecursion preDefs *> pure terminationBy)
-          (wfRecursion preDefs terminationBy))
+          (structuralRecursion preDefs)
+          (wfRecursion preDefs 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}")

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -7,12 +7,13 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.WF.TerminationBy
 import Lean.Elab.PreDefinition.WF.PackDomain
 import Lean.Elab.PreDefinition.WF.PackMutual
+import Lean.Elab.PreDefinition.WF.Rel
 
 namespace Lean.Elab
 open WF
 open Meta
 
-def wfRecursion (preDefs : Array PreDefinition) (terminationBy : TerminationBy) : TermElabM TerminationBy := do
+def wfRecursion (preDefs : Array PreDefinition) (wfStx? : Option Syntax) : TermElabM Unit := do
   withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef
@@ -22,7 +23,9 @@ def wfRecursion (preDefs : Array PreDefinition) (terminationBy : TerminationBy)
       trace[Elab.definition.wf] "{preDef.declName}, {preDef.levelParams}, {preDef.value}"
     let unaryPreDef ← packMutual unaryPreDefs
     trace[Elab.definition.wf] "{unaryPreDef.declName} := {unaryPreDef.value}"
-    check unaryPreDef.value
+    check unaryPreDef.value -- TODO: remove
+    let (wf, r) ← elabWF unaryPreDef wfStx?
+    trace[Elab.definition.wf] "{wf}"
   -- TODO
   throwError "well-founded recursion has not been implemented yet"
 

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.PreDefinition.Basic
+
+namespace Lean.Elab.WF
+open Meta
+open Term
+
+def elabWF (unaryPreDef : PreDefinition) (wfStx? : Option Syntax) : TermElabM (Expr × Expr) := do
+  if let some wfStx := wfStx? then
+    withDeclName unaryPreDef.declName do
+      let α := unaryPreDef.type.bindingDomain!
+      let u ← getLevel α
+      let r ← mkFreshExprMVar (← mkArrow α (← mkArrow α (mkSort levelZero)))
+      let expectedType := mkApp2 (mkConst ``WellFounded [u]) α r
+      let w ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
+      let r ← instantiateMVars r
+      let pendingMVarIds ← getMVars w
+      discard <| logUnassignedUsingErrorInfos pendingMVarIds
+      return (r, w)
+  else
+    -- TODO: try to synthesize some default relation
+    throwError "'termination_by' modifier missing"
+
+end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/TerminationBy.lean

@@ -37,7 +37,7 @@ def expandTerminationBy (terminationBy? : Option Syntax) (cliques : Array (Array
   else
     return TerminationBy.none
 
-def TerminatioBy.erase (t : TerminationBy) (clique : Array Name) : TerminationBy :=
+def TerminationBy.erase (t : TerminationBy) (clique : Array Name) : TerminationBy :=
   match t with
   | TerminationBy.none   => TerminationBy.none
   | TerminationBy.one .. => TerminationBy.none

tests/lean/sanitychecks.lean.expected.out

@@ -3,7 +3,7 @@ sanitychecks.lean:1:8-1:15: error: fail to show termination for
 with errors
 structural recursion cannot be used
 
-well-founded recursion has not been implemented yet
+'termination_by' modifier missing
 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 instance

tests/lean/termination_by.lean

@@ -13,21 +13,6 @@ mutual
  termination_by measure
 end
 
-mutual
-  def f (n : Nat) :=
-    match n with
-    | 0 => 1
-    | n+1 => f n * 2
-end
-termination_by measure
-
-
-def g (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g n * 3
-termination_by measure
-
 def g' (n : Nat) :=
   match n with
   | 0 => 1

tests/lean/termination_by.lean.expected.out

@@ -1,6 +1,4 @@
 termination_by.lean:8:0-8:22: error: invalid 'termination_by' in mutually inductive datatype declaration
 termination_by.lean:13:1-13:23: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by.lean:22:15-22:22: error: unused 'termination_by' element
-termination_by.lean:29:15-29:22: error: unused 'termination_by' element
-termination_by.lean:36:2-36:3: error: function 'h' not found in current declaration
-termination_by.lean:54:7-54:14: error: invalid 'termination_by' element, 'Test.g' and 'Test.f' are in the same clique
+termination_by.lean:21:2-21:3: error: function 'h' not found in current declaration
+termination_by.lean:39:7-39:14: error: invalid 'termination_by' element, 'Test.g' and 'Test.f' are in the same clique