Mv translation techno from Coquelicot to math-comp to file Coquelicot_ssr.v.

FEM/Coquelicot_ssr.v

+Require Import Epsilon_instances choiceType_from_Epsilon.
+
+From Coquelicot Require Import Coquelicot.
+
+From mathcomp Require Import bigop vector ssrfun tuple fintype matrix perm order.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat ssralg.
+From mathcomp Require Import seq path poly choice finfun finset fingroup all_algebra.
+From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
+
+Require Import Rstruct.
+
+
+(*Local Open Scope ring_scope.*)
+
+(** Bridge between canonical structures from Coquelicot to math-comp/ssreflect. *)
+
+
+Section AbelianGroup_zmodType.
+
+Variable G : AbelianGroup.
+
+Axiom AG_eq_EM_T : forall (r1 r2 : G), {r1 = r2} + {r1 <> r2}.
+
+Definition eqAG (r1 r2 : G) : bool :=
+  if AG_eq_EM_T r1 r2 is left _ then true else false.
+
+Lemma eqAG_P : Equality.axiom eqAG.
+Proof.
+by move=> r1 r2; rewrite /eqAG; case: AG_eq_EM_T=> H; apply: (iffP idP).
+Qed.
+
+Canonical Structure AG_eq_Mixin := EqMixin eqAG_P.
+
+Canonical Structure AbelianGroup_eqType := Eval hnf in EqType G AG_eq_Mixin.
+
+Axiom AG_epsilon_statement :
+  forall (P : G -> Prop), {x | (exists x0, P x0) -> P x}.
+
+Definition AG_choice_Mixin := EpsilonChoiceMixin AG_epsilon_statement.
+
+Canonical Structure AbelianGroup_choiceType := Eval hnf in ChoiceType G AG_choice_Mixin.
+
+Lemma AG_plusA : associative (@plus G).
+Proof.
+exact: plus_assoc.
+Qed.
+
+Lemma AG_plusC : commutative (@plus G).
+Proof.
+exact: plus_comm.
+Qed.
+
+Lemma AG_plus_zero_l : left_id (@zero G) plus.
+Proof.
+exact: plus_zero_l.
+Qed.
+
+Lemma AG_plus_opp_l : left_inverse (@zero G) opp plus.
+Proof.
+exact: plus_opp_l.
+Qed.
+
+Definition AG_zmodType_Mixin :=
+  ZmodMixin AG_plusA AG_plusC
+    AG_plus_zero_l AG_plus_opp_l.
+
+Canonical Structure AbelianGroup_zmodType := Eval hnf in ZmodType G AG_zmodType_Mixin.
+
+End AbelianGroup_zmodType.
+
+
+Section Ring_ringType.
+
+(* Ring from Coquelicot is a ringType from math-comp. *)
+
+Variable G : Ring.
+
+Lemma Ring_multA : @associative (AbelianGroup_zmodType G) (@mult G).
+Proof.
+exact: mult_assoc.
+Qed.
+
+Lemma Ring_mult_1_l : left_id (@one G) mult.
+Proof.
+exact: mult_one_l.
+Qed.
+
+Lemma Ring_mult_1_r : right_id (@one G) mult.
+Proof.
+exact: mult_one_r.
+Qed.
+
+Lemma Ring_mult_plus_distr_r : right_distributive (@mult G) plus.
+Proof.
+exact: mult_distr_l.
+Qed.
+
+Lemma Ring_mult_plus_distr_l : left_distributive (@mult G) plus.
+Proof.
+exact: mult_distr_r.
+Qed.
+
+Axiom Ring_1_neq_0 : (@one G) != zero.
+
+Definition Ring_ringType_Mixin := 
+  RingMixin Ring_multA mult_one_l mult_one_r mult_distr_r mult_distr_l Ring_1_neq_0.
+
+Canonical Structure Ring_ringType :=
+  (*Ring.Pack  (zmodType_AbelianGroup G)
+    (Ring.Class _ _ ringType_Ring_mixin) (zmodType_AbelianGroup G)*).
+
+The term "Ring_multA" has type "@associative (Ring.sort G) (@mult G)" while it is expected to have type
+ "@associative (GRing.Zmodule.sort ?R) ?mul".
+
+
+End Ring_ringType.

FEM/_CoqProject

@@ -13,3 +13,4 @@ Rstruct.v
 finite_element.v
 poly_Mathcomp.v
 ssr_Coquelicot.v
+Coquelicot_ssr.v

FEM/ssr_Coquelicot.v

-(*From Coq Require Import Lia Reals Lra.
-From Coq Require Import PropExtensionality FunctionalExtensionality ClassicalDescription ClassicalChoice ClassicalEpsilon.
-From Coq Require Import List.*)
 From Coquelicot Require Import Coquelicot.
 
-(*
-Add LoadPath "../Lebesgue" as Lebesgue.
-From Lebesgue Require Import Function LInt_p FinBij.
-*)
-
-Add LoadPath "../LM" as LM.
-From LM Require Import linear_map.
-
 From mathcomp Require Import bigop vector ssrfun tuple fintype matrix perm order.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat ssralg.
 From mathcomp Require Import seq path poly choice finfun finset fingroup all_algebra.
-
-(*From SsrMultinomials Require Import mpoly.*)
-
 From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
 
-(*Require Import Rstruct.*)
-
-
-(** Matrices are a ModuleSpace *)
+Require Import Rstruct.
 
 Local Open Scope ring_scope.
 
+(** Bridge between canonical structures from math-comp/ssreflect to Coquelicot. *)
+
 Section zmodType_AbelianGroup.
 
 Variable K : zmodType.
@@ -50,15 +35,16 @@ Proof.
 intros; rewrite zmodType_plus_comm; apply GRing.addNr.
 Qed.
 
-Definition zmodType_AbelianGroup_mixin :=
+Definition zmodType_AbelianGroup_Mixin :=
   AbelianGroup.Mixin K +%R -%R 0
     zmodType_plus_comm zmodType_plus_assoc zmodType_plus_zero_r zmodType_plus_opp_r.
 
 Canonical zmodType_AbelianGroup :=
-  AbelianGroup.Pack K zmodType_AbelianGroup_mixin K.
+  AbelianGroup.Pack K zmodType_AbelianGroup_Mixin K.
 
 End zmodType_AbelianGroup.
 
+
 Section ringType_Ring.
 
 (* ringType from math-comp is a Ring from Coquelicot. *)
@@ -91,83 +77,30 @@ Proof.
 apply GRing.mulrDr.
 Qed.
 
-Definition ringType_Ring_mixin :=
+Definition ringType_Ring_Mixin :=
   Ring.Mixin (zmodType_AbelianGroup G)  _ _
    ringType_mult_assoc ringType_mult_one_r ringType_mult_one_l ringType_mult_distr_r ringType_mult_distr_l.
 
-Canonical ringType_Ring :=
+Canonical Structure ringType_Ring :=
   Ring.Pack  (zmodType_AbelianGroup G)
-    (Ring.Class _ _ ringType_Ring_mixin) (zmodType_AbelianGroup G).
-
-End ringType_Ring.
-
-(*
-Section Facts2.
-
-Variable K : ringType.
-Variable m n : nat.
-
-Lemma truc : forall (A B : ringType_Ring K),  mult A B = mult B A.
-intros A B.
-rewrite <- mult_one_r.
-Admitted.
-
-(* i.e: A B \in 'M[K]_(m,n) which is a zmodType *)
- 
-Lemma truc3 : forall (A B : zmodType_AbelianGroup (matrix_zmodType K m n)),
-   plus A B = plus B A.
-intros A B.
-Admitted.
-
-(* write a lemma using ringType elements and operations,
-  but prove this lemma by applying coquelicot lemmas using the canonicals *)
-
-Lemma truc2 : forall (A B : K),  A * B = B * A.
-intros A B.
-rewrite -(@mult_one_r (ringType_Ring K) A).
-unfold mult; simpl.
-Admitted.
-
+    (Ring.Class _ _ ringType_Ring_Mixin) (zmodType_AbelianGroup G).
 
-Lemma matrix_plus_comm : forall A B : 'M[K]_(m, n), A + B = B + A.
-Proof.
-apply addmxC.
-Qed.
-
-Lemma matrix_plus_assoc : forall A B C : 'M[K]_(m, n), A + (B + C) = (A + B) + C.
-Proof.
-apply addmxA.
-Qed.
-
-Lemma matrix_plus_zero_r : forall A : 'M[K]_(m, n), A + 0 = A.
-Proof.
-intros; rewrite matrix_plus_comm; apply add0mx.
-Qed.
-
-Lemma matrix_plus_opp_r : forall A : 'M[K]_(m, n), A + (- A) = 0.
-Proof.
-intros; rewrite matrix_plus_comm; apply addNmx.
-Qed.
-
-Definition matrix_AbelianGroup_mixin :=
-  AbelianGroup.Mixin 'M[K]_(m, n) (@addmx K m n) (@oppmx K m n) 0
-    matrix_plus_comm matrix_plus_assoc matrix_plus_zero_r matrix_plus_opp_r.
+(* TODO: make (ringType_Ring real_ringType) of type R_Ring. *)
 
-Canonical matrix_AbelianGroup :=
-  AbelianGroup.Pack 'M[K]_(m, n) matrix_AbelianGroup_mixin 'M[K]_(m, n).
+End ringType_Ring.
 
-End Facts2.
-*)
 
 Section matrix_ModuleSpace.
 
+(** Matrices are a ModuleSpace *)
+
 Variable K : ringType.
 Variable m n : nat.
 
 Lemma matrix_scal_assoc: forall x y (A : 'M[K]_(m, n)),
    scalemx x (scalemx y A) = scalemx (x * y) A.
 Proof.
-apply scalemxA.
+apply scalemxA. (* exact: scalemxA is fine too! *)
 Qed.
 
 Lemma matrix_scal_one: forall (A : 'M[K]_(m, n)), scalemx 1 A = A.
@@ -181,13 +114,10 @@ Proof.
 apply scalemxDr.
 Qed.
 
-Lemma scalemxDl x y (A : 'M[K]_(m, n)) : scalemx (x + y) A = scalemx x A + scalemx y A.
-Proof. by apply/matrixP=> i j; rewrite !mxE GRing.mulrDl. Qed.
-
 Lemma matrix_scal_distr_l: forall (x y : K) (A : 'M[K]_(m, n)),
   scalemx (x + y) A = scalemx x A + scalemx y A.
 Proof.
-apply scalemxDl.
+intros; apply scalemxDl.
 Qed.
 
 (* The K below should be seen as a Ring that is why we constructed 
@@ -202,7 +132,22 @@ Definition matrix_ModuleSpace_mixin :=
 
 Canonical matrix_ModuleSpace :=
   ModuleSpace.Pack (ringType_Ring K) (zmodType_AbelianGroup (matrix_zmodType K m n))
-    (ModuleSpace.Class (ringType_Ring K) (zmodType_AbelianGroup (matrix_zmodType K m n)) _ matrix_ModuleSpace_mixin) (zmodType_AbelianGroup (matrix_zmodType K m n)).
+    (ModuleSpace.Class (ringType_Ring K) (zmodType_AbelianGroup (matrix_zmodType K m n))
+      _ matrix_ModuleSpace_mixin)
+    (zmodType_AbelianGroup (matrix_zmodType K m n)).
+
+Variable d : nat.
+
+(*Canonical Structure rV_ModuleSpace := Eval hnf in ModuleSpace (ringType_Ring real_ringType).*)
+(*'rV[R]_d*)
 
 End matrix_ModuleSpace.
 
+
+Section toto.
+
+Lemma toto : ringType_Ring real_ringType = R_Ring.
+Proof.
+Admitted.
+
+End toto.