tactic.wlog - mathlib docs

meta def tactic.wlog (vars' : list expr) (h_cases fst_case : expr) (perms : list (list expr)) :

meta def tactic.interactive.wlog (h : interactive.parse (optional lean.parser.ident)) (pat : interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))) (cases : interactive.parse (optional (lean.parser.tk ":=" *> interactive.types.texpr))) (perms : interactive.parse (optional (lean.parser.tk "using" *> (interactive.types.list_of (lean.parser.many lean.parser.ident) <|> (λ (x : list name), [x]) <$> lean.parser.many lean.parser.ident)))) (discharger : tactic unit := tactic.solve_by_elim <|> tactic.tautology {classical := bool.tt, closer := has_pure.pure ()} <|> (using_smt (smt_tactic.intros >> smt_tactic.solve_goals))) :

tactic unit

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.

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.
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.
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.
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.

source

def tactic_doc.tactic.wlog :

tactic_doc_entry

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

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 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.
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.
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.
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.