@Hugo Herbelin What do you mean by invertible constructor in #14798?
Is that basically anything that looks like a record?
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
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.
@Hugo Herbelin Just for curiosity sake, do you have an example of a non-invertible constructor according to your definition ?
A constructor in a truncated type would not necessarily be invertible (e.g.
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.
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