SProp Unification Failure · Coq users

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.

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

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.

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.

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.

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.

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

Patrick Nicodemus (Dec 11 2022 at 04:27):

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?

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

Stream: Coq users

Topic: SProp Unification Failure

Patrick Nicodemus (Dec 11 2022 at 02:00):