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.