feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) (#…

…15735)

Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>

src/tactic/cache.lean

@@ -48,8 +48,8 @@ by its variant `haveI` described below.
 
 * `substI`: like `subst`, but can also substitute in type-class arguments
 
-* `haveI`/`letI`: `have`/`let` followed by `resetI`. Used to add typeclasses
-  to the context so that they can be used in typeclass inference.
+* `haveI`/`letI`/`rsufficesI`: `have`/`let`/`rsuffices` followed by `resetI`. Used
+  to add typeclasses to the context so that they can be used in typeclass inference.
 
 * `exactI`: `resetI` followed by `exact`. Like `exact`, but uses all
   variables in the context for typeclass inference.

src/tactic/rcases.lean

@@ -945,5 +945,34 @@ add_tactic_doc
   decl_names := [`tactic.interactive.obtain],
   tags       := ["induction"] }
 
+/--
+The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage
+of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain`
+on the expression, and then `rotate 1`.
+-/
+meta def rsuffices (h : parse obtain_parse) : tactic unit :=
+focus1 $ obtain h >> tactic.rotate 1
+
+add_tactic_doc
+{ name       := "rsuffices",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.rsuffices],
+  tags       := ["induction"] }
+
+/--
+The `rsufficesI` tactic is an instance-cache aware version of `rsuffices`; it resets the instance
+cache on the resulting goals.
+-/
+
+meta def rsufficesI (h : parse obtain_parse) : tactic unit :=
+rsuffices h ; resetI
+
+add_tactic_doc
+{ name       := "rsufficesI",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.rsufficesI],
+  tags       := ["induction", "type class"] }
+
+
 end interactive
 end tactic

test/rcases.lean

@@ -240,3 +240,114 @@ example {α n} (h : foo α n) : true := by test_rcases_hint "_ | ⟨n, h_ᾰ⟩"
 
 example {α} (V : set α) (h : ∃ p, p ∈ (V.foo V) ∩ (V.foo V)) :=
 by test_rcases_hint "⟨⟨h_w_fst, h_w_snd⟩, ⟨⟩⟩" 0
+
+section rsuffices
+
+/-- These next few are duplicated from `rcases/obtain` tests, with the goal order swapped. -/
+
+example : true :=
+begin
+  rsuffices ⟨n : ℕ, h : n = n, -⟩ : ∃ n : ℕ, n = n ∧ true,
+  { guard_hyp n : ℕ,
+    guard_hyp h : n = n,
+    success_if_fail {assumption},
+    trivial },
+  { existsi 0, simp },
+end
+
+example : true :=
+begin
+  rsuffices : ∃ n : ℕ, n = n ∧ true,
+  { trivial },
+  { existsi 0, simp },
+end
+
+example : true :=
+begin
+  rsuffices (h : true) | ⟨⟨⟩⟩ : true ∨ false,
+  { guard_hyp h : true,
+    trivial },
+  { left, trivial },
+end
+
+example : true :=
+begin
+  success_if_fail {rsuffices ⟨h, h2⟩},
+  trivial
+end
+
+example (x y : α × β) : true :=
+begin
+  rsuffices ⟨⟨a, b⟩, c, d⟩ : (α × β) × (α × β),
+  { guard_hyp a : α,
+    guard_hyp b : β,
+    guard_hyp c : α,
+    guard_hyp d : β,
+    trivial },
+  { exact ⟨x, y⟩ }
+end
+
+-- This test demonstrates why `swap` is not used in the implementation of `rsuffices`:
+-- it would make the _second_ goal the one requiring ⟨x, y⟩, not the last one.
+example (x y : α ⊕ β) : true :=
+begin
+  rsuffices ⟨a|b, c|d⟩ : (α ⊕ β) × (α ⊕ β),
+  { guard_hyp a : α, guard_hyp c : α, trivial },
+  { guard_hyp a : α, guard_hyp d : β, trivial },
+  { guard_hyp b : β, guard_hyp c : α, trivial },
+  { guard_hyp b : β, guard_hyp d : β, trivial },
+  exact ⟨x, y⟩,
+end
+
+example {α} (V : set α) (w : true → ∃ p, p ∈ (V.foo V) ∩ (V.foo V)) : true :=
+begin
+  rsuffices ⟨a, h⟩ : ∃ p, p ∈ (V.foo V) ∩ (V.foo V),
+  { trivial },
+  { exact w trivial },
+end
+
+-- Now some tests that ensure that things stay in the correct order.
+
+-- This test demonstrates why `focus1` is required in the definition of `rsuffices`; otherwise
+-- the `∃ ...` goal would get put _after_ the `true` goal.
+example : nonempty ℕ ∧ true :=
+begin
+  split,
+  rsuffices ⟨n : ℕ, hn⟩ : ∃ n, _,
+  { exact ⟨n⟩ },
+  { exact true },
+  { exact ⟨0, trivial⟩ },
+  { trivial },
+end
+
+section instances
+
+example (h : Π {α}, inhabited α) : inhabited (α ⊕ β) :=
+begin
+  rsufficesI (ha | hb) : inhabited α ⊕ inhabited β,
+  { exact ⟨sum.inl default⟩ },
+  { exact ⟨sum.inr default⟩ },
+  { exact sum.inl h }
+end
+
+include β
+-- this test demonstrates that the `resetI` also applies onto the goal.
+example (h : Π {α}, inhabited α) : inhabited α :=
+begin
+  have : inhabited β := h,
+  rsufficesI t : β,
+  { exact h },
+  { exact default }
+end
+
+example (h : Π {α}, inhabited α) : β :=
+begin
+  rsufficesI ht : inhabited β,
+  { guard_hyp ht : inhabited β,
+    exact default },
+  { exact h }
+end
+
+end instances
+
+end rsuffices