These tactics deal with statements in logic. Remember that
tauto, listed above, is also good a these.
contraposeTransforms the goal into its contrapositive.
contrapose turns a goal P → Q into ¬ Q → ¬ P
contrapose h first reverts the local assumption h, and then uses contrapose and intro h
contrapose h with new_h uses the name new_h for the introduced hypothesis
push_neg
Push negations into the conclusion of a hypothesis.
For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into
h : ∃ x, ∀ y, y < x. Variable names are conserved.
This tactic pushes negations inside expressions. For instance, given a hypothesis
h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
writing push_neg at h will turn h into
h : ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
(The pretty printer does not use the abbreviations ∀ δ > 0 and ∃ ε > 0 but this issue
has nothing to do with push_neg).
Note that names are conserved by this tactic, contrary to what would happen with simp
using the relevant lemmas. One can also use this tactic at the goal using push_neg,
at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal
using say push_neg at h h' ⊢ as usual.
This tactic has two modes: in standard mode, it transforms ¬(p ∧ q) into p → ¬q, whereas in
distrib mode it produces ¬p ∨ ¬q. To use distrib mode, use set_option push_neg.use_distrib true.
tfae_have
tfae_have introduces hypotheses for proving goals of the form TFAE [P₁, P₂, ...]. Specifically,
tfae_have i <arrow> j := ... introduces a hypothesis of type Pᵢ <arrow> Pⱼ to the local
context, where <arrow> can be →, ←, or ↔. Note that i and j are natural number indices
(beginning at 1) used to specify the propositions P₁, P₂, ... that appear in the goal.
example (h : P → R) : TFAE [P, Q, R] := by tfae_have 1 → 3 := h ...
The resulting context now includes tfae_1_to_3 : P → R.
Once sufficient hypotheses have been introduced by tfae_have, tfae_finish can be used to close
the goal. For example,
example : TFAE [P, Q, R] := by tfae_have 1 → 2 := sorry /- proof of P → Q -/ tfae_have 2 → 1 := sorry /- proof of Q → P -/ tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/ tfae_finish
All features of have are supported by tfae_have, including naming, matching,
destructuring, and goal creation. These are demonstrated below.
example : TFAE [P, Q] := by -- assert `tfae_1_to_2 : P → Q`: tfae_have 1 → 2 := sorry -- assert `hpq : P → Q`: tfae_have hpq : 1 → 2 := sorry -- match on `p : P` and prove `Q` via `f p`: tfae_have 1 → 2 | p => f p -- assert `pq : P → Q`, `qp : Q → P`: tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry -- assert `h : P → Q`; `?a` is a new goal: tfae_have h : 1 → 2 := f ?a ...
tfae_finish
tfae_finish is used to close goals of the form TFAE [P₁, P₂, ...] once a sufficient collection
of hypotheses of the form Pᵢ → Pⱼ or Pᵢ ↔ Pⱼ have been introduced to the local context.
tfae_have can be used to conveniently introduce these hypotheses; see tfae_have.
Example:
example : TFAE [P, Q, R] := by tfae_have 1 → 2 := sorry /- proof of P → Q -/ tfae_have 2 → 1 := sorry /- proof of Q → P -/ tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/ tfae_finish
use
use e₁, e₂, ⋯ is similar to exists, but unlike exists it is equivalent to applying the tactic
refine ⟨e₁, e₂, ⋯, ?_, ⋯, ?_⟩ with any number of placeholders (rather than just one) and
then trying to close goals associated to the placeholders with a configurable discharger (rather
than just try trivial).
Examples:
example : ∃ x : Nat, x = x := ⊢ ∃ x, x = x All goals completed! 🐙
example : ∃ x : Nat, ∃ y : Nat, x = y := ⊢ ∃ x y, x = y All goals completed! 🐙
example : ∃ x : String × String, x.1 = x.2 := ⊢ ∃ x, x.1 = x.2 All goals completed! 🐙
use! e₁, e₂, ⋯ is similar but it applies constructors everywhere rather than just for
goals that correspond to the last argument of a constructor. This gives the effect that
nested constructors are being flattened out, with the supplied values being used along the
leaves and nodes of the tree of constructors.
With use! one can feed in each 42 one at a time:
example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42 example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
The second line makes use of the fact that use! tries refining with the argument before
applying a constructor. Also note that use/use! by default uses a tactic
called use_discharger to discharge goals, so use! 42 will close the goal in this example since
use_discharger applies rfl, which as a consequence solves for the other Nat metavariable.
These tactics take an optional discharger to handle remaining explicit Prop constructor arguments.
By default it is use (discharger := try with_reducible use_discharger) e₁, e₂, ⋯.
To turn off the discharger and keep all goals, use (discharger := skip).
To allow "heavy refls", use (discharger := try use_discharger).
wlog
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 additional 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.
choose
choose a b h h' using hyp takes a hypothesis hyp of the form
∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b
for some P Q : X → Y → A → B → Prop and outputs
into context a function a : X → Y → A, b : X → Y → B and two assumptions:
h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and
h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.
choose! a b h h' using hyp does the same, except that it will remove dependency of
the functions on propositional arguments if possible. For example if Y is a proposition
and A and B are nonempty in the above example then we will instead get
a : X → A, b : X → B, and the assumptions
h : ∀ (x : X) (y : Y), P x y (a x) (b x) and
h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).
The using hyp part can be omitted,
which will effectively cause choose to start with an intro hyp.
Examples:
example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := h:∀ (n m : ℕ), ∃ i j, m = n + i ∨ m + j = n⊢ True
i:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True
i:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True
i:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True
i:ℕ → ℕ → ℕj:ℕ → ℕ → ℕh:∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n⊢ True
All goals completed! 🐙
example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := h:∀ i < 7, ∃ j, i < j ∧ j < i + i⊢ True
f:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True
f:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True
f:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True
f:ℕ → ℕh:∀ i < 7, i < f ih':∀ i < 7, f i < i + i⊢ True
All goals completed! 🐙
peelPeels matching quantifiers off of a given term and the goal and introduces the relevant variables.
peel e peels all quantifiers (at reducible transparency),
using this for the name of the peeled hypothesis.
peel e with h is peel e but names the peeled hypothesis h.
If h is _ then uses this for the name of the peeled hypothesis.
peel n e peels n quantifiers (at default transparency).
peel n e with x y z ... h peels n quantifiers, names the peeled hypothesis h,
and uses x, y, z, and so on to name the introduced variables; these names may be _.
If h is _ then uses this for the name of the peeled hypothesis.
The length of the list of variables does not need to equal n.
peel e with x₁ ... xₙ h is peel n e with x₁ ... xₙ h.
There are also variants that apply to an iff in the goal:
peel n peels n quantifiers in an iff.
peel with x₁ ... xₙ peels n quantifiers in an iff and names them.
Given p q : ℕ → Prop, h : ∀ x, p x, and a goal ⊢ : ∀ x, q x, the tactic peel h with x h'
will introduce x : ℕ, h' : p x into the context and the new goal will be ⊢ q x. This works
with ∃, as well as ∀ᶠ and ∃ᶠ, and it can even be applied to a sequence of quantifiers. Note
that this is a logically weaker setup, so using this tactic is not always feasible.
For a more complex example, given a hypothesis and a goal:
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε ⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε
(which differ only in </≤), applying peel h with ε hε N n hn h_peel will yield a tactic state:
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε ε : ℝ hε : 0 < ε N n : ℕ hn : N ≤ n h_peel : 1 / (n + 1 : ℝ) < ε ⊢ 1 / (n + 1 : ℝ) ≤ ε
and the goal can be closed with exact h_peel.le.
Note that in this example, h and the goal are logically equivalent statements, but peel
cannot be immediately applied to show that the goal implies h.
In addition, peel supports goals of the form (∀ x, p x) ↔ ∀ x, q x, or likewise for any
other quantifier. In this case, there is no hypothesis or term to supply, but otherwise the syntax
is the same. So for such goals, the syntax is peel 1 or peel with x, and after which the
resulting goal is p x ↔ q x. The congr! tactic can also be applied to goals of this form using
congr! 1 with x. While congr! applies congruence lemmas in general, peel can be relied upon
to only apply to outermost quantifiers.
Finally, the user may supply a term e via ... using e in order to close the goal
immediately. In particular, peel h using e is equivalent to peel h; exact e. The using syntax
may be paired with any of the other features of peel.
This tactic works by repeatedly applying lemmas such as forall_imp, Exists.imp,
Filter.Eventually.mp, Filter.Frequently.mp, and Filter.Eventually.of_forall.
leftApplies the first constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.
example : True ∨ False := ⊢ True ∨ False
⊢ True
All goals completed! 🐙
rightApplies the second constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.
example {p q : Prop} (h : q) : p ∨ q := p:Propq:Proph:q⊢ p ∨ q
p:Propq:Proph:q⊢ q
All goals completed! 🐙
contradiction
contradiction closes the main goal if its hypotheses are "trivially contradictory".
Inductive type/family with no applicable constructors
example (h : False) : p := p:Sort ?u.9h:False⊢ p All goals completed! 🐙
Injectivity of constructors
example (h : none = some true) : p := p:Sort ?u.75h:none = some true⊢ p All goals completed! 🐙 --
Decidable false proposition
example (h : 2 + 2 = 3) : p := p:Sort ?u.203h:2 + 2 = 3⊢ p All goals completed! 🐙
Contradictory hypotheses
example (h : p) (h' : ¬ p) : q := p:Propq:Sort ?u.17h:ph':¬p⊢ q All goals completed! 🐙
Other simple contradictions such as
example (x : Nat) (h : x ≠ x) : p := p:Sort ?u.17x:ℕh:x ≠ x⊢ p All goals completed! 🐙
exfalso
exfalso converts a goal ⊢ tgt into ⊢ False by applying False.elim.