From 9e68c1e1c6daf90aeb813d06175d4305870a01ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Feb 2020 20:06:56 -0800 Subject: [PATCH] feat: add `generalize` and `replaceLocalDecl` --- src/Init/Lean/Meta/AppBuilder.lean | 6 +++++ src/Init/Lean/Meta/LevelDefEq.lean | 3 +-- src/Init/Lean/Meta/Tactic.lean | 2 ++ src/Init/Lean/Meta/Tactic/Generalize.lean | 31 +++++++++++++++++++++++ src/Init/Lean/Meta/Tactic/Intro.lean | 4 +-- src/Init/Lean/Meta/Tactic/LocalDecl.lean | 25 ++++++++++++++++++ src/Init/Lean/Meta/Tactic/Rewrite.lean | 2 +- src/Init/Lean/Meta/Tactic/Util.lean | 6 +++++ 8 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 src/Init/Lean/Meta/Tactic/Generalize.lean create mode 100644 src/Init/Lean/Meta/Tactic/LocalDecl.lean diff --git a/src/Init/Lean/Meta/AppBuilder.lean b/src/Init/Lean/Meta/AppBuilder.lean index 23bcdf7711..4c79ca4c06 100644 --- a/src/Init/Lean/Meta/AppBuilder.lean +++ b/src/Init/Lean/Meta/AppBuilder.lean @@ -202,5 +202,11 @@ else do pure $ mkAppN (mkConst `Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2] | _ => throwEx $ Exception.appBuilder `Eq.rec "invalid motive" #[motive] +def mkEqMP (eqProof pr : Expr) : MetaM Expr := +mkAppM `Eq.mp #[eqProof, pr] + +def mkEqMPR (eqProof pr : Expr) : MetaM Expr := +mkAppM `Eq.mpr #[eqProof, pr] + end Meta end Lean diff --git a/src/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean index 21a6928c13..7f17b569f5 100644 --- a/src/Init/Lean/Meta/LevelDefEq.lean +++ b/src/Init/Lean/Meta/LevelDefEq.lean @@ -189,8 +189,7 @@ numPostponed ← getNumPostponed; if numPostponed == 0 then pure true else traceCtx `Meta.isLevelDefEq.postponed $ processPostponedAux () - -private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit := +def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit := modify $ fun s => { env := env, mctx := mctx, postponed := postponed, .. s } /-- diff --git a/src/Init/Lean/Meta/Tactic.lean b/src/Init/Lean/Meta/Tactic.lean index 7cd37d31fe..2523657cf5 100644 --- a/src/Init/Lean/Meta/Tactic.lean +++ b/src/Init/Lean/Meta/Tactic.lean @@ -12,3 +12,5 @@ import Init.Lean.Meta.Tactic.Clear import Init.Lean.Meta.Tactic.Assert import Init.Lean.Meta.Tactic.Target import Init.Lean.Meta.Tactic.Rewrite +import Init.Lean.Meta.Tactic.Generalize +import Init.Lean.Meta.Tactic.LocalDecl diff --git a/src/Init/Lean/Meta/Tactic/Generalize.lean b/src/Init/Lean/Meta/Tactic/Generalize.lean new file mode 100644 index 0000000000..c86a6811ec --- /dev/null +++ b/src/Init/Lean/Meta/Tactic/Generalize.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.KAbstract +import Init.Lean.Meta.Tactic.Util + +namespace Lean +namespace Meta + +def generalize (mvarId : MVarId) (e : Expr) (x : Name) : MetaM MVarId := do +withMVarContext mvarId $ do + checkNotAssigned mvarId `generalize; + tag ← getMVarTag mvarId; + target ← getMVarType mvarId; + target ← instantiateMVars target; + targetAbst ← kabstract target e; + unless targetAbst.hasLooseBVars $ + throwTacticEx `generalize mvarId ("failed to find expression in the target"); + eType ← inferType e; + let targetNew := Lean.mkForall x BinderInfo.default eType targetAbst; + unlessM (isTypeCorrect targetNew) $ + throwTacticEx `generalize mvarId ("result is not type correct"); + mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag; + assignExprMVar mvarId (mkApp mvarNew e); + pure mvarNew.mvarId! + +end Meta +end Lean diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean index 723b82e9f3..59c269c10e 100644 --- a/src/Init/Lean/Meta/Tactic/Intro.lean +++ b/src/Init/Lean/Meta/Tactic/Intro.lean @@ -68,8 +68,8 @@ def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do (fvarIds, mvarId) ← introN mvarId 1 [name]; pure (fvarIds.get! 0, mvarId) -def intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := do -(fvarIds, mvarId) ← introN mvarId 1 []; +def intro1 (mvarId : MVarId) (useUnusedNames := true) : MetaM (FVarId × MVarId) := do +(fvarIds, mvarId) ← introN mvarId 1 [] useUnusedNames; pure (fvarIds.get! 0, mvarId) end Meta diff --git a/src/Init/Lean/Meta/Tactic/LocalDecl.lean b/src/Init/Lean/Meta/Tactic/LocalDecl.lean new file mode 100644 index 0000000000..eb51efce3c --- /dev/null +++ b/src/Init/Lean/Meta/Tactic/LocalDecl.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.AppBuilder +import Init.Lean.Meta.Tactic.Util +import Init.Lean.Meta.Tactic.Assert +import Init.Lean.Meta.Tactic.Intro +import Init.Lean.Meta.Tactic.Clear + +namespace Lean +namespace Meta + +def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (newType : Expr) (eqProof : Expr) : MetaM (FVarId × MVarId) := do +withMVarContext mvarId $ do + localDecl ← getLocalDecl fvarId; + newTypePr ← mkEqMP eqProof (mkFVar fvarId); + mvarId ← assert mvarId localDecl.userName newType newTypePr; + (fvarIdNew, mvarId) ← intro1 mvarId; + (do mvarId ← clear mvarId fvarId; pure (fvarIdNew, mvarId)) <|> pure (fvarIdNew, mvarId) + +end Meta +end Lean diff --git a/src/Init/Lean/Meta/Tactic/Rewrite.lean b/src/Init/Lean/Meta/Tactic/Rewrite.lean index b9776de78e..a5c8f7c795 100644 --- a/src/Init/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Init/Lean/Meta/Tactic/Rewrite.lean @@ -40,7 +40,7 @@ withMVarContext mvarId $ do eEqE ← mkEq e e; let eEqEAbst := mkApp eEqE.appFn! eAbst; let motive := Lean.mkLambda `_a BinderInfo.default α eEqEAbst; - unlessM (withAtLeastTransparency TransparencyMode.default $ isTypeCorrect motive) $ + unlessM (isTypeCorrect motive) $ throwTacticEx `rewrite mvarId ("motive is not type correct"); eqRefl ← mkEqRefl e; eqPrf ← mkEqNDRec motive eqRefl heq; diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean index 0eb31ad85b..154eacfb25 100644 --- a/src/Init/Lean/Meta/Tactic/Util.lean +++ b/src/Init/Lean/Meta/Tactic/Util.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Lean.Meta.Basic +import Init.Lean.Meta.LevelDefEq namespace Lean namespace Meta @@ -36,6 +37,11 @@ mctx ← getMCtx; opts ← getOptions; pure $ ppGoal env mctx opts mvarId +@[inline] protected def orelse{α} (x y : MetaM α) : MetaM α := do +s ← get; catch x (fun _ => do restore s.env s.mctx s.postponed; y) + +instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩ + @[init] private def regTraceClasses : IO Unit := registerTraceClass `Meta.Tactic