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
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