[Merged by Bors] - feat: port split_ifs tactic

Mathlib.lean

@@ -142,6 +142,7 @@ import Mathlib.Tactic.SimpTrace
 import Mathlib.Tactic.Simps.Basic
 import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SolveByElim
+import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SudoSetOption

Mathlib/Mathport/Syntax.lean

@@ -318,8 +318,6 @@ syntax termList := " [" term,* "]"
 /- N -/ syntax (name := simpResult) "simp_result "
   (&"only ")? (simpArgs)? " => " tacticSeq : tactic
 
-/- M -/ syntax (name := splitIfs) "split_ifs" (ppSpace location)? (" with " binderIdent+)? : tactic
-
 /- S -/ syntax (name := suggest) "suggest" (config)? (ppSpace num)?
   (simpArgs)? (" using " (colGt binderIdent)+)? : tactic
 

Mathlib/Tactic/SplitIfs.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2018 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, David Renshaw
+-/
+import Lean
+import Mathlib.Init.Logic
+import Mathlib.Tactic.Core
+
+/-!
+Tactic to split if-then-else expressions.
+-/
+
+namespace Mathlib.Tactic
+
+open Lean Elab.Tactic Parser.Tactic Lean.Meta
+
+/-- Simulates the `<;>` tactic combinator.
+-/
+private def tac_and_then : TacticM Unit → TacticM Unit → TacticM Unit :=
+fun tac1 tac2 => focus do
+  tac1
+  allGoals tac2
+
+/-- A position where a split may apply.
+-/
+private inductive SplitPosition
+| target
+| hyp (fvarId: FVarId)
+
+/-- Collects a list of positions pointed to by `loc` and their types.
+-/
+private def getSplitCandidates (loc : Location) : TacticM (List (SplitPosition × Expr)) :=
+match loc with
+| Location.wildcard => do
+   let candidates ← (← getLCtx).getFVarIds.mapM
+     (fun fvarId => do
+       let typ ← instantiateMVars (← inferType (mkFVar fvarId))
+       return (SplitPosition.hyp fvarId, typ))
+   pure ((SplitPosition.target, ← getMainTarget) :: candidates.toList)
+| Location.targets hyps tgt => do
+   let candidates ← (← hyps.mapM getFVarId).mapM
+     (fun fvarId => do
+       let typ ← instantiateMVars (← inferType (mkFVar fvarId))
+       return (SplitPosition.hyp fvarId, typ))
+   if tgt
+   then return (SplitPosition.target, ← getMainTarget) :: candidates.toList
+   else return candidates.toList
+
+/-- Finds an if condition to split. If successful, returns the position and the condition.
+-/
+private def findIfCondAt (loc : Location) : TacticM (Option (SplitPosition × Expr)) := do
+  for (pos, e) in  (← getSplitCandidates loc) do
+    if let some cond := SplitIf.findIfToSplit? e
+    then return some (pos, cond)
+  return none
+
+/-- `Simp.Discharge` strategy to use in `reduceIfsAt`. Delegates to
+`SplitIf.discharge?`, and additionally supports discharging `True`, to
+better match the behavior of mathlib3's `split_ifs`.
+-/
+private def discharge? (e : Expr) : SimpM (Option Expr) := do
+  let e ← instantiateMVars e
+  if let some e1 ← SplitIf.discharge? false e
+    then return some e1
+  if e.isConstOf `True
+    then return some (mkConst `True.intro)
+  return none
+
+/-- Simplifies if-then-else expressions after cases have been split out.
+-/
+private def reduceIfsAt (loc : Location) : TacticM Unit := do
+  let ctx ← SplitIf.getSimpContext
+  let _ ← simpLocation ctx discharge? loc
+  pure ()
+
+/-- Splits a single if-then-else expression and then reduces the resulting goals.
+Has a similar effect as `SplitIf.splitIfTarget?` or `SplitIf.splitIfLocalDecl?` from
+core Lean 4. We opt not to use those library functions so that we can better mimic
+the behavior of mathlib3's `split_ifs`.
+-/
+private def splitIf1 (cond: Expr) (hName : Name) (loc : Location) : TacticM Unit := do
+  let splitCases := liftMetaTactic fun mvarId => do
+    let (s1, s2) ← mvarId.byCases cond hName
+    pure [s1.mvarId, s2.mvarId]
+  tac_and_then splitCases (reduceIfsAt loc)
+
+/-- Pops off the front of the list of names, or generates a fresh name if the
+list is empty.
+-/
+private def getNextName (hNames: IO.Ref (List Name)) : MetaM Name := do
+  match ←hNames.get with
+  | [] => mkFreshUserName `h
+  | n::ns => do hNames.set ns; pure n
+
+/-- 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)
+
+/-- Main loop of split_ifs. Pulls names for new hypotheses from `hNames`.
+Stops if it encounters a condition in the passed-in `List Expr`.
+-/
+private partial def splitIfsCore (loc : Location) (hNames : IO.Ref (List Name)) :
+  List Expr → TacticM Unit := fun done => do
+  let some (_,cond) ← findIfCondAt loc
+      | Meta.throwTacticEx `split_ifs (←getMainGoal) "no if-the-else conditions to split"
+
+  -- If `cond` is `¬p` then use `p` instead.
+  let cond := if cond.isAppOf `Not then cond.getAppArgs[0]! else cond
+
+  if done.contains cond then return ()
+  let no_split ← valueKnown cond
+  if no_split then
+    tac_and_then (reduceIfsAt loc) (splitIfsCore loc hNames (cond::done) <|> pure ())
+  else do
+    let hName ← getNextName hNames
+    tac_and_then (splitIf1 cond hName loc) ((splitIfsCore loc hNames (cond::done)) <|> pure ())
+
+/-- Splits all if-then-else-expressions into multiple goals.
+Given a goal of the form `g (if p then x else y)`, `split_ifs` will produce
+two goals: `p ⊢ g x` and `¬p ⊢ g y`.
+If there are multiple ite-expressions, then `split_ifs` will split them all,
+starting with a top-most one whose condition does not contain another
+ite-expression.
+`split_ifs at *` splits all ite-expressions in all hypotheses as well as the goal.
+`split_ifs with h₁ h₂ h₃` overrides the default names for the hypotheses.
+-/
+syntax (name := splitIfs) "split_ifs" (ppSpace location)? (" with " (colGt binderIdent)+)? : tactic
+
+elab_rules : tactic
+| `(tactic| split_ifs $[$loc:location]? $[with $withArg*]?) =>
+  let loc := match loc with
+  | none => Location.targets #[] true
+  | some loc => expandLocation loc
+  let names := match withArg with
+  | none => []
+  | some args => args.map (λ s => if let `(binderIdent| $x:ident) := s
+                                  then x.getId
+                                  else `_) |>.toList
+  withMainContext do
+    let names ← IO.mkRef names
+    splitIfsCore loc names []

test/SplitIfs.lean

@@ -0,0 +1,65 @@
+import Mathlib.Tactic.SplitIfs
+
+example (x : Nat) (p : Prop) [Decidable p] : x = if p then x else x := by
+  split_ifs with h1
+  · rfl
+  · rfl
+
+example (x y : Nat) (p : Prop) [Decidable p] (h : if p then x = y else y = x) : x = y := by
+  split_ifs at h
+  · exact h
+  · exact h.symm
+
+example (x : Nat) (p q : Prop) [Decidable p] [Decidable q] :
+    x = if p then (if q then x else x) else x := by
+  split_ifs
+  · rfl
+  · rfl
+  · rfl
+
+example (x : Nat) (p : Prop) [Decidable p] :
+    x = if (if p then False else True) then x else x := by
+  split_ifs
+  · rfl
+  · rfl
+  · rfl
+
+example (p : Prop) [Decidable p] : if if ¬p then p else True then p else ¬p := by
+  split_ifs with h1 h2
+  · assumption
+  · assumption
+
+example (p q : Prop) [Decidable p] [Decidable q] :
+    if if if p then ¬p else q then p else q then q else ¬p ∨ ¬q := by
+  split_ifs with h1 h2 h3
+  · exact h2
+  · exact Or.inr h2
+  · exact Or.inl h1
+  · exact Or.inr h3
+
+example (p : Prop) [Decidable p] (h : (if p then 1 else 2) > 3) : False := by
+  split_ifs at h
+  cases h
+  · case inl.step h => cases h
+  · case inr h =>
+    cases h
+    case step h =>
+      cases h
+      case step h => cases h
+
+example (p : Prop) [Decidable p] (x : Nat) (h : (if p then 1 else 2) > x) :
+     x < (if ¬p then 1 else 0) + 1 := by
+   split_ifs at * <;> assumption
+
+example (p : Prop) [Decidable p] : if if ¬p then p else True then p else ¬p := by
+  split_ifs <;>
+  assumption
+
+example (p q : Prop) [Decidable p] [Decidable q] :
+     if if if p then ¬p else q then p else q then q else ¬p ∨ ¬q := by
+  split_ifs <;>
+  simp [*]
+
+example : True := by
+  fail_if_success { split_ifs }
+  trivial