Type to Prop

Stream: general

[Bernd Losert]

Say I have a complex proposition involving multiple conjunctions, disjunctions, existensial, and so on. I would like to "package" this proposition as an inductive type in order to give sane names to each of its parts. Can I use this type in proofs even though it's not a Prop? Will I run into problems with tactics that expect a Prop and not a Type?

[Eric Wieser]

Are you aware that you can do:

structure foo : Prop :=
(x : some_prop)

[Eric Wieser]

That is, it sounds like you want to be able to use structure, not Type. "inductive prop"s are a thing too.

[Anne Baanen]

In principle there is no objection to using tactics in Type. The main issue you might run into is (lack of) definitional equality: you might expect all tactic-generated proofs of e.g. and' a b to look like and'.intro a b, but it might actually unfold to something very complicated. Such definitional issues don't matter in Prop because of proof irrelevance.

[Anne Baanen]

Also what @Eric Wieser said, you probably want to try using inductive foo : Prop instead?

[Bernd Losert]

I'll try Wieser's suggestion. Looks promosing.