prove bigop_ext lemma and merge files

FEM/comb_lin.v

 From Coq Require Import Lia Reals Lra FunctionalExtensionality.
 
-
 From Coquelicot Require Import Coquelicot.
 
 From mathcomp Require Import bigop vector all_algebra fintype tuple ssrfun.
@@ -10,27 +9,45 @@ From mathcomp Require Import seq path ssralg div tuple finfun.
 Add LoadPath "../LM" as LM.
 From LM Require Import linear_map.
 
+Notation "''' E ^ n" := ('I_n -> E)
+  (at level 8, E at level 2, n at level 2, format "''' E ^ n").
+
+(*
+Variables (R : Type) (idx : R) (op : R -> R -> R).
+Variable I : Type.
+Lemma big_pred0_eq (r : seq I) F : \big[op/idx]_(i <- r | false) F i = idx.
+Proof. 
+rewrite big_hasC.
+move => //.
+rewrite has_pred0.
+easy.
+Qed.*)
 
 Section bigop_compl.
 
+Context {A : Type}.
+Variables (idx : A) (op : A -> A -> A).
+
 Lemma bigop_ext :
-  forall {A : Type} (idx : A) (op : A -> A -> A) n (F G : 'I_n -> A),
+  forall n (F G : 'I_n -> A),
     (forall i : 'I_n, F i = G i) ->
     \big[op/idx]_(i < n) F i = \big[op/idx]_(i < n) G i.
 Proof.
-Admitted.
-
+intros n F G Hi.
+apply eq_bigr; easy.
+Qed.
 
-Lemma bigop_plus_0 : forall a, 
-   \big[plus%R/0]_(i < 0 | false) a i = 0.
+(* Check big_pred0_eq *)
+Lemma bigop_idx : forall F : 'I_0 -> A,
+   \big[op/idx]_(i < 0) F i = idx.
 Proof.
-intros a; apply big_pred0_eq.
+intros F.
+apply big_ord0.
 Qed.
 
-Search "big" "scal".
 (*
-Lemma bigop_plus_1 : forall a, 
-  \big[plus/0]_(i < 1) a i = a 0%R.
+Lemma bigop_plus_1 : forall F : 'I_1 -> A, 
+  \big[op/idx]_(i < 1) F i = F 0%R.
 Proof.
 intros a.
 apply big_ord1.
@@ -60,6 +77,9 @@ Section Linearity.
 
 Context {E F : ModuleSpace R_Ring}.
 
+(* Check big_endo. *)
+
+(*
 Lemma bigop_plus_linear: forall (v : E -> F) n (a : 'I_n-> R) (q : 'I_n -> E),
  is_linear_mapping v ->
   v (\big[plus%R/zero]_(i < n) scal (a i) (q i)) =
@@ -79,7 +99,7 @@ rewrite IHn.
 f_equal; intuition.*)
 admit.
 Admitted.
-
+*)
 (*
 Lemma sum_pn_scal : forall  l n (v:E),
   scal (sum_pn l n) v = sum_pn (fun i => scal (l i) v) n.
@@ -94,11 +114,6 @@ Qed.
 *)
 End Linearity.
 
-
-Notation "''' E ^ n" := ('I_n -> E)
-  (at level 8, E at level 2, n at level 2, format "''' E ^ n").
-
-
 Section Comb_lin1.
 
 Context {E : ModuleSpace R_Ring}.
@@ -140,16 +155,13 @@ Lemma comb_lin_ext :
     (forall i, scal (L i) (B i) = scal (M i) (C i)) ->
     comb_lin L B = comb_lin M C.
 Proof.
-intros L M B C H.
-unfold comb_lin.
-f_equal.
-apply functional_extensionality.
-intros i; rewrite H; easy.
+intros L M B C H; apply eq_bigr; easy.
 Qed.
 
 Lemma comb_lin_0_l : forall (L : 'R^n) B, L = zero -> comb_lin L B = zero.
 Proof.
 intros L B HL; rewrite HL.
+(* *)
 unfold comb_lin; apply bigop_zero.
 intros i; simpl; apply scal_zero_l.
 Qed.
@@ -178,9 +190,17 @@ f_equal; try easy.
 rewrite scal_assoc; easy.
 Qed.
 
+Lemma comb_lin_0 :
+  forall (L : 'R^n) (B : 'E^n),
+    (forall i, scal (L i) (B i) = zero) ->
+    comb_lin L B = zero.
+Proof.
+intros L B H.
+apply comb_lin_0_l.
 
-End Comb_lin1.
+Admitted.
 
+End Comb_lin1.
 
 Section Comb_lin2.
 
@@ -191,6 +211,8 @@ Lemma comb_lin_fun_compat :
   forall (L : 'R^n) (f : '(E -> F)^n) x,
     (comb_lin L f) x = comb_lin L (fun i => f i x).
 Proof.
+intros L f x.
+unfold comb_lin.
 Admitted.
 
 Lemma linear_mapping_comb_lin_compat :

FEM/kronecker.v

@@ -93,7 +93,6 @@ Section kronecker_bigop.
 Context {E : ModuleSpace R_Ring}.
 
 Lemma kronecker_bigop_l : forall n (j : 'I_n),
-  (*(j < n)%nat -> *)
   \big[plus%R/zero]_(i < n) (kronecker i j) = 1.
 Proof.
 (* old try *)
@@ -108,7 +107,6 @@ intros i; rewrite mult_one_l; easy.
 Admitted.
 
 Lemma kronecker_bigop_r : forall n (i : 'I_n),
-  (*(i < n)%nat -> *)
   \big[plus%R/zero]_(j < n) (kronecker i j) = 1.
 Proof.
 (*intros i n H1.
@@ -134,16 +132,18 @@ End kronecker_bigop.
 Section kronecker_bigop_scal.
 
 Context {E : ModuleSpace R_Ring}.
-Variable I : Type.
-Variable P : pred I.
 
 Lemma kronecker_bigop_scal_in_l : forall n (j : 'I_n) (a : 'E^n),
-  (* (j < n)%nat -> *)
   \big[plus/zero]_(i < n) scal (kronecker i j) (a i) = a j.
 Proof.
 intros n j a.
 induction n.
-erewrite <- big_pred0_eq. 
+(* *)
+erewrite <- bigop_plus_0.
+f_equal.
+admit.
+apply functional_extensionality; intros i; f_equal.
+ 
 (*
 rewrite bigop_plus_0; easy.
 (* *)