# mathlib3documentation

tactic.nontriviality

# The nontriviality tactic. #

meta def tactic.nontriviality_by_elim (α : expr)  :

Tries to generate a nontrivial α instance by performing case analysis on subsingleton_or_nontrivial α, attempting to discharge the subsingleton branch using lemmas with @[nontriviality] attribute, including subsingleton.le and eq_iff_true_of_subsingleton.

Tries to generate a nontrivial α instance using nontrivial_of_ne or nontrivial_of_lt and local hypotheses.

Attempts to generate a nontrivial α hypothesis.

The tactic first looks for an instance using apply_instance.

If the goal is an (in)equality, the type α is inferred from the goal. Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α.

The nontriviality tactic will first look for strict inequalities amongst the hypotheses, and use these to derive the nontrivial instance directly.

Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α, and attempt to discharge the subsingleton goal using simp [lemmas] with nontriviality, where [lemmas] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using [lemmas].

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
assumption,
end

example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
apply mul_comm,
end

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 :=
begin
nontriviality R, -- there is now a nontrivial R hypothesis available.
dec_trivial
end

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
success_if_fail { nontriviality α }, -- Fails
nontriviality α using [myeq], -- There is now a nontrivial α hypothesis available
assumption
end



Attempts to generate a nontrivial α hypothesis.

The tactic first looks for an instance using apply_instance.

If the goal is an (in)equality, the type α is inferred from the goal. Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α.

The nontriviality tactic will first look for strict inequalities amongst the hypotheses, and use these to derive the nontrivial instance directly.

Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α, and attempt to discharge the subsingleton goal using simp [lemmas] with nontriviality, where [lemmas] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using [lemmas].

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
assumption,
end

example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
apply mul_comm,
end

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 :=
begin
nontriviality R, -- there is now a nontrivial R hypothesis available.
dec_trivial
end

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
success_if_fail { nontriviality α }, -- Fails
nontriviality α using [myeq], -- There is now a nontrivial α hypothesis available
assumption
end