wlog_tac

bossLib.wlog_tac : term quotation -> term quotation list -> tactic

Also exported as wlogLib.wlog_tac.

Enrich the hypotheses with a proposition that can be assumed without loss of generality.

The user provides term quotations that parse to a proposition P and a list of variables. Typically there are 2 subgoals. The first subgoal is to prove that the general case of the original goal follows from the specific case where P holds; the second subgoal is the original goal with P added to the assumptions. The first subgoal is always present, and the subgoals (if any) produced by strip_assume_tac P |- P follows.

If the goal is hyp ?- t then the first subgoal is hyp, !vars. ant ==> t, ~P ?- t where ant is the conjunction of P and those hypotheses of the original subgoal where any variable in the user-provided list occurs free. The universal quantification is over the variables in the user-provided list plus any variable that appears free in P or t and is not a local constant. For convenience ~P is always added to the assumptions in the first subgoal because the case for P follows immediately from the hypothesis. Passing a non-empty list of variables allows to quantify over local constants in the hypothesis !vars. ant ==> t.

Detailed description: Given wlog_tac q vars_q let asm ?- c be the the goal. q is parsed in the goal context to a proposition P. vars_q are parsed to variables in the goal context. Let efv (effectively free variables) be the free variables of P and c that are not free in the assumptions and are not in vars from left to right and first P, then c. Let gen_vars be vars @ efv. Let asm' be the elements of asm in which any of vars is a free variable. Let ant be the result of splicing p :: asm'. The first subgoal is asm, (!(gen_vars). ant ==> c), ~P ?- c. The proposition P is added to the assumptions with strip_assume_tac. If this generates subgoals (as is usually the case), then those subgoals follow.

A typical use case is to continue the proof assuming one case where all cases are symmetric. The first subgoal is a good candidate to be solved by a first order prover like PROVE_TAC or METIS_TAC providing to it the appropriate symmetry theorems.

Example

In the following examples assume arithmeticTheory is open.

> g(`ABS_DIFF x y + ABS_DIFF y z <= ABS_DIFF x z`);
val it =
   Proof manager status: 3 proofs.
   3. Incomplete goalstack:
        Initial goal:
         0.  p ⇒ q
        ------------------------------------
             r
        
        Current goal:
         0.  p ⇒ q
        ------------------------------------
             p
   
   2. Incomplete goalstack:
        Initial goal:
        p ∧ q ⇒ r ∧ s
        
        Current goal:
         0.  p
         1.  q
        ------------------------------------
             p'
   
   1. Incomplete goalstack:
        Initial goal:
        ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
> e(wlog_tac `x <= z` []);
OK..
2 subgoals:
val it =
   
    0.  x ≤ z
   ------------------------------------
        ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
   
    0.  ∀x z y. x ≤ z ⇒ ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
    1.  ¬(x ≤ z)
   ------------------------------------
        ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z

The first subgoal can be solved by prove_tac [ABS_DIFF_SYM, LESS_EQ_CASES, ADD_COMM].

> g`MAX x y <= z <=> x <= z /\ y <= z`
val it =
   Proof manager status: 4 proofs.
   4. Incomplete goalstack:
        Initial goal:
         0.  p ⇒ q
        ------------------------------------
             r
        
        Current goal:
         0.  p ⇒ q
        ------------------------------------
             p
   
   3. Incomplete goalstack:
        Initial goal:
        p ∧ q ⇒ r ∧ s
        
        Current goal:
         0.  p
         1.  q
        ------------------------------------
             p'
   
   2. Incomplete goalstack:
        Initial goal:
        ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
        
        Current goal:
         0.  ∀x z y. x ≤ z ⇒ ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
         1.  ¬(x ≤ z)
        ------------------------------------
             ABS_DIFF x y + ABS_DIFF y z ≤ ABS_DIFF x z
   
   1. Incomplete goalstack:
        Initial goal:
        MAX x y ≤ z ⇔ x ≤ z ∧ y ≤ z
> e(wlog_tac `x <= y` []);
OK..
2 subgoals:
val it =
   
    0.  x ≤ y
   ------------------------------------
        MAX x y ≤ z ⇔ x ≤ z ∧ y ≤ z
   
    0.  ∀x y z. x ≤ y ⇒ (MAX x y ≤ z ⇔ x ≤ z ∧ y ≤ z)
    1.  ¬(x ≤ y)
   ------------------------------------
        MAX x y ≤ z ⇔ x ≤ z ∧ y ≤ z

The first subgoal can be solved by prove_tac [LESS_EQ_CASES, MAX_COMM];

Failure

Never fails.

See also

bossLib.wlog_then