From 29730157ff16d7e0bd686d7bdfae88565d6893e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2020 17:11:33 -0800 Subject: [PATCH] feat: support for `_` and `?hole` at all `induction/cases` variants This commit also improves error position. --- src/Lean/Elab/Tactic/Induction.lean | 93 ++++++++++++-------- tests/lean/inductionErrors.lean | 81 +++++++++++++++++ tests/lean/inductionErrors.lean.expected.out | 30 +++++++ tests/lean/run/casesUsing.lean | 41 +++++++++ 4 files changed, 206 insertions(+), 39 deletions(-) create mode 100644 tests/lean/inductionErrors.lean create mode 100644 tests/lean/inductionErrors.lean.expected.out diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index b3d6f4f4fd..f5cce15e84 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -24,6 +24,25 @@ private def getAltName (alt : Syntax) : Name := alt[0].getId.eraseMacroScopes private def getAltVarNames (alt : Syntax) : Array Name := alt[1].getArgs.map Syntax.getId private def getAltRHS (alt : Syntax) : Syntax := alt[3] +-- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic +def isHoleRHS (rhs : Syntax) : Bool := + rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole + +def evalAltRhs (mvarId : MVarId) (rhs : Syntax) (remainingGoals : Array MVarId) : TacticM (Array MVarId) := do + if isHoleRHS rhs then + let gs' ← withMVarContext mvarId $ withRef rhs do + let mvarDecl ← getMVarDecl mvarId + let val ← elabTermEnsuringType rhs mvarDecl.type + assignExprMVar mvarId val + let gs' ← getMVarsNoDelayed val + tagUntaggedGoals mvarDecl.userName `induction gs'.toList + pure gs' + pure (remainingGoals ++ gs') + else + setGoals [mvarId] + closeUsingOrAdmit rhs + pure remainingGoals + /- Helper method for creating an user-defined eliminator/recursor application. -/ @@ -77,7 +96,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E let s ← get let ctx ← read unless s.targetPos < ctx.targets.size do - throwError! "invalid 'eliminate', insufficient number of targets" + throwError! "insufficient number of targets for '{elimName}'" let target := ctx.targets[s.targetPos] let expectedType ← getArgExpectedType let target ← Term.ensureHasType expectedType target @@ -124,8 +143,16 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N return altInfo.numFields throwError! "unknown alternative name '{altName}'" +private def checkAltNames (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax) : TacticM Unit := + for altStx in altsSyntax do + let altName := getAltName altStx + if altName != `_ then + unless alts.any fun (n, _) => n == altName do + throwErrorAt! altStx "invalid alternative name '{altName}'" + def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax) (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do + checkAltNames alts altsSyntax let usedWildcard := false let hasAlts := altsSyntax.size > 0 let subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here @@ -158,18 +185,19 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax : subgoals := subgoals.push altMVarId else throwError! "alternative '{altName}' has not been provided" - | some altStx => withRef altStx do - let altRhs := getAltRHS altStx - let altVarNames := getAltVarNames altStx - let (_, altMVarId) ← introN altMVarId numFields altVarNames.toList - match (← Cases.unifyEqs numEqs altMVarId {}) with - | none => throwError! "alternative '{altName}' is not needed" - | some (altMVarId, _) => - let (_, altMVarId) ← introNP altMVarId numGeneralized - for fvarId in toClear do - altMVarId ← tryClear altMVarId fvarId - setGoals [altMVarId] - closeUsingOrAdmit altRhs + | some altStx => + subgoals ← withRef altStx do + let altRhs := getAltRHS altStx + let altVarNames := getAltVarNames altStx + let (_, altMVarId) ← introN altMVarId numFields altVarNames.toList + match (← Cases.unifyEqs numEqs altMVarId {}) with + | none => throwError! "alternative '{altName}' is not needed" + | some (altMVarId, _) => + let (_, altMVarId) ← introNP altMVarId numGeneralized + for fvarId in toClear do + altMVarId ← tryClear altMVarId fvarId + withRef altStx[2] do -- use `=>` position to report errors + evalAltRhs altMVarId altRhs subgoals if usedWildcard then altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_ unless altsSyntax.isEmpty do @@ -378,17 +406,13 @@ private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRe throwErrorAt remainingAlts[0] "unused alternative" pure { recName := recName, altVars := altVars, altRHSs := altRHSs } --- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic -def isHoleRHS (rhs : Syntax) : Bool := - rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.hole - private def processResult (altRHSs : Array Syntax) (result : Array Meta.InductionSubgoal) (numToIntro : Nat := 0) : TacticM Unit := do if altRHSs.isEmpty then setGoals $ result.toList.map fun s => s.mvarId else unless altRHSs.size == result.size do throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})" - let gs := [] + let gs := #[] for i in [:result.size] do let subgoal := result[i] let rhs := altRHSs[i] @@ -396,20 +420,8 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio let mvarId := subgoal.mvarId if numToIntro > 0 then (_, mvarId) ← introNP mvarId numToIntro - if isHoleRHS rhs then - let gs' ← withMVarContext mvarId $ withRef rhs do - let mvarDecl ← getMVarDecl mvarId - let val ← elabTermEnsuringType rhs mvarDecl.type - assignExprMVar mvarId val - let gs' ← getMVarsNoDelayed val - let gs' := gs'.toList - tagUntaggedGoals mvarDecl.userName `induction gs' - pure gs' - gs := gs ++ gs' - else - setGoals [mvarId] - closeUsingOrAdmit rhs - setGoals gs + gs ← evalAltRhs mvarId rhs gs + setGoals gs.toList private def generalizeTerm (term : Expr) : TacticM Expr := do match term with @@ -433,12 +445,14 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do else if stx[2].isNone then throwError! "eliminator must be provided when multiple targets are used (use 'using ')" - let elimName := stx[2][1].getId - let elimInfo ← getElimInfo elimName + let elimId := stx[2][1] + let elimName := elimId.getId + let elimInfo ← withRef elimId do getElimInfo elimName let (mvarId, _) ← getMainGoal let tag ← getMVarTag mvarId withMVarContext mvarId do - let result ← ElimApp.mkElimApp elimName elimInfo targets tag + let result ← withRef stx[1] do -- use target position as reference + ElimApp.mkElimApp elimName elimInfo targets tag assignExprMVar mvarId result.elimApp let elimArgs := result.elimApp.getAppArgs let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i] @@ -513,12 +527,13 @@ def evalCasesOn (target : Expr) (withAlts : Syntax) : TacticM Unit := do let altRHSs := recInfo.altRHSs.filter fun stx => !stx.isMissing processResult altRHSs result -def evalCasesUsing (elimName : Name) (targets : Array Expr) (withAlts : Syntax) : TacticM Unit := do - let elimInfo ← getElimInfo elimName +def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr) (withAlts : Syntax) : TacticM Unit := do + let elimName := elimId.getId + let elimInfo ← withRef elimId do getElimInfo elimName let (mvarId, _) ← getMainGoal let tag ← getMVarTag mvarId withMVarContext mvarId do - let result ← ElimApp.mkElimApp elimName elimInfo targets tag + let result ← withRef targetRef $ ElimApp.mkElimApp elimName elimInfo targets tag let elimArgs := result.elimApp.getAppArgs let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i] let motiveType ← inferType elimArgs[elimInfo.motivePos] @@ -539,6 +554,6 @@ def evalCasesUsing (elimName : Name) (targets : Array Expr) (withAlts : Syntax) throwErrorAt stx[1] "multiple targets are only supported when a user-defined eliminator is provided with 'using'" evalCasesOn targets[0] withAlts else - evalCasesUsing stx[2][1].getId targets withAlts + evalCasesUsing stx[2][1] (targetRef := stx[1]) targets withAlts end Lean.Elab.Tactic diff --git a/tests/lean/inductionErrors.lean b/tests/lean/inductionErrors.lean new file mode 100644 index 0000000000..32b3038cb7 --- /dev/null +++ b/tests/lean/inductionErrors.lean @@ -0,0 +1,81 @@ +universes u + +axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat) + (diag : (a : Nat) → motive a a) + (upper : (delta a : Nat) → motive a (a + delta.succ)) + (lower : (delta a : Nat) → motive (a + delta.succ) a) + : motive y x + +theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | lower d => apply Or.inl -- Error + | upper d => apply Or.inr -- Error + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx2 -- Error + | lower d => apply Or.inl + | upper d => apply Or.inr + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex3 (p q : Nat) : p ≤ q ∨ p > q := by + cases p /- Error -/ using elimEx + | lower d => apply Or.inl + | upper d => apply Or.inr + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex4 (p q : Nat) : p ≤ q ∨ p > q := by + cases p using Nat.add -- Error + | lower d => apply Or.inl + | upper d => apply Or.inr + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex5 (x : Nat) : 0 + x = x := by + match x with + | 0 => done -- Error + | y+1 => done -- Error + +theorem ex5b (x : Nat) : 0 + x = x := by + cases x + | zero => done -- Error + | succ y => done -- Error + +inductive Vec : Nat → Type + | nil : Vec 0 + | cons : Bool → {n : Nat} → Vec n → Vec (n+1) + +theorem ex6 (x : Vec 0) : x = Vec.nil := by + cases x using Vec.casesOn + | nil => rfl + | cons => done -- Error + +theorem ex7 (x : Vec 0) : x = Vec.nil := by + cases x -- Error: TODO: improve error location + | nil => rfl + | cons => done + +theorem ex8 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | lower d => apply Or.inl; admit + | upper2 /- Error -/ d => apply Or.inr + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex9 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | lower d => apply Or.inl; admit + | _ => apply Or.inr; admit + | diag => apply Or.inl; apply Nat.leRefl + +theorem ex10 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | lower d => apply Or.inl; admit + | upper d => apply Or.inr; admit + | diag => apply Or.inl; apply Nat.leRefl + | _ /- error unused -/ => admit + +theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | lower d => apply Or.inl; admit + | upper d => apply Or.inr; admit + | lower d /- error unused -/ => apply Or.inl; admit + | diag => apply Or.inl; apply Nat.leRefl diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out new file mode 100644 index 0000000000..43b988707e --- /dev/null +++ b/tests/lean/inductionErrors.lean.expected.out @@ -0,0 +1,30 @@ +inductionErrors.lean:12:12: error: unsolved goals +case upper +q d : Nat +⊢ q + Nat.succ d > q +inductionErrors.lean:11:12: error: unsolved goals +case lower +p d : Nat +⊢ p ≤ p + Nat.succ d +inductionErrors.lean:16:19: error: unknown constant 'elimEx2' +inductionErrors.lean:22:8: error: insufficient number of targets for 'elimEx' +inductionErrors.lean:28:16: error: unexpected eliminator resulting type + Nat +inductionErrors.lean:35:11: error: unsolved goals +x : Nat +⊢ 0 + 0 = 0 +inductionErrors.lean:36:11: error: unsolved goals +x y : Nat +⊢ 0 + (y + 1) = y + 1 +inductionErrors.lean:40:14: error: unsolved goals +case zero +⊢ 0 + Nat.zero = Nat.zero +inductionErrors.lean:41:14: error: unsolved goals +case succ +y : Nat +⊢ 0 + Nat.succ y = Nat.succ y +inductionErrors.lean:50:4: error: alternative 'cons' is not needed +inductionErrors.lean:53:2: error: alternative for 'Vec.cons' is not needed +inductionErrors.lean:60:4: error: invalid alternative name 'upper2' +inductionErrors.lean:74:4: error: unused alternative +inductionErrors.lean:80:4: error: unused alternative diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean index 88e7b73e47..ee49770b8d 100644 --- a/tests/lean/run/casesUsing.lean +++ b/tests/lean/run/casesUsing.lean @@ -91,3 +91,44 @@ theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by have heq := Nat.modEqOfLt hgt rw [← heq] at hgt assumption + +theorem ex11 {p q : Prop } (h : p ∨ q) : q ∨ p := by + induction h using Or.casesOn + | inr h => ?myright + | inl h => ?myleft + case myleft => exact Or.inr h + case myright => exact Or.inl h + +theorem ex12 {p q : Prop } (h : p ∨ q) : q ∨ p := by + cases h using Or.casesOn + | inr h => ?myright + | inl h => ?myleft + case myleft => exact Or.inr h + case myright => exact Or.inl h + +theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | diag => ?hdiag + | lower d => ?hlower + | upper d => ?hupper + case hdiag => apply Or.inl; apply Nat.leRefl + case hlower => apply Or.inl; show p ≤ p + d.succ; admit + case hupper => apply Or.inr; show q + d.succ > q; admit + +theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | diag => ?hdiag + | lower d => _ + | upper d => ?hupper + case hdiag => apply Or.inl; apply Nat.leRefl + case lower => apply Or.inl; show p ≤ p + d.succ; admit + case hupper => apply Or.inr; show q + d.succ > q; admit + +theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by + cases p, q using elimEx + | diag => ?hdiag + | lower d => _ + | upper d => ?hupper + { apply Or.inl; apply Nat.leRefl } + { apply Or.inr; show q + d.succ > q; admit } + { apply Or.inl; show p ≤ p + d.succ; admit }