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

feat: support for _ and ?hole at all induction/cases variants

Browse source 
This commit also improves error position.
This commit is contained in:
Leonardo de Moura 2020-11-03 17:11:33 -08:00
parent 730b6aa3a3
commit 29730157ff
4 changed files with 206 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

93
src/Lean/Elab/Tactic/Induction.lean
View file

@ -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 <eliminator-name>')"
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

81
tests/lean/inductionErrors.lean Normal file
View file

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

30
tests/lean/inductionErrors.lean.expected.out Normal file
View file

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

41
tests/lean/run/casesUsing.lean
View file

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