Zulip Chat Archive

Stream: general

Topic: Type to Prop

Bernd Losert (Dec 06 2021 at 12:08):

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 (Dec 06 2021 at 12:11):

Are you aware that you can do:

structure foo : Prop :=
(x : some_prop)

Eric Wieser (Dec 06 2021 at 12:12):

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

Anne Baanen (Dec 06 2021 at 12:12):

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 (Dec 06 2021 at 12:13):

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

Bernd Losert (Dec 06 2021 at 12:15):

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

Last updated: Aug 03 2023 at 10:10 UTC