From 4b220c915a2d865ca99f7a641f3300112acb9d65 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 23:38:25 +0100
Subject: [PATCH] Proof of filterP_cast_ord_incrF. WIP: filterP_ord_incrF_S.
---
FEM/Algebra/ord_compl.v | 38 ++++++++++++++++++++++++++++++++------
1 file changed, 32 insertions(+), 6 deletions(-)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index cb6faa36..1ea1d80e 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2275,14 +2275,40 @@ Lemma unfilterP_ord_inj :
unfilterP_ord HP0 i = unfilterP_ord HP0 j -> i = j.
Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.
+Lemma filterP_ord_incrF_S :
+ forall {n} (P : 'I_n -> Prop), incrF_S (fun j : 'I_(lenPF P) => filterP_ord j).
+Proof.
+intros n P j Hj1.
+
+
+(*
+destruct (lt_eq_lt_dec (filterP_ord j1) (filterP_ord j2))
+ as [[H | H] | H]; [easy | exfalso..].
+apply ord_inj, filterP_ord_inj in H; subst; contradict Hj; apply Nat.lt_irrefl.
+*)
+
+(*
+enum_val
+nth sorted
+
+mem : pT -> mem_pred T
+enum_mem : mem_pred T -> seq T := filter Finite.enum mA
+enum A := (enum_mem (mem A))
+enum_val : 'I_#|[eta A]| -> T := nth (enum_default i) (enum A) i
+enum_rank : T -> 'I_#|[eta T]| := enum_rank_in (erefl true) x
+enum_rank_in : x0 \in A -> T -> 'I_#|[eta A]|
+
+nth_image : nth y0 [seq f x | x in A] i = f (enum_val i)
+enum_val_nth : enum_val i = nth x (enum A) i
+enum_valK : cancel enum_val enum_rank
+enum_rankK : cancel enum_rank enum_val
+nth_codom : nth y0 (codom f) i = f (enum_val i)
+*)
+Admitted.
+
Lemma filterP_ord_incrF :
forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).
-Proof.
-intros n P j1 j2 Hj.
-
-
-
-Admitted.
+Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.
Lemma filterP_cast_ord_incrF :
forall {n1 n2} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop}
--
GitLab