split_ifs

Stream: mathlib4

[Dan Velleman]

Can someone explain these examples:

import Mathlib.tactic

example (u : Nat) (h : u = u) : (if u = u then 0 else 1) = 0 := by
  split_ifs
  rfl
  done

example (u : Nat) : (if u = u then 0 else 1) = 0 := by
  have h : u = u := by rfl
  split_ifs
  rfl; rfl
  done

In the first proof, after the split_ifs the goal is 0 = 0, and rfl completes the proof. In the second proof, after split_ifs there are two 0 = 0 goals, one with the additional hypothesis u = u and one with the additional hypothesis ¬u = u, so one needs two invocations of rfl to complete the proof. Why the difference? The tactic state when split_ifs is invoked appears to be the same in the two examples.

[Jireh Loreaux]

This seems like a missing withMainContext in the implementation of split_ifs to me, but I'm not super knowledgable about these things.

[Jireh Loreaux]

If you do show_term split_ifs you can see the difference in what it produces.

[Ruben Van de Velde]

I think split_ifs looks for hypotheses that match the condition to avoid creating pointless subgoals

[Jireh Loreaux]

Right, but it should have found it in the second example, unless it didn't get the new context after the have

[Ruben Van de Velde]

Oh sorry, I missed the have

[Jireh Loreaux]

@David Renshaw since you ported this tactic, maybe you see the problem here? It's not immediately obvious to me.

[Damiano Testa]

Exceedingly often, weird tactic behaviour after have is due to the presence of metadata introduced by the have.

[Damiano Testa]

A quick look at the tactic makes me wonder whether there are a couple of whnfR missing in getSplitCandidates, around the getMainTargets, but I'm not at a computer to be able to check.

[David Renshaw]

This makes the behavior of the two versions match:

diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean
index d41c91ddab..7a408e2004 100644
--- a/Mathlib/Tactic/SplitIfs.lean
+++ b/Mathlib/Tactic/SplitIfs.lean
@@ -102,9 +102,11 @@ private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : Me
 -/
 private def valueKnown (cond : Expr) : TacticM Bool := do
   let hTypes ← (((← getLCtx).getFVarIds.map mkFVar).mapM inferType : MetaM _)
-  let hTypes := hTypes.toList
   let not_cond := mkApp (mkConst `Not) cond
-  return (hTypes.contains cond) || (hTypes.contains not_cond)
+  for ht in hTypes do
+    if ← isDefEq cond ht then return true
+    if ← isDefEq not_cond ht then return true
+  return false

[David Renshaw]

(and causes some breakage in mathlib)

[David Renshaw]

Just doing instantiateMVars seems to works better...

[David Renshaw]

diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean
index d41c91ddab..13d9944826 100644
--- a/Mathlib/Tactic/SplitIfs.lean
+++ b/Mathlib/Tactic/SplitIfs.lean
@@ -101,10 +101,12 @@ private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : Me
 /-- Returns `true` if the condition or its negation already appears as a hypothesis.
 -/
 private def valueKnown (cond : Expr) : TacticM Bool := do
-  let hTypes ← (((← getLCtx).getFVarIds.map mkFVar).mapM inferType : MetaM _)
-  let hTypes := hTypes.toList
   let not_cond := mkApp (mkConst `Not) cond
-  return (hTypes.contains cond) || (hTypes.contains not_cond)
+  for h in ← getLocalHyps do
+    let ty ← instantiateMVars (← inferType h)
+    if cond == ty then return true
+    if not_cond == ty then return true
+  return false

[David Renshaw]

I opened a pull request with a fix:
#13916