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 underxs_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
.
-
wlog : p xs0 using [xs0, …, xsn]
Results in the case goalp xs0 ∨ ⋯ ∨ ps xsn
, the main goal(case : p xs0) ⊢ g xs0
and the invariance goals(case : p xsi) (this : g xs0) ⊢ g xsi
. -
wlog : p xs0 := r using xs0
The expressionr
is a proof of the shapep xs0 ∨ ⋯ ∨ p xsi
, it is also used to compute the variable permutations. -
wlog := r using xs0
The expressionr
is a proof of the shapep xs0 ∨ ⋯ ∨ p xsi
, it is also used to compute the variable permutations. This is not as stable as (2), for examplep
cannot be a disjunction. -
wlog : R x y using x y
andwlog : R x y
Produces the caseR x y ∨ R y x
. IfR
is ≤, then the disjunction discharged using linearity. Ifusing x y
is avoided thenx
andy
are the last two variables appearing in the expressionR x y
.