From 81923afa4c3c0e790ddb583cd7fb5cc593f629fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 19 Feb 2024 11:40:32 +0100
Subject: [PATCH] Function_compl: Rename f_inv_correct_{l,r} ->
 f_inv_can_{l,r}.

Function_sub:
Add def involS.
Add and prove involS_injS, involS_bijS.
Rename f_invS_canS_l <-> f_invS_canS_r.
Add and prove f_invS_uniq_{l,r}, f_invS_{bijS,injS,surjS},
              f_invS_eq_equiv, f_invS_neq_equiv,
              f_invS_ext, f_invS_invol{,_alt},
              f_invS_id{,_rev,_equiv}.

ord_compl, Finite_family, ModuleSpace_compl, AffineSpace, Finite_dim,
  poly_Lagrange, P_approx_k, FE_LagP:
Propagate new API (from Function_compl).

FE_LagP:
Propagate new API (from Function_sub).
---
 FEM/Algebra/AffineSpace.v       |   4 +-
 FEM/Algebra/Finite_dim.v        |  10 +-
 FEM/Algebra/Finite_family.v     |  34 ++---
 FEM/Algebra/ModuleSpace_compl.v |   2 +-
 FEM/Algebra/ord_compl.v         |  12 +-
 FEM/Compl/Function_compl.v      |  26 ++--
 FEM/Compl/Function_sub.v        | 220 +++++++++++++++++++-------------
 FEM/FE_LagP.v                   |   4 +-
 FEM/P_approx_k.v                |   4 +-
 FEM/poly_Lagrange.v             |   4 +-
 10 files changed, 180 insertions(+), 140 deletions(-)

diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index c715d6f2..9f919335 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -2107,8 +2107,8 @@ Lemma fct_lm_inv :
     fct_lm (f_inv Hf) (f O1) = f_inv (fct_lm_bijective_compat O1 Hf).
 Proof.
 intros f Hf O1; apply fun_ext; intros u2.
-rewrite -{1}(f_inv_correct_r (fct_lm_bijective_compat O1 Hf) u2); unfold fct_lm.
-rewrite transl_correct_l !f_inv_correct_l transl_correct_r; easy.
+rewrite -{1}(f_inv_can_r (fct_lm_bijective_compat O1 Hf) u2); unfold fct_lm.
+rewrite transl_correct_l !f_inv_can_l transl_correct_r; easy.
 Qed.
 
 Lemma is_affine_mapping_bij_compat :
diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index 15c52188..7b8d033b 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -1004,7 +1004,7 @@ intros n p B Hp HB L; rewrite {1}(permutF_f_inv_r Hp L) comb_lin_permutF;
     try now apply bij_inj.
 move=> /HB /extF_rev HL; apply extF; intros i.
 specialize (HL (p i)); rewrite zeroF in HL; rewrite zeroF -HL.
-unfold permutF; rewrite f_inv_correct_l; easy.
+unfold permutF; rewrite f_inv_can_l; easy.
 Qed.
 
 Lemma is_free_permutF_equiv :
@@ -1014,8 +1014,8 @@ Proof.
 intros n p B Hp; split. apply is_free_permutF; easy.
 rewrite <- (permutF_can p (f_inv Hp) B), permutF_can.
 apply is_free_permutF, f_inv_bij.
-apply f_inv_correct_l.
-apply f_inv_correct_r.
+apply f_inv_can_l.
+apply f_inv_can_r.
 Qed.
 
 Lemma is_lin_dep_not_uniq_decomp :
@@ -1490,10 +1490,10 @@ pose (gs:= f_inv Hfs).
 apply is_basis_ext with (mapF gs fBs).
 apply extF; intros i.
 rewrite mapF_correct; unfold fBs, gs.
-now rewrite f_inv_correct_l.
+now rewrite f_inv_can_l.
 assert (W: (@fullset (@sub_ms K E PE HPE) = image gs (image fs fullset))).
 apply subset_ext_equiv; split; intros x Hx; try easy.
-rewrite -(f_inv_correct_l Hfs x); easy.
+rewrite -(f_inv_can_l Hfs x); easy.
 assert (Hfs2 : is_linear_mapping fs).
 apply sub_ms_linear_mapping with f; try easy.
 (* *)
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 702bb6d6..caf258e4 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -1526,27 +1526,27 @@ assert (Hq2a : cancel p2 q2).
   destruct (ord_eq2_dec (p2' i2) (p2' nn1) (f ord_max)) as [[H | H] | [Ha Hb]].
   rewrite (transp_ord_correct_l0 H) transp_ord_correct_l1//; apply Hp2'c; easy.
   rewrite (transp_ord_correct_l1 H) transp_ord_correct_l0.
-  apply eq_sym, f_inv_eq_equiv; easy. apply f_inv_correct_l.
+  apply eq_sym, f_inv_eq_equiv; easy. apply f_inv_can_l.
   rewrite (transp_ord_correct_r Ha Hb) transp_ord_correct_r;
-      rewrite f_inv_correct_l; try easy.
+      rewrite f_inv_can_l; try easy.
   contradict Ha; subst; easy.
-  contradict Hb; subst; rewrite f_inv_correct_r; easy.
+  contradict Hb; subst; rewrite f_inv_can_r; easy.
 assert (Hq2b : cancel q2 p2).
   intros j2; unfold q2, p2.
   destruct (ord_eq2_dec j2 (p2' nn1) (f ord_max)) as [[H | H] | [Ha Hb]].
-  rewrite H f_inv_correct_l transp_ord_correct_l1// transp_ord_correct_l0//
-      f_inv_correct_r; easy.
+  rewrite H f_inv_can_l transp_ord_correct_l1// transp_ord_correct_l0//
+      f_inv_can_r; easy.
   rewrite H transp_ord_correct_l0// transp_ord_correct_l1//.
   apply not_eq_sym, (f_inv_neq_equiv Hp2'a) in Ha;
       rewrite (transp_ord_correct_r (not_eq_sym Ha) _).
   apply f_inv_neq_equiv, not_eq_sym in Ha;
-      rewrite f_inv_correct_r transp_ord_correct_r//.
+      rewrite f_inv_can_r transp_ord_correct_r//.
   contradict Hb; apply (f_inv_inj Hp2'a); easy.
 apply (Bijective Hq2a Hq2b).
 (* *)
 unfold p2, widenF in *; move: Hp2'a => /bij_equiv [Hp2'c _].
 intros i1; destruct (ord_eq_dec i1 ord_max) as [Hi1 | Hi1].
-rewrite Hi1 transp_ord_correct_l0// f_inv_correct_r//.
+rewrite Hi1 transp_ord_correct_l0// f_inv_can_r//.
 rewrite -{1}(widen_narrow_S Hi1); fold (f' (narrow_S Hi1)); rewrite Hp2'b.
 rewrite transp_ord_correct_r; try now f_equal; apply ord_inj.
 contradict Hi1; apply Hp2'c, widen_ord_inj in Hi1; easy.
@@ -1661,7 +1661,7 @@ exists (f_inv Hp1); split; [apply bij_inj, f_inv_bij |].
 intros A1 x0; apply extF; intros i2.
 destruct (im_dec f i2) as [[i1 Hi1] | Hi2]; unfold permutF, castF.
 (* *)
-rewrite (unfunF_correct_l _ i1)// -Hi1 Hp2 f_inv_correct_l.
+rewrite (unfunF_correct_l _ i1)// -Hi1 Hp2 f_inv_can_l.
 assert (Hi1' : (cast_ord (eq_sym (injF_plus_minus_r Hf))
     (widen_ord (m:=n2) (injF_leq Hf) i1) < n1)%coq_nat)
     by now simpl; apply /ltP.
@@ -1673,7 +1673,7 @@ assert (~ (cast_ord (eq_sym (injF_plus_minus_r Hf))
   simpl; contradict Hi2; move: Hi2 => /ltP Hi2.
   apply not_all_not_ex_equiv; exists (Ordinal Hi2).
   rewrite Hp2; unfold widenF, widen_ord; simpl.
-  rewrite -{3}(f_inv_correct_r Hp1 i2).
+  rewrite -{3}(f_inv_can_r Hp1 i2).
   f_equal; apply ord_inj; easy.
 rewrite concatF_correct_r; easy.
 Qed.
@@ -1798,7 +1798,7 @@ Lemma extendPF_permutF :
     injective p -> extendPF p (permutF p P) P.
 Proof.
 move=>> Hp i; left; exists (f_inv (injF_bij Hp) i); split; [| unfold permutF];
-    rewrite f_inv_correct_r; easy.
+    rewrite f_inv_can_r; easy.
 Qed.
 
 Lemma extendPF_incrF :
@@ -1816,10 +1816,10 @@ 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 -{2}(f_inv_can_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.
+unfold p1; rewrite f_inv_can_r; easy.
 (* *)
 rewrite !unfunF_correct_r//; intros k1; contradict Hi2.
 rewrite not_all_not_ex_equiv; exists (q1 k1); auto.
@@ -3909,12 +3909,12 @@ Proof. move=>> Hp A HA i j /HA /Hp; easy. Qed.
 Lemma permutF_f_inv_l :
   forall {n} {p} (Hp : bijective p) (A : 'E^n),
     A = permutF (f_inv Hp) (permutF p A).
-Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_correct_r. Qed.
+Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_can_r. Qed.
 
 Lemma permutF_f_inv_r :
   forall {n} {p} (Hp : bijective p) (A : 'E^n),
     A = permutF p (permutF (f_inv Hp) A).
-Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_correct_l. Qed.
+Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_can_l. Qed.
 
 Lemma permutF_invalF_l : forall {n} p (A : 'E^n), invalF (permutF p A) A.
 Proof. intros n p A i; exists (p i); easy. Qed.
@@ -4680,7 +4680,7 @@ intros n p P Hp; destruct n as [|n]; [rewrite !lenPF_nil; easy |].
 apply (bijS_eq_card p), (injS_surjS_bijS I_S_is_nonempty);
     [apply funS_correct; easy | move=>> _ _; apply Hp |].
 intros i Hi; exists (f_inv (injF_bij Hp) i); unfold permutF;
-    rewrite f_inv_correct_r; easy.
+    rewrite f_inv_can_r; easy.
 Qed.
 
 Lemma lenPF_permutF_f_inv_l :
@@ -5002,10 +5002,10 @@ Proof.
 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 (HP1' : P1 (q1 (p1 i1))) by now unfold p1; rewrite f_inv_can_r.
 assert (HP2 : P2 (f i1))
     by now rewrite (extendPF_unfunF_rev Hf HP) (unfunF_correct_l _ i1).
-assert (HP2' : P2 (f (q1 (p1 i1)))) by now rewrite f_inv_correct_r.
+assert (HP2' : P2 (f (q1 (p1 i1)))) by now rewrite f_inv_can_r.
 (* *)
 rewrite (filterPF_permutF HP1' Hq1b) -{2}(funF_unfunF x0 Hf A1).
 rewrite (filterPF_funF HP2' Hf HP).
diff --git a/FEM/Algebra/ModuleSpace_compl.v b/FEM/Algebra/ModuleSpace_compl.v
index 3f5afbda..4067ebbe 100644
--- a/FEM/Algebra/ModuleSpace_compl.v
+++ b/FEM/Algebra/ModuleSpace_compl.v
@@ -299,7 +299,7 @@ Lemma is_linear_mapping_bij_compat :
 Proof.
 intros f Hf1 [Hf2 Hf3]; split; intros;
     apply (bij_inj Hf1); [rewrite Hf2 | rewrite Hf3];
-    rewrite !f_inv_correct_r; easy.
+    rewrite !f_inv_can_r; easy.
 Qed.
 
 End Linear_mapping_Facts2.
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index b39d793b..5d17be45 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -623,7 +623,7 @@ Proof. intros; split; [apply bij_surj | apply surjF_bij]. Qed.
 
 Lemma incl_RgF :
   forall {n} {p : 'I_[n]} (P : 'I_n -> Prop), injective p -> incl P (Rg p).
-Proof. move=>> Hp i _; rewrite -(f_inv_correct_r (injF_bij Hp) i); easy. Qed.
+Proof. move=>> Hp i _; rewrite -(f_inv_can_r (injF_bij Hp) i); easy. Qed.
 
 End Fun_ord1.
 
@@ -708,7 +708,7 @@ assert (Hii : val ii < size (ord_enum n.+1)) by now rewrite size_ord_enum.
 assert (Hq : forall j : 'I_n.+1, q j < size (ord_enum n.+1))
     by now rewrite size_ord_enum.
 rewrite H; unfold comp; replace i with (val ii) by easy.
-rewrite !(nth_map ord0)// !nth_ord_enum f_inv_correct_r; easy.
+rewrite !(nth_map ord0)// !nth_ord_enum f_inv_can_r; easy.
 Qed.
 
 Definition in_ordS {n} (j : nat) : 'I_n.+1 :=
@@ -869,7 +869,7 @@ intros i Hi; rewrite size_map size_ord_enum in Hi; pose (ii := Ordinal Hi).
 assert (Hii : val ii < size In) by now rewrite size_ord_enum.
 replace i with (val ii) by easy.
 rewrite !(nth_map ord0)//; [| rewrite size_ord_enum; easy].
-rewrite !nth_ord_enum; unfold q2; rewrite f_inv_correct_l; easy.
+rewrite !nth_ord_enum; unfold q2; rewrite f_inv_can_l; easy.
 Qed.
 
 Lemma sort_perm_EX :
@@ -1551,7 +1551,7 @@ Lemma cast_f_ord_f_inv :
     cast_f_ord H (f_inv Hp1) = f_inv (cast_f_ord_bij H (bij_inj Hp1)).
 Proof.
 intros; subst; apply f_inv_uniq_l; intro;
-    rewrite !cast_f_ord_refl; apply f_inv_correct_l.
+    rewrite !cast_f_ord_refl; apply f_inv_can_l.
 Qed.
 
 End Cast_ord.
@@ -1849,8 +1849,8 @@ Lemma skip_f_ord_f_inv :
       f_inv (skip_f_ord_bij (bij_inj Hp) (f_inv Hp i0)).
 Proof.
 intros n p Hp i0; apply f_inv_uniq_l; intros j.
-rewrite -{1}(f_inv_correct_r Hp i0) -skip_f_ord_comp_alt skip_f_ord_id//.
-apply f_inv_correct_l.
+rewrite -{1}(f_inv_can_r Hp i0) -skip_f_ord_comp_alt skip_f_ord_id//.
+apply f_inv_can_l.
 Qed.
 
 (** Definition and properties of insert_f_ord. *)
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 3d341988..536da869 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -55,7 +55,7 @@ From FEM Require Import logic_compl.
   Support for the inverse of bijective functions.
   'f_inv_EX' states the strong existence of the (left and right) inverse of
     any bijective function.
-  'f_inv Hf' is the inverse of any function from any proof 'Hf' of its bijectivity.
+  'f_inv Hf' is the inverse of a function from any proof 'Hf' of its bijectivity.
   The inverse of any bijective function is unique and bijective.
   Involutive functions are the bijective functions equal to their inverse.
 *)
@@ -527,17 +527,17 @@ Proof. apply ex_EX; induction Hf as [g Hg1 Hg2]; exists g; easy. Qed.
 
 Definition f_inv : T2 -> T1 := proj1_sig f_inv_EX.
 
-Lemma f_inv_correct_l : cancel f f_inv.
+Lemma f_inv_can_l : cancel f f_inv.
 Proof. apply (proj2_sig f_inv_EX). Qed.
 
 Lemma f_inv_id_l : f_inv \o f = id.
-Proof. apply can_equiv, f_inv_correct_l. Qed.
+Proof. apply can_equiv, f_inv_can_l. Qed.
 
-Lemma f_inv_correct_r : cancel f_inv f.
+Lemma f_inv_can_r : cancel f_inv f.
 Proof. apply (proj2_sig f_inv_EX). Qed.
 
 Lemma f_inv_id_r : f \o f_inv = id.
-Proof. apply can_equiv, f_inv_correct_r. Qed.
+Proof. apply can_equiv, f_inv_can_r. Qed.
 
 End Inverse_Def.
 
@@ -549,13 +549,13 @@ Context {f : T1 -> T2}.
 Hypothesis Hf : bijective f.
 
 Lemma f_inv_uniq_l : forall (g : T2 -> T1), cancel f g -> g = f_inv Hf.
-Proof. move=>> H; apply (bij_can_uniq_r Hf H), f_inv_correct_l. Qed.
+Proof. move=>> H; apply (bij_can_uniq_r Hf H), f_inv_can_l. Qed.
 
 Lemma f_inv_uniq_r : forall (g : T2 -> T1), cancel g f -> g = f_inv Hf.
-Proof. move=>> H; apply (bij_can_uniq_l Hf H), f_inv_correct_r. Qed.
+Proof. move=>> H; apply (bij_can_uniq_l Hf H), f_inv_can_r. Qed.
 
 Lemma f_inv_bij : bijective (f_inv Hf).
-Proof. apply (bij_can_bij Hf), f_inv_correct_l. Qed.
+Proof. apply (bij_can_bij Hf), f_inv_can_l. Qed.
 
 Lemma f_inv_inj : injective (f_inv Hf).
 Proof. apply bij_inj, f_inv_bij. Qed.
@@ -566,8 +566,8 @@ Proof. apply bij_surj, f_inv_bij. Qed.
 Lemma f_inv_eq_equiv : forall x1 x2, x1 = f_inv Hf x2 <-> f x1 = x2.
 Proof.
 intros x1 x2; split.
-rewrite -{2}(f_inv_correct_r Hf x2); apply f_equal.
-rewrite -{2}(f_inv_correct_l Hf x1); apply f_equal.
+rewrite -{2}(f_inv_can_r Hf x2); apply f_equal.
+rewrite -{2}(f_inv_can_l Hf x1); apply f_equal.
 Qed.
 
 Lemma f_inv_neq_equiv : forall x1 x2, x1 <> f_inv Hf x2 <-> f x1 <> x2.
@@ -587,7 +587,7 @@ Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
 Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
 
 Lemma f_inv_invol : forall (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
-Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
+Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_can_r. Qed.
 
 Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
 Proof. apply f_inv_invol. Qed.
@@ -604,11 +604,11 @@ Hypothesis Hf : bijective f.
 Lemma f_inv_id : involutive f -> f_inv Hf = f.
 Proof.
 intros; apply (comp_inj_r (bij_inj Hf)).
-apply fun_ext; intro; rewrite !comp_correct H f_inv_correct_r; easy.
+apply fun_ext; intro; rewrite !comp_correct H f_inv_can_r; easy.
 Qed.
 
 Lemma f_inv_id_rev : f_inv Hf = f -> involutive f.
-Proof. intros H x; rewrite -{1}H; apply f_inv_correct_l. Qed.
+Proof. intros H x; rewrite -{1}H; apply f_inv_can_l. Qed.
 
 Lemma f_inv_id_equiv : f_inv Hf = f <-> involutive f.
 Proof. split; [apply f_inv_id_rev | apply f_inv_id]. Qed.
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index f9553257..2b2d9229 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -38,18 +38,22 @@ From FEM Require Import logic_compl Function_compl.
     (definition similar to surjective).
   'canS P1 f g' states that 'g' cancels 'f' on 'P1', ie it is its left inverse.
     (definition similar to cancel).
+  'involS P1 f' states that 'f' is involutive from 'P1' onto itself,
+    ie it cancels itself on 'P1'.
   'bijS P1 P2 f' states that 'f' is bijective from 'P1' onto 'P2'
     (definition similar to bijective).
+  'f_invS_EX' states the strong existence of the (left and right) inverse of
+    any bijective function from a subset onto another.
+  'f_invS Hf' is the inverse of a function from a subset onto another from any
+    proof 'Hf' of its bijectivity.
 *)
 
 
 Section Fun_sub_Def1.
 
 Context {T1 T2 : Type}.
-
 Variable P1 : T1 -> Prop.
 Variable P2 : T2 -> Prop.
-
 Variable f : T1 -> T2.
 
 Definition same_funS (g : T1 -> T2) : Prop := forall x1, P1 x1 -> f x1 = g x1.
@@ -73,11 +77,20 @@ End Fun_sub_Def1.
 
 Section Fun_sub_Def2.
 
-Context {T1 T2 : Type}.
+Context {T : Type}.
+Variable P : T -> Prop.
+Variable f : T -> T.
+
+Definition involS : Prop := canS P f f.
 
+End Fun_sub_Def2.
+
+
+Section Fun_sub_Def3.
+
+Context {T1 T2 : Type}.
 Variable P1 : T1 -> Prop.
 Variable P2 : T2 -> Prop.
-
 Variable f : T1 -> T2.
 
 Definition bijS_spec (g : T2 -> T1) : Prop :=
@@ -90,13 +103,12 @@ Proof.
 split; [intros [g Hg]; exists g; easy | intros [g Hg]; apply (BijS g Hg)].
 Qed.
 
-End Fun_sub_Def2.
+End Fun_sub_Def3.
 
 
 Section Same_funS_Facts.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 
 Lemma same_funS_refl : forall (f : T1 -> T2), same_funS P1 f f.
@@ -117,9 +129,7 @@ End Same_funS_Facts.
 Section RgS_Facts0.
 
 Context {T1 T2 : Type}.
-
 Variable P1 : T1 -> Prop.
-
 Variable f : T1 -> T2.
 
 Lemma imS_dec :
@@ -136,10 +146,8 @@ End RgS_Facts0.
 Section RgS_Facts1.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma RgS_eq : RgS P1 f = RgS_gen P1 (RgS P1 f) f.
@@ -171,10 +179,8 @@ End RgS_Facts1.
 Section RgS_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma RgS_ext : forall g, same_funS P1 f g -> RgS P1 f = RgS P1 g.
@@ -193,10 +199,8 @@ End RgS_Facts2.
 Section RgS_Facts3.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T3}.
 
@@ -254,10 +258,8 @@ End RgS_Facts3.
 Section FunS_Facts1.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma funS_correct : (forall x1, P1 x1 -> P2 (f x1)) -> funS P1 P2 f.
@@ -275,10 +277,8 @@ End FunS_Facts1.
 Section FunS_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T1 -> T2}.
 
@@ -291,9 +291,7 @@ End FunS_Facts2.
 Section FunS_Facts3.
 
 Context {T : Type}.
-
 Context {P : T -> Prop}.
-
 Context {f : T -> T}.
 
 Lemma funS_id : same_funS P f id -> funS P P f.
@@ -305,10 +303,8 @@ End FunS_Facts3.
 Section FunS_Facts4.
 
 Context {T1 T2 : Type}.
-
 Variable P1 : T1 -> Prop.
 Context {P2 : T2 -> Prop}.
-
 Variable f : T1 -> T2.
 
 Lemma funS_full_l : forall {f : T1 -> T2}, incl (Rg f) P2 -> funS fullset P2 f.
@@ -326,11 +322,9 @@ End FunS_Facts4.
 Section FunS_Facts5.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
 Context {P3 : T3 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T3}.
 
@@ -343,9 +337,7 @@ End FunS_Facts5.
 Section InjS_Facts1.
 
 Context {T : Type}.
-
 Context {P : T -> Prop}.
-
 Context {f : T -> T}.
 
 Lemma injS_id : same_funS P f (id : T -> T) -> injS P f.
@@ -357,9 +349,7 @@ End InjS_Facts1.
 Section InjS_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T1 -> T2}.
 
@@ -372,9 +362,7 @@ End InjS_Facts2.
 Section InjS_Facts3.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma injS_contra :
@@ -402,10 +390,8 @@ End InjS_Facts3.
 Section InjS_Facts4.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g h : T2 -> T1}.
 
@@ -423,10 +409,8 @@ End InjS_Facts4.
 Section InjS_Facts5.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-
 Context {f : T1 -> T2}.
 
 Lemma injS_comp_compat :
@@ -447,10 +431,8 @@ End InjS_Facts5.
 Section InjS_Facts6.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-
 Context {g h : T1 -> T2}.
 Context {f : T2 -> T3}.
 
@@ -467,9 +449,7 @@ End InjS_Facts6.
 Section SurjS_Facts1.
 
 Context {T : Type}.
-
 Context {P : T -> Prop}.
-
 Context {f : T -> T}.
 
 Lemma surjS_id : same_funS P f (id : T -> T) -> surjS P P f.
@@ -481,10 +461,8 @@ End SurjS_Facts1.
 Section SurjS_Facts1.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma surjS_correct : incl P2 (RgS P1 f) -> surjS P1 P2 f.
@@ -502,10 +480,8 @@ End SurjS_Facts1.
 Section SurjS_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T1 -> T2}.
 
@@ -521,7 +497,6 @@ End SurjS_Facts2.
 Section SurjS_Facts3.
 
 Context {T1 T2 : Type}.
-
 Context {f : T1 -> T2}.
 
 Lemma surj_S_equiv : surjective f <-> surjS fullset fullset f.
@@ -537,10 +512,8 @@ End SurjS_Facts3.
 Section SurjS_Facts4.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma surjS_RgS_gen_equiv : surjS P1 P2 f <-> RgS_gen P1 P2 f = P2.
@@ -565,10 +538,8 @@ End SurjS_Facts4.
 Section SurjS_Facts5.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g h : T2 -> T1}.
 
@@ -584,11 +555,9 @@ End SurjS_Facts5.
 Section SurjS_Facts6.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
 Context {P3 : T3 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T3}.
 
@@ -606,11 +575,9 @@ End SurjS_Facts6.
 Section SurjS_Facts7.
 
 Context {T1 T2 T3 : Type}.
-
 Variable P1 : T1 -> Prop.
 Context {P2 : T2 -> Prop}.
 Context {P3 : T3 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T2 -> T3}.
 
@@ -626,9 +593,7 @@ End SurjS_Facts7.
 Section CanS_Facts1.
 
 Context {T : Type}.
-
 Context {P : T -> Prop}.
-
 Context {f : T -> T}.
 
 Lemma canS_id_l : same_funS P f (id : T -> T) -> canS P f id.
@@ -643,10 +608,8 @@ End CanS_Facts1.
 Section CanS_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f f' : T1 -> T2}.
 Context {g g' : T2 -> T1}.
 
@@ -663,10 +626,8 @@ End CanS_Facts2.
 Section CanS_Facts3.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f f' : T1 -> T2}.
 Context {g g' : T2 -> T1}.
 
@@ -681,10 +642,8 @@ End CanS_Facts3.
 Section CanS_Facts4.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma canS_injS : forall (g : T2 -> T1), canS P1 f g -> injS P1 f.
@@ -729,10 +688,8 @@ End CanS_Facts4.
 Section CanS_Facts5.
 
 Context {T1 T2 : Type}.
-
 Variable P1 : T1 -> Prop.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T1}.
 
@@ -749,11 +706,8 @@ End CanS_Facts5.
 Section CanS_Facts6.
 
 Context {T1 T2 T3 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Context {P3 : T3 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {f1 : T2 -> T1}.
 Context {g : T2 -> T3}.
@@ -768,12 +722,25 @@ Qed.
 End CanS_Facts6.
 
 
-Section BijS_Facts1.
+Section InvolS_Facts.
 
 Context {T : Type}.
-
 Context {P : T -> Prop}.
+Context {f : T -> T}.
+
+Lemma involS_injS : involS P f -> injS P f.
+Proof. apply canS_injS. Qed.
 
+Lemma involS_bijS : funS P P f -> involS P f -> bijS P P f.
+Proof. intros; apply (BijS _ _ _ f); repeat split; easy. Qed.
+
+End InvolS_Facts.
+
+
+Section BijS_Facts1.
+
+Context {T : Type}.
+Context {P : T -> Prop}.
 Context {f : T -> T}.
 
 Lemma bijS_id : same_funS P f (id : T -> T) -> bijS P P f.
@@ -789,10 +756,8 @@ Section BijS_Facts2.
 
 Context {T1 T2 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T1 -> T2}.
 
@@ -812,10 +777,8 @@ Section BijS_Facts3.
 
 Context {T1 T2 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma bijS_ex_uniq :
@@ -858,10 +821,8 @@ End BijS_Facts3.
 Section BijS_Facts4.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma bijS_RgS : bijS P1 P2 f -> RgS P1 f = P2.
@@ -889,10 +850,8 @@ Section BijS_Facts5.
 
 Context {T1 T2 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma injS_surjS_bijS :
@@ -917,9 +876,7 @@ Section BijS_Facts6.
 
 Context {T1 T2 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
-
 Context {f : T1 -> T2}.
 
 Lemma bijS_RgS_equiv : bijS P1 (RgS P1 f) f <-> injS P1 f.
@@ -938,11 +895,9 @@ Section BijS_Facts7.
 
 Context {T1 T2 T3 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
 Context {P3 : T3 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T3}.
 
@@ -968,11 +923,9 @@ Section BijS_Facts8.
 
 Context {T1 T2 T3 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
 Variable P3 : T3 -> Prop.
-
 Context {f : T1 -> T2}.
 Variable g : T2 -> T3.
 
@@ -989,11 +942,9 @@ Section BijS_Facts9.
 
 Context {T1 T2 T3 : Type}.
 Hypothesis HT1 : inhabited T1.
-
 Variable P1 : T1 -> Prop.
 Context {P2 : T2 -> Prop}.
 Context {P3 : T3 -> Prop}.
-
 Variable f : T1 -> T2.
 Context {g : T2 -> T3}.
 
@@ -1009,10 +960,8 @@ End BijS_Facts9.
 Section BijS_FactsA.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g h : T2 -> T1}.
 
@@ -1031,10 +980,8 @@ End BijS_FactsA.
 Section BijS_FactsB.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Context {g : T2 -> T1}.
 
@@ -1063,10 +1010,8 @@ End BijS_FactsB.
 Section F_invS_Def.
 
 Context {T1 T2 : Type}.
-
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-
 Context {f : T1 -> T2}.
 Hypothesis Hf : bijS P1 P2 f.
 
@@ -1081,10 +1026,105 @@ Proof. apply (proj2_sig f_invS_EX). Qed.
 Lemma f_invS_funS_r : funS P2 P1 f_invS.
 Proof. apply (proj2_sig f_invS_EX). Qed.
 
-Lemma f_invS_canS_l : canS P2 f_invS f.
+Lemma f_invS_canS_l : canS P1 f f_invS.
 Proof. apply (proj2_sig f_invS_EX). Qed.
 
-Lemma f_invS_canS_r : canS P1 f f_invS.
+Lemma f_invS_canS_r : canS P2 f_invS f.
 Proof. apply (proj2_sig f_invS_EX). Qed.
 
 End F_invS_Def.
+
+
+Section F_invS_Facts1.
+
+Context {T1 T2 : Type}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+Context {f : T1 -> T2}.
+Hypothesis Hf : bijS P1 P2 f.
+
+Lemma f_invS_uniq_l :
+  forall (g : T2 -> T1), canS P1 f g -> same_funS P2 g (f_invS Hf).
+Proof. move=>> H; apply (bijS_canS_uniq_r Hf H), f_invS_canS_l. Qed.
+
+Lemma f_inSv_uniq_r :
+  forall (g : T2 -> T1),
+    funS P2 P1 g -> canS P2 g f -> same_funS P2 g (f_invS Hf).
+Proof.
+move=>> Hg H; apply: (bijS_canS_uniq_l Hf Hg _ H);
+    [apply f_invS_funS_r | apply f_invS_canS_r].
+Qed.
+
+Lemma f_invS_bijS : bijS P2 P1 (f_invS Hf).
+Proof. apply: (bijS_canS_bijS _ Hf); apply f_invS_canS_l. Qed.
+
+Lemma f_invS_injS : injS P2 (f_invS Hf).
+Proof. apply (bijS_injS P1), f_invS_bijS. Qed.
+
+Lemma f_invS_surjS : surjS P2 P1 (f_invS Hf).
+Proof. apply bijS_surjS, f_invS_bijS. Qed.
+
+Lemma f_invS_eq_equiv :
+  forall x1 x2, P1 x1 -> P2 x2 -> x1 = f_invS Hf x2 <-> f x1 = x2.
+Proof.
+intros x1 x2 Hx1 Hx2; split.
+rewrite -{2}(f_invS_canS_r Hf x2 Hx2); apply f_equal.
+rewrite -{2}(f_invS_canS_l Hf x1 Hx1); apply f_equal.
+Qed.
+
+Lemma f_invS_neq_equiv :
+  forall x1 x2, P1 x1 -> P2 x2 -> x1 <> f_invS Hf x2 <-> f x1 <> x2.
+Proof. intros; rewrite -iff_not_equiv; apply f_invS_eq_equiv; easy. Qed.
+
+End F_invS_Facts1.
+
+
+Section F_invS_Facts2.
+
+Context {T1 T2 : Type}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+Context {f g : T1 -> T2}.
+Hypothesis Hf : bijS P1 P2 f.
+Hypothesis Hg : bijS P1 P2 g.
+
+Lemma f_invS_ext : same_funS P1 f g -> same_funS P2 (f_invS Hf) (f_invS Hg).
+Proof.
+intros H x2 Hx2; apply (bijS_injS P2 Hf).
+3: rewrite -> (H (f_invS Hg _)), !f_invS_canS_r; [easy.. |].
+apply (f_invS_funS_r Hf (f_invS Hf x2)); easy.
+1,2: apply (f_invS_funS_r Hg (f_invS Hg x2)); easy.
+Qed.
+
+Lemma f_invS_invol :
+  forall (Hf1 : bijS P2 P1 (f_invS Hf)), same_funS P1 (f_invS Hf1) f.
+Proof. intros; apply same_funS_sym, f_invS_uniq_l, f_invS_canS_r. Qed.
+
+Lemma f_invS_invol_alt : same_funS P1 (f_invS (f_invS_bijS Hf)) f.
+Proof. apply f_invS_invol. Qed.
+
+End F_invS_Facts2.
+
+
+Section F_invS_Facts3.
+
+Context {T : Type}.
+Context {P : T -> Prop}.
+Context {f : T -> T}.
+Hypothesis Hf : bijS P P f.
+
+Lemma f_invS_id : involS P f -> same_funS P (f_invS Hf) f.
+Proof.
+intros Hf1; apply: (comp_injS_r _ _ _ (bijS_injS _ Hf)).
+apply f_invS_funS_r.
+apply f_invS_funS_l, Hf.
+intros x Hx; rewrite !comp_correct f_invS_canS_r// Hf1; easy.
+Qed.
+
+Lemma f_invS_id_rev : same_funS P (f_invS Hf) f -> involS P f.
+Proof. intros H x Hx; rewrite -(H x Hx) f_invS_canS_r; easy. Qed.
+
+Lemma f_invS_id_equiv : same_funS P (f_invS Hf) f <-> involS P f.
+Proof. split; [apply f_invS_id_rev | apply f_invS_id]. Qed.
+
+End F_invS_Facts3.
diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index b76c15e2..1780a99e 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -424,7 +424,7 @@ apply Phi_d_0_inv_compose; try easy.
 assert (H0 : p = compose p_ref ((Phi_d_0_inv dL vtx_cur Hvtx))).
 unfold p_ref, compose.
 apply fun_ext; intros x_cur.
-rewrite f_inv_correct_r; easy.
+rewrite f_inv_can_r; easy.
 rewrite H0 Y2.
 unfold compose.
 apply fun_ext; intros x.
@@ -526,7 +526,7 @@ assert (Y2 : forall y : 'R^dL.+1,  face_hyp_0 dL.+1 vtx_cur y ->
 unfold p0'.
 intros y Hy.
 unfold compose.
-rewrite (f_invS_canS_l (Phi_bijS dL vtx_cur Hvtx)); try easy.
+rewrite (f_invS_canS_r (Phi_bijS dL vtx_cur Hvtx)); try easy.
 unfold funS.
 rewrite Y2; try easy.
 apply val_eq in IH1.
diff --git a/FEM/P_approx_k.v b/FEM/P_approx_k.v
index c9a0048f..fad3ea6b 100644
--- a/FEM/P_approx_k.v
+++ b/FEM/P_approx_k.v
@@ -623,7 +623,7 @@ replace p with (compose (compose p f) (f_inv Hf2)).
 apply P_approx_k_d_compose_affine_mapping; try easy.
 now apply is_affine_mapping_bij_compat.
 unfold compose; apply fun_ext; intros x.
-now rewrite f_inv_correct_r.
+now rewrite f_inv_can_r.
 Qed.
 
 Lemma P_approx_k_d_affine_mapping_compose_basis : forall {d} k 
@@ -642,7 +642,7 @@ rewrite (proj1 HB) in H1.
 inversion H1 as (L,HL).
 apply span_ex; exists L; apply fun_ext; intros x.
 apply trans_eq with (compose (compose p (f_inv Hf2)) f x).
-unfold compose; now rewrite f_inv_correct_l.
+unfold compose; now rewrite f_inv_can_l.
 rewrite -HL; unfold compose.
 now rewrite 2!fct_comb_lin_r_eq.
 (* *)
diff --git a/FEM/poly_Lagrange.v b/FEM/poly_Lagrange.v
index fb5d1dfc..4991aa43 100644
--- a/FEM/poly_Lagrange.v
+++ b/FEM/poly_Lagrange.v
@@ -1614,13 +1614,13 @@ Definition Phi_d_0_inv :  (*'R^d*) fct_ModuleSpace -> (*'R^d*) fct_ModuleSpace :
 Lemma Phi_d_0_comp : forall x_cur : 'R^d, 
   x_cur = Phi_d_0 (Phi_d_0_inv x_cur).
 Proof.
-intros x_cur; apply esym, f_inv_correct_r.
+intros x_cur; apply esym, f_inv_can_r.
 Qed.
 
 Lemma Phi_d_0_inv_comp : forall x_ref : 'R^d, 
   x_ref = Phi_d_0_inv (Phi_d_0 x_ref).
 Proof.
-intros x_ref; apply esym, f_inv_correct_l.
+intros x_ref; apply esym, f_inv_can_l.
 Qed.
 
 End Phi_d_Facts_1.
-- 
GitLab