From 87308ebf68157055705d3ed0d6c1b348270230c7 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 22:01:51 +0100
Subject: [PATCH] ord_compl: Add and prove cast_ord_incrF,
filterP_cast_ord_incrF.
Finite_family:
WIP: filterP_ord_incrF (modified, use new incrF_Rg_eq_eq).
Modify filterP_f_ord_incrF.
---
FEM/Algebra/Finite_family.v | 23 +++++++++++------------
FEM/Algebra/ord_compl.v | 11 +++++++++++
2 files changed, 22 insertions(+), 12 deletions(-)
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index c28494ef..942574ec 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -4858,16 +4858,15 @@ Qed.
Lemma filterP_ord_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f) {P1 : 'Prop^n1}
- {P2 : 'Prop^n2} (HP : extendPF f P1 P2) {j1 : 'I_(lenPF P1)},
+ {P2 : 'Prop^n2} (HP : extendPF f P1 P2),
let H := lenPF_extendPF (incrF_inj Hf) HP in
- f (filterP_ord j1) = filterP_ord (cast_ord H j1).
+ f \o filterP_ord = filterP_ord \o (cast_ord H).
Proof.
-intros n1 n2 f Hf P1 P2 HP j1 H.
+intros n1 n2 f Hf P1 P2 HP H; apply incrF_Rg_eq_eq.
+apply incrF_comp; [apply filterP_ord_incrF | easy].
+apply filterP_cast_ord_incrF.
+
-(* trying high-level.
-move: (lenPF_n0_alt j1) => [i1 Hi1].
-move: (extendPF_unfunF_rev (incrF_inj Hf) HP) => HP2; subst.
-*)
@@ -4893,14 +4892,14 @@ Admitted.
Lemma filterP_f_ord_incrF :
forall {n1 n2} {f : 'I_{n1,n2}} (Hf : incrF f)
{P1 : 'Prop^n1} {P2 : 'Prop^n2} (HP : extendPF f P1 P2)
- {i1} (HP2 : P2 (f i1)) {j1 : 'I_(lenPF P1)},
+ {i1} (HP2 : P2 (f i1)),
let H := lenPF_extendPF (incrF_inj Hf) HP in
- filterP_f_ord f HP2 j1 = cast_ord H j1.
+ filterP_f_ord f HP2 = cast_ord H.
Proof.
-intros n1 n2 f Hf P1 P2 HP i1 HP2 j1 H.
+intros n1 n2 f Hf P1 P2 HP i1 HP2 H; apply extF; intros j1.
move: (extendPF_unfunF_rev (incrF_inj Hf) HP) => HP2'; subst.
-rewrite (filterP_f_ord_correct_alt _ (incrF_inj Hf) HP).
-apply filterP_ord_incrF.
+rewrite (filterP_f_ord_correct_alt _ (incrF_inj Hf) HP) -(comp_correct _ f).
+rewrite (filterP_ord_incrF Hf HP); easy.
Qed.
(* Was:
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 84dad81c..d845d2c2 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -984,6 +984,9 @@ intros Hi; apply ord_inj; simpl; rewrite Hi subn1 //.
move=>> ->; simpl; rewrite subn1 //.
Qed.
+Lemma cast_ord_incrF : forall {n1 n2} (H : n1 = n2), incrF (cast_ord H).
+Proof. easy. Qed.
+
(* Definition and properties of cast_f_ord. *)
Definition cast_f_ord {n1 n2} (H : n1 = n2) (p1 : 'I_[n1]) : 'I_[n2] :=
@@ -2084,6 +2087,14 @@ intros n P j1 j2 Hj.
Admitted.
+Lemma filterP_cast_ord_incrF :
+ forall {n1 n2} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop}
+ (H : lenPF P1 = lenPF P2),
+ incrF (filterP_ord \o (cast_ord H)).
+Proof.
+intros; apply incrF_comp; [apply cast_ord_incrF | apply filterP_ord_incrF].
+Qed.
+
Lemma filterP_cast_ord_eq :
forall {n m} {P : 'I_n -> Prop} (H1 H2 : m = lenPF P) (j : 'I_m),
filterP_ord (cast_ord H1 j) = filterP_ord (cast_ord H2 j).
--
GitLab