Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • mayero/coq-num-analysis
  • hamelin/test-ci-coq-num-analysis
  • arias/coq-num-analysis
3 results
Show changes
Commits on Source (6)
...@@ -563,7 +563,7 @@ Lemma fct_lm_ms_eq : ...@@ -563,7 +563,7 @@ Lemma fct_lm_ms_eq :
forall {f : E1 -> E2} O1 u1, fct_lm f O1 u1 = f (O1 + u1) - f O1. forall {f : E1 -> E2} O1 u1, fct_lm f O1 u1 = f (O1 + u1) - f O1.
Proof. unfold fct_lm; intros; rewrite ms_vect_eq ms_transl_eq; easy. Qed. Proof. unfold fct_lm; intros; rewrite ms_vect_eq ms_transl_eq; easy. Qed.
Lemma fct_lm_ms_eq_ex: Lemma fct_lm_ms_eq_ex :
forall {f lf : E1 -> E2}, forall {f lf : E1 -> E2},
lin_map lf -> lin_map lf ->
lf = fct_lm f 0 <-> exists c2, f = lf + (fun=> c2). lf = fct_lm f 0 <-> exists c2, f = lf + (fun=> c2).
......
...@@ -191,7 +191,7 @@ Lemma has_aff_dim_EX : ...@@ -191,7 +191,7 @@ Lemma has_aff_dim_EX :
forall PE n, has_aff_dim PE n -> { A : 'E^n.+1 | aff_basis PE A }. forall PE n, has_aff_dim PE n -> { A : 'E^n.+1 | aff_basis PE A }.
Proof. move=>> H; apply ex_EX; induction H as [A H]; exists A; easy. Qed. Proof. move=>> H; apply ex_EX; induction H as [A H]; exists A; easy. Qed.
Lemma has_aff_dim_ex: Lemma has_aff_dim_ex :
forall PE n, (exists A : 'E^n.+1, aff_basis PE A) -> has_aff_dim PE n. forall PE n, (exists A : 'E^n.+1, aff_basis PE A) -> has_aff_dim PE n.
Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed. Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed.
......
...@@ -120,7 +120,7 @@ Definition scalF_rev_closed : Prop := ...@@ -120,7 +120,7 @@ Definition scalF_rev_closed : Prop :=
Definition lc_closed : Prop := Definition lc_closed : Prop :=
forall n L (B : 'E^n), inclF B PE -> PE (lin_comb L B). forall n L (B : 'E^n), inclF B PE -> PE (lin_comb L B).
Definition compatible_ms : Prop:= compatible_g PE /\ scal_closed. Definition compatible_ms : Prop := compatible_g PE /\ scal_closed.
End Compatible_ModuleSpace_Def. End Compatible_ModuleSpace_Def.
......
...@@ -200,9 +200,9 @@ Lemma skipF_itemF_diag : ...@@ -200,9 +200,9 @@ Lemma skipF_itemF_diag :
forall n i0 (x : G), skipF i0 (itemF n.+1 i0 x) = 0. forall n i0 (x : G), skipF i0 (itemF n.+1 i0 x) = 0.
Proof. intros; rewrite skipF_replaceF; easy. Qed. Proof. intros; rewrite skipF_replaceF; easy. Qed.
Lemma skipF_itemF_0: Lemma skipF_itemF_0 :
forall (n : nat) (i0 : 'I_n.+1) (H:i0 <> ord0) (x : G), forall (n : nat) (i0 : 'I_n.+1) (H : i0 <> ord0) (x : G),
skipF ord0 (itemF n.+1 i0 x) = itemF n (lower_S H) x. skipF0 (itemF n.+1 i0 x) = itemF n (lower_S H) x.
Proof. Proof.
intros n i0 x H; rewrite skipF_first; unfold liftF_S; extF j. intros n i0 x H; rewrite skipF_first; unfold liftF_S; extF j.
case (ord_eq_dec (lift_S j) i0); intros H1. case (ord_eq_dec (lift_S j) i0); intros H1.
...@@ -501,7 +501,7 @@ Lemma lastF_zero_compat : ...@@ -501,7 +501,7 @@ Lemma lastF_zero_compat :
(forall i : 'I_(n1 + n2), (n1 <= i)%coq_nat -> A i = 0) -> lastF A = 0. (forall i : 'I_(n1 + n2), (n1 <= i)%coq_nat -> A i = 0) -> lastF A = 0.
Proof. move=>>; erewrite <- lastF_zero; apply lastF_compat. Qed. Proof. move=>>; erewrite <- lastF_zero; apply lastF_compat. Qed.
Lemma splitF_zero_compat: Lemma splitF_zero_compat :
forall {n1 n2} (A : 'G^(n1 + n2)), A = 0 -> firstF A = 0 /\ lastF A = 0. forall {n1 n2} (A : 'G^(n1 + n2)), A = 0 -> firstF A = 0 /\ lastF A = 0.
Proof. move=>>; apply splitF_compat. Qed. Proof. move=>>; apply splitF_compat. Qed.
......
...@@ -293,7 +293,7 @@ Section Monoid_Morphism_Sum_Facts3. ...@@ -293,7 +293,7 @@ Section Monoid_Morphism_Sum_Facts3.
Context {G1 G2 : AbelianMonoid}. Context {G1 G2 : AbelianMonoid}.
Context {T : Type}. Context {T : Type}.
Lemma sum_compF_r: Lemma sum_compF_r :
forall {n} (u : G1 -> G2) (f : '(T -> G1)^n), forall {n} (u : G1 -> G2) (f : '(T -> G1)^n),
morphism_m u -> sum (compF_r u f) = u \o sum f. morphism_m u -> sum (compF_r u f) = u \o sum f.
Proof. Proof.
......
...@@ -410,7 +410,7 @@ Section Sum_Facts3. ...@@ -410,7 +410,7 @@ Section Sum_Facts3.
Context {G : AbelianMonoid}. Context {G : AbelianMonoid}.
Context {T1 T2 : Type}. Context {T1 T2 : Type}.
Lemma sum_compF_l: Lemma sum_compF_l :
forall {n} (u : '(T2 -> G)^n) (f : T1 -> T2), sum (compF_l u f) = sum u \o f. forall {n} (u : '(T2 -> G)^n) (f : T1 -> T2), sum (compF_l u f) = sum u \o f.
Proof. Proof.
intros; fun_ext; intros; fun_ext;
......
...@@ -1756,7 +1756,7 @@ Hypothesis HG2 : @plus_is_reg_r G. ...@@ -1756,7 +1756,7 @@ Hypothesis HG2 : @plus_is_reg_r G.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grlex_S : Lemma grlex_S :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
grlex R x y <-> grlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ x ord0 <> y ord0 /\ R (x ord0) (y ord0) \/ sum x = sum y /\ x ord0 <> y ord0 /\ R (x ord0) (y ord0) \/
...@@ -1770,7 +1770,7 @@ Qed. ...@@ -1770,7 +1770,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grcolex_S : Lemma grcolex_S :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
grcolex R x y <-> grcolex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ x ord_max <> y ord_max /\ R (x ord_max) (y ord_max) \/ sum x = sum y /\ x ord_max <> y ord_max /\ R (x ord_max) (y ord_max) \/
...@@ -1784,7 +1784,7 @@ Qed. ...@@ -1784,7 +1784,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grsymlex_S : Lemma grsymlex_S :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
grsymlex R x y <-> grsymlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ y ord0 <> x ord0 /\ R (y ord0) (x ord0) \/ sum x = sum y /\ y ord0 <> x ord0 /\ R (y ord0) (x ord0) \/
...@@ -1803,7 +1803,7 @@ Proof. tauto. Qed. ...@@ -1803,7 +1803,7 @@ Proof. tauto. Qed.
(* The proof depends on the equality decidability hypothesis HG1, (* The proof depends on the equality decidability hypothesis HG1,
and the plus regularity hypothesis HG2. *) and the plus regularity hypothesis HG2. *)
Lemma grsymlex_S_mo : Lemma grsymlex_S_mo :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
monomial_order R -> monomial_order R ->
grsymlex R x y <-> grsymlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
...@@ -1826,7 +1826,7 @@ Qed. ...@@ -1826,7 +1826,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grevlex_S : Lemma grevlex_S :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
grevlex R x y <-> grevlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ y ord_max <> x ord_max /\ R (y ord_max) (x ord_max) \/ sum x = sum y /\ y ord_max <> x ord_max /\ R (y ord_max) (x ord_max) \/
...@@ -1841,7 +1841,7 @@ Qed. ...@@ -1841,7 +1841,7 @@ Qed.
(* The proof depends on the equality decidability hypothesis HG1, (* The proof depends on the equality decidability hypothesis HG1,
and the plus regularity hypothesis HG2. *) and the plus regularity hypothesis HG2. *)
Lemma grevlex_S_mo : Lemma grevlex_S_mo :
forall R {n} (x y :'G^n.+1), forall R {n} (x y : 'G^n.+1),
monomial_order R -> monomial_order R ->
grevlex R x y <-> grevlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/ sum x <> sum y /\ R (sum x) (sum y) \/
......
...@@ -98,7 +98,7 @@ Definition multF_closed : Prop := ...@@ -98,7 +98,7 @@ Definition multF_closed : Prop :=
Definition one_closed : Prop := PK 1. Definition one_closed : Prop := PK 1.
Definition compatible_r : Prop:= compatible_g PK /\ mult_closed /\ one_closed. Definition compatible_r : Prop := compatible_g PK /\ mult_closed /\ one_closed.
End Compatible_Ring_Def. End Compatible_Ring_Def.
...@@ -308,7 +308,7 @@ Definition sub_mult (x y : PK_g) : PK_g := ...@@ -308,7 +308,7 @@ Definition sub_mult (x y : PK_g) : PK_g :=
Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1). Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1).
Lemma sub_mult_assoc: Lemma sub_mult_assoc :
forall x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z. forall x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z.
Proof. intros; apply val_inj, mult_assoc. Qed. Proof. intros; apply val_inj, mult_assoc. Qed.
......
...@@ -45,7 +45,7 @@ Close Scope R_scope. ...@@ -45,7 +45,7 @@ Close Scope R_scope.
From Algebra Require Import Algebra_wDep. From Algebra Require Import Algebra_wDep.
From FEM Require Import multi_index poly_Pdk poly_LagP1k poly_LagPd1_ref. From FEM Require Import multi_index poly_Pdk poly_LagP1k poly_LagPd1_ref.
From FEM Require Import geom_transf_affine poly_LagPd1. From FEM Require Import geom_transf_affine poly_LagPd1.
From FEM Require Import LagP_node FE FE_transf. From FEM Require Import LagP_node_ref LagP_node FE FE_transf.
Local Open Scope Monoid_scope. Local Open Scope Monoid_scope.
Local Open Scope Group_scope. Local Open Scope Group_scope.
...@@ -153,6 +153,33 @@ Qed. ...@@ -153,6 +153,33 @@ Qed.
(** Induction step: unisolvence result for d,k>1. *) (** Induction step: unisolvence result for d,k>1. *)
Lemma unisolvence_inj_Hface :
forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat -> PI d k.+1 ->
forall i {vtx p}, aff_indep_ms vtx -> Pdk d.+1 k.+1 p ->
(forall (idk : [0..(pbinom d.+1 k.+1).+1)),
Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) ->
forall x, Hface vtx i x -> p x = 0.
Proof.
intros d k Hd Hk H i vtx p Hvtx Hp1 Hp2 x Hx.
assert (HSd : (0 < d.+1)%coq_nat) by apply S_pos.
assert (HSk : (0 < k.+1)%coq_nat) by apply S_pos.
rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
fold (T_geom_Hface_invS Hvtx i x).
pose (pi := fun y => p (T_geom_Hface vtx i y));
fold (pi (T_geom_Hface_invS Hvtx i x)).
rewrite (H _ vtx_ref_aff_indep pi)//.
apply T_geom_Hface_comp; easy.
extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi; rewrite -node_ref_node.
destruct (ord_eq_dec i ord0) as [-> | Hi].
(* i = ord0 *)
rewrite T_geom_Hface_0_node//; apply Hp2, node_Hface_0; [easy.. |].
apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
(* i <> ord0 *)
rewrite T_geom_Hface_S_node//; apply Hp2, (node_Hface_S Hvtx _ Hi HSd HSk).
rewrite Adk_inv_correct_r;
[apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
Qed.
Lemma unisolvence_inj_ind_LagPSdSk : Lemma unisolvence_inj_ind_LagPSdSk :
forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat -> forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat ->
PI d.+1 k -> PI d k.+1 -> PI d.+1 k.+1. PI d.+1 k -> PI d k.+1 -> PI d.+1 k.+1.
...@@ -300,7 +327,7 @@ Section FE_LagPdk_from_ref. ...@@ -300,7 +327,7 @@ Section FE_LagPdk_from_ref.
Lem 1604 (for k=0), p. 101.#<BR># Lem 1604 (for k=0), p. 101.#<BR>#
It is actually directly on the linear forms, rather than on the nodes. *) It is actually directly on the linear forms, rather than on the nodes. *)
Lemma Sigma_LagPd0_eq_from_ref : Lemma Sigma_LagPd0_eq_from_ref :
forall {d} (vtx :'R^{d.+1,d}) id0 p, forall {d} (vtx : 'R^{d.+1,d}) id0 p,
Sigma_LagPd0 vtx id0 p = Sigma_LagPd0 vtx id0 p =
Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)). Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)).
Proof. Proof.
...@@ -314,7 +341,7 @@ Qed. ...@@ -314,7 +341,7 @@ Qed.
Lem 1604 (for k>0), p. 101.#<BR># Lem 1604 (for k>0), p. 101.#<BR>#
It is actually directly on the linear forms, rather than on the nodes. *) It is actually directly on the linear forms, rather than on the nodes. *)
Lemma Sigma_LagPSdSk_eq_from_ref : Lemma Sigma_LagPSdSk_eq_from_ref :
forall {d} k (vtx :'R^{d.+1,d}) i p, forall {d} k (vtx : 'R^{d.+1,d}) i p,
Sigma_LagPSdSk k vtx i p = Sigma_LagPSdSk k vtx i p =
Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)). Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)).
Proof. Proof.
...@@ -323,7 +350,7 @@ rewrite comp_correct -node_ref_node T_geom_node; easy. ...@@ -323,7 +350,7 @@ rewrite comp_correct -node_ref_node T_geom_node; easy.
Qed. Qed.
Variable d k : nat. Variable d k : nat.
Context {vtx :'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
Definition FE_LagPdk_ref := FE_LagPdk k (@vtx_ref_aff_indep d). Definition FE_LagPdk_ref := FE_LagPdk k (@vtx_ref_aff_indep d).
...@@ -375,7 +402,7 @@ Section Face_unisolvence. ...@@ -375,7 +402,7 @@ Section Face_unisolvence.
Context {d k : nat}. Context {d k : nat}.
Hypothesis Hd : (1 < d)%coq_nat. Hypothesis Hd : (1 < d)%coq_nat.
Hypothesis Hk : (0 < k)%coq_nat. Hypothesis Hk : (0 < k)%coq_nat.
Context {vtx :'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
(** (**
...@@ -384,24 +411,24 @@ Hypothesis Hvtx : aff_indep_ms vtx. ...@@ -384,24 +411,24 @@ Hypothesis Hvtx : aff_indep_ms vtx.
Case i=0. *) Case i=0. *)
Lemma Hface_0_unisolvence : Lemma Hface_0_unisolvence :
forall p, Pdk d k p -> forall p, Pdk d k p ->
(forall idk : 'I_(pbinom d k).+1, (forall (idk : 'I_(pbinom d k).+1),
((pbinom d k.-1).+1 <= idk)%coq_nat -> p (node vtx idk) = 0) <-> Hface vtx ord0 (node vtx idk) -> p (node vtx idk) = 0) <->
(forall x, Hface vtx ord0 x -> p x = 0). (forall x, Hface vtx ord0 x -> p x = 0).
Proof. Proof.
assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl. assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
intros p Hp; split; intros p Hp; split; [| intros H idk Hidk; apply H; easy].
[| intros H idk Hidk; apply H, node_Hface_0; easy].
intros H x Hx; destruct d as [| d1]; [easy |]. intros H x Hx; destruct d as [| d1]; [easy |].
assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono. assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx ord0) x)//. rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx ord0) x)//.
fold (T_geom_Hface_invS Hvtx ord0 x). fold (T_geom_Hface_invS Hvtx ord0 x).
pose (p0:= fun y => p (T_geom_Hface vtx ord0 y)); pose (p0 := fun y => p (T_geom_Hface vtx ord0 y));
fold (p0 (T_geom_Hface_invS Hvtx ord0 x)). fold (p0 (T_geom_Hface_invS Hvtx ord0 x)).
rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep p0)//. rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep p0)//.
apply T_geom_Hface_comp; easy. apply T_geom_Hface_comp; easy.
extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, p0. extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, p0.
rewrite -node_ref_node T_geom_Hface_0_node//. rewrite -node_ref_node T_geom_Hface_0_node//.
apply H, Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//. apply H, node_Hface_0; [easy.. |].
apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
Qed. Qed.
(** (**
...@@ -410,12 +437,12 @@ Qed. ...@@ -410,12 +437,12 @@ Qed.
Case i<>0. *) Case i<>0. *)
Lemma Hface_S_unisolvence : Lemma Hface_S_unisolvence :
forall {i} (Hi : i <> ord0) p, Pdk d k p -> forall {i} (Hi : i <> ord0) p, Pdk d k p ->
(forall idk, Adk d k idk (lower_S Hi) = O -> p (node vtx idk) = 0) <-> (forall (idk : 'I_(pbinom d k).+1),
Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) <->
(forall x, Hface vtx i x -> p x = 0). (forall x, Hface vtx i x -> p x = 0).
Proof. Proof.
assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl. assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
intros i Hi p Hp; split; intros i Hi p Hp; split; [| move=> H idk Hidk; apply H; easy].
[| move=> H idk /(node_Hface_S Hvtx) Hidk; apply H, Hidk; easy].
intros H x Hx; destruct d as [| d1]; [easy |]. intros H x Hx; destruct d as [| d1]; [easy |].
assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono. assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//. rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
...@@ -426,7 +453,7 @@ rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep pi)//. ...@@ -426,7 +453,7 @@ rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep pi)//.
apply T_geom_Hface_comp; easy. apply T_geom_Hface_comp; easy.
extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi. extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi.
rewrite -node_ref_node T_geom_Hface_S_node//. rewrite -node_ref_node T_geom_Hface_S_node//.
apply H; rewrite Adk_inv_correct_r; apply H, (node_Hface_S Hvtx _ Hi Hd0 Hk); rewrite Adk_inv_correct_r;
[apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum]. [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
Qed. Qed.
......
...@@ -173,6 +173,7 @@ Variable vtx : 'R^{d.+1,d}. ...@@ -173,6 +173,7 @@ Variable vtx : 'R^{d.+1,d}.
sub_vtx 0 = \underline{v}_0 = v_0, sub_vtx 0 = \underline{v}_0 = v_0,
sub_vtx i = \underline{v}_i = a_{(k-1)e^i}, for i <> 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). 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). Lemma sub_vtxF : sub_vtx = mapF (T_geom vtx) (sub_vtx_ref k).
Proof. easy. Qed. Proof. easy. Qed.
...@@ -262,7 +263,7 @@ Variable vtx : 'R^{d.+1,d}. ...@@ -262,7 +263,7 @@ Variable vtx : 'R^{d.+1,d}.
Lemma T_geom_sub_nodeF : Lemma T_geom_sub_nodeF :
mapF (T_geom vtx) (sub_node k vtx_ref) = sub_node k vtx. mapF (T_geom vtx) (sub_node k vtx_ref) = sub_node k vtx.
Proof. Proof.
rewrite !sub_nodeF -mapF_comp T_geom_assoc -sub_vtx_refF sub_vtxF; easy. rewrite !sub_nodeF -mapF_comp T_geom_comp -sub_vtx_refF sub_vtxF; easy.
Qed. Qed.
(** (**
......
...@@ -60,8 +60,19 @@ Lemma node_ref_eqF : ...@@ -60,8 +60,19 @@ Lemma node_ref_eqF :
forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)). forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)).
Proof. intros; unfold node_ref; extF; rewrite div_eq mult_comm_R; easy. Qed. Proof. intros; unfold node_ref; extF; rewrite div_eq mult_comm_R; easy. Qed.
Lemma node_ref_inj : injective node_ref.
Proof.
case (Nat.eq_dec k 0); intros Hk.
(* *)
intros [i Hi] [j Hj] _; subst; apply ord_inj; simpl.
rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
(* *)
intros idk jdk; rewrite !node_ref_eqF;
move=> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
Qed.
Lemma node_ref_CSdk : Lemma node_ref_CSdk :
forall idk, (0 < d)%coq_nat -> (0 < k)%coq_nat -> forall (idk : 'I_(pbinom d k).+1), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
sum (node_ref idk) = 1 <-> ((pbinom d k.-1).+1 <= idk)%coq_nat. sum (node_ref idk) = 1 <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
Proof. Proof.
move=>> Hd Hk; rewrite -Adk_last_layer// node_ref_eqF -scal_sum_r sum_INR. move=>> Hd Hk; rewrite -Adk_last_layer// node_ref_eqF -scal_sum_r sum_INR.
...@@ -70,32 +81,20 @@ rewrite scal_eq_K mult_comm_R div_one_equiv// INR_eq_equiv; easy. ...@@ -70,32 +81,20 @@ rewrite scal_eq_K mult_comm_R div_one_equiv// INR_eq_equiv; easy.
Qed. Qed.
Lemma node_ref_ASdki : Lemma node_ref_ASdki :
forall idk j, (0 < k)%coq_nat -> forall idk i, (0 < k)%coq_nat -> node_ref idk i = 0 <-> Adk d k idk i = 0.
node_ref idk j = 0 <-> Adk d k idk j = 0%nat.
Proof. Proof.
move=>> /INR_n0 /invertible_equiv_R Hk. move=>> /INR_n0 /invertible_equiv_R Hk.
unfold node_ref; rewrite div_zero_equiv//; apply INR_0_equiv. unfold node_ref; rewrite div_zero_equiv// INR_0_equiv; easy.
Qed.
Lemma node_ref_inj : injective node_ref.
Proof.
case (Nat.eq_dec k 0); intros Hk.
(* *)
intros [i Hi] [j Hj] _; subst; apply ord_inj; simpl.
rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
(* *)
intros idk jdk; rewrite !node_ref_eqF;
move=> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
Qed. Qed.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1605 (for [vtx_ref]), Eq (9.95), p. 101. #<BR># Lem 1605 (for [vtx_ref]), Eq (9.95), p. 101. #<BR>#
\hat{a}_alpha \in \hat{Hface}_0 <-> alpha \in CSdk. *) \hat{a}_alpha \in \hat{Hface}_0 <-> alpha \in CSdk, ie \sum alpha = k. *)
Lemma node_ref_Hface_ref_0 : Lemma node_ref_Hface_ref_0 :
forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat -> forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
Hface_ref ord0 (node_ref idk) <-> ((pbinom d k.-1).+1 <= idk)%coq_nat. Hface_ref ord0 (node_ref idk) <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
Proof. intros; rewrite Hface_ref_0_eq//; apply node_ref_CSdk; easy. Qed. Proof. intros; rewrite Hface_ref_0_eq// node_ref_CSdk; easy. Qed.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
...@@ -106,7 +105,7 @@ Lemma node_ref_Hface_ref_S : ...@@ -106,7 +105,7 @@ Lemma node_ref_Hface_ref_S :
forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0), forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0),
(0 < d)%coq_nat -> (0 < k)%coq_nat -> (0 < d)%coq_nat -> (0 < k)%coq_nat ->
Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O. Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O.
Proof. intros; rewrite Hface_ref_S_eq; apply node_ref_ASdki; easy. Qed. Proof. intros; rewrite Hface_ref_S_eq node_ref_ASdki; easy. Qed.
End Node_ref_Facts1. End Node_ref_Facts1.
......
...@@ -98,20 +98,71 @@ Qed. ...@@ -98,20 +98,71 @@ Qed.
End T_geom_Facts1. End T_geom_Facts1.
Section T_geom_Facts2. Section T_geom_ref_Facts.
Context {d : nat}. Context {d : nat}.
Variable vtx1 vtx2 : 'R^{d.+1,d}.
Lemma T_geom_assoc : (**
T_geom vtx1 \o T_geom vtx2 = T_geom (mapF (T_geom vtx1) vtx2). #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1549, p. 82. *)
Lemma T_geom_ref :
forall vtx, vtx = vtx_ref -> T_geom vtx = (id : 'R^d -> 'R^d).
Proof. Proof.
apply: (am_ext_gen_full_ms _ _ vtx_ref); intros; subst; fun_ext x; destruct (aff_indep_aff_gen_R _
has_dim_Rn vtx_ref_aff_indep x) as [L [HL ->]].
apply T_geom_baryc; easy.
Qed.
Lemma T_geom_scal_ref :
forall a vtx, invertible a -> vtx = vtx_ref ->
@T_geom d (mapF (scal a) vtx) = scal a.
Proof.
intros; fun_ext; rewrite T_geom_lc lc_scal_r -T_geom_lc T_geom_ref; easy.
Qed.
End T_geom_ref_Facts.
Section T_geom_f_Facts2.
Context {d : nat}.
Lemma T_geom_inj_l : injective (@T_geom d).
Proof. move=> v1 v2 H; extF; rewrite -(T_geom_vtx v1) H T_geom_vtx; easy. Qed.
Lemma T_geom_comp :
forall( vtx1 vtx2 : 'R^{d.+1,d}),
T_geom vtx1 \o T_geom vtx2 = T_geom (mapF (T_geom vtx1) vtx2).
Proof.
intros; apply: (am_ext_gen_full_ms _ _ vtx_ref);
[apply am_comp_ms |..]; [apply T_geom_am.. | apply vtx_ref_aff_gen |]. [apply am_comp_ms |..]; [apply T_geom_am.. | apply vtx_ref_aff_gen |].
intro; rewrite comp_correct !T_geom_vtx; easy. intro; rewrite comp_correct !T_geom_vtx; easy.
Qed. Qed.
End T_geom_Facts2. Lemma T_geom_sym :
forall( vtx1 vtx2 : 'R^{d.+1,d}),
mapF (T_geom vtx1) vtx2 = mapF (T_geom vtx2) vtx1.
Proof.
intros; extF; rewrite !mapF_correct; unfold T_geom.
assert (H : forall i, vtx1 i = barycenter_ms (LagPd1_ref^~ (vtx1 i)) vtx_ref)
by now intro; rewrite LagPd1_ref_barycF.
apply extF in H; rewrite H.
(*
LagPd1_ref_barycF : barycenter_ms (LagPd1_ref^~ x_ref) vtx_ref = x_ref
baryc_comm_r_R : barycenter L2 (barycenter L1 A) = barycenter L1 (mapF (barycenter L2) A)
*)
Admitted.
Lemma T_geom_comm :
forall( vtx1 vtx2 : 'R^{d.+1,d}),
T_geom vtx1 \o T_geom vtx2 = T_geom vtx2 \o T_geom vtx1.
Proof. intros; rewrite !T_geom_comp T_geom_sym; easy. Qed.
End T_geom_f_Facts2.
Section T_geom_inv_Facts. Section T_geom_inv_Facts.
...@@ -174,16 +225,7 @@ Proof. ...@@ -174,16 +225,7 @@ Proof.
intros; apply T_geom_inj; rewrite T_geom_inv_can_r T_geom_baryc; easy. intros; apply T_geom_inj; rewrite T_geom_inv_can_r T_geom_baryc; easy.
Qed. Qed.
End T_geom_inv_Facts. (* TODO FC (05/03/2025): is the following useful? *)
Section T_geom_K_geom_Facts.
(* TODO FC (05/03/2025): is this section useful? *)
Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.
Let K_geom_ref : 'R^d -> Prop := convex_envelop vtx_ref. Let K_geom_ref : 'R^d -> Prop := convex_envelop vtx_ref.
Let K_geom : 'R^d -> Prop := convex_envelop vtx. Let K_geom : 'R^d -> Prop := convex_envelop vtx.
...@@ -193,7 +235,7 @@ Proof. ...@@ -193,7 +235,7 @@ Proof.
move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_baryc; easy. move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_baryc; easy.
Qed. Qed.
Lemma T_geom_inv_K_geom_incl : incl K_geom (preimage (T_geom_inv Hvtx) K_geom_ref). Lemma T_geom_inv_K_geom_incl : incl K_geom (preimage T_geom_inv K_geom_ref).
Proof. Proof.
move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_inv_baryc; easy. move=>> [L HL1 HL2]; unfold K_geom, preimage; rewrite T_geom_inv_baryc; easy.
Qed. Qed.
...@@ -204,45 +246,27 @@ Qed. ...@@ -204,45 +246,27 @@ Qed.
Lemma T_geom_K_geom_eq : image (T_geom vtx) K_geom_ref = K_geom. Lemma T_geom_K_geom_eq : image (T_geom vtx) K_geom_ref = K_geom.
Proof. Proof.
apply subset_ext_equiv; split; [apply image_incl_equiv, T_geom_K_geom_incl | apply subset_ext_equiv; split; [apply image_incl_equiv, T_geom_K_geom_incl |
rewrite -(f_inv_preimage (T_geom_bij Hvtx)); apply T_geom_inv_K_geom_incl]. rewrite -(f_inv_preimage T_geom_bij); apply T_geom_inv_K_geom_incl].
Qed. Qed.
Lemma T_geom_inv_K_geom_eq : image (T_geom_inv Hvtx) (K_geom) = K_geom_ref. Lemma T_geom_inv_K_geom_eq : image T_geom_inv (K_geom) = K_geom_ref.
Proof. Proof.
rewrite -T_geom_K_geom_eq -image_comp T_geom_inv_id_l image_id; easy. rewrite -T_geom_K_geom_eq -image_comp T_geom_inv_id_l image_id; easy.
Qed. Qed.
End T_geom_K_geom_Facts. End T_geom_inv_Facts.
Section T_geom_ref_Facts. Section T_geom_inv_ref_Facts.
Context {d : nat}. Context {d : nat}.
(**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1549, p. 82. *)
Lemma T_geom_ref :
forall vtx, vtx = vtx_ref -> T_geom vtx = (id : 'R^d -> 'R^d).
Proof.
intros; subst; fun_ext x; destruct (aff_indep_aff_gen_R _
has_dim_Rn vtx_ref_aff_indep x) as [L [HL ->]].
apply T_geom_baryc; easy.
Qed.
Lemma T_geom_inv_ref : Lemma T_geom_inv_ref :
forall vtx (H : aff_indep_ms vtx), forall vtx (H : aff_indep_ms vtx),
vtx = vtx_ref -> T_geom_inv H =(id : 'R^d -> 'R^d). vtx = vtx_ref -> T_geom_inv H = (id : 'R^d -> 'R^d).
Proof. intros; subst; apply f_inv_is_id, T_geom_ref; easy. Qed. Proof. intros; subst; apply f_inv_is_id, T_geom_ref; easy. Qed.
Lemma T_geom_scal_ref : End T_geom_inv_ref_Facts.
forall a vtx, invertible a -> vtx = vtx_ref ->
@T_geom d (mapF (scal a) vtx) = scal a.
Proof.
intros; fun_ext; rewrite T_geom_lc lc_scal_r -T_geom_lc T_geom_ref; easy.
Qed.
End T_geom_ref_Facts.
Section T_geom_permutF_Def. Section T_geom_permutF_Def.
...@@ -250,7 +274,7 @@ Section T_geom_permutF_Def. ...@@ -250,7 +274,7 @@ Section T_geom_permutF_Def.
Context {d : nat}. Context {d : nat}.
Variable vtx : 'R^{d.+1,d}. Variable vtx : 'R^{d.+1,d}.
(** [pi_d] is a permutation of [0..d]. (** [pi_d] is a permutation of [0..d.+1).
The intention is to switch vertices. *) The intention is to switch vertices. *)
Variable pi_d : 'I_[d.+1]. Variable pi_d : 'I_[d.+1].
...@@ -267,7 +291,7 @@ Section T_geom_permutF_Facts. ...@@ -267,7 +291,7 @@ Section T_geom_permutF_Facts.
Context {d : nat}. Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx: aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
Context {pi_d : 'I_[d.+1]}. Context {pi_d : 'I_[d.+1]}.
Hypothesis Hpi_d : injective pi_d. Hypothesis Hpi_d : injective pi_d.
...@@ -350,7 +374,7 @@ Section T_geom_transpF_Facts. ...@@ -350,7 +374,7 @@ Section T_geom_transpF_Facts.
Context {d : nat}. Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx: aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
Definition T_geom_transpF_inv (i0 : 'I_d.+1) : 'R^d -> 'R^d := Definition T_geom_transpF_inv (i0 : 'I_d.+1) : 'R^d -> 'R^d :=
T_geom_permutF_inv Hvtx (transp_ord_inj ord_max i0). T_geom_permutF_inv Hvtx (transp_ord_inj ord_max i0).
......
...@@ -295,7 +295,7 @@ Section T_geom_permutF_Facts. ...@@ -295,7 +295,7 @@ Section T_geom_permutF_Facts.
Context {d : nat}. Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx: aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
Context {pi_d : 'I_[d.+1]}. Context {pi_d : 'I_[d.+1]}.
Hypothesis Hpi_d : injective pi_d. Hypothesis Hpi_d : injective pi_d.
...@@ -342,7 +342,7 @@ Section T_geom_transpF_Facts. ...@@ -342,7 +342,7 @@ Section T_geom_transpF_Facts.
Context {d : nat}. Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx: aff_indep_ms vtx. Hypothesis Hvtx : aff_indep_ms vtx.
Lemma LagPd1_eq_transpF : Lemma LagPd1_eq_transpF :
forall i0 j, LagPd1 Hvtx j = forall i0 j, LagPd1 Hvtx j =
......
...@@ -29,6 +29,7 @@ COPYING file for more details. ...@@ -29,6 +29,7 @@ COPYING file for more details.
** Additional notations ** Additional notations
- <<[0..n)>> is for ['I_n];
- ['I_{m,n}] is for ['I_m -> 'I_n]; - ['I_{m,n}] is for ['I_m -> 'I_n];
- ['I_[n]] is for ['I_{n,n}]; - ['I_[n]] is for ['I_{n,n}];
- ['I_{m,n,p}] is for ['I_m -> 'I_{n,p}]. - ['I_{m,n,p}] is for ['I_m -> 'I_{n,p}].
......
...@@ -14,6 +14,7 @@ ...@@ -14,6 +14,7 @@
-arg "-w -ambiguous-paths" -arg "-w -ambiguous-paths"
-docroot . -docroot .
# Options for coqdoc: --no-index -toc -g (or -l)
# #
# Requisite. # Requisite.
......