feat: unfolding induction theorems to unfold bif (#8301)

This PR unfolds functions in the unfolding induction principle properly
when they use `bif` (a.k.a. `Bool.cond`).

src/Lean/Meta/Tactic/FunInd.lean

@@ -605,8 +605,7 @@ def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
         expr := f
         proof? := (mkAppN (mkConst ``if_neg us) #[c, h, hc, α, t, f])
       }
-    else
-      return { expr := e}
+    return { expr := e}
   | dite@dite α c h t f =>
     let us := dite.constLevels!
     if (← isDefEq c (← inferType hc)) then
@@ -619,10 +618,22 @@ def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
         expr := f.beta #[hc]
         proof? := (mkAppN (mkConst ``dif_neg us) #[c, h, hc, α, t, f])
       }
-    else
-      return { expr := e }
+    return { expr := e }
+  | cond@cond α c t f =>
+    let us := cond.constLevels!
+    if (← isDefEq (← inferType hc) (← mkEq c (mkConst ``Bool.true))) then
+      return {
+        expr := t
+        proof? := (mkAppN (mkConst ``Bool.cond_pos us) #[α, c, t, f, hc])
+      }
+    if (← isDefEq (← inferType hc) (← mkEq c (mkConst ``Bool.false))) then
+      return {
+        expr := f
+        proof? := (mkAppN (mkConst ``Bool.cond_neg us) #[α, c, t, f, hc])
+      }
+    return { expr := e }
   | _ =>
-      return { expr := e }
+    return { expr := e }
 
 def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
   if e.isLet then
@@ -764,12 +775,14 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
   | cond _α c t f =>
     let c' ← foldAndCollect oldIH newIH isRecCall c
-    let t' ← withLocalDecl `h .default (← mkEq c' (toExpr true)) fun h => M2.branch do
-      let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
+    let t' ← withLocalDecl `h .default (← mkEq c' (mkConst ``Bool.true)) fun h => M2.branch do
+      let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall t
+      mkLambdaFVars #[h] t'
+    let f' ← withLocalDecl `h .default (← mkEq c' (mkConst ``Bool.false)) fun h => M2.branch do
+      let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
+        buildInductionBody toErase toClear goal' oldIH newIH isRecCall f
       mkLambdaFVars #[h] t'
-    let f' ← withLocalDecl `h .default (← mkEq c' (toExpr false)) fun h => M2.branch do
-      let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
-      mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp4 (mkConst ``Bool.dcond [u]) goal c' t' f'
   | _ =>

tests/lean/run/funind_unfolding.lean

@@ -537,3 +537,24 @@ info: duplicatedDiscriminant.fun_cases_unfolding (motive : Nat → Bool → Prop
 -/
 #guard_msgs(pass trace, all) in
 #check duplicatedDiscriminant.fun_cases_unfolding
+
+set_option linter.unusedVariables false in
+def with_bif_tailrec : Nat → Nat
+  | 0 => 0
+  | n+1 =>
+    bif n % 2 == 0 then
+      with_bif_tailrec n
+    else
+      with_bif_tailrec (n-1)
+termination_by n => n
+
+/--
+info: with_bif_tailrec.induct_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0)
+  (case2 : ∀ (n : Nat), (n % 2 == 0) = true → motive n (with_bif_tailrec n) → motive n.succ (with_bif_tailrec n))
+  (case3 :
+    ∀ (n : Nat),
+      (n % 2 == 0) = false → motive (n - 1) (with_bif_tailrec (n - 1)) → motive n.succ (with_bif_tailrec (n - 1)))
+  (a✝ : Nat) : motive a✝ (with_bif_tailrec a✝)
+-/
+#guard_msgs in
+#check with_bif_tailrec.induct_unfolding