# mathlibdocumentation

tactic.wlog

meta def tactic.wlog (vars' : list expr) (h_cases fst_case : expr) (perms : list (list expr)) :
meta def tactic.interactive.wlog (pat : interactive.parse ) (cases : interactive.parse ) (perms : interactive.parse (optional (lean.parser.tk "using" *> <|> (λ (x : , [x]) <\$> ) (discharger : := ) :

Without loss of generality: reduces to one goal under variables permutations.

Given a goal of the form g xs, a predicate p over a set of variables, as well as variable permutations xs_i. Then wlog produces goals of the form

• The case goal, i.e. the permutation xs_i covers all possible cases: ⊢ p xs_0 ∨ ⋯ ∨ p xs_n
• The main goal, i.e. the goal reduced to xs_0: (h : p xs_0) ⊢ g xs_0
• The invariant goals, i.e. g is invariant under xs_i: (h : p xs_i) (this : g xs_0) ⊢ gs xs_i

Either the permutation is provided, or a proof of the disjunction is provided to compute the permutation. The disjunction need to be in assoc normal form, e.g. p₀ ∨ (p₁ ∨ p₂). In many cases the invariant goals can be solved by AC rewriting using cc etc.

For example, on a state (n m : ℕ) ⊢ p n m the tactic wlog h : n ≤ m using [n m, m n] produces the following states:

• (n m : ℕ) ⊢ n ≤ m ∨ m ≤ n
• (n m : ℕ) (h : n ≤ m) ⊢ p n m
• (n m : ℕ) (h : m ≤ n) (this : p n m) ⊢ p m n

wlog supports different calling conventions. The name h is used to give a name to the introduced case hypothesis. If the name is avoided, the default will be case.

1. wlog : p xs0 using [xs0, …, xsn]
Results in the case goal p xs0 ∨ ⋯ ∨ ps xsn, the main goal (case : p xs0) ⊢ g xs0 and the invariance goals (case : p xsi) (this : g xs0) ⊢ g xsi.

2. wlog : p xs0 := r using xs0
The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations.

3. wlog := r using xs0
The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations. This is not as stable as (2), for example p cannot be a disjunction.

4. wlog : R x y using x y and wlog : R x y
Produces the case R x y ∨ R y x. If R is ≤, then the disjunction discharged using linearity. If using x y is avoided then x and y are the last two variables appearing in the expression R x y.

Without loss of generality: reduces to one goal under variables permutations.

Given a goal of the form g xs, a predicate p over a set of variables, as well as variable permutations xs_i. Then wlog produces goals of the form

• The case goal, i.e. the permutation xs_i covers all possible cases: ⊢ p xs_0 ∨ ⋯ ∨ p xs_n
• The main goal, i.e. the goal reduced to xs_0: (h : p xs_0) ⊢ g xs_0
• The invariant goals, i.e. g is invariant under xs_i: (h : p xs_i) (this : g xs_0) ⊢ gs xs_i

Either the permutation is provided, or a proof of the disjunction is provided to compute the permutation. The disjunction need to be in assoc normal form, e.g. p₀ ∨ (p₁ ∨ p₂). In many cases the invariant goals can be solved by AC rewriting using cc etc.

For example, on a state (n m : ℕ) ⊢ p n m the tactic wlog h : n ≤ m using [n m, m n] produces the following states:

• (n m : ℕ) ⊢ n ≤ m ∨ m ≤ n
• (n m : ℕ) (h : n ≤ m) ⊢ p n m
• (n m : ℕ) (h : m ≤ n) (this : p n m) ⊢ p m n

wlog supports different calling conventions. The name h is used to give a name to the introduced case hypothesis. If the name is avoided, the default will be case.

1. wlog : p xs0 using [xs0, …, xsn]
Results in the case goal p xs0 ∨ ⋯ ∨ ps xsn, the main goal (case : p xs0) ⊢ g xs0 and the invariance goals (case : p xsi) (this : g xs0) ⊢ g xsi.

2. wlog : p xs0 := r using xs0
The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations.

3. wlog := r using xs0
The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations. This is not as stable as (2), for example p cannot be a disjunction.

4. wlog : R x y using x y and wlog : R x y
Produces the case R x y ∨ R y x. If R is ≤, then the disjunction discharged using linearity. If using x y is avoided then x and y are the last two variables appearing in the expression R x y.