Some ssr tactics do not seem to cohabit well with strict propositions, for instance the `have`

tactic:

```
From Coq Require Import ssreflect StrictProp.
Goal True.
(* build anything in SProp *)
have h := (fun x : sEmpty => x).
constructor.
Fail Qed.
(*
The command has indeed failed with message:
Illegal application:
The term "ssr_have" of type
"forall Plemma Pgoal : Type, Plemma -> (Plemma -> Pgoal) -> Pgoal"
cannot be applied to the terms
"sEmpty -> sEmpty" : "SProp"
"True" : "Prop"
"(fun x : sEmpty => x) : sEmpty -> sEmpty" : "sEmpty -> sEmpty"
"fun _ : sEmpty -> sEmpty => I" : "(sEmpty -> sEmpty) -> True"
The 1st term has type "SProp" which should be coercible to
"Type".
*)
```

Are there plans to handle SProp in ssr ? Should this kind of issues be tracked somewhere (in coq issues or mathcomp issues) ?

There are a lot of FIXME all over the place for SProp.

Given that there seem to be a non-trivial runtime cost when fixing them I am very wary of the battle plan...

Hum, is SProp <= Type? (this what the error says) Sorry for being ignorant on this TT matter.

If it is not the case, then the fix is to have a `ssr_have_sprop`

helper constant and pick the right one at runtime. Since the term is type checked anyway, I guess the overhead of typing the type to know what to pick would not be very expensive.

Nope.

So I guess we need 4 of these... since it has the type of the goal and the type of cut formula... how nice

what was it called? sort polymorphism?

Enrico Tassi said:

what was it called? sort polymorphism?

yes, some people are working on that

well, they got one silly use case right here ;-)

strictly speaking `have`

(as `cut`

) can be implemented without a constant, but that constant makes the `cut`

blocked. Dunno if it is still relevant these days.

So this implementation choice for `have`

is a matter of efficiency in unification or conversion problems ?

In the case of `have`

, I sometimes write an have for a strict proposition, get to Qed, realize it's invalid and go back in the script replacing all occurences of have with `pose`

/`pose proof`

or `assert`

, so it's more of an annoyance than a real problem (and I would perfectly understand if it were classified as won't fix until we have some working system of sort polymorphism).

Frankly I don't know, it predates my involvement in SSR. I imagine "conversion problems" if one has proof terms around (in the types he converts).

@Kenji Maillard indeed, the current fix for your example would be to use (possibly ssreflect's) `pose`

instead of `have:

```
Goal True.
pose h (x : sEmpty) := x.
constructor.
Qed.
```

But this does not provide access to a proof mode for local definitions/lemmas. But my understanding is that anyway the current state of affairs is still shaky when using tactics on strict goals...

Now that I think more about it, I believe that at some point in time Coq was beta-normalizing proofs (possibly at section closing time, to better detect unused variables).

If you do so, and you don't have an opaque ssr_have lemma to protect cuts, you may end up rediscovering the cost of cut elimination...

I don't think it is still the case, so maybe we can remove the hard lemma from have's implementation.

Isn't there some normalization (or at least some unfoldings) happening when checking guard conditions in fixpoint ?

@Kenji Maillard yes, and it's doing that in a backtracking way that might trigger cubic (?) behaviours

Last updated: Jun 10 2023 at 06:31 UTC