Have a look at the CI in https://github.com/HoTT/HoTT/pull/1383

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.

What is going on and how can we avoid this?

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

to

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

What should we do to fix this?

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

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.

Ali Caglayan said:

It seems to me that rewrite is just sticking

`_ind`

to the end of whatever`core.eq.type`

was set as.

Indeed (by calling function `lookup_eliminator`

).

What would need to be done to avoid this then? Would we need to change `rewrite`

to not call `lookup_eliminator`

?

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

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.

Would we need to change rewrite to not call

`lookup_eliminator`

?

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

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.

This is all in fold_match

Ali Caglayan said:

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.

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

Last updated: Jan 31 2023 at 13:02 UTC