max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add introNP and intro1P

Browse source 
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`.
This commit is contained in:
Leonardo de Moura 2020-09-18 12:35:25 -07:00
parent 02e6f019c4
commit 12aabcb731
10 changed files with 48 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -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

6
src/Lean/Elab/Tactic/Generalize.lean
View file

@ -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

4
src/Lean/Meta/Match/CaseValues.lean
View file

@ -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;

4
src/Lean/Meta/Tactic/Assert.lean
View file

@ -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)))
{};

4
src/Lean/Meta/Tactic/Cases.lean
View file

@ -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,

8
src/Lean/Meta/Tactic/Induction.lean
View file

@ -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);

4
src/Lean/Meta/Tactic/Injection.lean
View file

@ -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) []

38
src/Lean/Meta/Tactic/Intro.lean
View file

@ -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

2
src/Lean/Meta/Tactic/Replace.lean
View file

@ -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

4
src/Lean/Meta/Tactic/Subst.lean
View file

@ -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);