From 2001e1708f6bc051345f06aa8a9841e5a1f85793 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2020 13:47:27 -0800 Subject: [PATCH] feat: add support for `cases h_1:e_1, ..., h_n:e_n using elim` --- src/Lean/Elab/Tactic/Induction.lean | 88 +++++++++++++++-------------- tests/lean/run/casesUsing.lean | 30 ++++++++++ 2 files changed, 76 insertions(+), 42 deletions(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 3cfd749a0f..eb36a475c4 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -30,8 +30,8 @@ private def getAltRHS (alt : Syntax) : Syntax := alt[3] namespace ElimApp structure Context := - (elimInfo : ElimInfo) - (targetTerms : Array Syntax) -- targets provided by the user + (elimInfo : ElimInfo) + (targets : Array Expr) -- targets provided by the user structure State := (argPos : Nat := 0) -- current argument position @@ -54,13 +54,6 @@ private def getBindingName : M Name := return (← get).fType.bindingName! /- Return the next argument expected type. This method assumes `fType` is a function type. -/ private def getArgExpectedType : M Expr := return (← get).fType.bindingDomain! -private def elabNextTarget : M Unit := do - unless (← get).targetPos < (← read).targetTerms.size do - throwError! "invalid 'eliminate', insufficient number of targets" - let target ← Term.elabTerm (← read).targetTerms[(← get).targetPos] (← getArgExpectedType) - modify fun s => { s with targetPos := s.targetPos + 1 } - addNewArg target - private def getFType : M Expr := do let fType ← whnfForall (← get).fType modify fun s => { s with fType := fType } @@ -70,7 +63,7 @@ structure Result := (elimApp : Expr) (alts : Array (Name × MVarId) := #[]) -partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targetTerms : Array Syntax) (tag : Name) : TermElabM Result := do +partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do let rec loop : M Unit := do match (← getFType) with | Expr.forallE binderName _ _ c => @@ -81,7 +74,15 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targetTerms : Arr addNewArg motive else if ctx.elimInfo.targetsPos.contains argPos then if c.binderInfo.isExplicit then - elabNextTarget + let s ← get + let ctx ← read + unless s.targetPos < ctx.targets.size do + throwError! "invalid 'eliminate', insufficient number of targets" + let target := ctx.targets[s.targetPos] + let expectedType ← getArgExpectedType + let target ← Term.ensureHasType expectedType target + modify fun s => { s with targetPos := s.targetPos + 1 } + addNewArg target else let target ← mkFreshExprMVar (← getArgExpectedType) addNewArg target @@ -102,7 +103,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targetTerms : Arr pure () let f ← Term.mkConst elimName let fType ← inferType f - let (_, s) ← loop.run { elimInfo := elimInfo, targetTerms := targetTerms } $.run { f := f, fType := fType } + let (_, s) ← loop.run { elimInfo := elimInfo, targets := targets } $.run { f := f, fType := fType } Lean.Elab.Term.synthesizeAppInstMVars s.instMVars pure { elimApp := (← instantiateMVars s.f), alts := s.alts } @@ -408,21 +409,20 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio done setGoals gs -private def generalizeMajor (major : Expr) : TacticM Expr := do - match major with - | Expr.fvar .. => pure major +private def generalizeTerm (term : Expr) : TacticM Expr := do + match term with + | Expr.fvar .. => pure term | _ => liftMetaTacticAux fun mvarId => do - mvarId ← Meta.generalize mvarId major `x false + mvarId ← Meta.generalize mvarId term `x false let (fvarId, mvarId) ← Meta.intro1 mvarId pure (mkFVar fvarId, [mvarId]) @[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focusAux do let targets := stx[1].getSepArgs if targets.size == 1 then - let target := targets[0] - let major ← withMainMVarContext $ elabTerm target none - let major ← generalizeMajor major + let major ← withMainMVarContext $ elabTerm targets[0] none + let major ← generalizeTerm major let n ← generalizeVars stx major let recInfo ← getRecInfo stx major let (mvarId, _) ← getMainGoal @@ -466,39 +466,43 @@ private def getTargetHypothesisName? (target : Syntax) : Option Name := private def getTargetTerm (target : Syntax) : Syntax := target[1] -private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do - match h? with - | none => withMainMVarContext $ elabTerm major none - | some h => withMainMVarContext do - let lctx ← getLCtx - let x ← mkFreshUserName `x - let major ← elabTerm major none - evalGeneralizeAux h? major x - withMainMVarContext do +private def elabTaggedTerm (h? : Option Name) (termStx : Syntax) : TacticM Expr := + withMainMVarContext $ withRef termStx do + let term ← elabTerm termStx none + match h? with + | none => pure term + | some h => let lctx ← getLCtx - match lctx.findFromUserName? x with - | some decl => pure decl.toExpr - | none => throwError "failed to generalize" + let x ← mkFreshUserName `x + evalGeneralizeAux h? term x + withMainMVarContext do + let lctx ← getLCtx + match lctx.findFromUserName? x with + | some decl => pure decl.toExpr + | none => throwError "failed to generalize" + +def elabTargets (targets : Array Syntax) : TacticM (Array Expr) := + targets.mapM fun target => do + let h? := getTargetHypothesisName? target + let term ← elabTaggedTerm h? (getTargetTerm target) + generalizeTerm term /- Default `cases` tactic that uses `casesOn` eliminator -/ -def evalCasesOn (target : Syntax) (withAlts : Syntax) : TacticM Unit := do - let h? := getTargetHypothesisName? target - let major ← elabMajor h? (getTargetTerm target) - let major ← generalizeMajor major +def evalCasesOn (target : Expr) (withAlts : Syntax) : TacticM Unit := do let (mvarId, _) ← getMainGoal - let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true - let result ← Meta.cases mvarId major.fvarId! recInfo.altVars + let (recInfo, ctorNames) ← getRecInfoDefault target withAlts true + let result ← Meta.cases mvarId target.fvarId! recInfo.altVars checkCasesResult result ctorNames recInfo.altRHSs let result := result.map (fun s => s.toInductionSubgoal) let altRHSs := recInfo.altRHSs.filter fun stx => !stx.isMissing processResult altRHSs result -def evalCasesUsing (targets : Array Syntax) (elimName : Name) (withAlts : Syntax) : TacticM Unit := do +def evalCasesUsing (elimName : Name) (targets : Array Expr) (withAlts : Syntax) : TacticM Unit := do let elimInfo ← getElimInfo elimName let (mvarId, _) ← getMainGoal let tag ← getMVarTag mvarId withMVarContext mvarId do - let result ← ElimApp.mkElimApp elimName elimInfo (targets.map (·[1])) tag + let result ← 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] @@ -511,14 +515,14 @@ def evalCasesUsing (targets : Array Syntax) (elimName : Name) (withAlts : Syntax @[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focusAux do -- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> withAlts - let targets := stx[1].getSepArgs + let targets ← elabTargets stx[1].getSepArgs let withAlts := stx[3] checkAlts withAlts if stx[2].isNone then unless targets.size == 1 do - throwErrorAt targets[1] "multiple targets are only supported when a user-defined eliminator is provided with 'using'" + throwErrorAt stx[1] "multiple targets are only supported when a user-defined eliminator is provided with 'using'" evalCasesOn targets[0] withAlts else - evalCasesUsing targets stx[2][1].getId withAlts + evalCasesUsing stx[2][1].getId targets withAlts end Lean.Elab.Tactic diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean index cfb96dde87..024023eb57 100644 --- a/tests/lean/run/casesUsing.lean +++ b/tests/lean/run/casesUsing.lean @@ -47,3 +47,33 @@ theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by apply Or.inr rw time2Eq rfl + +def ex4 {α} (xs : List α) (h : xs = [] → False) : α := by + cases he:xs + | nil => apply False.elim; exact h he; done + | cons x _ => exact x + +def ex5 {α} (xs : List α) (h : xs = [] → False) : α := by + cases he:xs using List.casesOn + | nil => apply False.elim; exact h he; done + | cons x _ => exact x + +theorem ex6 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := + match he:f xs with + | true => False.elim (h₂ (h₁ he)) + | false => rfl + +theorem ex7 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by + cases he:f xs + | true => exact False.elim (h₂ (h₁ he)) + | false => rfl + +theorem ex8 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by + cases he:f xs using Bool.casesOn + | true => exact False.elim (h₂ (h₁ he)) + | false => rfl + +theorem ex9 {α} (xs : List α) (h : xs = [] → False) : Nonempty α := by + cases xs using List.rec + | nil => apply False.elim; apply h; rfl + | cons x _ => apply Nonempty.intro; assumption