Stream: math-comp devs

Topic: Compatibility of ssreflect and SProp


view this post on Zulip Kenji Maillard (Nov 02 2021 at 16:01):

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) ?

view this post on Zulip Pierre-Marie Pédrot (Nov 02 2021 at 16:02):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 02 2021 at 16:03):

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

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:06):

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.

view this post on Zulip Pierre-Marie Pédrot (Nov 02 2021 at 16:08):

Nope.

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:10):

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

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:10):

what was it called? sort polymorphism?

view this post on Zulip Kenji Maillard (Nov 02 2021 at 16:10):

Enrico Tassi said:

what was it called? sort polymorphism?

yes, some people are working on that

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:11):

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

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:12):

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.

view this post on Zulip Kenji Maillard (Nov 02 2021 at 16:23):

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

view this post on Zulip Enrico Tassi (Nov 02 2021 at 16:25):

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

view this post on Zulip Assia Mahboubi (Nov 04 2021 at 12:47):

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

view this post on Zulip Enrico Tassi (Nov 04 2021 at 13:52):

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.

view this post on Zulip Kenji Maillard (Nov 04 2021 at 14:25):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 04 2021 at 14:27):

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


Last updated: Aug 11 2022 at 02:03 UTC