fix: induction tactic must check expected major premise type

`whnfUntil` now returns `Option Expr`.

src/Init/Lean/Meta/Tactic/Induction.lean

@@ -127,13 +127,16 @@ recType ← inferType rec;
 let numMinors := recInfo.produceMotive.length;
 finalizeAux mvarId givenNames recInfo reverted major initialArity indices numMinors baseSubst (recInfo.paramsPos.length + 1) 0 rec recType false #[]
 
+private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) : MetaM α :=
+throwTacticEx `induction mvarId ("unexpected major premise type " ++ indentExpr majorType)
+
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recName : Name) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) :
     MetaM (Array InductionSubgoal) :=
 withMVarContext mvarId $ do
   checkNotAssigned mvarId `induction;
   majorLocalDecl ← getLocalDecl majorFVarId;
   recInfo ← mkRecursorInfo recName;
-  majorType ← whnfUntil majorLocalDecl.type recInfo.typeName;
+  some majorType ← whnfUntil majorLocalDecl.type recInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type;
   majorType.withApp $ fun _ majorTypeArgs => do
     recInfo.paramsPos.forM $ fun paramPos? => do {
       match paramPos? with
@@ -179,7 +182,7 @@ withMVarContext mvarId $ do
       target ← getMVarType mvarId;
       targetLevel ← getLevel target;
       majorLocalDecl ← getLocalDecl majorFVarId;
-      majorType ← whnfUntil majorLocalDecl.type recInfo.typeName;
+      some majorType ← whnfUntil majorLocalDecl.type recInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type;
       majorType.withApp $ fun majorTypeFn majorTypeArgs => do
         match majorTypeFn with
         | Expr.const majorTypeFnName majorTypeFnLevels _ => do

src/Init/Lean/Meta/WHNF.lean

@@ -160,8 +160,10 @@ match e.getAppFn with
 def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
 whnfHeadPredAux pred e
 
-def whnfUntil (e : Expr) (declName : Name) : MetaM Expr :=
-whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e
+def whnfUntil (e : Expr) (declName : Name) : MetaM (Option Expr) := do
+e ← whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e;
+if e.isAppOf declName then pure e
+else pure none
 
 def getStuckMVar? (e : Expr) : MetaM (Option MVarId) :=
 WHNF.getStuckMVar? getConst whnf e

tests/lean/run/induction1.lean

@@ -90,3 +90,10 @@ begin
   induction h₁ using Iff.elim with
   | _ h _ => exact h h₂
 end
+
+theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q :=
+begin
+  failIfSuccess (induction h₁ using Iff.elim);
+  induction h₂ using Iff.elim with
+  | _ h _ => exact h h₃
+end