Ali Caglayan (Aug 22 2021 at 15:01): Ali Caglayan (Aug 22 2021 at 15:01):@Hugo Herbelin What do you mean by invertible constructor in #14798?
Ali Caglayan (Aug 22 2021 at 15:04):Is that basically anything that looks like a record?
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.
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 ?
Hugo Herbelin (Aug 23 2021 at 09:56):A constructor in a truncated type would not necessarily be invertible (e.g. ex_intro).
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.
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: Sep 09 2024 at 04:02 UTC