exfalso
converts a goal ⊢ tgt
into ⊢ False
by applying False.elim
.
Instances For
_
in tactic position acts like the done
tactic: it fails and gives the list
of goals if there are any. It is useful as a placeholder after starting a tactic block
such as by _
to make it syntactically correct and show the current goal.
Instances For
fail_if_success t
fails if the tactic t
succeeds.
Instances For
rwa
calls rw
, then closes any remaining goals using assumption
.
Instances For
Like exact
, but takes a list of terms and checks that all goals are discharged after the tactic.
Instances For
by_contra h
proves ⊢ p
by contradiction,
introducing a hypothesis h : ¬p
and proving False
.
- If
p
is a negation¬q
,h : q
will be introduced instead of¬¬q
. - If
p
is decidable, it usesDecidable.byContradiction
instead ofClassical.byContradiction
. - If
h
is omitted, the introduced variable_: ¬p
will be anonymous.
Instances For
Given a proof h
of p
, absurd h
changes the goal to ⊢ ¬ p
.
If p
is a negation ¬q
then the goal is changed to ⊢ q
instead.
Instances For
iterate n tac
runs tac
exactly n
times.
iterate tac
runs tac
repeatedly until failure.
To run multiple tactics, one can do iterate (tac₁; tac₂; ⋯)
or
iterate
tac₁
tac₂
⋯
Instances For
repeat' tac
runs tac
on all of the goals to produce a new list of goals,
then runs tac
again on all of those goals, and repeats until tac
fails on all remaining goals.
Instances For
repeat1 tac
applies tac
to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
Instances For
subst_eqs
applies subst
to all equalities in the context as long as it makes progress.
Instances For
split_ands
applies And.intro
until it does not make progress.
Instances For
fapply e
is like apply e
but it adds goals in the order they appear,
rather than putting the dependent goals first.
Instances For
eapply e
is like apply e
but it does not add subgoals for variables that appear
in the types of other goals. Note that this can lead to a failure where there are
no goals remaining but there are still metavariables in the term:
example (h : ∀ x : Nat, x = x → True) : True := by
eapply h
rfl
-- no goals
-- (kernel) declaration has metavariables '_example'
Instances For
conv
tactic to close a goal using an equality theorem.
Instances For
The conv
tactic equals
claims that the currently focused subexpression is equal
to the given expression, and proves this claim using the given tactic.
example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
conv in (_ - _) => equals 0 =>
-- current goal: ⊢ n - n = 0
apply Nat.sub_self
-- current goal: P (fun n => 0)