Hi,

I am encountering the following error message ```
The term "f" has type "Box i j" while it is expected to have type
"Box (i ++ []) (j ++ [])".
```

when defining some operations on types.

What bugs me is that the Coq had no issues equating `Box i j`

and `Box ([] ++ i) ([] ++ j)`

.

This is somehow expected since `[]++i`

can be simplified (compare the proofs of `app_nil_r`

and `app_nil_l`

).

I wonder if there a way to add hints to the type resolution for non trivial cases, i.e., lemmas like `app_nil_r`

?

Thanks

This is not possible *per se*, as the type-checker knows only about certain equalities, and these are "hardcoded", so it is not possible to change these from the user side (although being able to do this is a long dream, and there is currently work in progress on a Coq Enhancement Proposal to allow this in some reasonable cases). However, depending on your setting you might be able to use of of the various mechanisms to hook into elaboration to try and automatically "change" `f`

to something that has the right type, by performing the relevant rewrites. But this might incur more problems than it solves, though…

Indeed, I followed some advice from https://stackoverflow.com/questions/52514957/coq-use-equality-of-types-for-type-checking-a-term-in-a-definition and defined my own cast operator.

I could define the following lemma, using the `cast`

function discussed in this post

```
Lemma box_plus_id_right2 {i j} (f : Box i j) :
box_plus f Box_plus_id ≈ cast (Box i j) (Box_app_nil i j) (p i j) f.
```

but this is a dead-end as it won't be usable in another record that requires typical commutativity lemma definitions, i.e. without a cast.

Also, the proof term is just ugly.

The sibling lemma is much trivial

```
Lemma box_plus_id_left {i j} (f : Box i j) :
box_plus Box_plus_id f ≈ f.
Proof.
now decompose.
Qed.
```

where `decompose`

is just destruct + simpl.

It seems the CEP you mentioned is fairly advanced. Any chance it can make it to 8.19?

In my experience, the issue you're hitting is an indication that you shouldn't be using dependent types, and that refactoring your development to have `Box : Type`

with `get_i get_j : Box -> _`

and then proving the properties you want about these projections on the side will simplify the code. Is this feasible in your case?

Indeed, I started refactoring like you suggested yesterday. Will see how far this goes.

Jerome Hugues said:

It seems the CEP you mentioned is fairly advanced. Any chance it can make it to 8.19?

These things take time, not sure this CEP is lined up for 8.19… But maybe we can ask the people who know? @Théo Winterhalter @Yann Leray?

I hope that we get it for 8.19 (and I *think* this is the plan). But this wouldn't help much with the problem at hand since you'd have to axiomatize lists. Also, I think that recommending rewrite rules to work around fundamental issues about decidability of type checking is a recipe for disaster (especially if it's a blanket answer to newcomers struggling with Coq) but YMMV.

branch is in 2 weeks so I'm not very optimistic about it getting in 8.19

isn't the PR basically ready though?

I agree that recommanding rewrite rules as the solve-all mechanism to patch all kind of issues with definitional equalities is very much handing everyone an awesome footgun and letting them run wild. (Note that I did *not* advise this as a solution.) Yet, one of the basic elements of propaganda for rewrite rules is to have "+ compute on both sides" which is also the problem at hand here…

one of the basic elements of propaganda

That's precisely the propaganda I'm propaganding against. Rewrite rules are an *advanced* feature to hack the rules of your type theory, not a magic wand to solve your unification issues. The commutative plus is a very bad advertisement, RR should be put on the same shelf as type-in-type. We don't recommend our users to unset universe checking when they face inconsistencies, do we?

Do they need to be so advanced and unsafe? As an outsider, I thought there was research on automatically checking if some proven rewrite rules are also safe.

Dunno how advanced that is, and how well it transfers from CIC (with say eliminators?) to Coq.

(and I remember seeing surprises in Agda)

In any case, using indexed types here will remain problematic until safe rewrite rules are available

As long as you add rewrite rules on fresh symbols and they are confluent (which Agda checks, not sure the v1 implementation in Coq does), they are relatively safe (subject reduction is still ok, and all invertibilities of conversion rules that the conversion-checker relies on are still true too – the only incompleteness that can creep in can come from non-termination). At least that is the pen-and-paper version. But 1) there are non-trivial interactions with pattern-matching (and the guard condition), which is a big source of headaches 2) I'm not sure we want to replace all/many of the currently defined symbols (such as +) into primitive constants + RR…

another perhaps obvious what-if: could one conceivably prove rewrite rules confluent in Coq itself and use MetaCoq to get them added?

relatively safe

You can break consistency just like with axioms, though.

Pierre-Marie Pédrot said:

relatively safe

You can break consistency just like with axioms, though.

Ofc, I forget that having a working type-checker is not enough for most people's desires ^^' But if you add only consistent RR (in the sense that for a symbol `foo`

you only add rewrite rules such that there is some `foo'`

definable in CIC which propositionally satisfies all these equations together), you are conservative over ETT, and thus in particular consistent (if ETT is, at least)?

Karl Palmskog said:

another perhaps obvious what-if: could one conceivably prove rewrite rules confluent in Coq itself and use MetaCoq to get them added?

Well, it would still need to be a modular criterion otherwise you would have to redo the proof every time.

Karl Palmskog said:

another perhaps obvious what-if: could one conceivably prove rewrite rules confluent in Coq itself and use MetaCoq to get them added?

I think actually the criterion that is implemented in Agda implies confluence but is stronger than it. The pragma is that you want a *modular* criterion, ie you can check sets of rules in isolation, and if each set satisfies the criterion the whole union also will. That way, you do not need to re-check the interaction between new RR and all the ones you have in context each time you define one (and also no issues at importing two modules defining their RR, etc.)

The current plan by @Yann Leray is to be a bit more flexible, but only recheck confluence of the part of the union that are not orthogonal (ie that add rewrite rules to the same symbol).

anyway, I ask because I was using the Maude rewriting logic for a while, and it had a confluence checker for rules, but it was incomplete and one would have liked to be able to prove confluence or something stronger manually

I agree that anything that is incomplete should come with an espace hatch to be able to inject proofs. I guess we'll study how feasible and how needed it is when we reach that point. :smile:

(Should we move this discussion to a different thread btw?)

I was about to suggest it ;-) I like the exchange, but it seems a huge chunk of it belong to the CEP or the GitHub PR

That being said, thanks for the discussion: I understand a lot more the issues with the RR and why you are cautious about them.

21 messages were moved from this topic to #Coq users > Rewriting rules extension by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC