Merge branch 'slice' into port/CategoryTheory.Equivalence

Mathlib/Tactic/Core.lean

@@ -7,7 +7,7 @@ import Std.Tactic.Simpa
 import Mathlib.Lean.Expr
 
 /-!
-# 
+#
 
 Generally useful tactics.
 
@@ -142,40 +142,37 @@ def iterateAtMost : Nat → m Unit → m Unit
 
 /-- `iterateExactly' n t` executes `t` `n` times. If any iteration fails, the whole tactic fails.
 -/
-def iterateExactly' : Nat → m Unit → m Unit 
-| 0, _ => pure () 
+def iterateExactly' : Nat → m Unit → m Unit
+| 0, _ => pure ()
 | n+1, tac => tac *> iterateExactly' n tac
 
 /--
 `iterateRange m n t`: Repeat the given tactic at least `m` times and
 at most `n` times or until `t` fails. Fails if `t` does not run at least `m` times.
 -/
-def iterateRange : Nat → Nat → m Unit → m Unit 
+def iterateRange : Nat → Nat → m Unit → m Unit
 | 0, 0, _   => pure ()
 | 0, b, tac => iterateAtMost b tac
-| (a+1), n, tac => do 
-  let _ ← tac 
-  let _ ← iterateRange a (n-1) tac 
-  pure ()
+| (a+1), n, tac => do tac; iterateRange a (n-1) tac
 
 /-- Repeats a tactic until it fails. Always succeeds. -/
 partial def iterateUntilFailure (tac : m Unit) : m Unit :=
   try tac; iterateUntilFailure tac catch _ => pure ()
 
-/-- `iterateUntilFailureWithResults` is a helper tactic which returns the results of `tac`'s 
-iterative application along the lines of `iterateUntilFailure`. Always succeeds.
+/-- `iterateUntilFailureWithResults` is a helper tactic which accumulates the list of results
+obtained from iterating `tac` until it fails. Always succeeds.
 -/
-partial def iterateUntilFailureWithResults {α : Type} (tac : TacticM α) : TacticM (List α) := do
+partial def iterateUntilFailureWithResults {α : Type} (tac : m α) : m (List α) := do
   try
     let a ← tac
     let l ← iterateUntilFailureWithResults tac
     pure (a :: l)
   catch _ => pure []
 
-/-- `iterateUntilFailureCount` is similiar to `iterateUntilFailure` except it counts 
-the number of successful calls to `tac`. Always succeeds. 
+/-- `iterateUntilFailureCount` is similar to `iterateUntilFailure` except it counts
+the number of successful calls to `tac`. Always succeeds.
 -/
-def iterateUntilFailureCount {α : Type} (tac : TacticM α) : TacticM Nat := do
+def iterateUntilFailureCount {α : Type} (tac : m α) : m Nat := do
   let r ← iterateUntilFailureWithResults tac
   return r.length
 

Mathlib/Tactic/Slice.lean

@@ -10,12 +10,11 @@ import Mathlib.Tactic.Conv
 /-!
 # The `slice` tactic
 
-Applies a tactic to an interval of terms from a term obtained by repeated application 
-of `Category.comp`. 
+Applies a tactic to an interval of terms from a term obtained by repeated application
+of `Category.comp`.
 
 -/
 
-
 open CategoryTheory
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta
 
@@ -27,13 +26,20 @@ open Tactic
 open Parser.Tactic.Conv
 
 /--
-`evalSlice` 
-- rewrites the target express using `Category.assoc`. 
+`slice` is a conv tactic; if the current focus is a composition of several morphisms,
+`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.
+Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
+ -/
+syntax (name := slice) "slice " num num : conv
+
+/--
+`evalSlice`
+- rewrites the target expression using `Category.assoc`.
 - uses `congr` to split off the first `a-1` terms and rotates to `a`-th (last) term
-- it counts the number `k` of rewrites as it uses `←Category.assoc` to bring the target to 
+- counts the number `k` of rewrites as it uses `←Category.assoc` to bring the target to
   left associated form; from the first step this is the total number of remaining terms from `C`
-- it now splits off `b-a` terms from target using `congr` leaving the desired subterm 
-- finally, it rewrites it once more using `Category.assoc` to bring it right associated 
+- it now splits off `b-a` terms from target using `congr` leaving the desired subterm
+- finally, it rewrites it once more using `Category.assoc` to bring it to right-associated
   normal form
 -/
 def evalSlice (a b : Nat) : TacticM Unit := do
@@ -49,25 +55,25 @@ def evalSlice (a b : Nat) : TacticM Unit := do
   let _ ← iterateUntilFailureWithResults do
     evalTactic (← `(conv| rw [Category.assoc]))
 
-/-- `slice` is implemented by `evalSlice` -/
-elab "slice" a:num b:num : conv => evalSlice a.getNat b.getNat
+/-- `slice` is implemented by `evalSlice`. -/
+elab "slice " a:num b:num : conv => evalSlice a.getNat b.getNat
 
-/-- 
-`sliceLHS a b => tac` is a conv tactic which enters the LHS of a target, 
-uses `slice` to extract the `a` through `b` terms, and then applies 
-`tac` to the result. 
+/--
+`slice_lhs a b => tac` zooms to the left hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
 -/
-syntax (name := sliceLHS) "sliceLHS" num num " => " convSeq : tactic
+syntax (name := sliceLHS) "slice_lhs " num num " => " convSeq : tactic
 macro_rules
-  | `(tactic| sliceLHS $a $b => $seq) =>
+  | `(tactic| slice_lhs $a $b => $seq) =>
     `(tactic| conv => lhs; slice $a $b; ($seq:convSeq))
 
 /--
-`sliceRHS a b => tac` works as `sliceLHS` but on the RHS similarly
+`slice_rhs a b => tac` zooms to the right hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
 -/
-syntax (name := sliceRHS) "sliceRHS" num num " => " convSeq : tactic
+syntax (name := sliceRHS) "slice_rhs " num num " => " convSeq : tactic
 macro_rules
-  | `(tactic| sliceRHS $a $b => $seq) =>
+  | `(tactic| slice_rhs $a $b => $seq) =>
     `(tactic| conv => rhs; slice $a $b; ($seq:convSeq))
 
 /- Porting note: update when `add_tactic_doc` is supported` -/

test/slice.lean

@@ -13,3 +13,9 @@ example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫
     lhs
     slice 1 1
     rw [h₁]
+
+example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫ l := by
+  slice_lhs 1 1 => rw [h₁]
+
+example (h₁ : f₁ = f₂) : ((f₂ ≫ g) ≫ h) ≫ l = f₁ ≫ g ≫ h ≫ l := by
+  slice_rhs 1 1 => rw [h₁]