From 3348f6cf14f1d3ba7f77ac7e59911ad976792b43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr> Date: Mon, 5 Feb 2024 10:37:14 +0100 Subject: [PATCH] Function_sub: Rename injS_inj -> inj_S_equiv, surjS_surj -> surj_S_equiv, bijS_bij -> bij_S_equiv. Sub_struct, Finite_dim: Propagate new API (from Function_sub). --- FEM/Algebra/Finite_dim.v | 2 +- FEM/Algebra/Sub_struct.v | 16 ++++++++-------- FEM/Compl/Function_sub.v | 10 ++++------ 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v index 04581d12..378e9de0 100644 --- a/FEM/Algebra/Finite_dim.v +++ b/FEM/Algebra/Finite_dim.v @@ -1503,7 +1503,7 @@ apply compatible_ms_image; try easy. apply compatible_ms_fullset. apply (bijS_injS inhabited_ms fullset). replace (image fs fullset) with (@fullset PIs). -apply bijS_bij; try apply inhabited_ms. +apply bij_S_equiv; try apply inhabited_ms. apply f_inv_bij. apply subset_ext_equiv; split; intros (x,Hx1) Hx2; try easy. rewrite image_eq; inversion Hx1 as (y,Hy). diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v index c3ad5be2..469a424a 100644 --- a/FEM/Algebra/Sub_struct.v +++ b/FEM/Algebra/Sub_struct.v @@ -115,14 +115,14 @@ Hypothesis HfS : forall x1, val (fS x1) = f (val x1). Lemma sub_inj : injS P1 f -> injective fS. Proof. -intros Hf; apply injS_inj. +intros Hf; apply inj_S_equiv. move=> [x1 Hx1] [y1 Hy1] _ _ /(f_equal val); rewrite !HfS; simpl. move=> /(Hf _ _ Hx1 Hy1) H1; apply val_inj; simpl; easy. Qed. Lemma sub_surj : surjS P1 P2 f -> surjective fS. Proof. -intros Hf; apply surjS_surj. +intros Hf; apply surj_S_equiv. intros [x2 Hx2] _; destruct (Hf _ Hx2) as [x1 [Hx1a Hx1b]]. exists (mk_sub Hx1a); split; [| apply val_inj; rewrite HfS]; easy. Qed. @@ -485,12 +485,12 @@ Qed. Lemma mm_inj_rev : injective f -> Ker f = zero_sub_struct. Proof. -rewrite -KerS_full injS_inj; apply (mmS_injS_rev compatible_m_fullset Hf). +rewrite -KerS_full inj_S_equiv; apply (mmS_injS_rev compatible_m_fullset Hf). Qed. Lemma mm_bij_rev : bijective f -> Ker f = zero_sub_struct /\ Rg f = fullset. Proof. -rewrite -KerS_full -RgS_gen_full bijS_bij; [| apply inhabited_m]. +rewrite -KerS_full -RgS_gen_full bij_S_equiv; [| apply inhabited_m]. apply (mmS_bijS_gen_rev compatible_m_fullset Hf). Qed. @@ -1104,7 +1104,7 @@ Proof. apply Ker_m_zero_equiv, morphism_g_m; easy. Qed. Lemma gm_inj : incl (Ker f) zero_sub_struct -> injective f. Proof. -rewrite -KerS_full injS_inj; apply (gmS_injS compatible_g_fullset Hf). +rewrite -KerS_full inj_S_equiv; apply (gmS_injS compatible_g_fullset Hf). Qed. Lemma gm_inj_rev : injective f -> Ker f = zero_sub_struct. @@ -1112,13 +1112,13 @@ Proof. apply mm_inj_rev, morphism_g_m; easy. Qed. Lemma gm_inj_equiv : injective f <-> Ker f = zero_sub_struct. Proof. -rewrite -KerS_full injS_inj; apply (gmS_injS_equiv compatible_g_fullset Hf). +rewrite -KerS_full inj_S_equiv; apply (gmS_injS_equiv compatible_g_fullset Hf). Qed. Lemma gm_bij : incl (Ker f) zero_sub_struct -> incl fullset (Rg f) -> bijective f. Proof. -rewrite -KerS_full -RgS_full bijS_bij; [| apply inhabited_g]. +rewrite -KerS_full -RgS_full bij_S_equiv; [| apply inhabited_g]. apply (gmS_bijS_gen compatible_g_fullset Hf), funS_full. Qed. @@ -1127,7 +1127,7 @@ Proof. apply mm_bij_rev, morphism_g_m; easy. Qed. Lemma gm_bij_equiv : bijective f <-> Ker f = zero_sub_struct /\ Rg f = fullset. Proof. -rewrite -KerS_full -RgS_gen_full bijS_bij; [| apply inhabited_g]. +rewrite -KerS_full -RgS_gen_full bij_S_equiv; [| apply inhabited_g]. rewrite (gmS_bijS_gen_equiv compatible_g_fullset Hf); easy. Qed. diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v index f1858e20..2f77f222 100644 --- a/FEM/Compl/Function_sub.v +++ b/FEM/Compl/Function_sub.v @@ -321,20 +321,18 @@ Variable PF : F -> Prop. Variable f : E -> F. -(* TODO FC (27/11/2023): maybe apply iff_sym to the statements. *) - -Lemma injS_inj : injective f <-> injS fullset f. +Lemma inj_S_equiv : injective f <-> injS fullset f. Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed. -Lemma surjS_surj : surjective f <-> surjS fullset fullset f. +Lemma surj_S_equiv : surjective f <-> surjS fullset fullset f. Proof. split; intros Hf. intros y _; destruct (Hf y) as [x Hx]; exists x; easy. intros y; destruct (Hf y) as [x Hx]; [| exists x]; easy. Qed. -Lemma bijS_bij : bijective f <-> bijS fullset fullset f. -Proof. rewrite bij_equiv bijS_equiv// injS_inj surjS_surj; easy. Qed. +Lemma bij_S_equiv : bijective f <-> bijS fullset fullset f. +Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed. End Function_sub_Facts3. -- GitLab