Kenji Maillard (Nov 02 2021 at 16:01): 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) ?
Pierre-Marie Pédrot (Nov 02 2021 at 16:02):There are a lot of FIXME all over the place for SProp.
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...
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.
Pierre-Marie Pédrot (Nov 02 2021 at 16:08):Nope.
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
Enrico Tassi (Nov 02 2021 at 16:10):what was it called? sort polymorphism?
Kenji Maillard (Nov 02 2021 at 16:10):Enrico Tassi said:
what was it called? sort polymorphism?
yes, some people are working on that
Enrico Tassi (Nov 02 2021 at 16:11):well, they got one silly use case right here ;-)
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.
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).
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).
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...
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.
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 ?
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: Oct 13 2024 at 01:02 UTC