mathlib3 documentation

tactic.wlog

Without loss of generality tactic #

The tactic wlog h : P will add an assumption h : P to the main goal, and add a new goal that requires showing that the case h : ¬ P can be reduced to the case where P holds (typically by symmetry). The new goal will be placed at the top of the goal stack.

source
meta def tactic.take_pi_args  :
ℕ → expr → list name

A helper function to retrieve the names of the first n arguments to a Pi-expression.

source
meta def tactic.interactive.wlog (H : interactive.parse lean.parser.ident) (t : interactive.parse (lean.parser.tk ":" *> interactive.types.texpr)) (revert : interactive.parse (lean.parser.tk "generalizing" *> (option.none <$ lean.parser.tk "*" <|> option.some <$> lean.parser.many lean.parser.ident) <|> has_pure.pure option.none)) (h : interactive.parse (optional (lean.parser.tk "with" *> lean.parser.ident))) :
tactic unit

wlog h : P will add an assumption h : P to the main goal, and add a side goal that requires showing that the case h : ¬ P can be reduced to the case where P holds (typically by symmetry).

The side goal will be at the top of the stack. In this side goal, there will be two assumptions:

  • h : ¬ P: the assumption that P does not hold
  • this: which is the statement that in the old context P suffices to prove the goal. By default, the name this is used, but the idiom with H can be added to specify the name: wlog h : P with H.

Typically, it is useful to use the variant wlog h : P generalizing x y, to revert certain parts of the context before creating the new goal. In this way, the wlog-claim this can be applied to x and y in different orders (exploiting symmetry, which is the typical use case).

By default, the entire context is reverted.

source
def tactic_doc.tactic.wlog  :
tactic_doc_entry

wlog h : P will add an assumption h : P to the main goal, and add a side goal that requires showing that the case h : ¬ P can be reduced to the case where P holds (typically by symmetry).

The side goal will be at the top of the stack. In this side goal, there will be two assumptions:

  • h : ¬ P: the assumption that P does not hold
  • this: which is the statement that in the old context P suffices to prove the goal. By default, the name this is used, but the idiom with H can be added to specify the name: wlog h : P with H.

Typically, it is useful to use the variant wlog h : P generalizing x y, to revert certain parts of the context before creating the new goal. In this way, the wlog-claim this can be applied to x and y in different orders (exploiting symmetry, which is the typical use case).

By default, the entire context is reverted.