How to extract propositions from instance's (non-)existence?

Stream: new members

[Chung Thai Nguyen]

There is a structure called Irreducible (https://github.com/leanprover-community/mathlib4/blob/0d1fc2182203e994dddc69190f494eb361b18963/Mathlib/Algebra/Prime/Defs.lean#L99)

structure Irreducible [Monoid M] (p : M) : Prop where
  /-- `p` is not a unit -/
  not_unit : ¬IsUnit p
  /-- if `p` factors then one factor is a unit -/
  isUnit_or_isUnit' : ∀ a b, p = a * b → IsUnit a ∨ IsUnit b

Currently my code assumes a specific polynomial to be NOT Irreducible, the assumption is like this:

h_neg_irreducible : ¬Irreducible (poly)

But now I want to convert this assumption of non-existence of an instance of Irreducible into propositions about its properties:

IsUnit (poly) ∨ ∃ a b, poly = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b

Could you give me some ideas on which tactics can I use to achieve this goal? I really appreciate any help from you. Thank you.

[Vlad Tsyrklevich]

You can use by_contra h and then apply docs#irreducible_iff. You will get better answers if you post an #mwe to fill-in.

[Vlad Tsyrklevich]

ah I see now that you specified it's a hypothesis, simp [irreducible_iff] at h should do it.

[Chung Thai Nguyen]

Vlad Tsyrklevich said:

ah I see now that you specified it's a hypothesis, simp [irreducible_iff] at h should do it.

Thank you so much @Vlad Tsyrklevich. This is the final working #mwe using apply docs#irreducible_iff.

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Group.Units.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.RingTheory.Ideal.Span

variable {F3: Type*} [Field F3]
variable {poly: Polynomial F3}

instance polyIrreducible : Irreducible (poly: Polynomial F3) := by
  by_contra h_neg_irreducible
  unfold Irreducible at h_neg_irreducible
  simp [irreducible_iff] at h_neg_irreducible
  -- split h_neg_irreducible into two cases and derive contradiction in both cases
  simp only [imp_iff_not_or] at h_neg_irreducible
  -- consider cases and prove both cases lead to contradiction
  cases h_neg_irreducible
  case inl left_case => -- left_case : ¬¬IsUnit poly
    sorry
  case inr right_case => -- right_case : ∃ x x_1, poly = x * x_1 ∧ ¬IsUnit x ∧ ¬IsUnit x_1
    sorry

[Ruben Van de Velde]

(That's not a #mwe, if only because it doesn't have imports)

[Vlad Tsyrklevich]

(hover over the code and press the button in the top-right to see)

[Chung Thai Nguyen]

Ruben Van de Velde said:

(That's not a #mwe, if only because it doesn't have imports)

Thank you for your feedback. I will post a full #mwe soon.

[Chung Thai Nguyen]

I've updated the #mwe. Thank you you all.

[Kevin Buzzard]

But now what exactly is the question? I don't see IsUnit (poly) ∨ ∃ a b, poly = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b in the #mwe. Can you write down the Lean code for the exact theorem you want to prove?

[Kevin Buzzard]

Is this the question?

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Group.Units.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.RingTheory.Ideal.Span

variable {F3: Type*} [Field F3]
variable {poly: Polynomial F3}

example (h_neg_irreducible : ¬Irreducible (poly)) :
    IsUnit (poly) ∨ ∃ a b, poly = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b :=
  sorry

Your mwe seems unrelated to your question.

[Chung Thai Nguyen]

I've just added comments the #mwe, with cases we can prove each case separately. That's what I needed.

[Kevin Buzzard]

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Group.Units.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.RingTheory.Ideal.Span

variable {F3: Type*} [Field F3]
variable {poly: Polynomial F3}

example (h_neg_irreducible : ¬Irreducible (poly)) :
    IsUnit (poly) ∨ ∃ a b, poly = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b := by
  rw [irreducible_iff] at h_neg_irreducible
  push_neg at h_neg_irreducible
  tauto

[Chung Thai Nguyen]

Great. Thank you for this very clean approach. push_neg looks really useful.

[Chung Thai Nguyen]

btw do you think that the way we have to use a supporting theorem like irreducible_iff to decompose a structure is a bit repetitive? Because we will have to create such a theorem for every structure? Especially for structures that extend other structures and more (nested extension), it would be complex and long.

So I'm looking for a way to get the proposition that represents the existence/non-existence of an instance of a structure in the most clean way. Do you have any ideas?

[Riccardo Brasca]

Using irreducible_iff instead of unfolding a definition makes a proof more robust. Imagine that tomorrow for some reason someone changes the definition of Irreducible, to something mathematically equivalent but expressed in a different way, maybe more convenient for formalization. Of course the proof of irreducible_iff would need to be fixed, but all the other proofs will work automatically. On the other hand proofs unfolding the definition will break.

[Riccardo Brasca]

In an ideal world all definitions should have a good API, and after the API is developed nobody should never unfold the definition. For example you really don't want to know how ℤ is defined in mathlib (at least if you are a mathematician), but the point is that you don't need to know it.

[Chung Thai Nguyen]

Riccardo Brasca said:

Using irreducible_iff instead of unfolding a definition makes a proof more robust. Imagine that tomorrow for some reason someone changes the definition of Irreducible, to something mathematically equivalent but expressed in a different way, maybe more convenient for formalization. Of course the proof of irreducible_iff would need to be fixed, but all the other proofs will work automatically. On the other hand proofs unfolding the definition will break.

Yep I got your point.
My concern is how can we unfold definitions that are abstract like this? Or do we have to trace back to all of the dependencies to gather the full definitions and put them into a theorem? Because I don't have the concrete propositions, I have to find a longer way around it.

/-- A domain is a nontrivial semiring such that multiplication by a non zero element
is cancellative on both sides. In other words, a nontrivial semiring `R` satisfying
`∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c` and
`∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c`.

This is implemented as a mixin for `Semiring α`.
To obtain an integral domain use `[CommRing α] [IsDomain α]`. -/
@[stacks 09FE]
class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop

[Riccardo Brasca]

The short answer is: don't unfold the definition. If you find a missing lemma in the API add it, but in proofs of "serious" theorems you should never unfold.

[Chung Thai Nguyen]

Riccardo Brasca said:

The short answer is: don't unfold the definition. If you find a missing lemma in the API add it, but in proofs of "serious" theorems you should never unfold.

Yep. Thank you for your answer.

[Riccardo Brasca]

the fact that isDoman_iff does not exist is probably because nobody wants it. We surely have that all the trivial stuff hold for a domain. And if you want to provide an instance of IsDomain is much better to use the where syntax.

[Riccardo Brasca]

The rationale is something like: "Prop valued structures deserve an iff lemma, other structures don't"