From de1bcddd15f339e35f10840f2c000e8d0f4261b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sat, 3 Feb 2024 02:09:40 +0100
Subject: [PATCH] Add and prove sorted_enum_ord, sorted_filter_enum_ord. Proof
of filterP_ord_incrF_S. WIP: sorted_ordP.
---
FEM/Algebra/ord_compl.v | 65 +++++++++++++++++++++++------------------
1 file changed, 37 insertions(+), 28 deletions(-)
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 1ea1d80e..a1a52a87 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2257,7 +2257,7 @@ Qed.
(* FC (18/12/2023): useful? *)
Lemma unfilterP_ord_correct_in :
- forall {n} (P : 'I_n -> Prop) {i0} (HP0 : P i0) i,
+ forall {n} {P : 'I_n -> Prop} {i0} (HP0 : P i0) {i},
P i -> exists j, i = filterP_ord j /\ unfilterP_ord HP0 i = j.
Proof.
intros n P i0 HP0 i Hi; exists (unfilterP_ord HP0 i); split; [| easy].
@@ -2275,36 +2275,45 @@ 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).
+Lemma sorted_ordP :
+ forall {T : Type} {leT : rel T} {l : seq T} x0 x1,
+ reflect (forall (i : 'I_(size l)) (Hi1 : i.+1 < size l),
+ leT (nth x0 l i) (nth x1 l (Ordinal Hi1))) (sorted leT l).
Proof.
-intros n P j Hj1.
+intros T leT l x0 x1.
+(* Use sortedP. *)
+Admitted.
+Lemma sorted_enum_ord : forall {n}, sorted ord_ltn (enum 'I_n).
+Proof.
+intros n; destruct n as [|n]; [rewrite (size0nil (size_enum_ord _)); easy |].
+apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
+unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
+Qed.
-(*
-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 sorted_filter_enum_ord :
+ forall {n} (P : 'I_n -> Prop),
+ sorted ord_ltn (filter (fun i => asbool (P i)) (enum 'I_n)).
+Proof.
+intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
+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.
+apply /ltP; fold (ord_ltn (filterP_ord j) (filterP_ord (Ordinal Hj1))).
+unfold filterP_ord, enum_val, enum_mem; rewrite -enumT; simpl.
+move: (sorted_filter_enum_ord P) => /sorted_ordP H0.
+assert (H1 : lenPF P = size (filter (fun i => asbool (P i)) (enum 'I_n))).
+ unfold lenPF; rewrite cardE; unfold enum_mem; do 2 f_equal.
+ rewrite filter_predT; easy.
+pose (jj := cast_ord H1 j).
+assert (Hjj1 : jj.+1 < size (filter (fun i => asbool (P i)) (enum 'I_n)))
+ by now unfold jj; simpl; rewrite -H1.
+apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
+Qed.
Lemma filterP_ord_incrF :
forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).
--
GitLab