Swap bound variable tactic #

This files defines a tactic swap_var whose main purpose is to be a weaker version of wlog that juggles bound names.

It is a helper around the core tactic rename.

swap_var old new renames all names named old to new and vice versa in the goal and all hypotheses.

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact ‹P› }
end

See also #

source

meta def tactic.interactive.swap_var (renames : interactive.parse swap_args_parser) :

tactic unit

swap_var [x y, P ↔ Q] swaps the names x and y, P and Q. Such a swapping can be used as a weak wlog if the tactic proofs use the same names.

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact ‹P› }
end

source

def tactic_doc.tactic.swap_var :

tactic_doc_entry

swap_var [x y, P ↔ Q] swaps the names x and y, P and Q. Such a swapping can be used as a weak wlog if the tactic proofs use the same names.

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact ‹P› }
end