From 56684530f3335bfd9ea1c41df642354d0893da3c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 30 Jan 2024 17:33:30 +0100
Subject: [PATCH] Rm useless map_injS_uniq (use map_inj_in_uniq instead). Add
injS_equiv_seq (WIP).
---
FEM/Algebra/ord_compl.v | 32 ++++++++++++--------------------
1 file changed, 12 insertions(+), 20 deletions(-)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index a47bf748..84dad81c 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -118,29 +118,20 @@ move=>>; rewrite rcons_uniq.
move=> /andP [Hx _]; apply nth_rcons_r_rev; easy.
Qed.
-Lemma map_injS_uniq :
- forall {P : pred T} {sT : subType (T:=T) P} {f : T -> sT} {s : seq T},
- injS P f -> all P s -> uniq (map f s) = uniq s.
+Lemma injS_equiv_seq :
+ forall {P : pred T} {sT : subType (T:=T) P} {f : T -> sT},
+ injS P f <-> forall s, all P s -> { in s &, injective f }.
Proof.
-intros P sT f s Hf Hs.
+intros P sT f; split.
+(* *)
+intros H s Hs x y Hx Hy; apply H.
+admit.
+admit.
+(* *)
+intros H x y Hx Hy; apply (H [:: x; y]).
-(*
-map_uniq :
- forall [T1 T2 : eqType] [f : T1 -> T2] [s : seq T1], uniq [seq f i | i <- s] -> uniq s
-map_inj_uniq :
- forall [T1 T2 : eqType] [f : T1 -> T2] (s : seq T1),
- injective f -> uniq (map f s) = uniq s
-
-pmap_sub_uniq :
- forall [T : eqType] [P : pred T] (sT : subType (T:=T) P) [s : seq T],
- uniq s -> uniq (pmap insub s)
-
-map_pK : pcancel g f -> cancel (map g) (pmap f)
-pmap_filter : ocancel f g -> map g (pmap f s) = filter (isSome f) s
-mem_pmap : (u \in pmap f s) = (Some u \in [seq f i | i <- s])
-*)
Admitted.
End Seq_compl2.
@@ -694,7 +685,8 @@ pose (il := map in_ordS jl : seq 'I_n.+1); exists il; [split |].
(* *)
rewrite ord_enumS_eq; apply perm_map; easy.
(* *)
-rewrite (map_injS_uniq in_ordS_injS); [rewrite (perm_uniq Hjl2); apply iota_uniq |].
+rewrite map_inj_in_uniq; [rewrite (perm_uniq Hjl2); apply iota_uniq |].
+apply injS_equiv_seq; [apply in_ordS_injS |].
rewrite (perm_all _ Hjl2); apply /allPP; [intros; apply /ltP |].
intros j Hj; rewrite mem_iota in Hj; apply /ltP; easy.
(* *)
--
GitLab