Converting between prop type classes and their field prop

Stream: new members

[Peter Hansen]

Is there a way to automatically convert between a proposition type class instance (like of IsTrichotomous) and its underlying proposition? I can prove they're equivalent (and even equal using propext).

import Mathlib.Order.Defs.Unbundled

variable (X : Sort*) (𝓡 : X → X → Prop)

example : IsTrichotomous X 𝓡 ↔ ∀ (a b : X), (𝓡 a b ∨ a = b ∨ 𝓡 b a) :=
  ⟨fun h ↦ h.trichotomous, fun h ↦ ⟨h⟩⟩

example : IsTrichotomous X 𝓡 = ∀ (a b : X), (𝓡 a b ∨ a = b ∨ 𝓡 b a) :=
  propext ⟨fun h ↦ h.trichotomous, fun h ↦ ⟨h⟩⟩

But I was hoping for a simpler way to switch between an instance of a prop class
and its propositional field. To avoid a XY-problem scenario, my original goal
was to show that a relation is 'mutually exclusive trichotomous' iff it
is both 'trichotomous' and 'asymmetric'.

variable (X : Sort*) (𝓡 : X → X → Prop)

local infixl : 100 " ≺ " => 𝓡
local infixl : 100 " ⊀ " => (fun x y ↦ ¬𝓡 x y)

def MuExTrichotomous : Prop :=
  ∀ a b, (a ≺ b ∨ a = b ∨ b ≺ a) ∧
         (a ≺ b → a ≠ b ∧ b ⊀ a ) ∧
         (a = b → a ⊀ b ∧ b ⊀ a) ∧
         (b ≺ a → a ⊀ b ∧ a ≠ b)

theorem MuExTrichotomousIff' : MuExTrichotomous X 𝓡 ↔
  (∀ a b, a ≺ b ∨ a = b ∨ b ≺ a) ∧ (∀ a b, a ≺ b → b ⊀ a) := by
  simp_all [MuExTrichotomous]
  aesop

theorem MuExTrichotomousIff : MuExTrichotomous X 𝓡 ↔ IsTrichotomous X 𝓡 ∧ IsAsymm X 𝓡 := by
  rw [MuExTrichotomousIff']
  have h1 : (∀ a b, a ≺ b ∨ a = b ∨ b ≺ a) ↔ IsTrichotomous X 𝓡 :=
    ⟨fun h ↦ ⟨h⟩, fun h ↦ h.trichotomous⟩
  have h2 : (∀ a b, a ≺ b → b ⊀ a) ↔ IsAsymm X 𝓡 :=
    ⟨fun h ↦ ⟨h⟩, fun h ↦ h.asymm⟩
  rw [← h1, ← h2]

Is there a simpler way to show a prop class is equivalent to some alternative
definition?

Side Question: While playing with the definition of the unbundled order defs,
I noticed ne_of_irrefl assumes a Type* rather than a Sort*. Why is this?
It seems it should hold just as well given a Sort*. The same goes for all
other theorems in the same scope.

[Eric Wieser]

@[mk_iff]

[Peter Hansen]

If you could spare a few more key strokes and show me how to use mk_iff I would very grateful :smiling_face:

I figured it out.

mk_iff_of_inductive_prop IsAsymm IsAsymmUnfold
mk_iff_of_inductive_prop IsTrichotomous IsTrichotomousUnfold

theorem MuExTrichotomousIff : MuExTrichotomous X 𝓡 ↔ IsTrichotomous X 𝓡 ∧ IsAsymm X 𝓡 := by
  rw [IsAsymmUnfold, IsTrichotomousUnfold]
  unfold MuExTrichotomous
  aesop

[Peter Hansen]

Eric Wieser said:

@[mk_iff]

Thanks a lot for pointing me in right direction. This will come in very handy. Though I would still also like to know if I have a point concerning docs#ne_of_irrefl being defined on a Type* instead of a Sort*.