From 58d807bbfa5d952d48c3e7dda70f47bdcef19a7e 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 11:41:14 +0100
Subject: [PATCH] nat_compl: Compact some proofs. Add todo about naming.

ord_compl:
More stable version of insert_concat_r_ord_0.

Finite_family:
Propagate new API (from ord_compl).
---
 FEM/Algebra/Finite_family.v |  6 ++++--
 FEM/Algebra/nat_compl.v     | 30 +++++++++++++-----------------
 FEM/Algebra/ord_compl.v     |  6 ++++--
 3 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 2f90603e..60c78495 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -2837,8 +2837,10 @@ Proof.
 intros; unfold castF_1pS; rewrite castF_refl.
 apply extF; intros i; destruct (ord_eq_dec i ord0) as [Hi | Hi].
 rewrite Hi insertF_correct_l// concatF_correct_l; easy.
-assert (Hi' : ~ (i < 1)%coq_nat) by now apply ord_n0_equiv_alt.
-rewrite insertF_correct_r insert_concat_r_ord_0 concatF_correct_r; easy.
+assert (Hi' : ~ (cast_ord (sym_eq (add1n n)) i < 1)%coq_nat)
+    by now rewrite cast_ord_id; apply ord_n0_equiv_alt.
+rewrite insertF_correct_r insert_concat_r_ord_0 concatF_correct_r.
+f_equal; apply ord_inj; easy.
 Qed.
 
 Lemma insertF_concatF_max :
diff --git a/FEM/Algebra/nat_compl.v b/FEM/Algebra/nat_compl.v
index 15f5b7c3..3a800578 100644
--- a/FEM/Algebra/nat_compl.v
+++ b/FEM/Algebra/nat_compl.v
@@ -10,6 +10,8 @@ From Lebesgue Require Import nat_compl Subset_dec logic_compl.
 From FEM Require Import logic_compl.
 
 
+(* TODO FC (05/02/2024): maybe drop the nat_ prefix, or put it everywhere... *)
+
 Section nat_compl.
 
 Lemma nat_plus_0_l : forall {n1 n2}, n1 = 0 -> n1 + n2 = n2.
@@ -71,7 +73,7 @@ Lemma nat2_ind_11 :
     (forall m n, m <> 0 -> n <> 0 -> P m n -> P m n.+1) ->
     forall m n, m <> 0 -> n <> 0 -> P m n.
 Proof.
-intros P Hm1 H1n H m n; destruct m, n; try easy; intros _ _.
+intros P Hm1 H1n H m n; destruct m, n; [easy.. |]; intros _ _.
 apply (nat2_ind (fun m n => P m.+1 n.+1)); auto.
 Qed.
 
@@ -81,8 +83,7 @@ Lemma nat2_ind_alt_1l :
     (forall m n, m <> 0 -> P m.+1 n -> P m n.+1 -> P m.+1 n.+1) ->
     forall m n, m <> 0 -> P m n.
 Proof.
-intros P Hm0 H1n H m; destruct m; try easy; induction m; try easy.
-induction n; auto.
+intros P Hm0 H1n H m; destruct m; try easy; induction m; [| induction n]; auto.
 Qed.
 
 Lemma nat2_ind_alt_1r :
@@ -91,8 +92,8 @@ Lemma nat2_ind_alt_1r :
     (forall m n, n <> 0 -> P m.+1 n -> P m n.+1 -> P m.+1 n.+1) ->
     forall m n, n <> 0 -> P m n.
 Proof.
-intros P Hm1 H0n H; induction m; try easy.
-intros n; destruct n; try easy; induction n; auto.
+intros P Hm1 H0n H; induction m;
+    [| intros n; destruct n; [easy.. | induction n]]; auto.
 Qed.
 
 Lemma nat2_ind_alt_00 :
@@ -103,12 +104,8 @@ Lemma nat2_ind_alt_00 :
 Proof.
 (*intros P Hm0 H0n H; induction m; induction n; intros [H0 | H0]; auto.*)
 intros P Hm0 H0n H m n [H0 | H0].
-(* *)
-apply nat2_ind_alt_1l; auto.
-intros n'; induction n'; auto.
-(* *)
-apply nat2_ind_alt_1r; auto.
-intros m'; induction m'; auto.
+apply nat2_ind_alt_1l; auto; intros n'; induction n'; auto.
+apply nat2_ind_alt_1r; auto; intros m'; induction m'; auto.
 Qed.
 
 Lemma nat2_ind_alt :
@@ -117,8 +114,7 @@ Lemma nat2_ind_alt :
     (forall m n, P m.+1 n -> P m n.+1 -> P m.+1 n.+1) ->
     forall m n, P m n.
 Proof. (*intros P Hm0 H0n H; induction m; induction n; auto.*)
-intros P Hm0 H0n H m n; destruct m, n; try easy.
-apply nat2_ind_alt_00; auto.
+intros P Hm0 H0n H m n; destruct m, n; [.. | apply nat2_ind_alt_00]; auto.
 Qed.
 
 Lemma nat2_ind_alt_11 :
@@ -128,7 +124,7 @@ Lemma nat2_ind_alt_11 :
       P m.+1 n -> P m n.+1 -> P m.+1 n.+1) ->
     forall m n, (0 < m)%coq_nat -> (0 < n)%coq_nat -> P m n.
 Proof.
-intros P Hm1 H1n H m n; destruct m, n; try easy; intros _ _.
+intros P Hm1 H1n H m n; destruct m, n; [easy.. | intros _ _].
 apply (nat2_ind_alt (fun m n => P m.+1 n.+1)); clear m n.
 intros m; apply Hm1, Nat.neq_0_lt_0; easy.
 intros n; apply H1n, Nat.neq_0_lt_0; easy.
@@ -144,9 +140,9 @@ Proof.
 intros P HP; apply (strong_induction (fun m => forall n, P m n)); intros m Hm.
 apply strong_induction; intros n Hn.
 apply HP; move=> m1 n1 /Nat.le_lteq Hm1 /Nat.le_lteq Hn1 H1.
-destruct Hm1; subst; try now apply Hm.
-destruct Hn1; subst; try now apply Hn.
-lia.
+destruct Hm1; subst; [apply Hm; easy |].
+destruct Hn1; subst; [apply Hn; easy |].
+contradict H1; apply Nat.lt_irrefl.
 Qed.
 
 Lemma nat_le_total : forall m n, (m <= n)%coq_nat \/ (n <= m)%coq_nat.
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 00430625..7e2aeb94 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -1481,9 +1481,11 @@ Lemma insert_ord_max :
   forall {n} {i0 : 'I_n.+2} (Hi0 : ord_max <> i0), insert_ord Hi0 = ord_max.
 Proof. intros; apply sym_eq, skip_insert_ord_eq, skip_ord_max; intuition. Qed.
 
-(* Note that 1 + n is actually n.+1. *)
+(* Note that 1 + n is actually n.+1 and we could avoid using cast_ord.
+ But this could change in the future, in the next form is more stable. *)
 Lemma insert_concat_r_ord_0 :
-  forall {n} {i : 'I_(1 + n)} (Hi1 : i <> ord0) (Hi2 : ~ (i < 1)%coq_nat),
+  forall {n} {i : 'I_n.+1}
+      (Hi1 : i <> ord0) (Hi2 : ~ (cast_ord (sym_eq (add1n n)) i < 1)%coq_nat),
     insert_ord Hi1 = concat_r_ord Hi2.
 Proof.
 intros n i Hi1 Hi2; rewrite insert_ord_correct_r.
-- 
GitLab