mulr_rev out of forms.v

math-comp · Dec 21, 2023 · d1d4cb8 · d1d4cb8
1 parent 316b42b
commit d1d4cb8
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 20 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -76,6 +76,13 @@
 	`ae_eq_mul1l`,
 	`ae_eq_abse`
 
+- move from `forms.v` to `mathcomp_extra.v`:
+  + structure `revop`
+
+- move from `derive.v` to `mathcomp_extra.v`:
+  + definition `mulr_rev`
+  + canonical `rev_mulr`
+
 ### Renamed
 
 - in `exp.v`:
@@ -90,6 +97,9 @@
 
 ### Removed
 
+- in `forms.v`:
+  + lemmas `eq_map_mx`, `map_mx_id`
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -1485,3 +1485,12 @@ exists n.+1; rewrite nm2/= -addn1.
 rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
 by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
 Qed.
+
+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
+}.
+
+Definition mulr_rev {R : ringType} (y x : R) := x * y.
+Canonical rev_mulr {R : ringType} :=
+  @RevOp _ _ _ mulr_rev (@GRing.mul [ringType of R]) (fun _ _ => erefl).
diff --git a/theories/derive.v b/theories/derive.v
@@ -808,10 +808,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 [ringType of R])
-  (fun _ _ => erefl).
-
 Lemma mulr_is_linear x : linear (@GRing.mul [ringType of R] x : R -> R).
 Proof. by move=> ???; rewrite mulrDr scalerAr. Qed.
 Canonical mulr_linear x := Linear (mulr_is_linear x).

diff --git a/theories/forms.v b/theories/forms.v
@@ -1,10 +1,7 @@
-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 algC.
+From mathcomp Require Import algnum fieldext vector.
+From mathcomp Require Import mathcomp_extra.
 
 (* From mathcomp Require classfun. *)
 
@@ -34,17 +31,14 @@ Notation "''e_' i" := (delta_mx 0 i)
 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 (R S : ringType) m n (M : 'M[R]_(m,n))
+(* NB(rei): already in MathComp *)
+(*Lemma eq_map_mx (R S : ringType) m n (M : 'M[R]_(m,n))
       (g f : R -> S) : f =1 g -> M ^ f = M ^ g.
-Proof. by move=> eq_fg; apply/matrixP=> i j; rewrite !mxE. Qed.
+Proof. by move=> eq_fg; apply/matrixP=> i j; rewrite !mxE. Qed.*)
 
-Lemma map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) : M ^ id = M.
-Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
+(* NB(rei): already in MathComp *)
+(*Lemma map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) : M ^ id = M.
+Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.*)
 
 Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) :
   f =1 id -> M ^ f = M.