Simple tactics that are used throughout Batteries. #
_
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.
Equations
Instances For
Like exact
, but takes a list of terms and checks that all goals are discharged after the tactic.
Equations
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.
Equations
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.
Equations
Instances For
fapply e
is like apply e
but it adds goals in the order they appear,
rather than putting the dependent goals first.
Equations
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'
Equations
Instances For
conv
tactic to close a goal using an equality theorem.
Equations
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)