Stream: Coq devs & plugin devs

Topic: Invertible constructor


view this post on Zulip Ali Caglayan (Aug 22 2021 at 15:01):

@Hugo Herbelin What do you mean by invertible constructor in #14798?

view this post on Zulip Ali Caglayan (Aug 22 2021 at 15:04):

Is that basically anything that looks like a record?

view this post on Zulip Hugo Herbelin (Aug 23 2021 at 09:29):

Ali Caglayan said:

Hugo Herbelin What do you mean by invertible constructor in #14798?

A constructor (or nesting of constructors) such that you can extract a component by projection. E.g. (x,y) out of which x can be extracted with fst, or S mout of which m can be extracted by pred, etc. This extension allows to resolve quite common situations of the form ?P (x,y) := x = y.

view this post on Zulip Kenji Maillard (Aug 23 2021 at 09:53):

@Hugo Herbelin Just for curiosity sake, do you have an example of a non-invertible constructor according to your definition ?

view this post on Zulip Hugo Herbelin (Aug 23 2021 at 09:56):

A constructor in a truncated type would not necessarily be invertible (e.g. ex_intro).

view this post on Zulip Hugo Herbelin (Aug 23 2021 at 09:58):

Incidentally, the implementation only considers one-constructor types at the current time. Already for pred, inverting (in a generic way) would require to build match m with S n => n | 0 => ?[q] end and it is not clear if, how and when ?q should/could be instantiated.

view this post on Zulip Kenji Maillard (Aug 23 2021 at 10:10):

Right, exists is only invertible in Prop, not unconditionally.. And conversely I guess the only constructors that are safe to consider invertible with respect to "any" extension to Coq are records with (primitive?) projections


Last updated: Oct 16 2021 at 07:02 UTC