From 10db5fe4bbf358d9f5fe99050b25f53fda0badd8 Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Fri, 18 Mar 2022 13:53:43 +0100
Subject: [PATCH] Finite dimension

---
 FEM/Finite_dim.v | 108 +++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 96 insertions(+), 12 deletions(-)

diff --git a/FEM/Finite_dim.v b/FEM/Finite_dim.v
index 1d88a9c1..dfc9dc09 100644
--- a/FEM/Finite_dim.v
+++ b/FEM/Finite_dim.v
@@ -1,3 +1,4 @@
+From Coq Require Import ClassicalDescription Epsilon.
 From Coquelicot Require Import Coquelicot.
 Add LoadPath "../LM" as LM.
 From LM Require Import check_sub_structure.
@@ -33,9 +34,23 @@ Record FiniteDim := FD {
 }.
 *)
 
-Lemma toto : forall P: FiniteDim, compatible_m P.
+Lemma FiniteDim_zero : forall P: FiniteDim, P zero.
 Proof.
-intros P; destruct P; simpl.
+intros P; unfold phi.
+exists (fun _ => zero).
+apply sym_eq; clear.
+induction (dim P).
+unfold sum_n, sum_n_m, Iter.iter_nat; simpl.
+rewrite plus_zero_r.
+apply (scal_zero_l (B P 0%nat)).
+rewrite sum_Sn.
+rewrite IHn, plus_zero_l.
+apply (scal_zero_l (B P (S n))).
+Qed.
+
+Lemma FiniteDim_compatible_m : forall P: FiniteDim, compatible_m P.
+Proof.
+intros P.
 unfold phi; simpl.
 split.
 split.
@@ -48,15 +63,7 @@ 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))).
+apply FiniteDim_zero.
 intros x l (Lx,HLx).
 exists (fun n => scal l (Lx n)).
 rewrite HLx.
@@ -68,4 +75,81 @@ Qed.
 
 (*Check (forall P: FiniteDim, Sg_ModuleSpace (toto P)).*)
 
-End FD.
\ No newline at end of file
+End FD.
+
+
+Section FD_bij.
+
+
+Context {E1 : ModuleSpace R_AbsRing}.
+Context {E2 : ModuleSpace R_AbsRing}.
+
+Variable F1: @FiniteDim E1.
+Variable F2: @FiniteDim E2.
+
+Hypothesis F12_dim: dim F1 = dim F2.
+
+Definition F1_to_F2 : E1 -> E2.
+intros x.
+case (excluded_middle_informative (F1 x)); intros H.
+2: apply zero. (*not in F1 *)
+unfold phi in H.
+apply constructive_indefinite_description in H.
+destruct H as (L,HL).
+apply (sum_n (fun n : nat => scal (L n) (B F2 n)) (dim F2)).
+Defined.
+
+
+Lemma F1_to_F2_in_F2 : forall x, F2 (F1_to_F2 x).
+Proof.
+intros x; unfold F1_to_F2.
+destruct (excluded_middle_informative (F1 x)).
+2: apply FiniteDim_zero.
+destruct (constructive_indefinite_description _) as (L,HL).
+exists L; easy.
+Qed.
+
+Definition F2_to_F1 : E2 -> E1.
+intros x.
+case (excluded_middle_informative (F2 x)); intros H.
+2: apply zero. (*not in F2 *)
+unfold phi in H.
+apply constructive_indefinite_description in H.
+destruct H as (L,HL).
+apply (sum_n (fun n : nat => scal (L n) (B F1 n)) (dim F1)).
+Defined.
+
+
+Lemma F2_to_F1_in_F1 : forall x, F1 (F2_to_F1 x).
+Proof.
+intros x; unfold F2_to_F1.
+destruct (excluded_middle_informative (F2 x)).
+2: apply FiniteDim_zero.
+destruct (constructive_indefinite_description _) as (L,HL).
+exists L; easy.
+Qed.
+
+Lemma F2_to_F1_to_F2 : forall x, F2 x -> (F1_to_F2 (F2_to_F1 x)) = x.
+Proof.
+intros x Hx.
+generalize (F2_to_F1_in_F1 x).
+unfold F2_to_F1.
+destruct (excluded_middle_informative (F2 x)).
+2: contradict Hx; easy.
+destruct (constructive_indefinite_description _) as (L,HL).
+intros Hxx.
+unfold F1_to_F2.
+destruct (excluded_middle_informative (F1 _)).
+2: contradict Hxx; easy.
+destruct (constructive_indefinite_description _) as (L',HL').
+rewrite HL.
+(* Pb: la base doit être non-redondante *)
+Admitted.
+
+
+
+
+
+
+
+End FD_bij.
-- 
GitLab