Stream: Coq users

Topic: SProp Unification Failure


view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 02:00):

From HoTT Require Import Basics.

Section StrictProp.
  Context (P Q : SProp).
  Context (P_to_Q : forall _ : P, Q).
  Context (Q_to_P : forall _: Q, P).

  Definition PQ_Equiv : IsEquiv P_to_Q.
  Proof.
    unshelve eapply Build_IsEquiv.
    - exact Q_to_P.
    - intro x.
             (* Prove P_to_Q (Q_to_P x) = x *)
      reflexivity.

I think the proof of reflexivity should succeed, but I get the error message

Unable to unify "x" with "P_to_Q (Q_to_P x)".

This is surprising as SProp has definitional proof irrelevance.

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 02:01):

Now in this example I have not assumed cumulative universe checking, which is a problem as an IsEquiv is only defined between two types. So I should expect some kind of error eventually. But it doesn't make sense to me why I should get a unification error.

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 02:02):

If I do add the assumption of cumulativity I still get the error. Now maybe I can chalk that up to the warning that typechecking is not complete if cumulativity is assumed.

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 02:06):

If I prove forall (x : Q), x = P_to_Q (Q_to_P x) as a lemma on its own, I can prove it by reflexivity and then I can use that lemma later.

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 02:30):

Also when the documentation says "Status of SProp is experimental In particular, conversion checking through bytecode or native code compilation currently does not understand proof irrelevance." To my understanding there are two versions of Coqc and Coqctop, one is the bytecode version and one is the native code compilation version, so this error messages reads to me something like "In particular, conversion checking in Coq does not understand proof irrelevance."
It would be helpful to say what works in SProp.

view this post on Zulip Paolo Giarrusso (Dec 11 2022 at 02:43):

The "two versions of coqc/coqtop" issue should be orthogonal, that text is most likely talking about the vm_compute and native_compute tactics

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 04:27):

I tried to minimize it and got an anomaly which i reported on the issue tracker

view this post on Zulip Patrick Nicodemus (Dec 11 2022 at 18:27):

Ok, I talked to Gaetan Gilbert on the Github issue tracker and he said that this is to be expected as part of how Cumulative SProp works, I guess that typechecking /unification is undecidable in general if this flag is enabled but are there any positive guidelines which suggest when we should be able to unify?

view this post on Zulip Gaëtan Gilbert (Dec 11 2022 at 18:32):

https://coq.github.io/doc/master/refman/addendum/sprop.html#issues-with-non-cumulativity
the "The implementation of proof irrelevance uses inferred "relevance" marks on binders to determine which variables are irrelevant. " paragraph
any use of cumulativity which makes a binder change proof relevance status will stop coq from considering that variable irrelevant


Last updated: Jun 25 2024 at 18:02 UTC