Stream: Coq users

Topic: Bug related to SProp?

view this post on Zulip Martin C (Feb 02 2021 at 10:19):

Hello,

I am struggling to understand why tst is able to be defined, while tst' is not (only difference it seems is the explicit type annotation on H H')... I am on Coq 8.13.

Is it expected behaviour? Are we not allowed to use type inference when dealing with SProp? 

Lemma tst :
  forall {sP : SProp} {T : Type} (H H' : sP) (f : sP -> T), f H = f H'.
Proof.
  intros.
  refine (eq_refl _).
Defined.

Lemma tst' :
  forall {sP : SProp} {T : Type} H H' (f : sP -> T), f H = f H'.
Proof.
  intros.
  Fail refine (eq_refl _).
Abort.

Thank you

Martin

view this post on Zulip Kenji Maillard (Feb 02 2021 at 10:27):

Hi @Martin C. I think this behaviour is expected with current implementation of SProp: in order to use definitional irrelevance, variables have to be marked as definitionally irrelevant and by the time the type of H and H' is found out to be sP : SProp they have already been marked as relevant (by default this is the only safe choice).
I'm not sure how fundamental this restriction is, but I guess backtracking to relabel H and H' as definitionally proof-irrelevant could be costly. As a result, the current design expects the user to explicitly annotate strict proposition when she relie on their peculiar behavior.

view this post on Zulip Kenji Maillard (Feb 02 2021 at 10:29):

See also this paragraph in the documentation

view this post on Zulip Kenji Maillard (Feb 02 2021 at 10:32):

And there seem to be a solution I was not aware of (but probably a bit fragile...)

Lemma tst' :
  forall {sP : SProp} {T : Type} H H' (f : sP -> T), f H = f H'.
Proof.
  intros.
  Fail refine (eq_refl _).
  exact_no_check (@eq_refl T (f H)).
Qed.

view this post on Zulip Martin C (Feb 02 2021 at 10:49):

Ok, understood, thank you very much for the detailed answer

view this post on Zulip Paolo Giarrusso (Feb 02 2021 at 12:00):

FWIW, the “fragility” of exact_no_check is that it will accept everything; all the checking will be done at Qed time.

view this post on Zulip Paolo Giarrusso (Feb 02 2021 at 12:00):

Which suggests the implementation restriction you mention doesn’t extend to the kernel.

view this post on Zulip Gaëtan Gilbert (Feb 02 2021 at 12:07):

because the kernel doesn't have holes

Last updated: Sep 30 2023 at 05:01 UTC