From d782a97f5c347dc941b338ee52358a321764ecce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Jan 2022 17:00:54 -0800 Subject: [PATCH] feat: add `WF.mkProof` for `WF.mkEqns` --- src/Lean/Elab/PreDefinition/Eqns.lean | 37 +++++++++++++++ .../Elab/PreDefinition/Structural/Eqns.lean | 37 --------------- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 47 +++++++++++++++++-- src/Lean/Expr.lean | 3 ++ tests/lean/run/wfEqns1.lean | 27 +++++++++++ 5 files changed, 111 insertions(+), 40 deletions(-) create mode 100644 tests/lean/run/wfEqns1.lean diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 73dd34ec4d..b2c05727de 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index b5aba952ef..495ad881ff 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 6be541d17e..497eea7822 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/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] diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 11b77283f8..bcf8603a23 100644 --- a/src/Lean/Expr.lean +++ b/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 diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean new file mode 100644 index 0000000000..98c8cb685f --- /dev/null +++ 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