diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index f1dd7f32f463e87af462a3e4a93124ebb35c76df..3c54e44b4009d0d0752204da9f642f65947d63f5 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -1604,11 +1604,11 @@ exists (unfun0F f L1); repeat split; try easy.
apply unfun0F_ub; easy.
apply barycenter_correct_equiv; try easy; unfold is_comb_aff.
rewrite -comb_lin_filter_n0F_l filter_n0F_unfun0F.
-pose (Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf'))); fold Hp1.
-pose (q1 := f_inv Hp1); pose (Hq1 := f_inv_inj Hp1);
- fold q1 Hq1; fold q1 in Hp1, Hq1.
+pose (q1 := proj1_sig (injF_restr_bij_EX Hf')); fold q1.
+pose (Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf'))); fold q1 in Hq1a.
+pose (Hq1b := bij_inj Hq1a).
rewrite 2!comb_lin_castF_l.
-rewrite -(comb_lin_permutF Hq1) -comb_lin_filter_n0F_l in HG1.
+rewrite -(comb_lin_permutF Hq1b) -comb_lin_filter_n0F_l in HG1.
rewrite -HG1; f_equal; rewrite -castF_sym_equiv.
apply sym_eq; rewrite -castF_sym_equiv.
rewrite filter_n0F_gen_unfun0F_l; repeat f_equal.
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 46fd0207315e64f1153c15c5ac0f2dedc9fb0d7c..83da1b867c895b982c3ff2ca74989c4a95d5e7b3 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1490,35 +1490,27 @@ Qed.
Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop :=
forall (i1 j1 : 'I_n1), (i1 < j1)%coq_nat -> (f i1 < f j1)%coq_nat.
-Lemma injF_restr_bij_EX :
+Lemma incrF_inj : forall {n1 n2} {f : 'I_{n1,n2}}, incrF f -> injective f.
+Proof.
+move=>> Hf i1 j1; apply contra_equiv;
+ move=> /ord_neq_compat /not_eq [H1 | H1]; [| apply not_eq_sym];
+ apply ord_neq, Nat.lt_neq, Hf, H1.
+Qed.
+
+Lemma injF_restr_bij_EX' :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
{ p1 : 'I_[n1] | bijective p1 /\
exists (g : 'I_{n1,n2}), incrF g /\ f = g \o p1 }. (* g := f \o f_inv Hp1 *)
Proof.
(* Hint: pas besoin d'induction!
p1^-1 est la permutation permettant de trier f 'I_n1 et q = f o p1^-1. *)
-intros n1 n2 f Hf; apply constructive_indefinite_description;
- induction n1 as [|n1 Hn1].
-(* *)
-exists id; split; [apply bij_id |].
-destruct n2 as [|n2]; [exists id | exists (fun=> ord0)];
- (split; [| apply fun_ext]); intros [i Hi]; easy.
-(* *)
-pose (f' := fun i1 => f (widen_S i1)).
-assert (Hf' : injective f') by now move=> i1 j1 /Hf /widen_ord_inj.
-destruct (Hn1 _ Hf') as [p' [Hp' [g' [Hg' H']]]]; clear Hn1.
-pose (p'1 := f_inv Hp').
-(*
-pose (nn1 := widen_ord (inj_ord_leq Hf) ord_max).
-pose (p := fun i2 => transp_ord (p' nn1) (f ord_max) (p' i2)).
-exists p; repeat split.
-*)
-
-
-
-
-
+Admitted.
+Lemma injF_restr_bij_EX :
+ forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
+ { q1 : 'I_[n1] | bijective q1 /\ incrF (f \o q1) }.
+Proof.
+(* Hint: pas besoin d'induction, q1 est la permutation permettant de trier f 'I_n1. *)
Admitted.
End Fun_ord.
@@ -1724,6 +1716,30 @@ move=>> Hp i; left; exists (f_inv (injF_bij Hp) i); split; [| unfold permutF];
rewrite f_inv_correct_r; easy.
Qed.
+Lemma extendPF_incrF :
+ forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
+ {P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2),
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ extendPF (f \o q1) (permutF q1 P1) P2.
+Proof.
+intros n1 n2 f Hf P1 P2 HP q1.
+pose (Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf))).
+pose (Hq1b := proj2 (proj2_sig (injF_restr_bij_EX Hf))).
+pose (p1 := f_inv Hq1a); fold q1 in Hq1a, Hq1b.
+apply extendPF_unfunF_equiv; [apply (incrF_inj Hq1b) |].
+rewrite (extendPF_unfunF_rev Hf HP); apply extF; intros i2.
+destruct (im_dec f i2) as [[k1 ->] | Hi2].
+(* *)
+unfold permutF.
+rewrite -{2}(f_inv_correct_r Hq1a k1) -(comp_correct q1 f); fold p1.
+rewrite (unfunF_correct_l _ k1)//
+ (unfunF_correct_l _ (p1 k1) _ (incrF_inj Hq1b))//.
+unfold p1; rewrite f_inv_correct_r; easy.
+(* *)
+rewrite !unfunF_correct_r//; intros k1; contradict Hi2.
+rewrite not_all_not_ex_equiv; exists (q1 k1); auto.
+Qed.
+
End ExtendPF_Facts.
@@ -4599,6 +4615,29 @@ destruct j1 as [j1 Hj1]; simpl in Hj.
move: (leq_addr j n1); rewrite Hj leqNgt; contradict Hj1; apply /negP; easy.
Qed.
+Lemma filterP_ord_incrF :
+ forall {n1 n2} {g : 'I_{n1,n2}} (Hg : incrF g) {P1 : 'Prop^n1}
+ {P2 : 'Prop^n2} (HP : extendPF g P1 P2) {j1 : 'I_(lenPF P1)},
+ g (filterP_ord j1) =
+ filterP_ord (cast_ord (lenPF_extendPF (incrF_inj Hg) HP) j1).
+Proof.
+intros n1 n2 g Hg P1 P2 HP j1.
+
+
+Admitted.
+
+Lemma filterP_f_ord_incrF :
+ forall {n1 n2} {g : 'I_{n1,n2}} (Hg : incrF g)
+ {P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF g P1 P2)
+ {i1} (HP2 : P2 (g i1)) {j1 : 'I_(lenPF P1)},
+ filterP_f_ord g HP2 j1 = cast_ord (lenPF_extendPF (incrF_inj Hg) HP) j1.
+Proof.
+intros n1 n2 g Hg P1 P2 HP i1 HP2 j1.
+move: (extendPF_unfunF_rev (incrF_inj Hg) HP) => HP2'; subst.
+apply filterP_ord_inj; rewrite (filterP_f_ord_correct _ (incrF_inj Hg) HP).
+apply filterP_ord_incrF.
+Qed.
+
(* Was:
Lemma filterPF_funF :
forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2}
@@ -4669,51 +4708,31 @@ rewrite HA2; [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
rewrite Rg_compl; easy.
Qed.
-Lemma filterP_f_ord_incr :
- forall {n1 n2} {g : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2}
- {i1} (HP2 : P2 (g i1)) (H : lenPF P1 = lenPF P2) {j1 : 'I_(lenPF P1)},
- incrF g -> filterP_f_ord g HP2 j1 = cast_ord H j1.
-Proof.
-intros n1 n2 g P1 P2 i1 HP2 H j1 Hg; unfold filterP_f_ord.
-
-
-
-
-Admitted.
-
Lemma filterPF_unfunF :
forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
{P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop} (HP : extendPF f P1 P2)
{A1 : 'F^n1} x0 i1,
P1 i1 ->
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filterPF P2 (unfunF f A1 x0) =
- castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hq1)
+ castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hq1b)
(filterPF (permutF q1 P1) (permutF q1 A1))).
Proof.
-intros F n1 n2 f Hf P1 P2 HP A1 x0 i1 HP1 Hp1 q1 Hq1; fold q1 in Hq1.
-pose (p1 := proj1_sig (injF_restr_bij_EX Hf)); pose (Hp1' := bij_inj Hp1).
-destruct (proj2 (proj2_sig (injF_restr_bij_EX Hf))) as [g [Hg1 Hg2]].
-fold p1 in Hp1, Hp1', Hg2.
-assert (Hg2' : forall k1, f k1 = g (p1 k1)) by now intros; rewrite Hg2.
-assert (Hg3 : g = f \o q1).
- rewrite Hg2; unfold q1; apply fun_ext; intro.
- rewrite !comp_correct f_inv_correct_r; easy.
-assert (Hg3' : forall k1, g k1 = f (q1 k1)) by now intros; rewrite Hg3.
-assert (HP1' : P1 (q1 (p1 i1))) by now unfold q1; rewrite f_inv_correct_l.
+intros F n1 n2 f Hf P1 P2 HP A1 x0 i1 HP1 q1 Hq1a Hq1b.
+pose (Hq1c := proj2 (proj2_sig (injF_restr_bij_EX Hf)));
+ pose (p1 := f_inv Hq1a); fold q1 in Hq1a, Hq1b, Hq1c.
+assert (HP1' : P1 (q1 (p1 i1))) by now unfold p1; rewrite f_inv_correct_r.
assert (HP2 : P2 (f i1))
by now rewrite (extendPF_unfunF_rev Hf HP) (unfunF_correct_l _ i1).
-assert (HP2' : P2 (g (p1 i1))) by now rewrite -Hg2'.
-subst g.
+assert (HP2' : P2 (f (q1 (p1 i1)))) by now rewrite f_inv_correct_r.
(* *)
-rewrite (filterPF_permutF HP1' Hq1) -{2}(funF_unfunF x0 Hf A1).
+rewrite (filterPF_permutF HP1' Hq1b) -{2}(funF_unfunF x0 Hf A1).
rewrite (filterPF_funF HP2' Hf HP).
-apply extF; intros j2; unfold castF, funF, filterP_f_ord_n; f_equal.
-rewrite -(filterP_f_ord_comp_l HP1' Hq1).
-rewrite (filterP_f_ord_incr HP2'
- (eq_trans (lenPF_permutF Hq1) (lenPF_extendPF Hf HP)) Hg1).
+apply extF; intros j2; unfold castF, funF; f_equal.
+rewrite -(filterP_f_ord_comp_l HP1' Hq1b).
+rewrite (filterP_f_ord_incrF Hq1c (extendPF_incrF Hf HP)).
rewrite 2!cast_ord_comp cast_ord_id; easy.
Qed.
@@ -4727,14 +4746,14 @@ Qed.
Lemma filter_neqF_gen_unfunF :
forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
(A1 : 'E^n1) x0 (B1 : 'F^n1) y0,
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_neqF_gen (unfunF f A1 x0) x0 (unfunF f B1 y0) =
- castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1)
+ castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1b)
(filter_neqF_gen (permutF q1 A1) x0 (permutF q1 B1))).
Proof.
-intros F n1 n2 f Hf A1 x0 B1 y0 Hp1 q1 Hq1.
+intros F n1 n2 f Hf A1 x0 B1 y0 q1 Hq1a Hq1b.
destruct (excluded_middle_informative (forall i1, A1 i1 = x0)) as [HA1 | HA1].
apply eqAF_nil; left; apply lenPF0_alt; intuition.
move: HA1 => /not_all_ex_not_equiv [i0 Hi0].
@@ -4746,14 +4765,14 @@ Qed.
Lemma filter_neqF_gen_unfunF_l :
forall {F : Type} (HF : inhabited F) {n1 n2}
{f : 'I_{n1,n2}} (Hf : injective f) (A1 : 'E^n1) x0 (B2 : 'F^n2),
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_neqF_gen (unfunF f A1 x0) x0 B2 =
- castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1)
+ castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1b)
(filter_neqF_gen (permutF q1 A1) x0 (permutF q1 (funF f B2)))).
Proof.
-intros F [y0] n1 n2 f Hf A1 x0 B2 Hp1 q1 Hq1.
+intros F [y0] n1 n2 f Hf A1 x0 B2 q1 Hq1a Hq1b.
rewrite -(filter_neqF_gen_unfunF _ _ _ _ y0); apply filterPF_ext_r; intro.
move=> /(proj1 contra_equiv (unfunF_correct_r _ _)) /not_all_not_ex [i1 ->].
rewrite unfunF_funF// maskPF_correct_l//.
@@ -4761,11 +4780,11 @@ Qed.
Lemma filter_neqF_unfunF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (A1 : 'E^n1) x0,
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_neqF (unfunF f A1 x0) x0 =
- castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1)
+ castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1b)
(filter_neqF (permutF q1 A1) x0)).
Proof.
intros; unfold filter_neqF; rewrite filter_neqF_gen_unfunF_l;
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index 6a0a7610d8b756e6d02cd3828b65aaac8a35d7c8..d327b691e1f97ba5e958ae4e1d29f4d4d9010051 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -580,11 +580,11 @@ Proof. move=>>; apply len_neqF_unfunF. Qed.
Lemma filter_n0F_gen_unfun0F :
forall {H : AbelianMonoid} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
(u1 : 'G^n1) (v1 : 'H^n1),
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_n0F_gen (unfun0F f u1) (unfun0F f v1) =
- castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1)
+ castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
(filter_n0F_gen (permutF q1 u1) (permutF q1 v1))).
Proof.
intros; unfold filter_n0F_gen;
@@ -594,11 +594,11 @@ Qed.
Lemma filter_n0F_gen_unfun0F_l :
forall {H : AbelianMonoid} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
(u1 : 'G^n1) (u2 : 'H^n2),
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_n0F_gen (unfun0F f u1) u2 =
- castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1)
+ castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
(filter_n0F_gen (permutF q1 u1) (permutF q1 (funF f u2)))).
Proof.
intros; unfold filter_n0F_gen; rewrite filter_neqF_gen_unfunF_l;
@@ -607,11 +607,11 @@ Qed.
Lemma filter_n0F_unfun0F :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (u1 : 'G^n1),
- let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
- let q1 := f_inv Hp1 in
- let Hq1 := f_inv_inj Hp1 in
+ let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+ let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+ let Hq1b := bij_inj Hq1a in
filter_n0F (unfun0F f u1) =
- castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1)
+ castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
(filter_n0F (permutF q1 u1))).
Proof.
intros; unfold filter_n0F; rewrite filter_neqF_unfunF; apply castF_eq_l.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 4c697dc3c3e0ee23daa2004e51352e14bfc0bd82..9ff4ffa4b45f8180e88bc28cf8ae4b68cfafef9c 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -57,7 +57,7 @@ End Function_Facts1.
Section Function_Facts2.
Lemma comp_correct :
- forall {U V W : Type} {f : U -> V} {g : V -> W} {x}, (g \o f) x = g (f x).
+ forall {U V W : Type} (f : U -> V) (g : V -> W) x, (g \o f) x = g (f x).
Proof. easy. Qed.
Lemma comp_assoc :