mulr_rev out of forms.v (#1122)

Cleanup mulr_rev and revop

CHANGELOG_UNRELEASED.md

@@ -33,6 +33,9 @@
 
 ### Changed
 
+- in `forms.v`:
+  + notation ``` u ``_ _ ```
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -92,6 +95,14 @@
 - in `measure.v`:
   + lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup`
     (use `measurable0`, `measurableC`, `measurable_bigcup` instead)
+- in `derive.v`:
+  + definition `mulr_rev`
+  + canonical `rev_mulr`
+  + lemmas `mulr_is_linear`, `mulr_rev_is_linear`
+
+- in `forms.v`
+  + canonical `rev_mulmx`
+  + structure `revop`
 
 ### Infrastructure
 

classical/mathcomp_extra.v

@@ -459,7 +459,7 @@ Inductive boxed T := Box of T.
 Reserved Notation "`1- r" (format "`1- r", at level 2).
 Reserved Notation "f \^-1" (at level 3, format "f \^-1", left associativity).
 
-(* To be backported to finmap *)
+(* TODO: To be backported to finmap *)
 
 Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
     (f : X -> nat) : A != fset0 ->

theories/derive.v

@@ -826,19 +826,6 @@ Proof.
 by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc.
 Qed.
 
-Definition mulr_rev (y x : R) := x * y.
-Canonical rev_mulr := @RevOp _ _ _ mulr_rev (@GRing.mul R) (fun _ _ => erefl).
-
-Lemma mulr_is_linear x : linear (@GRing.mul R x : R -> R).
-Proof. by move=> ???; rewrite mulrDr scalerAr. Qed.
-HB.instance Definition _ x := GRing.isLinear.Build R R R _ ( *%R x)
-  (mulr_is_linear x).
-
-Lemma mulr_rev_is_linear y : linear (mulr_rev y : R -> R).
-Proof. by move=> ???; rewrite /mulr_rev mulrDl scalerAl. Qed.
-HB.instance Definition _ y := GRing.isLinear.Build R R R _ (mulr_rev y)
-  (mulr_rev_is_linear y).
-
 Lemma mulr_is_bilinear :
   bilinear_for
     (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)

theories/forms.v

@@ -1,11 +1,7 @@
 From HB Require Import structures.
-From mathcomp
-Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
-From mathcomp
-Require Import matrix mxalgebra vector falgebra ssrnum algC algnum.
-From mathcomp
-Require Import fieldext.
-From mathcomp Require Import vector.
+From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
+From mathcomp Require Import matrix mxalgebra vector falgebra ssrnum fieldext.
+From mathcomp Require Import vector mathcomp_extra.
 
 (**md**************************************************************************)
 (* # Bilinear forms                                                           *)
@@ -31,18 +27,13 @@ Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
 Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
 Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").
 
-Notation "u '``_' i" := (u (GRing.zero [the zmodType of 'I_1]) i) : ring_scope.
+Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope.
 Notation "''e_' i" := (delta_mx 0 i)
  (format "''e_' i", at level 3) : ring_scope.
 
 Local Notation "M ^ phi" := (map_mx phi M).
 Local Notation "M ^t phi" := (map_mx phi (M ^T)) (phi at level 30, at level 30).
 
-Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
-  fun_of_revop :> X -> Y -> Z;
-  _ : forall x, f x =1 fun_of_revop^~ x
-}.
-
 Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) :
   f =1 id -> M ^ f = M.
 Proof. by move=> /eq_map_mx->; rewrite map_mx_id. Qed.
@@ -197,9 +188,6 @@ End BidirectionalLinearZ.
 
 End BilinearTheory.
 
-Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
-  (@mulmx R m n p) (fun _ _ => erefl).
-
 Lemma mulmx_is_bilinear (R : comRingType) m n p :
   bilinear_for
     (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)