feat: add WF.mkProof for WF.mkEqns

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -113,4 +113,41 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
 def mkBaseNameFor (env : Environment) (declName : Name) : Name :=
   Lean.mkBaseNameFor env declName `eq_1 `_eqns
 
+/-- Try to close goal using `rfl` with smart unfolding turned off. -/
+def tryURefl (mvarId : MVarId) : MetaM Bool :=
+  withOptions (smartUnfolding.set . false) do
+    try applyRefl mvarId; return true catch _ => return false
+
+/-- Delta reduce the equation left-hand-side -/
+def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
+  let target ← getMVarType' mvarId
+  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
+  let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
+  replaceTargetDefEq mvarId (← mkEq lhs rhs)
+
+def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
+  let target ← getMVarType' mvarId
+  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
+  let some rhs ← delta? rhs.consumeMData (. == declName) | return none
+  replaceTargetDefEq mvarId (← mkEq lhs rhs)
+
+private partial def whnfAux (e : Expr) : MetaM Expr := do
+  let e ← whnfR e
+  match e with
+  | Expr.proj _ _ s _ => e.updateProj! (← whnfAux s)
+  | _ => e
+
+/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
+def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
+  let target ← getMVarType' mvarId
+  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
+  let lhs' ← whnfAux lhs
+  if lhs' != lhs then
+    return some (← replaceTargetDefEq mvarId (← mkEq lhs' rhs))
+  else
+    return none
+
+def tryContradiction (mvarId : MVarId) : MetaM Bool := do
+  try contradiction mvarId { genDiseq := true }; return true catch _ => return false
+
 end Lean.Elab.Eqns

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -14,43 +14,6 @@ namespace Lean.Elab
 open Meta
 open Eqns
 
-/-- Try to close goal using `rfl` with smart unfolding turned off. -/
-def tryURefl (mvarId : MVarId) : MetaM Bool :=
-  withOptions (smartUnfolding.set . false) do
-    try applyRefl mvarId; return true catch _ => return false
-
-/-- Delta reduce the equation left-hand-side -/
-def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
-  let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
-  replaceTargetDefEq mvarId (← mkEq lhs rhs)
-
-def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
-  let some rhs ← delta? rhs.consumeMData (. == declName) | return none
-  replaceTargetDefEq mvarId (← mkEq lhs rhs)
-
-private partial def whnfAux (e : Expr) : MetaM Expr := do
-  let e ← whnfR e
-  match e with
-  | Expr.proj _ _ s _ => e.updateProj! (← whnfAux s)
-  | _ => e
-
-/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
-def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
-  let lhs' ← whnfAux lhs
-  if lhs' != lhs then
-    return some (← replaceTargetDefEq mvarId (← mkEq lhs' rhs))
-  else
-    return none
-
-def tryContradiction (mvarId : MVarId) : MetaM Bool := do
-  try contradiction mvarId { genDiseq := true }; return true catch _ => return false
-
 namespace Structural
 
 structure EqnInfo where

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

@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Rewrite
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 
@@ -18,17 +19,57 @@ structure EqnInfo where
   declNameNonRec : Name
   deriving Inhabited
 
-private def mkProof (declName : Name) (type : Expr) : MetaM Expr :=
-  mkSorry type false -- TODO
+private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
+  let target ← getMVarType' mvarId
+  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
+  if lhs.isAppOf ``WellFounded.fix then
+    return mvarId
+  else
+    deltaLHSUntilFix (← deltaLHS mvarId)
+
+private def rwFixEq (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
+  let target ← getMVarType' mvarId
+  let some (_, lhs, rhs) ← target.eq? | unreachable!
+  let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
+  let r ← rewrite mvarId target h
+  replaceTargetEq mvarId r.eNew r.eqProof
+
+private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
+  trace[Elab.definition.wf.eqns] "proving: {type}"
+  withNewMCtxDepth do
+    let main ← mkFreshExprSyntheticOpaqueMVar type
+    let (_, mvarId) ← intros main.mvarId!
+    go (← rwFixEq (← deltaLHSUntilFix mvarId))
+    instantiateMVars main
+where
+  go (mvarId : MVarId) : MetaM Unit := do
+    trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
+    if (← tryURefl mvarId) then
+      return ()
+    else if (← tryContradiction mvarId) then
+      return ()
+    else if let some mvarId ← simpMatch? mvarId then
+      go mvarId
+    else if let some mvarId ← simpIf? mvarId then
+      go mvarId
+    else if let some mvarId ← whnfReducibleLHS? mvarId then
+      go mvarId
+    else if let some mvarId ← deltaRHS? mvarId declName then
+      go mvarId
+    else if let some mvarIds ← casesOnStuckLHS? mvarId then
+      mvarIds.forM go
+    else
+      throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set . false) do
+  let baseName := Eqns.mkBaseNameFor (← getEnv) declName
+  -- let unfoldLemma ← mkUnfoldLemma declName info baseName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes info.declNames goal.mvarId!
-  let baseName := Eqns.mkBaseNameFor (← getEnv) declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]

src/Lean/Expr.lean

@@ -822,6 +822,9 @@ def betaRev (f : Expr) (revArgs : Array Expr) : Expr :=
   if revArgs.size == 0 then f
   else betaRevAux revArgs revArgs.size f 0
 
+def beta (f : Expr) (args : Array Expr) : Expr :=
+  betaRev f args.reverse
+
 def isHeadBetaTargetFn : Expr → Bool
   | Expr.lam _ _ _ _ => true
   | Expr.mdata _ b _ => isHeadBetaTargetFn b

tests/lean/run/wfEqns1.lean

@@ -0,0 +1,27 @@
+import Lean
+
+open Lean
+open Lean.Meta
+def tst (declName : Name) : MetaM Unit := do
+  IO.println (← getEqnsFor? declName)
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by measure fun
+  | Sum.inl n => n
+  | Sum.inr n => n
+decreasing_by
+  simp [measure, invImage, InvImage, Nat.lt_wfRel]
+  apply Nat.lt_succ_self
+
+#print isEven
+
+#eval tst ``isEven
+#check @isEven.eq_1
+#check @isEven.eq_2