A way to make a non-Prop structure Prop

Stream: Is there code for X?

[Emilie (Shad Amethyst)]

In the proof of Rubin's theorem, I have this awkward structure, where IsAlgebraicallyDisjoint f g means ∀ h, ¬Commute f h → BigThing g h and where BigThing translates to "there exists a pair i₁, i₂ such that i₁, i₂ and ⁅i₁, ⁅i₂, h⁆⁆ commute with g and ⁅i₁, ⁅i₂, h⁆⁆ ≠ 1".

Obviously I can't just have one big equation with everything, but at the same time I can't see an easy way to split this relationship into multiples parts.
The "cleanest" solution I had found so far was to create a separate structure for BigThing, which stores i₁, i₂ and their properties.

My issue is that BigThing is then not a Prop (it contains data), and so IsAlgebraicallyDisjoint f g isn't a Prop either, so I can't use it in Iff relationships, for instance. I know I'll never need to compute what's in this pair i₁, i₂.

Is there a clean way to make IsAlgebraicallyDisjoint a Prop? Right now the best I can come up with is to have ∃ _ : BigThing g h, True

[Anatole Dedecker]

The typical way would be to use docs#Nonempty. Internally it would be exactly the same trick, but it has a nicer API

[Yury G. Kudryashov]

Another way is to create a Prop-values IsBigThing g h i₁ i₂ and use ∀ h, ¬Commute f h → ∃ i₁ i₂, IsBigThing g h i₁ i₂. The choice between 2 approaches depends on how you want to deal with API about BigThing do you want it to contain data or pass i₁, i₂ as implicit arguments around?

[Yury G. Kudryashov]

E.g., if you're going to prove something assuming (h : IsBigThing g h i₁ i₂) (h' : IsBigThing g h i₂ i₃), then it looks much better like this, not like (a b : BigThing g h) (hab : a.i2 = b.i1).

[Emilie (Shad Amethyst)]

I don't need to know about the contents of BigThing outside of any proof, really

[Joachim Breitner]

Could you use an imductive with a single constructor rather than a structure? Then you can let it live in Prop.

[Kyle Miller]

Do you mean something different from using structure A : Prop where ... syntax? That's a Prop-valued structure.

[Kyle Miller]

Oh right, I forgot that this isn't allowed if the fields aren't themselves Props

[Joachim Breitner]

Right, that’s what I tried and found too. But

inductive BigThing : Prop where
  | mk : ∀ i1 i2, … -> BigThing

does work and at least gives you pattern-matching syntax. Although not much is gained over

def BigThing := ∃ i1 i2, (… \and …)

I guess.

[Emilie (Shad Amethyst)]

Nonempty is exactly defined as a forgetful inductive type :)