Implicit argument inconsistency for `reflect` lemmas

[agontard]

I do not know of a reason why the following should have different implicit arguments

analysis/reals_stdlib/Rstruct.v

Lines 247 to 248 in fe37644

	Lemma RltP : forall x y, reflect (Rlt x y) (x < y)%R.
	Proof. exact: RltbP. Qed.

(from boot/ssrnat.v)

  Lemma ltP m n : reflect (m < n)%coq_nat (m < n).
  Proof. exact leP. Qed.
  Arguments ltP {m n}.

As a user, the second format is better to use, in particular with reflect_eq, see for example:

Notation "H **" := (reflect_eq H).
(...)
  rewrite thm1 ltP** andP** eqP** thm2.
  rewrite thm3 (RltP _ _)** (RleP _ _)** thm4.

[affeldt-aist]

Thanks for reporting the inconsistency.

Rstruct.v has clearly not been curated as much as MathComp files.
Still, for example, order.Order.TotalTheory.ltP does not have its x, y arguments implicit.
I am not sure about the policy here (@CohenCyril ?).
At least, the change has been implemented as PR #1806 so that the CI can give use a clue.

[CohenCyril]

They should be explicit so that one can write have [] := ltP x y for example.

[CohenCyril]

Sidenote: reflect_eq will hopfully become useless when typeclasses on Type and Prop get merge and reflect can be a rewritable relation.

[CohenCyril]

@affeldt-aist in #1806 (comment)_ wrote

Yes, the PR was done quickly to check the CI to fuel the discussion. It could be closed now, except that @agontard maybe found an inconsistency in MathComp proper (shouldn't the arguments of ltP be made explicit after all?).

Actually, after giving it a few more thoughts and taking a closer look, since this class of lemmas is seldom used directly with a have [] :=, I think you are right that, right now, these are most useful with maximal implicits instead, both for rewriting and applying high order view lemmas.

[affeldt-aist]

this class of lemmas is seldom used directly with a have [] :=,

There is a number of instances of have [|] := leP a b or have [|] := ltP a b for example (not the same ltP though).

[CohenCyril]

There is a number of instances of have [|] := leP a b or have [|] := ltP a b for example (not the same ltP though).

They are not the same kind of "P"-lemmas : they are spec lemmas and not reflect lemmas...