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

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.

See also this paragraph in the documentation

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

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

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

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

because the kernel doesn't have holes

Last updated: Jun 24 2024 at 12:02 UTC