(**
This file is part of the Coq Numerical Analysis library

Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(**

 * Bibliography

 #<DIV><A NAME="RR9557v1"></A></DIV>#
 [[RR9557v1]]
 François Clément and Vincent Martin,
 Finite element method. Detailed proofs to be formalized in Coq,
 RR-9557, first version, Inria Paris, 2024,
 #<A HREF="https://inria.hal.science/hal-04713897v1">#
 https://inria.hal.science/hal-04713897v1#</A>#.
*)

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Algebra Require Import Algebra_wDep.
From FEM Require Import R_compl multi_index poly_Pdk poly_LagP1k.
From FEM Require Import poly_LagPd1_ref LagP_node_ref.
From FEM Require Import geom_transf_affine poly_LagPd1.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.


Section Nodes_Facts1.

Context {d k : nat}.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1604, p. 101. *)
Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := T_geom vtx node_ref_d0.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Def 1588, Eq (9.80), p. 97. *)
Lemma node_d0_eq : forall vtx, node_d0 vtx = isobarycenter_ms vtx.
Proof.
intro; unfold node_d0; rewrite node_ref_d0_eqF T_geom_am;
    [rewrite T_geom_vtxF | apply invertible_plusn1_R]; easy.
Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1599, p. 100. *)
Lemma node_ref_d0_node : node_ref_d0 = node_d0 vtx_ref.
Proof. unfold node_d0; extF; rewrite T_geom_ref; easy. Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1604, p. 101. *)
Definition node (vtx : 'R^{d.+1,d}) (idk : 'I_(pbinom d k).+1) : 'R^d :=
  T_geom vtx (node_ref idk).

Lemma nodeF : forall vtx, node vtx = mapF (T_geom vtx) node_ref.
Proof. easy. Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1599, p. 100. *)
Lemma node_ref_node : node_ref = node vtx_ref.
Proof. unfold node; extF; rewrite T_geom_ref; easy. Qed.

Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.

Lemma node_inj : injective (node vtx).
Proof. move=>> /(T_geom_inj Hvtx) /node_ref_inj; easy. Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1605, Eq (9.95), p. 101. #<BR>#
 a_alpha \in Hface_0 <-> alpha \in CSdk. *)
Lemma node_Hface_0 :
  forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
    Hface vtx ord0 (node vtx idk) <-> sum (Adk d k idk) = k.
Proof.
intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
apply node_ref_Hface_ref_0; easy.
Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1605, Eq (9.96), p. 101. #<BR>#
 For i between 0 and d-1, we have
 a_alpha \in Hface_{i+1} iff alpha \in ASdki, ie alpha_i = 0. *)
Lemma node_Hface_S :
  forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0),
    (0 < d)%coq_nat -> (0 < k)%coq_nat ->
    Hface vtx i (node vtx idk) <-> Adk d k idk (lower_S Hi) = O.
Proof.
intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
apply node_ref_Hface_ref_S; easy.
Qed.

End Nodes_Facts1.


Section Nodes_Facts2.

(** We need a dimension which is structurally nonzero.
 We take d = d1.+1 with d1 : nat. *)
Context {d1 k : nat}.
Let d := d1.+1.
Variable vtx : 'R^{d.+1,d}.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1607, p. 102, case i=0.#<BR># 
 See also Rem 1606. *)
Lemma T_geom_Hface_0_node :
  forall (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat ->
    T_geom_Hface vtx ord0 (node_ref idk) =
      node vtx (Adk_inv d k (inj_CSdk idk)).
Proof.
intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_0_node_ref//.
Qed.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1607, p. 102, case i>0.#<BR>#
 See also Rem 1606. *)
Lemma T_geom_Hface_S_node :
  forall {i} (Hi : i <> ord0) (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat ->
    T_geom_Hface vtx i (node_ref idk) =
      node vtx (Adk_inv d k (inj_ASdki (lower_S Hi) idk)).
Proof.
intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//.
Qed.

End Nodes_Facts2.


Section Nodes_d1.

Context {d : nat}.

Lemma node_vtx_d1 : forall vtx, node vtx = castF (eq_sym (pbinomS_1_r d)) vtx.
Proof.
intro; extF; unfold node; rewrite node_vtx_ref_d1;
    unfold castF; rewrite T_geom_vtx; easy.
Qed.

Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.

Lemma LagPd1_decomp_node :
  forall {p}, Pdk d 1 p ->
    p = lin_comb (mapF p (node vtx))
      (castF (eq_sym (pbinomS_1_r d)) (LagPd1 Hvtx)).
Proof.
intro; rewrite node_vtx_d1 mapF_castF lc_castF; apply LagPd1_decomp_vtx.
Qed.

End Nodes_d1.


Section Sub_vertices_Def.

Context {d : nat}.
Variable k : nat.
Variable vtx : 'R^{d.+1,d}.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Def 1594, Eq (9.88), p. 98.
 sub_vtx 0 = \underline{v}_0 = v_0,
 sub_vtx i = \underline{v}_i = a_{(k-1)e^i}, for i <> 0. *)
Definition sub_vtx (i : 'I_d.+1) : 'R^d := T_geom vtx (sub_vtx_ref k i).
(* Could be: sub_vtx i := T_geom (sub_vtx_ref k) vtx. *)

Lemma sub_vtxF : sub_vtx = mapF (T_geom vtx) (sub_vtx_ref k).
Proof. easy. Qed.

End Sub_vertices_Def.


Section Sub_vertices_Facts0.

Context {d k : nat}.

Lemma sub_vtx_refF : @sub_vtx_ref d k = sub_vtx k vtx_ref.
Proof. rewrite sub_vtxF T_geom_ref; easy. Qed.

End Sub_vertices_Facts0.


Section Sub_vertices_Facts1.

Context {d k : nat}.
Hypothesis Hk : (1 < k)%coq_nat.
Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1597, pp. 99-100. *)
Lemma sub_vtx_aff_indep : aff_indep_ms (sub_vtx k vtx).
Proof.
apply (am_aff_indep (T_geom_am _));
    [apply T_geom_inj | apply sub_vtx_ref_aff_indep]; easy.
Qed.

End Sub_vertices_Facts1.


Section Sub_nodes_Def.

Context {d : nat}.
Variable k : nat.
Variable vtx : 'R^{d.+1,d}.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1604, p. 101. *)
Definition sub_node (idk : [0..(pbinom d k.-1).+1)) : 'R^d :=
  T_geom vtx (sub_node_ref idk).

Lemma sub_nodeF : sub_node = mapF (T_geom vtx) sub_node_ref.
Proof. easy. Qed.

Lemma sub_node_node : sub_node = node (sub_vtx k vtx).
Proof.
rewrite sub_nodeF nodeF sub_vtxF -T_geom_comp mapF_comp.
f_equal.


Admitted.

End Sub_nodes_Def.


Section Sub_nodes_Facts1.

Context {d k : nat}.
Hypothesis Hk : (1 < k)%coq_nat.
Variable vtx : 'R^{d.+1,d}.

(**
 #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
 Lem 1598, p. 100. *)
Lemma sub_node_eq :
  sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx).
Proof. extF; unfold sub_node; rewrite sub_node_ref_eq//. Qed.

End Sub_nodes_Facts1.


Section Sub_nodes_Facts2.

Context {d k : nat}.
Hypothesis Hd : (0 < d)%coq_nat.
Hypothesis Hk : (1 < k)%coq_nat.
Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.

(** sub_node \notin Hface_0 *)
Lemma sub_node_out_Hface_0 :
  forall (idk : [0..(pbinom d k.-1).+1)),
    ~ Hface vtx ord0 (sub_node k vtx idk).
Proof.
intro; rewrite -T_geom_Hface_eq// sub_nodeF mapF_correct Im_equiv;
    [apply sub_node_ref_out_Hface_ref_0 | apply T_geom_inj]; easy.
Qed.

End Sub_nodes_Facts2.