From 360cebf68002c0c56902cefe658401851e64b59e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2020 11:18:02 -0700
Subject: [PATCH] fix: `induction` tactic must check expected major premise
 type

`whnfUntil` now returns `Option Expr`.
---
 src/Init/Lean/Meta/Tactic/Induction.lean | 7 +++++--
 src/Init/Lean/Meta/WHNF.lean             | 6 ++++--
 tests/lean/run/induction1.lean           | 7 +++++++
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/Meta/Tactic/Induction.lean b/src/Init/Lean/Meta/Tactic/Induction.lean
index 70b9608204..5f7712b494 100644
--- a/src/Init/Lean/Meta/Tactic/Induction.lean
+++ b/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
diff --git a/src/Init/Lean/Meta/WHNF.lean b/src/Init/Lean/Meta/WHNF.lean
index e72f32e412..8d79fc56e6 100644
--- a/src/Init/Lean/Meta/WHNF.lean
+++ b/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
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index 15407ef668..0e37260fc3 100644
--- a/tests/lean/run/induction1.lean
+++ b/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