1.14. Miscellaneous

nontriviality

Attempts to generate a Nontrivial α hypothesis.

The tactic first checks to see that there is not already a Nontrivial α instance before trying to synthesize one using other techniques.

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 [h₁, h₂, ..., hₙ, nontriviality], where [h₁, h₂, ..., hₙ] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using h₁, h₂, ..., hₙ.

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := byR:Typeinst✝:OrderedRing Ra:Rh:0 < a⊢ 0 < a nontrivialityR:Typeinst✝¹:OrderedRing Ra:Rh:0 < ainst✝:Nontrivial R⊢ 0 < a -- There is now a `Nontrivial R` hypothesis available. assumptionAll goals completed! 🐙 example {R : Type} [CommRing R] {r s : R} : r * s = s * r := byR:Typeinst✝:CommRing Rr:Rs:R⊢ r * s = s * r nontrivialityR:Typeinst✝:CommRing Rr:Rs:Ra✝:Nontrivial R⊢ r * s = s * r -- There is now a `Nontrivial R` hypothesis available. apply mul_commAll goals completed! 🐙

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 := by
  nontriviality R -- there is now a `Nontrivial R` hypothesis available.
  dec_trivial

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

example {α : Type} (a b : α) (h : a = b) : myeq a b := by
  success_if_fail nontriviality α -- Fails
  nontriviality α using myeq -- There is now a `Nontrivial α` hypothesis available
  assumption

inhabit

inhabit α tries to derive a Nonempty α instance and then uses it to make an Inhabited α instance. If the target is a Prop, this is done constructively. Otherwise, it uses Classical.choice.

subsingleton

The subsingleton tactic tries to prove a goal of the form x = y or HEq x y using the fact that the types involved are subsingletons (a type with exactly zero or one terms). To a first approximation, it does apply Subsingleton.elim. As a nicety, subsingleton first runs the intros tactic.

• If the goal is an equality, it either closes the goal or fails.

• subsingleton [inst1, inst2, ...] can be used to add additional Subsingleton instances to the local context. This can be more flexible than have := inst1; have := inst2; ...; subsingleton since the tactic does not require that all placeholders be solved for.

Techniques the subsingleton tactic can apply:

• proof irrelevance

• heterogeneous proof irrelevance (via proof_irrel_heq)

• using Subsingleton (via Subsingleton.elim)

• proving BEq instances are equal if they are both lawful (via lawful_beq_subsingleton)

Properties

The tactic is careful not to accidentally specialize Sort _ to Prop, avoiding the following surprising behavior of apply Subsingleton.elim:

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

The reason this example goes through is that it applies the ∀ (p : Prop), Subsingleton p instance, specializing the universe level metavariable in Sort _ to 0.

measurability

The tactic measurability solves goals of the form Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ, or MeasurableSet s by applying lemmas tagged with the measurability user attribute.

borelize

The behaviour of borelize α depends on the existing assumptions on α.

• if α is a topological space with instances [MeasurableSpace α] [BorelSpace α], then borelize α replaces the former instance by borel α;

• otherwise, borelize α adds instances borel α : MeasurableSpace α and ⟨rfl⟩ : BorelSpace α.

Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

arith_mult

arith_mult solves goals of the form IsMultiplicative f for f : ArithmeticFunction R by applying lemmas tagged with the user attribute arith_mult.

subsingleton

The subsingleton tactic tries to prove a goal of the form x = y or HEq x y using the fact that the types involved are subsingletons (a type with exactly zero or one terms). To a first approximation, it does apply Subsingleton.elim. As a nicety, subsingleton first runs the intros tactic.

• If the goal is an equality, it either closes the goal or fails.

• subsingleton [inst1, inst2, ...] can be used to add additional Subsingleton instances to the local context. This can be more flexible than have := inst1; have := inst2; ...; subsingleton since the tactic does not require that all placeholders be solved for.

Techniques the subsingleton tactic can apply:

• proof irrelevance

• heterogeneous proof irrelevance (via proof_irrel_heq)

• using Subsingleton (via Subsingleton.elim)

• proving BEq instances are equal if they are both lawful (via lawful_beq_subsingleton)

Properties

The tactic is careful not to accidentally specialize Sort _ to Prop, avoiding the following surprising behavior of apply Subsingleton.elim:

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

The reason this example goes through is that it applies the ∀ (p : Prop), Subsingleton p instance, specializing the universe level metavariable in Sort _ to 0.

ext

Applies extensionality lemmas that are registered with the @[ext] attribute.

• ext pat* applies extensionality theorems as much as possible, using the patterns pat* to introduce the variables in extensionality theorems using rintro. For example, the patterns are used to name the variables introduced by lemmas such as funext.

• Without patterns,ext applies extensionality lemmas as much as possible but introduces anonymous hypotheses whenever needed.

• ext pat* : n applies ext theorems only up to depth n.

The ext1 pat* tactic is like ext pat* except that it only applies a single extensionality theorem.

Unused patterns will generate warning. Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.

funext

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying the funext lemma until the goal target is not reducible to

  |-  ((fun x => ...) = (fun x => ...))

The variant funext h₁ ... hₙ applies funext n times, and uses the given identifiers to name the new hypotheses. Patterns can be used like in the intro tactic. Example, given a goal

  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))

funext (a, b) applies funext once and performs pattern matching on the newly introduced pair.