Why does registering `core.eq.type` change rewrite behavior? · Coq users

The behavior of rewrite seems to change when core.eq.type is registered. Before doing this rewrite <- (inv_V q). would rewrite along the equality however now it looks for a subterm (inv_V q) in the goal.

Hugo Herbelin (Aug 20 2020 at 15:22):

Hi, the problem is actually not to bind core.eq.type per se but to bind core.eq.type to an equality in Type. This is because this affects the default form of the _ind elimination scheme which changes from:

forall (A : Type) (a : A) (P : A -> Prop), P a -> forall y : A, eq A a y -> P y

forall (A : Type) (a : A) (P : forall a0 : A, eq A a a0 -> Prop), P a (refl A a) -> forall (y : A) (e : eq A a y), P y e

Then unification (which rewrite expects to be non-trivial, i.e. with - in your case - inv_V q actually occurring in the goal) does not work any more.

Ali Caglayan (Aug 20 2020 at 16:23):

Gaëtan Gilbert (Aug 20 2020 at 16:40):

Don't register the auto generated eliminator, instead define a less dependent one and register that

Ali Caglayan (Aug 20 2020 at 18:08):

I'm a bit confused however since the problem only occurs when core.eq.type is set. Setting core.eq.ind doesn't seem to effect anything. It seems to me that rewrite is just sticking _ind to the end of whatever core.eq.type was set as.

Hugo Herbelin (Aug 21 2020 at 13:22):

Ali Caglayan (Aug 21 2020 at 14:20):

What would need to be done to avoid this then? Would we need to change rewrite to not call lookup_eliminator?

Paolo Giarrusso (Aug 22 2020 at 09:00):

Could you unset Default Elimination Schemes and write your own scheme with the _ind name?

Hugo Herbelin (Aug 22 2020 at 09:13):

Actually, the code already avoids lookup_eliminator if there is a coq.eq.ind (resp. coq.eq.rect) is registered and the statement is in Prop (resp. Type or Set). So, in the PathGroupoids.v case, core.eq.ind had no impact. It is core.eq.rect which would have one.

An extra requirement is also to bind core.eq.ind or core.eq.rect to the non-dependent eliminators (which is not the case for paths_ind and paths_rect in HoTT, thus requiring indeed to write your own scheme). To rewrite from left to right, core.eq.ind_r and core.eq.rect_r also matter.

Hugo Herbelin (Aug 22 2020 at 09:28):

Since there is a way to register ind and rect eliminator, calling lookup_eliminator indeed does not seem so anymore really necessary in the code of rewrite. Relying on registrations should be enough (and either failing or using the automatic generation of a scheme if the registration is missing).

Ali Caglayan (Aug 22 2020 at 16:33):

I had a poke around in rewrite.ml so it looks like Ind_tables.lookup_scheme is called which depends on the sorts in question. This is a Names.Constant.t in a maybe. I tried to use the registered variables core.eq.rect and friends but I am not sure how to adapt the existing code the use these.

Ali Caglayan (Aug 22 2020 at 16:34):

Hugo Herbelin (Aug 24 2020 at 07:03):

rewrite.ml is for setoid rewriting. The basics of rewriting are in tactics/equality.ml. Look at function find_elim. I suspect that we could drop the whole case mentioning lookup_eliminator, redirecting to the find_scheme part if the expected ind, rect, ind_r, ... is not found when calling eq_elimination_ref. At the same time, we could primitively add the various cases corresponding to core.identity.type and core.JMeq.type in eq_elimination_ref.

The function fold_match in rewrite.ml is to replace a match ... with ... end by a combinator case_rect ... ... so that congruence of a setoid equality is easier to apply.

Stream: Coq users

Topic: Why does registering `core.eq.type` change rewrite behavior?

Ali Caglayan (Aug 18 2020 at 15:02):