tactic.swap_var

# 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


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

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