feat: FunInd: omit cases proved by contradiction (#8171)

This PR omits cases from functional induction/cases principles that are
implemented `by contradiction` (or, more generally, `False.elim`,
`absurd` or `noConfusion). Breaking change in the sense that there are
fewer goals to prove after using functional induction.

Fixes #8103.

src/Lean/Meta/Tactic/FunInd.lean

@@ -203,6 +203,11 @@ something goes wrong, one still gets a useful induction principle, just maybe wi
 not fully simplified.
 -/
 
+register_builtin_option backward.funind.contradiction : Bool := {
+  defValue := true
+  descr    := "omit cases by contradiction (temporary bootstrap option)"
+}
+
 set_option autoImplicit false
 
 namespace Lean.Tactic.FunInd
@@ -719,6 +724,28 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     return mkApp4 (mkConst ``Bool.dcond [u]) goal c' t' f'
   | _ =>
 
+
+  -- Check for unreachable cases. We look for the kind of expressions that `by contradiction`
+  -- produces
+  if backward.funind.contradiction.get (← getOptions) then
+    match_expr e with
+    | False.elim _ h => do
+      return ← mkFalseElim goal h
+    | absurd _ _ h₁ h₂ => do
+      return ← mkAbsurd goal h₁ h₂
+    | _ => pure ()
+    if e.isApp && e.getAppFn.isConst && isNoConfusion (← getEnv) e.getAppFn.constName! then
+      let arity := (← inferType e.getAppFn).getNumHeadForalls -- crucially not reducing the noConfusionType in the type
+      let h := e.getArg! (arity - 1)
+      let hType ← inferType h
+      -- The following duplicates a bit of code from the contradiction tactic, maybe worth extracting
+      -- into a common helper at some point
+      if let some (_, lhs, rhs) ← matchEq? hType then
+        if let some lhsCtor ← matchConstructorApp? lhs then
+        if let some rhsCtor ← matchConstructorApp? rhs then
+        if lhsCtor.name != rhsCtor.name then
+          return (← mkNoConfusion goal h)
+
   -- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction
   match_expr goal with
   | And goal₁ goal₂ => match_expr e with

src/Std/Data/DTreeMap/Internal/Balancing.lean

@@ -7,6 +7,10 @@ prelude
 import Init.Data.AC
 import Std.Data.DTreeMap.Internal.Balanced
 
+-- Temporary bootstrapping fix
+#guard_msgs(drop error) in
+set_option backward.funind.contradiction false
+
 /-!
 # Balancing operations
 

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/issue7550.lean

@@ -30,11 +30,6 @@ termination_by structural fuel
 /--
 error: tactic 'fail' failed
 case case1
-x y fuel x✝ : Nat
-hfuel✝ : x✝ < 0
-⊢ Bug.divCore x✝ y 0 hfuel✝ = 42
-
-case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : 0 < y ∧ y ≤ x✝
@@ -42,7 +37,7 @@ this✝ : x✝ - y < x✝
 ih1✝ : Bug.divCore (x✝ - y) y fuel✝ ⋯ = 42
 ⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
 
-case case3
+case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : ¬(0 < y ∧ y ≤ x✝)
@@ -56,11 +51,6 @@ protected theorem divCore_eq_div : Bug.divCore x y fuel h = 42 := by
 /--
 error: tactic 'fail' failed
 case case1
-x y fuel x✝ : Nat
-hfuel✝ : x✝ < 0
-⊢ Bug.divCore x✝ y 0 hfuel✝ = 42
-
-case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : 0 < y ∧ y ≤ x✝
@@ -68,7 +58,7 @@ this✝ : x✝ - y < x✝
 ih1✝ : Bug.divCore (x✝ - y) y fuel✝ ⋯ = 42
 ⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
 
-case case3
+case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : ¬(0 < y ∧ y ≤ x✝)

tests/lean/run/issue8103.lean

@@ -0,0 +1,111 @@
+def foo (n m : Nat) (h : n < m) : Nat :=
+  match m with
+  | 0 => by contradiction -- This case should not show up in the principles below
+  | m+1 => match n with
+    | 0 => 0
+    | n+1 => foo n m (Nat.succ_lt_succ_iff.mp h)
+
+/--
+info: foo.induct (motive : (n m : Nat) → n < m → Prop) (case1 : ∀ (m : Nat) (h : 0 < m + 1), 0 < m.succ → motive 0 m.succ h)
+  (case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
+  (h : n < m) : motive n m h
+-/
+#guard_msgs in
+#check foo.induct
+
+/--
+info: foo.induct_unfolding (motive : (n m : Nat) → n < m → Nat → Prop)
+  (case1 : ∀ (m : Nat) (h : 0 < m + 1), 0 < m.succ → motive 0 m.succ h 0)
+  (case2 :
+    ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ (foo n m ⋯) → motive n.succ m.succ h (foo n m ⋯))
+  (n m : Nat) (h : n < m) : motive n m h (foo n m h)
+-/
+#guard_msgs in
+#check foo.induct_unfolding
+
+
+/--
+info: foo.fun_cases (motive : (n m : Nat) → n < m → Prop)
+  (case1 : ∀ (m : Nat) (h : 0 < m + 1), 0 < m + 1 → 0 < m.succ → motive 0 m.succ h)
+  (case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m + 1 → n.succ < m.succ → motive n.succ m.succ h) (n m : Nat)
+  (h : n < m) : motive n m h
+-/
+#guard_msgs in
+#check foo.fun_cases
+
+def bar (n m : Nat) (h : n = m) : Nat :=
+  match m with
+  | 0 => 0
+  | m+1 => match n with
+    | 0 => by contradiction
+    | n+1 => bar n m (Nat.succ.inj h)
+
+/--
+info: bar.induct (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h : 0 = 0), motive 0 0 h)
+  (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
+  (h : n = m) : motive n m h
+-/
+#guard_msgs in
+#check bar.induct
+
+/--
+info: bar.induct_unfolding (motive : (n m : Nat) → n = m → Nat → Prop) (case1 : ∀ (h : 0 = 0), motive 0 0 h 0)
+  (case2 :
+    ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ (bar n m ⋯) → motive n.succ m.succ h (bar n m ⋯))
+  (n m : Nat) (h : n = m) : motive n m h (bar n m h)
+-/
+#guard_msgs in
+#check bar.induct_unfolding
+
+/--
+info: bar.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h : 0 = 0), motive 0 0 h)
+  (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
+  (h : n = m) : motive n m h
+-/
+#guard_msgs in
+#check bar.fun_cases
+
+def baz (n : Nat) (h : n ≠ 0) : Nat :=
+  match n with
+  | 0 => by contradiction
+  | k + 1 => if h : k = 0 then 0 else baz k h
+
+
+/--
+info: baz.induct (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 + 1 ≠ 0), motive (Nat.succ 0) h)
+  (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 → motive k.succ h) (n : Nat) (h : n ≠ 0) :
+  motive n h
+-/
+#guard_msgs in
+#check baz.induct
+
+/--
+info: baz.induct_unfolding (motive : (n : Nat) → n ≠ 0 → Nat → Prop) (case1 : ∀ (h : 0 + 1 ≠ 0), motive (Nat.succ 0) h 0)
+  (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 (baz k h_1) → motive k.succ h (baz k h_1)) (n : Nat)
+  (h : n ≠ 0) : motive n h (baz n h)
+-/
+#guard_msgs in
+#check baz.induct_unfolding
+
+/--
+info: baz.fun_cases (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 + 1 ≠ 0), Nat.succ 0 ≠ 0 → motive (Nat.succ 0) h)
+  (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0), ¬k = 0 → k.succ ≠ 0 → motive k.succ h) (n : Nat) (h : n ≠ 0) : motive n h
+-/
+#guard_msgs in
+#check baz.fun_cases
+
+
+def mean (n m : Nat) (h : n = m) : Nat :=
+  match m with
+  | 0 => 0
+  | m+1 => match n with
+    | 0 => (by contradiction : Bool → Nat) true -- overapplied `noConfusion`
+    | n+1 => Nat.noConfusion h fun h' => mean n m h' -- non-contradictory `noConfusion`
+
+/--
+info: mean.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h : 0 = 0), motive 0 0 h)
+  (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
+  (h : n = m) : motive n m h
+-/
+#guard_msgs in
+#check mean.fun_cases