From 7b496bf44b990a250ff5844fda41ecd9ddff2881 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jan 2025 16:54:55 +0100 Subject: [PATCH] feat: improve `cases` tactic used in `grind` (#6516) This PR enhances the `cases` tactic used in the `grind` tactic and ensures that it can be applied to arbitrary expressions. --- src/Lean/Meta/Tactic/Cases.lean | 71 ++++++++++++++++++--------- src/Lean/Meta/Tactic/Grind/Cases.lean | 33 +++++++------ src/Lean/Meta/Tactic/Grind/Intro.lean | 2 +- tests/lean/run/grind_cases_tac.lean | 43 ++++++++++++++++ 4 files changed, 109 insertions(+), 40 deletions(-) create mode 100644 tests/lean/run/grind_cases_tac.lean diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index ecc00556bd19..56e8b8514a27 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -66,30 +66,31 @@ structure GeneralizeIndicesSubgoal where numEqs : Nat /-- - Similar to `generalizeTargets` but customized for the `casesOn` motive. - Given a metavariable `mvarId` representing the - ``` - Ctx, h : I A j, D |- T - ``` - where `fvarId` is `h`s id, and the type `I A j` is an inductive datatype where `A` are parameters, - and `j` the indices. Generate the goal - ``` - Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T - ``` - Remark: `(j == j' -> h == h')` is a "telescopic" equality. - Remark: `j` is sequence of terms, and `j'` a sequence of free variables. - The result contains the fields - - `mvarId`: the new goal - - `indicesFVarIds`: `j'` ids - - `fvarId`: `h'` id - - `numEqs`: number of equations in the target -/ -def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndicesSubgoal := +Given a metavariable `mvarId` representing the goal +``` +Ctx |- T +``` +and an expression `e : I A j`, where `I A j` is an inductive datatype where `A` are parameters, +and `j` the indices. Generate the goal +``` +Ctx, j' : J, h' : I A j' |- j == j' -> e == h' -> T +``` +Remark: `(j == j' -> e == h')` is a "telescopic" equality. +Remark: `j` is sequence of terms, and `j'` a sequence of free variables. +The result contains the fields +- `mvarId`: the new goal +- `indicesFVarIds`: `j'` ids +- `fvarId`: `h'` id +- `numEqs`: number of equations in the target + +If `varName?` is not none, it is used to name `h'`. +-/ +def generalizeIndices' (mvarId : MVarId) (e : Expr) (varName? : Option Name := none) : MetaM GeneralizeIndicesSubgoal := mvarId.withContext do let lctx ← getLCtx let localInsts ← getLocalInstances mvarId.checkNotAssigned `generalizeIndices - let fvarDecl ← fvarId.getDecl - let type ← whnf fvarDecl.type + let type ← whnfD (← inferType e) type.withApp fun f args => matchConstInduct f (fun _ => throwTacticEx `generalizeIndices mvarId "inductive type expected") fun val _ => do unless val.numIndices > 0 do throwTacticEx `generalizeIndices mvarId "indexed inductive type expected" unless args.size == val.numIndices + val.numParams do throwTacticEx `generalizeIndices mvarId "ill-formed inductive datatype" @@ -98,9 +99,10 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi let IAType ← inferType IA forallTelescopeReducing IAType fun newIndices _ => do let newType := mkAppN IA newIndices - withLocalDeclD fvarDecl.userName newType fun h' => + let varName ← if let some varName := varName? then pure varName else mkFreshUserName `x + withLocalDeclD varName newType fun h' => withNewEqs indices newIndices fun newEqs newRefls => do - let (newEqType, newRefl) ← mkEqAndProof fvarDecl.toExpr h' + let (newEqType, newRefl) ← mkEqAndProof e h' let newRefls := newRefls.push newRefl withLocalDeclD `h newEqType fun newEq => do let newEqs := newEqs.push newEq @@ -112,7 +114,7 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi let auxType ← mkForallFVars newIndices auxType let newMVar ← mkFreshExprMVarAt lctx localInsts auxType MetavarKind.syntheticOpaque tag /- assign mvarId := newMVar indices h refls -/ - mvarId.assign (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls) + mvarId.assign (mkAppN (mkApp (mkAppN newMVar indices) e) newRefls) let (indicesFVarIds, newMVarId) ← newMVar.mvarId!.introNP newIndices.size let (fvarId, newMVarId) ← newMVarId.intro1P return { @@ -122,6 +124,29 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi numEqs := newEqs.size } +/-- +Similar to `generalizeTargets` but customized for the `casesOn` motive. +Given a metavariable `mvarId` representing the +``` +Ctx, h : I A j, D |- T +``` +where `fvarId` is `h`s id, and the type `I A j` is an inductive datatype where `A` are parameters, +and `j` the indices. Generate the goal +``` +Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T +``` +Remark: `(j == j' -> h == h')` is a "telescopic" equality. +Remark: `j` is sequence of terms, and `j'` a sequence of free variables. +The result contains the fields +- `mvarId`: the new goal +- `indicesFVarIds`: `j'` ids +- `fvarId`: `h'` id +- `numEqs`: number of equations in the target -/ +def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndicesSubgoal := + mvarId.withContext do + let fvarDecl ← fvarId.getDecl + generalizeIndices' mvarId fvarDecl.toExpr fvarDecl.userName + structure CasesSubgoal extends InductionSubgoal where ctorName : Name diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index 9dd44b4f270e..d7e620f4497c 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -11,28 +11,29 @@ namespace Lean.Meta.Grind The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users. This method implements it. This tactic is automatically applied when introducing local declarations with a type tagged with `[grind_cases]`. +It is also used for "case-splitting" on terms during the search. + It differs from the user-facing Lean `cases` tactic in the following ways: - It avoids unnecessary `revert` and `intro` operations. - It does not introduce new local declarations for each minor premise. Instead, the `grind` tactic preprocessor is responsible for introducing them. -- It assumes that the major premise (i.e., the parameter `fvarId`) is the latest local declaration in the current goal. - - If the major premise type is an indexed family, auxiliary declarations and (heterogeneous) equalities are introduced. However, these equalities are not resolved using `unifyEqs`. Instead, the `grind` tactic employs union-find and congruence closure to process these auxiliary equalities. This approach avoids applying substitution to propositions that have already been internalized by `grind`. -/ -def cases (mvarId : MVarId) (fvarId : FVarId) : MetaM (List MVarId) := mvarId.withContext do +def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do let tag ← mvarId.getTag - let type ← whnf (← fvarId.getType) + let type ← whnf (← inferType e) let .const declName _ := type.getAppFn | throwInductiveExpected type let .inductInfo _ ← getConstInfo declName | throwInductiveExpected type let recursorInfo ← mkRecursorInfo (mkCasesOnName declName) - let k (mvarId : MVarId) (fvarId : FVarId) (indices : Array Expr) (clearMajor : Bool) : MetaM (List MVarId) := do - let recursor ← mkRecursorAppPrefix mvarId `grind.cases fvarId recursorInfo indices - let mut recursor := mkApp (mkAppN recursor indices) (mkFVar fvarId) + let k (mvarId : MVarId) (fvarId : FVarId) (indices : Array FVarId) : MetaM (List MVarId) := do + let indicesExpr := indices.map mkFVar + let recursor ← mkRecursorAppPrefix mvarId `grind.cases fvarId recursorInfo indicesExpr + let mut recursor := mkApp (mkAppN recursor indicesExpr) (mkFVar fvarId) let mut recursorType ← inferType recursor let mut mvarIdsNew := #[] for _ in [:recursorInfo.numMinors] do @@ -41,22 +42,22 @@ def cases (mvarId : MVarId) (fvarId : FVarId) : MetaM (List MVarId) := mvarId.wi recursorType := recursorTypeNew let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tag recursor := mkApp recursor mvar - let mvarIdNew ← if clearMajor then - mvar.mvarId!.clear fvarId - else - pure mvar.mvarId! + let mvarIdNew ← mvar.mvarId!.tryClearMany (indices.push fvarId) mvarIdsNew := mvarIdsNew.push mvarIdNew mvarId.assign recursor return mvarIdsNew.toList if recursorInfo.numIndices > 0 then - let s ← generalizeIndices mvarId fvarId + let s ← generalizeIndices' mvarId e s.mvarId.withContext do - k s.mvarId s.fvarId (s.indicesFVarIds.map mkFVar) (clearMajor := false) + k s.mvarId s.fvarId s.indicesFVarIds + else if let .fvar fvarId := e then + k mvarId fvarId #[] else - let indices ← getMajorTypeIndices mvarId `grind.cases recursorInfo type - k mvarId fvarId indices (clearMajor := true) + let mvarId ← mvarId.assert (← mkFreshUserName `x) type e + let (fvarId, mvarId) ← mvarId.intro1 + mvarId.withContext do k mvarId fvarId #[] where throwInductiveExpected {α} (type : Expr) : MetaM α := do - throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {mkFVar fvarId}{indentExpr type}" + throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {e}{indentExpr type}" end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean index 5c3c9da4e115..b0b60282b922 100644 --- a/src/Lean/Meta/Tactic/Grind/Intro.lean +++ b/src/Lean/Meta/Tactic/Grind/Intro.lean @@ -68,7 +68,7 @@ private def isCasesCandidate (type : Expr) : MetaM Bool := do private def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do if (← isCasesCandidate (← fvarId.getType)) then - let mvarIds ← cases goal.mvarId fvarId + let mvarIds ← cases goal.mvarId (mkFVar fvarId) return mvarIds.map fun mvarId => { goal with mvarId } else return none diff --git a/tests/lean/run/grind_cases_tac.lean b/tests/lean/run/grind_cases_tac.lean new file mode 100644 index 000000000000..c63200ab146b --- /dev/null +++ b/tests/lean/run/grind_cases_tac.lean @@ -0,0 +1,43 @@ +import Lean + +open Lean Meta Grind Elab Tactic in +elab "cases' " e:term : tactic => withMainContext do + let e ← elabTerm e none + setGoals (← Grind.cases (← getMainGoal) e) + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → Vec α n → Vec α (n+1) + +def f (v : Vec α n) : Bool := + match v with + | .nil => true + | .cons .. => false + +/-- +info: n : Nat +v : Vec Nat n +h : f v ≠ false +⊢ n + 1 = 0 → HEq (Vec.cons 10 v) Vec.nil → False +--- +info: n : Nat +v : Vec Nat n +h : f v ≠ false +⊢ ∀ {n_1 : Nat} (a : Nat) (a_1 : Vec Nat n_1), n + 1 = n_1 + 1 → HEq (Vec.cons 10 v) (Vec.cons a a_1) → False +-/ +#guard_msgs (info) in +example (v : Vec Nat n) (h : f v ≠ false) : False := by + cases' (Vec.cons 10 v) + next => trace_state; sorry + next => trace_state; sorry + +/-- +info: ⊢ False → False +--- +info: ⊢ True → False +-/ +#guard_msgs (info) in +example : False := by + cases' (Or.inr (a := False) True.intro) + next => trace_state; sorry + next => trace_state; sorry