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.

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.