From 12aabcb73171e98cea297f68c5e59b1e16c6c68f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Sep 2020 12:35:25 -0700 Subject: [PATCH] feat: add `introNP` and `intro1P` Versions of `introN` and `intro1` that preserve the binder name. They are used to implement the idiom: "revert", do something, re-"intro"-tuce Before this commit `introNP mvarId n` was `intro1 mvarId n [] false`. --- src/Lean/Elab/Tactic/ElabTerm.lean | 10 ++++---- src/Lean/Elab/Tactic/Generalize.lean | 6 ++--- src/Lean/Meta/Match/CaseValues.lean | 4 +-- src/Lean/Meta/Tactic/Assert.lean | 4 +-- src/Lean/Meta/Tactic/Cases.lean | 4 +-- src/Lean/Meta/Tactic/Induction.lean | 8 +++--- src/Lean/Meta/Tactic/Injection.lean | 4 +-- src/Lean/Meta/Tactic/Intro.lean | 38 ++++++++++++++++++---------- src/Lean/Meta/Tactic/Replace.lean | 2 +- src/Lean/Meta/Tactic/Subst.lean | 4 +-- 10 files changed, 48 insertions(+), 36 deletions(-) diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 5980c58f7e..8302df8715 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -109,17 +109,17 @@ withMVarContext mvarId $ do | Expr.fvar fvarId _ => pure fvarId | _ => do type ← inferType e; - let intro (userName : Name) (useUnusedNames : Bool) : TacticM FVarId := do { - (fvarId, mvarId) ← liftMetaM $ do { + let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do { + (fvarId, mvarId) ← liftMetaM do { mvarId ← Meta.assert mvarId userName type e; - Meta.intro1 mvarId useUnusedNames + Meta.intro1Core mvarId preserveBinderNames }; setGoals $ mvarId::others; pure fvarId }; match userName? with - | none => intro `h true - | some userName => intro userName false + | none => intro `h false + | some userName => intro userName true end Tactic end Elab diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean index 9bdba563bd..bb1923a0a5 100644 --- a/src/Lean/Elab/Tactic/Generalize.lean +++ b/src/Lean/Elab/Tactic/Generalize.lean @@ -30,7 +30,7 @@ let rfl := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e; let val := mkApp2 mvar' e rfl; assignExprMVar mvarId val; let mvarId' := mvar'.mvarId!; -(_, mvarId') ← Meta.introN mvarId' 2 [] false; +(_, mvarId') ← Meta.introNP mvarId' 2; pure [mvarId'] private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit := @@ -39,7 +39,7 @@ liftMetaTactic $ fun mvarId => do mvarDecl ← getMVarDecl mvarId; match mvarDecl.type with | Expr.forallE _ _ b _ => do - (_, mvarId) ← Meta.intro1 mvarId false; + (_, mvarId) ← Meta.intro1P mvarId; eType ← inferType e; u ← Meta.getLevel eType; let eq := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0); @@ -61,7 +61,7 @@ def evalGeneralizeAux (h? : Option Name) (e : Expr) (x : Name) : TacticM Unit := match h? with | none => liftMetaTactic $ fun mvarId => do mvarId ← Meta.generalize mvarId e x false; - (_, mvarId) ← Meta.intro1 mvarId false; + (_, mvarId) ← Meta.intro1P mvarId; pure [mvarId] | some h => evalGeneralizeWithEq h e x <|> evalGeneralizeFallback h e x diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean index fd067d2fb1..0423e4a06a 100644 --- a/src/Lean/Meta/Match/CaseValues.lean +++ b/src/Lean/Meta/Match/CaseValues.lean @@ -39,9 +39,9 @@ withMVarContext mvarId $ do elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag; val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]; assignExprMVar mvarId val; - (elseH, elseMVarId) ← intro1 elseMVar.mvarId! false; + (elseH, elseMVarId) ← intro1P elseMVar.mvarId!; let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal }; - (thenH, thenMVarId) ← intro1 thenMVar.mvarId! false; + (thenH, thenMVarId) ← intro1P thenMVar.mvarId!; let symm := false; let clearH := false; (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH; diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean index 622b1ac94a..b0b00ae45c 100644 --- a/src/Lean/Meta/Tactic/Assert.lean +++ b/src/Lean/Meta/Tactic/Assert.lean @@ -80,8 +80,8 @@ withMVarContext mvarId $ do let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar; let args := #[val] ++ args; assignExprMVar mvarId (mkAppN mvarNew args); - (fvarIdNew, mvarIdNew) ← intro1 mvarNew.mvarId! false; - (fvarIdsNew, mvarIdNew) ← introN mvarIdNew fvarIds.size [] false; + (fvarIdNew, mvarIdNew) ← intro1P mvarNew.mvarId!; + (fvarIdsNew, mvarIdNew) ← introNP mvarIdNew fvarIds.size; let subst := fvarIds.size.fold (fun i (subst : FVarSubst) => subst.insert (fvarIds.get! i) (mkFVar (fvarIdsNew.get! i))) {}; diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index e1a4dd173f..ff7016c56a 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -98,8 +98,8 @@ withMVarContext mvarId $ do newMVar ← mkFreshExprMVarAt lctx localInsts auxType MetavarKind.syntheticOpaque tag; /- assign mvarId := newMVar indices h refls -/ assignExprMVar mvarId (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls); - (indicesFVarIds, newMVarId) ← introN newMVar.mvarId! newIndices.size [] false; - (fvarId, newMVarId) ← intro1 newMVarId false; + (indicesFVarIds, newMVarId) ← introNP newMVar.mvarId! newIndices.size; + (fvarId, newMVarId) ← intro1P newMVarId; pure { mvarId := newMVarId, indicesFVarIds := indicesFVarIds, diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean index 5059238694..bbb76b18ba 100644 --- a/src/Lean/Meta/Tactic/Induction.lean +++ b/src/Lean/Meta/Tactic/Induction.lean @@ -99,8 +99,8 @@ private partial def finalizeAux recType ← getTypeBody mvarId recType mvar; -- Try to clear major premise from new goal mvarId' ← tryClear mvar.mvarId! major.fvarId!; - (fields, mvarId') ← introN mvarId' nparams minorGivenNames true; - (extra, mvarId') ← introN mvarId' nextra [] false; + (fields, mvarId') ← introN mvarId' nparams minorGivenNames; + (extra, mvarId') ← introNP mvarId' nextra; let subst := reverted.size.fold (fun i (subst : FVarSubst) => if i < indices.size + 1 then subst @@ -170,8 +170,8 @@ withMVarContext mvarId $ do -- Revert indices and major premise preserving variable order (reverted, mvarId) ← revert mvarId ((indices.map Expr.fvarId!).push majorFVarId) true; -- Re-introduce indices and major - (indices', mvarId) ← introN mvarId indices.size [] false; - (majorFVarId', mvarId) ← intro1 mvarId false; + (indices', mvarId) ← introNP mvarId indices.size; + (majorFVarId', mvarId) ← intro1P mvarId; -- Create FVarSubst with indices let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (mkFVar (indices'.get! i.val))); trace! `Meta.Tactic.induction ("after revert&intro" ++ Format.line ++ MessageData.ofGoal mvarId); diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index f4c91a2b28..0a67c02e49 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -62,7 +62,7 @@ withMVarContext mvarId $ do eq ← mkEq a b; mvarId ← assert mvarId decl.userName eq pr; mvarId ← clear mvarId fvarId; - (fvarId, mvarId) ← intro1 mvarId false; + (fvarId, mvarId) ← intro1P mvarId; pure (fvarId, mvarId) def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult @@ -73,7 +73,7 @@ def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM Inj (fvarId, mvarId) ← heqToEq mvarId fvarId; injectionIntro n mvarId (fvarIds.push fvarId) remainingNames | n+1, mvarId, fvarIds, [] => do - (fvarId, mvarId) ← intro1 mvarId true; + (fvarId, mvarId) ← intro1 mvarId; (fvarId, mvarId) ← heqToEq mvarId fvarId; injectionIntro n mvarId (fvarIds.push fvarId) [] diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 96970e9f18..f341433e0f 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -9,7 +9,7 @@ namespace Lean namespace Meta @[specialize] -partial def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → Name × σ) +private partial def introNImpAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → Name × σ) : Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId) | 0, lctx, fvars, j, _, type => let type := type.instantiateRevRange j fvars.size fvars; @@ -31,7 +31,7 @@ partial def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name let lctx := lctx.mkLetDecl fvarId n type val; let fvar := mkFVar fvarId; let fvars := fvars.push fvar; - introNCoreAux i lctx fvars j s body + introNImpAux i lctx fvars j s body | (i+1), lctx, fvars, j, s, Expr.forallE n type body c => do let type := type.instantiateRevRange j fvars.size fvars; let type := type.headBeta; @@ -40,40 +40,52 @@ partial def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo; let fvar := mkFVar fvarId; let fvars := fvars.push fvar; - introNCoreAux i lctx fvars j s body + introNImpAux i lctx fvars j s body | (i+1), lctx, fvars, j, s, type => let type := type.instantiateRevRange j fvars.size fvars; adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $ withNewLocalInstances fvars j $ do newType ← whnf type; if newType.isForall then - introNCoreAux (i+1) lctx fvars fvars.size s newType + introNImpAux (i+1) lctx fvars fvars.size s newType else throwTacticEx `introN mvarId "insufficient number of binders" -@[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array FVarId × MVarId) := +@[specialize] private def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array FVarId × MVarId) := withMVarContext mvarId $ do checkNotAssigned mvarId `introN; mvarType ← getMVarType mvarId; lctx ← getLCtx; - (fvars, mvarId) ← introNCoreAux mvarId mkName n lctx #[] 0 s mvarType; + (fvars, mvarId) ← introNImpAux mvarId mkName n lctx #[] 0 s mvarType; pure (fvars.map Expr.fvarId!, mvarId) -def mkAuxName (useUnusedNames : Bool) (lctx : LocalContext) (defaultName : Name) : List Name → Name × List Name -| [] => (if useUnusedNames then lctx.getUnusedName defaultName else defaultName, []) -| n :: rest => (if n != "_" then n else if useUnusedNames then lctx.getUnusedName defaultName else defaultName, rest) +private def mkAuxNameImp (preserveBinderNames : Bool) (lctx : LocalContext) (binderName : Name) : List Name → Name × List Name +| [] => (if preserveBinderNames then binderName else lctx.getUnusedName binderName, []) +| n :: rest => (if n != "_" then n else if preserveBinderNames then binderName else lctx.getUnusedName binderName, rest) -def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useUnusedNames := true) : MetaM (Array FVarId × MVarId) := +def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (preserveBinderNames : Bool) : MetaM (Array FVarId × MVarId) := if n == 0 then pure (#[], mvarId) -else introNCore mvarId n (mkAuxName useUnusedNames) givenNames +else introNImp mvarId n (mkAuxNameImp preserveBinderNames) givenNames + +abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array FVarId × MVarId) := +introNCore mvarId n givenNames false + +abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) := +introNCore mvarId n [] true 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) (useUnusedNames := true) : MetaM (FVarId × MVarId) := do -(fvarIds, mvarId) ← introN mvarId 1 [] useUnusedNames; +def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId) := do +(fvarIds, mvarId) ← introNCore mvarId 1 [] preserveBinderNames; pure (fvarIds.get! 0, mvarId) +abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := do +intro1Core mvarId false + +abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) := do +intro1Core mvarId true + end Meta end Lean diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index b6274a5576..8a7999b2b8 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -83,7 +83,7 @@ withMVarContext mvarId do }; let finalize (targetNew : Expr) : MetaM MVarId := do { mvarId ← replaceTargetDefEq mvarId targetNew; - (_, mvarId) ← introN mvarId (numReverted-1) [] false; + (_, mvarId) ← introNP mvarId (numReverted-1); pure mvarId }; match target with diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index ca8bf85a85..a9240b5e45 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -36,7 +36,7 @@ withMVarContext mvarId $ do throwTacticEx `subst mvarId ("'" ++ a ++ "' occurs at" ++ indentExpr b); aLocalDecl ← getLocalDecl aFVarId; (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true; - (twoVars, mvarId) ← introN mvarId 2 [] false; + (twoVars, mvarId) ← introNP mvarId 2; trace! `Meta.Tactic.subst ("reverted variables " ++ toString vars); let aFVarId := twoVars.get! 0; let a := mkFVar aFVarId; @@ -66,7 +66,7 @@ withMVarContext mvarId $ do clear mvarId aFVarId else pure mvarId; - (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false; + (newFVars, mvarId) ← introNP mvarId (vars.size - 2); fvarSubst ← newFVars.size.foldM (fun i (fvarSubst : FVarSubst) => let var := vars.get! (i+2);