First try: vector space of finite dimension as a subspace

FEM/Finite_dim.v

+From Coquelicot Require Import Coquelicot.
+Add LoadPath "../LM" as LM.
+From LM Require Import check_sub_structure.
+
+
+Section FD.
+
+Context {E : ModuleSpace R_AbsRing}.
+
+
+Record FiniteDim := FD {
+  dim : nat ;
+  B : nat -> E ;
+  BO : B 0 = zero ; (* for an easier handling of dim=0 *)
+  phi :> E -> Prop 
+     := fun u => exists L : nat -> R,
+           u = sum_n (fun n => scal (L n) (B n)) dim ;
+}.
+
+
+(*
+Base orthonormée... 
+Context {E : Hilbert}.
+Record FiniteDim := FD {
+  dim : nat ;
+  B : nat -> E ;
+  BO : B 0 = zero ; (* for an easier handling of dim=0 *)
+  HB1 : forall (i:nat), (0 < i)%nat -> Hnorm (B i) = 1 ;
+  HB2 : forall i j, (0 < i < j)%nat -> (inner (B i) (B j)) = 0 ;
+  phi :> E -> Prop 
+     := fun u => exists L : nat -> R,
+           u = sum_n (fun n => scal (L n) (B n)) dim ;
+}.
+*)
+
+Lemma toto : forall P: FiniteDim, compatible_m P.
+Proof.
+intros P; destruct P; simpl.
+unfold phi; simpl.
+split.
+split.
+intros x y (Lx,HLx) (Ly,HLy).
+exists (fun n => minus (Lx n) (Ly n)).
+rewrite HLx, HLy.
+rewrite <- scal_opp_one.
+rewrite <- sum_n_scal_l, <- sum_n_plus.
+apply sum_n_ext; intros n.
+rewrite scal_opp_one.
+rewrite (scal_minus_distr_r (Lx n)); easy.
+exists zero.
+exists (fun _ => zero).
+apply sym_eq; clear.
+induction dim0.
+unfold sum_n, sum_n_m, Iter.iter_nat; simpl.
+rewrite plus_zero_r.
+apply (scal_zero_l (B0 0%nat)).
+rewrite sum_Sn.
+rewrite IHdim0, plus_zero_l.
+apply (scal_zero_l (B0 (S dim0))).
+intros x l (Lx,HLx).
+exists (fun n => scal l (Lx n)).
+rewrite HLx.
+rewrite <- sum_n_scal_l.
+apply sum_n_ext; intros n.
+rewrite scal_assoc; easy.
+Qed.
+
+
+(*Check (forall P: FiniteDim, Sg_ModuleSpace (toto P)).*)
+
+End FD.
\ No newline at end of file

FEM/quadrature.v

@@ -37,6 +37,14 @@ Hypothesis H_vert : (d < Nb_vert)%nat. (* dim E < Nb of vertices*)
 
 (* modéliser l'ev des fonctions à valeurs dans un ev pour abstraire (pour le rendre général) l'espace des polynomes ?? *)
 
+(* essai EVN *)
+Require Import Finite_dim.
+
+Variable Pol: (@FiniteDim (@fct_ModuleSpace E R_ModuleSpace)).
+Check (Pol (fun _ => 0)).
+Check (dim Pol).
+(* fin essai *)
+
 
 Definition geom : E -> Prop := 
   fun x => exists a : nat -> R, 
@@ -58,8 +66,8 @@ Definition sigma_hyp :=
 Hypothesis H_sigma_2 : forall p (* hyp que p est poly de deg <= k *), 
   (forall i, (i < Nb_vert)%nat ->  sigma i p = 0) -> forall x, p x = 0.
 
-Definition is_unisolvant : Prop :=  (* f : P *)
-  forall a : nat -> R, exists! f, P f /\ (forall i, (i < Nb_vert)%nat -> sigma i f = a i).
+Definition is_unisolvant : Prop :=  (*forall f : P,*)
+  forall a : nat -> R, exists! f, Pol f /\ (forall i, (i < Nb_vert)%nat -> sigma i f = a i).
 
 Lemma is_unisolvant_equiv : 
    is_unisolvant <->