feat(library/init): new repeat tactic

doc/changes.md

@@ -42,6 +42,11 @@ master branch (aka work in progress branch)
 
 *Changes*
 
+- `repeat { t }` behavior changed. Now, it applies `t` to each goal. If the application succeeds,
+  the tactic is applied recursively to all the generated subgoals until it eventually fails.
+  The recursion stops in a subgoal when the tactic has failed to make progress.
+  The previous `repeat` tactic was renamed to `iterate`.
+
 - Remove `[simp]` attribute from lemmas `or.assoc`, `or.comm`, `or.left_comm`, `and.assoc`, `and.comm`, `and.left_comm`, `add_assoc`, `add_comm`, `add_left_com`, `mul_assoc`, `mul_comm` and `mul_left_comm`.
   These lemmas were being used to "sort" arguments of AC operators: and, or, (+) and (*).
   This was producing unstable proofs. The old behavior can be retrieved by using the commands `local attribute [simp] ...` or `attribute [simp] ...` in the affected files.

library/init/meta/interactive.lean

@@ -604,6 +604,15 @@ tactic.contradiction
 meta def iterate : itactic → tactic unit :=
 tactic.iterate
 
+/--
+`repeat { t }` applies `t` to each goal. If the application succeeds,
+the tactic is applied recursively to all the generated subgoals until it eventually fails.
+The recursion stops in a subgoal when the tactic has failed to make progress.
+The tactic `repeat { t }` never fails.
+-/
+meta def repeat : itactic → tactic unit :=
+tactic.repeat
+
 /--
 `try { t }` tries to apply tactic `t`, but succeeds whether or not `t` succeeds.
 -/

library/init/meta/tactic.lean

@@ -727,6 +727,24 @@ do ng ← num_goals,
 meta def rotate : nat → tactic unit :=
 rotate_left
 
+private meta def repeat_aux (t : tactic unit) : list expr → list expr → tactic unit
+| []      r := set_goals r.reverse
+| (g::gs) r := do
+  ok ← try_core (set_goals [g] >> t),
+  match ok with
+  | none := repeat_aux gs (g::r)
+  | _    := do
+    gs' ← get_goals,
+    repeat_aux (gs' ++ gs) r
+  end
+
+/-- This tactic is applied to each goal. If the application succeeds,
+    the tactic is applied recursively to all the generated subgoals until it eventually fails.
+    The recursion stops in a subgoal when the tactic has failed to make progress.
+    The tactic `repeat` never fails. -/
+meta def repeat (t : tactic unit) : tactic unit :=
+do gs ← get_goals, repeat_aux t gs []
+
 /-- `first [t_1, ..., t_n]` applies the first tactic that doesn't fail.
    The tactic fails if all t_i's fail. -/
 meta def first {α : Type u} : list (tactic α) → tactic α

tests/lean/run/apply2.lean

@@ -4,4 +4,4 @@ example (p q : Prop) : p → q → p ∧ q ∧ p :=
 by do
   intros,
   c₁ ← return (expr.const `and.intro []),
-  repeat_at_most 10 (apply c₁ <|> assumption)
+  iterate_at_most 10 (apply c₁ <|> assumption)

tests/lean/run/back4.lean

@@ -13,7 +13,7 @@ lemma in_right {α : Type u} {a : α}   (l : list α) {r : list α} : a ∈ r
 example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] :=
 begin [smt]
   intros,
-  repeat {ematch_using [in_left, in_right, in_head, in_tail], try {close}}
+  iterate { ematch_using [in_left, in_right, in_head, in_tail], try {close} }
 end
 
 /- We mark lemmas for ematching. -/
@@ -22,7 +22,7 @@ attribute [ematch] in_left in_right in_head in_tail
 example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] :=
 begin [smt]
   intros,
-  repeat {ematch, try {close}}
+  iterate {ematch, try {close}}
 end
 
 example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] :=
@@ -34,6 +34,6 @@ end
 example (a b c : nat) (l₁ l₂ : list nat) : a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] :=
 begin [smt]
   intros,
-  repeat {ematch, try {close}},
+  iterate {ematch, try {close}},
   admit /- finish the proof admiting the goal -/
 end

tests/lean/run/ematch_loop.lean

@@ -10,7 +10,7 @@ set_option trace.smt.ematch true
 
 lemma ex1 (a b c : nat) : f a = b → p a :=
 begin [smt]
-  intros, repeat {ematch},
+  intros, iterate {ematch},
   ematch_using [px]
 end
 

tests/lean/run/ematch_partial_apps.lean

@@ -13,7 +13,7 @@ end
 example (a : list nat) (f : nat → nat) : a = [1, 2] → a^.map f = [f 1, f 2] :=
 begin [smt]
   intros,
-  repeat {ematch_using [list.map], try { close }},
+  iterate {ematch_using [list.map], try { close }},
 end
 
 attribute [ematch] list.map

tests/lean/run/heap.lean

@@ -28,5 +28,5 @@ lemma ex
 begin [smt]
   intros,
   smt_tactic.add_lemmas_from_facts,
-  repeat {ematch}
+  iterate { ematch }
 end

tests/lean/run/listex2.lean

@@ -59,5 +59,5 @@ lemma ex2 (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l
 begin [smt]
   intros,
   add_lemma [in_left, in_right, in_head, in_tail],
-  repeat {ematch} -- It will loop if there is a matching loop
+  iterate {ematch} -- It will loop if there is a matching loop
 end

tests/lean/run/repeat_tac.lean

@@ -0,0 +1,2 @@
+example (p q r s : Prop) : p → q → r → s → (p ∧ q) ∧ (r ∧ s ∧ p) ∧ (p ∧ r ∧ q) :=
+by intros; repeat { constructor }; assumption

tests/lean/run/smt_destruct.lean

@@ -6,7 +6,7 @@ by using_smt $ do
    trace_state,
    a_1 ← tactic.get_local `a_1,
    destruct a_1,
-   repeat close
+   iterate close
 
 lemma ex2 (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → false :=
 begin [smt]

tests/lean/run/smt_ematch2.lean

@@ -7,7 +7,7 @@ meta def no_ac : smt_config :=
 { cc_cfg := { ac := ff }}
 
 meta def blast : tactic unit :=
-using_smt_with no_ac $ intros >> repeat (ematch >> try close)
+using_smt_with no_ac $ intros >> iterate (ematch >> try close)
 
 section add_comm_monoid
 variables [add_comm_monoid α]

tests/lean/run/smt_ematch3.lean

@@ -27,7 +27,7 @@ begin
   intros,
   induction v₁,
   {[smt] ematch_using [app, zero_add] },
-  {[smt] with smt_cfg, repeat { ematch_using [app, add_succ, succ_add, add_comm, add_assoc] }}
+  {[smt] with smt_cfg, iterate { ematch_using [app, add_succ, succ_add, add_comm, add_assoc] }}
 end
 
 def rev : Π {n : nat}, vector α n → vector α n
@@ -39,8 +39,8 @@ lemma rev_app : ∀ {n₁ n₂ : nat} (v₁ : vector α n₁) (v₂ : vector α
 begin
   intros,
   induction v₁,
-  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_nil_right]}},
-  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_assoc, add_one]} }
+  {[smt] iterate {ematch_using [app, rev, zero_add, add_zero, add_comm, app_nil_right]}},
+  {[smt] iterate {ematch_using [app, rev, zero_add, add_zero, add_comm, app_assoc, add_one]} }
 end
 
 end vector

tests/lean/run/smt_tests3.lean

@@ -15,7 +15,7 @@ lemma ex2  (a : nat) : f a ≠ 0 :=
 begin [smt]
   induction a,
   { intros, ematch_using [f] },
-  { repeat {ematch_using [f, nat.add_one, nat.succ_ne_zero]}}
+  { iterate { ematch_using [f, nat.add_one, nat.succ_ne_zero] }}
 end
 
 lemma ex3 (a : nat) : f (a+1) = f a + 1 :=

tests/lean/run/u_eq_max_u_v.lean

@@ -3,7 +3,7 @@ universe variables u v u1 u2 v1 v2
 set_option pp.universes true
 
 open smt_tactic
-meta def blast : tactic unit := using_smt $ intros >> add_lemmas_from_facts >> repeat_at_most 3 ematch
+meta def blast : tactic unit := using_smt $ intros >> add_lemmas_from_facts >> iterate_at_most 3 ematch
 notation `♮` := by blast
 
 structure semigroup_morphism { α β : Type u } ( s : semigroup α ) ( t: semigroup β ) :=