is_derive_trmx

[yosakaon]

This PR introduces is_derive_trmx instance, which provides automatic differentiation for transposed matrices.
It is particularly useful as the development uses a row-vector convention rather than the more common column-vector convention found in physics and mechanics literature.

Most of the code is from robot-rocq, co-authored by @affeldt-aist.

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I was a bit surprised that we need to insert this have. Maybe there is some automation in interval_inference.v that does not work as expected? @proux01 ?

[proux01]

Goal is widen_itv 0%:itv <= x (with the order on Itv.t), of course this is convertible to 0 <= x%:num (as shown by rewrite /Order.le/= /Order.PreCancelPartial.le/=) but trigerring hints for auto for ge0 do not match that syntactic pattern https://github.com/math-comp/math-comp/blob/900e37912dbecbd3c04d3c1b320efe721d3f56dd/algebra/interval_inference.v#L770 . So I'd say it's not expected to be simpler, except maybe by rewrite -num_le/=

[affeldt-aist]

@proux If this file (radon_nikodym.v) imports unstable.v (which now contains an instance of ComLaw for (@maxr {nonneg K}), then this line produces an error that I cannot explain.
The issue is easily avoided by not importint unstable.v but this is certainly a problem that will occur again later. Could you take a look?

[proux01]

Well, using @maxr {nonneg K} is probably asking for troubles. Seems safer to use @maxr K and reinfer the nonnegativity of the result when needed with an interval instance on maxr (which we should already have). I would refrain from adding this kind of instances.

[affeldt-aist]

When dealing with bigmax, {nonneg _} is nice because we have a neutral elements (0) and therefore access to more bigop lemmas. We will try again without it.

[proux01]

Yes but then everything comes with an interval and a proof that the value is in that interval, so you loose equality, you'll probably rapidly need morphism lemmas for %:num and bigops and thing can become painful. So not sure we want to engage in that direction. I agree that writing (\bigmax_i (F i)%:num)%:nng can be a bit heavy though, not sure what's best.

[proux01]

And to explain the error:

Print Canonical Projections Order.max (* HB.about could maybe also do the job *)
(* without loading unstable.v *)
(* Order.max <- Monoid.Law.sort ( Order_max__canonical__Monoid_Law ) *)
(* Order_max__canonical__Monoid_Law : forall {R : realDomainType}, Monoid.Law.type -oo%E (from constructive_ereal.v) *)
(* after loading it *)
(* Order.max <- Monoid.Law.sort ( unstable.Order_max__canonical__Monoid_Law ) *)

due to canonical structures matching on a single key, there can only be a single instance of Monoid.Law.sort on Order.max and we have to choose between them. By the way, having it on ereal is already a bit strange.
I guess the correct fix would be to have a structure of "max is a monoid operator", which maybe is Order.BPreorder, and put the monoid instance on it (and then ensure that both ereal and nonneg have that BPreorder instance).

[affeldt-aist]

@holgerthies I found two things puzzling about the the instance on @maxr {nonneg _}, I pinged @proux01 but maybe you already figured it out?

[proux01]

This looks like essentially two times the same proof, couldn't it be factored? (I would expect ``derivable M -> derivable M^Tto be enough to provederivable M^T -> derivable M` since `derivable M^T -> derivable M^T^T` and `M^T^T = M`)