Stream: Coq users

Topic: Hints to address incompatible types ?


view this post on Zulip Jerome Hugues (Nov 10 2023 at 13:55):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 10 2023 at 18:06):

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…

view this post on Zulip Jerome Hugues (Nov 10 2023 at 18:29):

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?

view this post on Zulip Jason Gross (Nov 11 2023 at 21:30):

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?

view this post on Zulip Jerome Hugues (Nov 11 2023 at 22:36):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 13 2023 at 10:29):

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?

view this post on Zulip Pierre-Marie Pédrot (Nov 13 2023 at 10:47):

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.

view this post on Zulip Gaëtan Gilbert (Nov 13 2023 at 10:53):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 13 2023 at 10:53):

isn't the PR basically ready though?

view this post on Zulip Meven Lennon-Bertrand (Nov 13 2023 at 13:15):

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…

view this post on Zulip Pierre-Marie Pédrot (Nov 13 2023 at 13:37):

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?

view this post on Zulip Paolo Giarrusso (Nov 13 2023 at 18:51):

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.

view this post on Zulip Paolo Giarrusso (Nov 13 2023 at 18:52):

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

view this post on Zulip Paolo Giarrusso (Nov 13 2023 at 18:53):

(and I remember seeing surprises in Agda)

view this post on Zulip Paolo Giarrusso (Nov 13 2023 at 18:53):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 14 2023 at 10:02):

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…

view this post on Zulip Karl Palmskog (Nov 14 2023 at 10:03):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2023 at 10:03):

relatively safe

You can break consistency just like with axioms, though.

view this post on Zulip Meven Lennon-Bertrand (Nov 14 2023 at 10:09):

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

view this post on Zulip Théo Winterhalter (Nov 14 2023 at 10:11):

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.

view this post on Zulip Meven Lennon-Bertrand (Nov 14 2023 at 10:11):

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

view this post on Zulip Théo Winterhalter (Nov 14 2023 at 10:12):

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

view this post on Zulip Karl Palmskog (Nov 14 2023 at 10:14):

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

view this post on Zulip Théo Winterhalter (Nov 14 2023 at 10:16):

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:

view this post on Zulip Meven Lennon-Bertrand (Nov 14 2023 at 10:17):

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

view this post on Zulip Jerome Hugues (Nov 14 2023 at 11:28):

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.

view this post on Zulip Notification Bot (Nov 14 2023 at 12:14):

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


Last updated: Jun 13 2024 at 19:02 UTC