From 1a2cb404dfaf2dbd3a20fb4c64b8408763014f1c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 5 Feb 2024 22:52:54 +0100
Subject: [PATCH] Move stuff around. Add and prove ord_max_equiv_ge{q,},
 ord_nmax_equiv_lt{n,},               cast_ord_max_equiv_ge{q,},
 cast_ord_nmax_equiv_lt{n,},               lenPF_ind_r_in_S_alt. Higher-level
 proof of filterP_ord_ind_r_in_max. WIP: filterP_ord_ind_r_in_max_rev.

---
 FEM/Algebra/ord_compl.v | 102 ++++++++++++++++++++++++++++++++--------
 1 file changed, 83 insertions(+), 19 deletions(-)

diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index d3a0e855..c55c3f27 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -330,30 +330,32 @@ exists ord_max; apply ord_max_not_0.
 exists ord0; apply not_eq_sym; easy.
 Qed.
 
-Lemma ord0_equiv_leq : forall m {n} {i : 'I_n.+1}, i = ord0 <-> i <= (@ord0 m).
+Lemma ord0_equiv_leq : forall m {n} {i : 'I_n.+1}, i = ord0 <-> i <= @ord0 m.
 Proof.
 intros; rewrite ord0_equiv; destruct i as [i Hi]; simpl.
 split; [intros; subst | move=> /leP]; auto with arith.
 Qed.
 
 Lemma ord0_equiv_le :
-  forall m {n} {i : 'I_n.+1}, i = ord0 <-> (i <= (@ord0 m))%coq_nat.
+  forall m {n} {i : 'I_n.+1}, i = ord0 <-> (i <= @ord0 m)%coq_nat.
 Proof.
 intros m n i; rewrite (ord0_equiv_leq m); split; move=> /leP; easy.
 Qed.
 
-Lemma ord_n0_equiv_gtn : forall m {n} {i : 'I_n.+1}, i <> ord0 <-> (@ord0 m) < i.
+Lemma ord_n0_equiv_gtn : forall m {n} {i : 'I_n.+1}, i <> ord0 <-> @ord0 m < i.
 Proof. intros; rewrite -iff_not_r_equiv ord0_equiv_leq nltn_geq; easy. Qed.
 
 Lemma ord_n0_equiv_gt :
-  forall m {n} {i : 'I_n.+1}, i <> ord0 <-> ((@ord0 m) < i)%coq_nat.
+  forall m {n} {i : 'I_n.+1}, i <> ord0 <-> (@ord0 m < i)%coq_nat.
 Proof.
 intros m n i; rewrite (ord_n0_equiv_gtn m); split; move=> /ltP; easy.
 Qed.
 
+(* TODO FC (05/02/2024): rename into ord_n0_nlt. *)
 Lemma ord_not_0_gt : forall {n} {i : 'I_n.+1}, i <> ord0 -> ~ (i < 1)%coq_nat.
 Proof. intros n i H; contradict H; apply ord_inj; simpl; auto with zarith. Qed.
 
+(* TODO FC (05/02/2024): rename into ord_n0_equiv_nlt. *)
 Lemma ord_n0_equiv_alt :
   forall {n} {i : 'I_n.+1}, i <> ord0 <-> ~ (i < 1)%coq_nat.
 Proof.
@@ -361,9 +363,36 @@ intros; split. apply ord_not_0_gt.
 rewrite -contra_equiv; intros; subst; apply Nat.lt_0_1.
 Qed.
 
+(* TODO FC (05/02/2024): rename into ord0_equiv_lt. *)
 Lemma ord0_equiv_alt : forall {n} {i : 'I_n.+1}, i = ord0 <-> (i < 1)%coq_nat.
 Proof. move=>>; rewrite iff_not_equiv; apply ord_n0_equiv_alt. Qed.
 
+(* TODO FC (05/02/2024): rename into ord_gt_n0. *)
+Lemma ord_gt_not_0 : forall {n} {i j : 'I_n.+1}, (i < j)%coq_nat -> j <> ord0.
+Proof.
+intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; apply /leP; easy.
+Qed.
+
+Lemma ord_max_equiv_geq :
+  forall {n} {i : 'I_n.+1}, i = ord_max <-> @ord_max n <= i.
+Proof.
+intros; rewrite ord_max_equiv; destruct i as [i Hi]; simpl; split;
+    [intros; subst | move=> /leP; move: Hi => /leP]; auto with zarith.
+Qed.
+
+Lemma ord_max_equiv_ge :
+  forall {n} {i : 'I_n.+1}, i = ord_max <-> (@ord_max n <= i)%coq_nat.
+Proof. intros; rewrite ord_max_equiv_geq; split; move=> /leP; easy. Qed.
+
+Lemma ord_nmax_equiv_ltn :
+  forall {n} {i : 'I_n.+1}, i <> ord_max <-> i < @ord_max n.
+Proof. intros; rewrite -iff_not_r_equiv ord_max_equiv_geq nltn_geq; easy. Qed.
+
+Lemma ord_nmax_equiv_lt :
+  forall {n} {i : 'I_n.+1}, i <> ord_max <-> (i < @ord_max n)%coq_nat.
+Proof. intros; rewrite ord_nmax_equiv_ltn; split; move=> /ltP; easy. Qed.
+
+(* TODO FC (05/02/2024): rename into ord_nmax_lt. *)
 Lemma ord_not_max_lt : forall {n} {i : 'I_n.+1}, i <> ord_max -> (i < n)%coq_nat.
 Proof.
 intros n [i Hi] Hi1; simpl.
@@ -371,6 +400,7 @@ apply Nat.nle_gt; contradict Hi1; apply ord_inj; simpl.
 move: Hi => /ltP Hi2; auto with zarith.
 Qed.
 
+(* TODO FC (05/02/2024): rename into ord_lt_nmax. *)
 Lemma ord_lt_not_max :
   forall {n} {i j : 'I_n.+1}, (i < j)%coq_nat -> i <> ord_max.
 Proof.
@@ -378,6 +408,7 @@ intros n i [j Hj] H; apply ord_lt_neq; simpl in *.
 apply nat_lt_lt_S with j; try easy; apply /ltP; easy.
 Qed.
 
+(* TODO FC (05/02/2024): rename into ord_nmax_equiv_lt. *)
 Lemma ord_nmax_equiv_alt :
   forall {n} {i : 'I_n.+1}, i <> ord_max <-> (i < n)%coq_nat.
 Proof.
@@ -385,15 +416,11 @@ intros; split. apply ord_not_max_lt.
 intros Hi; apply (@ord_lt_not_max _ _ ord_max); easy.
 Qed.
 
+(* TODO FC (05/02/2024): rename into ord_max_equiv_nlt. *)
 Lemma ord_max_equiv_alt :
   forall {n} {i : 'I_n.+1}, i = ord_max <-> ~ (i < n)%coq_nat.
 Proof. move=>>; rewrite iff_not_r_equiv; apply ord_nmax_equiv_alt. Qed.
 
-Lemma ord_gt_not_0 : forall {n} {i j : 'I_n.+1}, (i < j)%coq_nat -> j <> ord0.
-Proof.
-intros n i j H; contradict H; rewrite H; apply Nat.nlt_ge; apply /leP; easy.
-Qed.
-
 Lemma ord_lt_S : forall {n} (i : 'I_n), i.+1 < n.+1.
 Proof.
 intros n [i Hi]; apply /ltP; rewrite -Nat.succ_lt_mono; apply /ltP; easy.
@@ -1252,7 +1279,7 @@ Qed.
 
 Lemma cast_ord0_equiv_leq :
   forall {m n p} (H0 : 0 < m) (H : n = p.+1) {i : 'I_n},
-    cast_ord H i = ord0 <-> i <= (Ordinal H0).
+    cast_ord H i = ord0 <-> i <= Ordinal H0.
 Proof.
 intros m n p H0 H i; rewrite (cast_ord_val H) (ord0_equiv_leq m); easy.
 Qed.
@@ -1278,6 +1305,32 @@ Proof.
 intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord0_equiv_le.
 Qed.
 
+Lemma cast_ord_max_equiv_geq :
+  forall {n p} (H : n = p.+1) {i : 'I_n},
+    cast_ord H i = ord_max <-> Ordinal (ltnSn p) <= i.
+Proof. intros n p H i; rewrite (cast_ord_val H) ord_max_equiv_geq; easy. Qed.
+
+Lemma cast_ord_max_equiv_ge :
+  forall {n p} (H : n = p.+1) {i : 'I_n},
+    cast_ord H i = ord_max <-> (Ordinal (ltnSn p) <= i)%coq_nat.
+Proof.
+intros n p H i; rewrite cast_ord_max_equiv_geq; split; move=> /leP; easy.
+Qed.
+
+Lemma cast_ord_nmax_equiv_ltn :
+  forall {n p} (H : n = p.+1) {i : 'I_n},
+    cast_ord H i <> ord_max <-> i < Ordinal (ltnSn p).
+Proof.
+intros; rewrite -iff_not_r_equiv nltn_geq; apply cast_ord_max_equiv_geq.
+Qed.
+
+Lemma cast_ord_nmax_equiv_lt :
+  forall {n p} (H : n = p.+1) {i : 'I_n},
+    cast_ord H i <> ord_max <-> (i < Ordinal (ltnSn p))%coq_nat.
+Proof.
+intros; rewrite -iff_not_r_equiv Nat.nlt_ge; apply cast_ord_max_equiv_ge.
+Qed.
+
 Lemma cast_ord_incrF : forall {n1 n2} (H : n1 = n2), incrF (cast_ord H).
 Proof. easy. Qed.
 
@@ -2300,6 +2353,11 @@ Lemma lenPF_ind_r_in_S :
     P ord_max -> lenPF P = (lenPF (fun i => P (widen_S i))).+1.
 Proof. move=>> HP; rewrite (lenPF_ind_r_in HP); apply addn1. Qed.
 
+Lemma lenPF_ind_r_in_S_alt :
+  forall {n} {P : 'I_n.+1 -> Prop},
+    P ord_max -> lenPF (fun i => P (widen_S i)) < lenPF P.
+Proof. intros; rewrite lenPF_ind_r_in_S; easy. Qed.
+
 Lemma lenPF_ind_r_out :
   forall {n} {P : 'I_n.+1 -> Prop},
     ~ P ord_max -> lenPF P = lenPF (fun i => P (widen_S i)).
@@ -2579,21 +2637,27 @@ Lemma filterP_ord_ind_r_in_max :
   forall {n} {P : 'I_n.+1 -> Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
     cast_ord (lenPF_ind_r_in_S HP) j = ord_max -> filterP_ord j = ord_max.
 Proof.
-move=> n P HP j /cast_ord_max Hj;
-    unfold filterP_ord, enum_val, enum_mem, mem; simpl.
-rewrite -enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
-    case_eq (asbool (P ord_max)); intros HP'.
-2: move: HP' => /(elimF (asboolP _)) //.
-rewrite nth_rcons_r// Hj;
-    unfold lenPF; rewrite cardE; unfold enum_mem, mem; simpl.
-rewrite filter_map size_map; unfold widen_S; do 2 f_equal.
-rewrite filter_predT; easy.
+intros n P HP j Hj; apply ord_max_equiv_ge.
+pose (f := filterP_ord \o cast_ord (sym_eq (lenPF_ind_r_in_S HP))).
+replace (filterP_ord _) with (f ord_max);
+    [| unfold f; rewrite -Hj comp_correct cast_ordK; easy].
+apply (incrF_cast_ord_max (lenPF_ind_r_in_S HP) filterP_ord ord_max);
+    [apply filterP_ord_incrF | rewrite filterP_ord_Rg_eq; easy].
 Qed.
 
 Lemma filterP_ord_ind_r_in_max_rev :
   forall {n} {P : 'I_n.+1 -> Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
     filterP_ord j = ord_max -> cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
 Proof.
+(*
+intros n P HP j Hj.
+destruct (ord_eq_dec (cast_ord (lenPF_ind_r_in_S HP) j) ord_max)
+    as [-> | Hj']; [easy | exfalso; move: Hj'].
+move=> /ord_neq_compat /=.
+move=> /cast_ord_nmax_equiv_lt. /filterP_ord_incrF.
+rewrite Hj; easy.
+*)
+
 intros n P HP j; rewrite cast_ord_max.
 unfold filterP_ord, enum_val, enum_mem, mem; simpl.
 rewrite -enumT enum_ordSr filter_rcons; simpl; unfold in_mem; simpl;
-- 
GitLab