From 8104ab7dd2da25cfba027407fe5248daeb270954 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 2 Feb 2024 11:00:26 +0100
Subject: [PATCH] WIP: perm_EX.
---
FEM/Algebra/ord_compl.v | 31 ++++++++++++++++++++++++++++---
1 file changed, 28 insertions(+), 3 deletions(-)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 76957c43..ad89ce59 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -693,8 +693,12 @@ End Ord_compl2.
Section Ord_compl3.
Context {T : eqType}.
+Context {leT : rel T}.
+
+Hypothesis HT0 : antisymmetric leT.
+Hypothesis HT1 : transitive leT.
+Hypothesis HT2 : total leT.
-Variable leT : rel T.
Variable x0 : T.
Lemma perm_EX :
@@ -702,12 +706,33 @@ Lemma perm_EX :
{ p : 'I_[size l2] | injective p &
l1 = map (fun i => nth x0 l2 (p i)) (ord_enum (size l2)) }.
Proof.
-intros l1 l2 Hl.
-
+intros l1 l2 Hla.
+assert (Hlb : size l1 = size l2) by now apply perm_size.
+pose (n := size l2); assert (Hn : size l2 = n) by easy.
+fold n in Hlb; fold n; destruct n as [|n].
+(* *)
+exists (fun_from_I_0 'I_0); [apply fun_from_I_0_inj |].
+rewrite (size0nil Hlb) (size0nil size_ord_enum); easy.
+(* *)
+move: (perm_sortP HT2 HT1 HT0 _ _ Hla) => Hlc.
+destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
+rewrite Hlb in il1, Hil1a, Hil1b, Hil1c.
+pose (p1 := fun i : 'I_n => nth ord0 il1 i).
+destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
+rewrite Hn in il2, Hil2a, Hil2b, Hil2c.
+pose (p2 := fun i : 'I_n => nth ord0 il2 i).
+(*
+perm_eq
+perm_mem : perm_eq s1 s2 -> s1 =i s2
+perm_map : perm_eq s t -> perm_eq (map f s) (map f t)
+perm_map_inj : injective f -> perm_eq (map f s) (map f t) -> perm_eq s t
+perm_sortP : total leT -> transitive leT -> antisymmetric leT ->
+ reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2)
+*)
Admitted.
Lemma sort_perm_EX :
--
GitLab