WIP: filterPF_unfunF.

FEM/Algebra/Finite_family.v

@@ -1493,7 +1493,7 @@ Definition incrF {n1 n2} (f : 'I_{n1,n2}) : Prop :=
 Lemma injF_restr_bij_EX :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
     { p : 'I_[n1] | bijective p /\
-      exists (q : 'I_{n1,n2}), incrF q /\ f = q \o p }. (* q := f \o f_inv Hp *)
+      exists (g : 'I_{n1,n2}), incrF g /\ f = g \o p }. (* g := f \o f_inv Hp *)
 Proof.
 (* Hint: pas besoin d'induction!
   p^-1 est la permutation permettant de trier f 'I_n1 et q = f o p^-1. *)
@@ -1506,7 +1506,7 @@ destruct n2 as [|n2]; [exists id | exists (fun=> ord0)];
 (* *)
 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' [q' [Hq' H']]]]; clear Hn1.
+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).
@@ -4622,29 +4622,26 @@ Lemma filterPF_unfunF :
       (Hf : injective f) (HP : extendPF f P1 P2)
       (A1 : 'F^n1) x0 i0,
     P1 i0 ->
-    let Hg1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
-    let g := f_inv Hg1 in
-    let Hg := f_inv_inj Hg1 in
+    let Hp1 := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+    let p := f_inv Hp1 in
+    let Hp := f_inv_inj Hp1 in
     filterPF P2 (unfunF f A1 x0) =
-      castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hg)
-        (filterPF (permutF g P1) (permutF g A1))).
-Proof.
-intros F n1 n2 f P1 P2 Hf HP A1 x0 i0 HP1 Hg1 g Hg.
-pose (p := proj1_sig (injF_restr_bij_EX Hf)); pose (i1 := p i0).
-assert (HP1' : permutF g P1 i1)
-    by now unfold permutF, i1, g; rewrite f_inv_correct_l.
-rewrite (filterPF_permutF Hg HP1').
-(*
-apply sym_eq; rewrite castF_sym_equiv -(filterPF_funF Hf HP) funF_unfunF//.
-apply extF; intros j1; unfold castF, funF.
-f_equal; unfold filterP_f_ord; rewrite f_inv_invol.
-*)
+      castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hp)
+        (filterPF (permutF p P1) (permutF p A1))).
+Proof.
+intros F n1 n2 f P1 P2 Hf HP A1 x0 i0 HP1 Hp1 p Hp.
+pose (p1 := proj1_sig (injF_restr_bij_EX Hf)); pose (i1 := p1 i0).
+assert (HP1' : permutF p P1 i1)
+    by now unfold permutF, i1, p; rewrite f_inv_correct_l.
+rewrite (filterPF_permutF Hp HP1') -{2}(funF_unfunF x0 Hf A1).
+assert (HP2 : P2 (f i0))
+    by now rewrite (extendPF_unfunF_rev Hf HP) (unfunF_correct_l _ i0 _ Hf).
+rewrite (filterPF_funF HP2 Hf HP).
+apply extF; intros j2; unfold castF, funF, filterP_f_ord_n, filterP_f_ord_p.
+f_equal; rewrite f_inv_invol.
+
+
 
-(*
-apply filterP_ord_inj.
-rewrite filterP_unfilterP_ord_in.
-rewrite filterP_unfilterP_ord_in_equiv out.
-*)