Tactic Combinators

1-- ; applies the next tactic to ALL goals
2example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
3  constructor <;> assumption
4  -- constructor creates 2 goals
5  -- assumption is applied to both
6
7-- Same as:
8example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
9  constructor
10  · assumption
11  · assumption
12
13-- Chain multiple
14example (a b : Nat) : a ≤ a + b ∧ b ≤ a + b := by
15  constructor <;> omega

1-- first tries tactics until one succeeds
2example (n : Nat) : n = n := by
3  first
4  | omega
5  | rfl
6  | trivial
7
8-- Useful when the right tactic depends on the goal
9example (a b : Nat) (h : a = b) : a = b ∨ a > b := by
10  first
11  | right; omega  -- fails
12  | left; exact h  -- succeeds

1-- repeat keeps applying until the tactic fails
2example : [1, 2, 3].length = 3 := by
3  repeat (first | rfl | simp [List.length])
4
5-- Useful for intro
6example : ∀ a b c : Nat, a + b + c = c + b + a := by
7  repeat intro
8  ring
9
10-- repeat can loop forever if the tactic always succeeds!
11-- Be careful with repeat simp (usually fine)

1-- try runs a tactic but doesn't fail if it fails
2example (a b : Nat) : a + b = b + a := by
3  try rfl  -- fails silently (a + b ≠ b + a by definition)
4  ring
5
6-- Useful for cleanup that might not apply
7example (n : Nat) : n + 0 = n := by
8  try simp  -- succeeds
9  try ring  -- already done, but try doesn't fail

1-- all_goals applies a tactic to all current goals
2example (a b c : Nat) : a = a ∧ b = b ∧ c = c := by
3  constructor
4  all_goals rfl
5
6-- Different from ; which chains
7example (P Q R : Prop) (hp : P) (hq : Q) (hr : R) : P ∧ Q ∧ R := by
8  refine ⟨?_, ?_, ?_⟩
9  all_goals assumption

1-- any_goals succeeds if any goal is solved
2example (a b : Nat) (ha : a = 1) (hb : b = 2) : a = 1 ∧ b = 2 := by
3  constructor
4  any_goals exact ha
5  exact hb
6
7-- Useful when only some goals can be handled
8example (n : Nat) : (n = 0 ∨ n > 0) ∧ n ≥ 0 := by
9  constructor
10  · omega
11  · omega

1-- focus restricts to the first goal
2example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
3  constructor
4  focus
5    -- Only works on first goal (P)
6    exact hp
7  -- Back to second goal (Q)
8  exact hq
9
10-- Rarely needed in practice; · does similar

1-- Reorder goals
2example (P Q R : Prop) (hp : P) (hq : Q) (hr : R) : P ∧ Q ∧ R := by
3  refine ⟨?a, ?b, ?c⟩
4  rotate_left 2  -- Move first 2 goals to the end
5  -- Now goals are: R, P, Q
6  · exact hr
7  · exact hp
8  · exact hq

1-- Pattern 1: Split and solve uniformly
2example (a b c d : Nat) : a ≤ a + b ∧ b ≤ b + c ∧ c ≤ c + d := by
3  refine ⟨?_, ?_, ?_⟩ <;> omega
4
5-- Pattern 2: Try multiple approaches
6example (n : Nat) (h : n > 0 ∨ n = 0) : n ≥ 0 := by
7  cases h with
8  | inl h => omega
9  | inr h => omega
10
11-- Pattern 3: Clean up trivial goals
12example (P : Prop) (hp : P) : P ∧ True ∧ P := by
13  refine ⟨?_, ?_, ?_⟩
14  · exact hp
15  · trivial
16  · exact hp

1-- done asserts there are no remaining goals
2example (n : Nat) : n = n := by
3  rfl
4  done  -- Confirms proof is complete
5
6-- Useful for sanity checking in complex proofs
7example (P : Prop) (hp : P) : P ∧ P := by
8  constructor <;> exact hp
9  done

1example (n : Nat) : n + 0 = n ∧ 0 + n = n := by
2  induction n with
3  | zero => constructor <;> rfl
4  | succ m ih => 
5    obtain ⟨ih1, ih2⟩ := ih
6    constructor
7    · simp [ih1]
8    · simp [ih2]

1example (a b c : Nat) (h1 : a = b) (h2 : b = c) : 
2    a + 1 = c + 1 ∧ a + 2 = c + 2 := by
3  constructor <;> omega

1-- Normalize then attempt automation
2example (a b : Nat) (h : a = b) : (a + 1) * (a + 1) = (b + 1) * (b + 1) := by
3  try ring_nf
4  rw [h]