From 8d47e8be3b7e95a213c2f1eb9f9707cd1c93bc08 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Nov 2020 18:28:26 -0800
Subject: [PATCH] feat: add basic `cases ... using ...` methods

---
 src/Lean/Elab/Tactic/Induction.lean | 107 +++++++++++++++++++++++++++-
 1 file changed, 106 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 2f3b929fe1..099e7fd6b0 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -5,8 +5,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Meta.RecursorInfo
 import Lean.Meta.CollectMVars
+import Lean.Meta.Tactic.ElimInfo
 import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
+import Lean.Elab.App
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Generalize
 
@@ -321,6 +323,109 @@ def evalCasesOn (target : Syntax) (withAlts : Syntax) : TacticM Unit := do
   let altRHSs := recInfo.altRHSs.filter fun stx => !stx.isMissing
   processResult altRHSs result
 
+/- `cases ... using ...` -/
+namespace CasesUsing
+
+structure Context :=
+  (elimInfo   : ElimInfo)
+  (targetsStx : Array Syntax) -- targets provided by the user
+
+structure State :=
+  (argPos    : Nat := 0) -- current argument position
+  (targetPos : Nat := 0) -- current target at targetsStx
+  (f         : Expr)
+  (fType     : Expr)
+  (alts      : Array (Name × Expr) := #[])
+  (instMVars : Array MVarId := #[])
+
+abbrev M := ReaderT Context $ StateRefT State TermElabM
+
+private def addInstMVar (mvarId : MVarId) : M Unit :=
+  modify fun s => { s with instMVars := s.instMVars.push mvarId }
+
+private def addNewArg (arg : Expr) : M Unit :=
+  modify fun s => { s with argPos := s.argPos+1, f := mkApp s.f arg, fType := s.fType.bindingBody!.instantiate1 arg }
+
+/- Return the binder name at `fType`. This method assumes `fType` is a function type. -/
+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).targetsStx.size do
+    throwError! "invalid 'eliminate', insufficient number of targets"
+  let target ← Term.elabTerm (← read).targetsStx[(← 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 }
+  pure fType
+
+structure Result :=
+  (elim : Expr)
+  (alts : Array (Name × Expr) := #[])
+
+partial def processArgs (elimName : Name) (elimInfo : ElimInfo) (targetsStx : Array Syntax) : TermElabM Result := do
+  let rec loop : M Unit := do
+    match (← getFType) with
+    | Expr.forallE binderName _ _ c =>
+      let ctx ← read
+      let argPos := (← get).argPos
+      if ctx.elimInfo.motivePos == argPos then
+        let motive ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.syntheticOpaque
+        addNewArg motive
+      else if ctx.elimInfo.targetsPos.contains argPos then
+        if c.binderInfo.isExplicit then
+          elabNextTarget
+        else
+          let target ← mkFreshExprMVar (← getArgExpectedType)
+          addNewArg target
+      else match c.binderInfo with
+        | BinderInfo.implicit =>
+          let arg ← mkFreshExprMVar (← getArgExpectedType)
+          addNewArg arg
+        | BinderInfo.instImplicit =>
+          let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+          addInstMVar arg.mvarId!
+          addNewArg arg
+        | _ =>
+          let alt ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.syntheticOpaque
+          modify fun s => { s with alts := s.alts.push (← getBindingName, alt) }
+          addNewArg alt
+      loop
+    | _ =>
+      pure ()
+  let f ← Term.mkConst elimName
+  let fType ← inferType f
+  let (_, s) ← loop.run { elimInfo := elimInfo, targetsStx := targetsStx } $.run { f := f, fType := fType }
+  Lean.Elab.Term.synthesizeAppInstMVars s.instMVars
+  let elim ← instantiateMVars s.f
+  pure { elim := elim, alts := s.alts }
+
+def eval (targets : Array Syntax) (elimName : Name) (withAlts : Syntax) : TacticM Unit := do
+  let elimInfo ← getElimInfo elimName
+  let (mvarId, rest) ← getMainGoal
+  withMVarContext mvarId do
+    let result ← processArgs elimName elimInfo (targets.map (·[0][1]))
+    let elimArgs := result.elim.getAppArgs
+    let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
+    let motiveType ← inferType elimArgs[elimInfo.motivePos]
+    let mvarId ← generalizeTargets mvarId motiveType targets
+    let (targetsNew, mvarId) ← introN mvarId targets.size
+    withMVarContext mvarId do
+      let type ← inferType (mkMVar mvarId)
+      let motive ← mkLambdaFVars (targetsNew.map mkFVar) type
+      let motiverInferredType ← inferType motive
+      unless (← isDefEqGuarded motiverInferredType motiveType) do
+        throwError! "type mismatch when assigning motive{indentExpr motive}\nhas type{indentExpr motiverInferredType}\nexpected type{indentExpr motiveType}"
+      assignExprMVar elimArgs[elimInfo.motivePos].mvarId! motive
+      -- TODO
+      setGoals (mvarId :: rest)
+
+end CasesUsing
+
 @[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
@@ -329,6 +434,6 @@ def evalCasesOn (target : Syntax) (withAlts : Syntax) : TacticM Unit := do
       throwErrorAt targets[1] "multiple targets are only supported when a user-defined eliminator is provided with 'using'"
     evalCasesOn targets[0] stx[3]
   else
-    throwUnsupportedSyntax
+    CasesUsing.eval targets stx[2][1].getId stx[3]
 
 end Lean.Elab.Tactic