From efc3a320fef291a078aef98480687cb19f47dbaa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Nov 2020 14:33:19 -0800
Subject: [PATCH] chore: prepare to fix ambiguity at `induction/cases` notation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

@Kha I was writing the following example
```
  ...
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih => cases h
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```
The current `syntax` assumes the `| cons b bs ih => ...` alternative
is part of the first `cases h`. Forcing the `|` to occur in a column
>= of the corresponding `cases` is not a nice solution since it would
preven us from writing the second `cases` as I wrote it above.
That is we would have to write
```
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih =>
    cases h
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```
or
```
  induction as
  | nil          => cases h -- `h` is an empty type
  | cons b bs ih => cases h
                    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
                    | tail a b bs h1 => ...
```
I think the best solution is to use `with` when we have explicit
alternatives with `|`. The new syntax is similar to `match ... with | ...`
That is, we would write
```
  ...
  induction as with
  | nil          => cases h
  | cons b bs ih => cases h with
    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
    | tail a b bs h1 => ...
```
---
 src/Lean/Elab/Tactic/Induction.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 5163585b26..9b883ad6fe 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -240,7 +240,10 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[1].getSepArgs
+  if inductionAlts.getNumArgs == 2 then
+    inductionAlts[1].getSepArgs -- TODO remove
+  else
+    inductionAlts[2].getSepArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]