From d0dd1031968c6565bdf7fbfc32fe335f8e0f9239 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 20 Feb 2024 09:33:57 +0100
Subject: [PATCH] logic_compl: Add alias classic_dec for
 excluded_middle_informative.

Finite_family, Finite_table, Monoid_compl, Ring_compl, AffineSpace,
  Sub_struct, Finite_dim, multi_index, FE:
Propagate new API (from logic_compl).
---
 FEM/Algebra/AffineSpace.v   |  8 ++-----
 FEM/Algebra/Finite_dim.v    | 45 +++++++++++++++++++++----------------
 FEM/Algebra/Finite_family.v | 19 ++++++----------
 FEM/Algebra/Finite_table.v  |  4 ++--
 FEM/Algebra/Monoid_compl.v  |  2 +-
 FEM/Algebra/Ring_compl.v    | 12 ++++------
 FEM/Algebra/Sub_struct.v    |  8 +++----
 FEM/Compl/Compl.v           |  1 +
 FEM/Compl/logic_compl.v     | 10 ++++++---
 FEM/FE.v                    |  4 ++--
 FEM/multi_index.v           |  6 ++---
 11 files changed, 59 insertions(+), 60 deletions(-)

diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index 9f919335..e97a0301 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -202,10 +202,9 @@ Context {E : AffineSpace V}.
 Lemma transl_EX :
   { f | forall (A : E), cancel (vect A) (f A) /\ cancel (f A) (vect A) }.
 Proof.
-apply constructive_indefinite_description.
 assert (H : forall (A : E), exists f, cancel (vect A) f /\ cancel f (vect A)).
   intros A; destruct (vect_l_bij A) as [f Hf1 Hf2]; exists f; easy.
-destruct (choice _ H) as [f Hf]; exists f; easy.
+apply ex_EX; destruct (choice _ H) as [f Hf]; exists f; easy.
 Qed.
 
 Definition transl : E -> V -> E := proj1_sig transl_EX.
@@ -1208,10 +1207,7 @@ Qed.
 
 Lemma barycenter_EX :
   forall {n L} (A : 'E^n), invertible (sum L) -> { G | is_comb_aff L A G }.
-Proof.
-intros; apply constructive_indefinite_description.
-apply is_comb_aff_ex; easy.
-Qed.
+Proof. intros; apply ex_EX, is_comb_aff_ex; easy. Qed.
 
 Definition barycenter {n} L (A : 'E^n) : E :=
   match invertible_dec (sum L) with
diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index 7b8d033b..25b6843c 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -1,3 +1,19 @@
+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
 From Coq Require Import ClassicalEpsilon.
 From Coq Require Import ssreflect ssrfun ssrbool.
 
@@ -73,10 +89,7 @@ Inductive span {n} (B : 'E^n) : E -> Prop :=
 
 Lemma span_EX :
   forall {n} (B : 'E^n) x, span B x -> { L | x = comb_lin L B }.
-Proof.
-move=>> Hx; apply constructive_indefinite_description.
-induction Hx as [L]; exists L; easy.
-Qed.
+Proof. move=>> Hx; apply ex_EX; induction Hx as [L]; exists L; easy. Qed.
 
 Lemma span_ex :
   forall {n} (B : 'E^n) x, (exists L, x = comb_lin L B) -> span B x.
@@ -138,10 +151,7 @@ Inductive has_dim (PE : E -> Prop) n : Prop :=
 
 Lemma has_dim_EX :
   forall (PE : E -> Prop) n, has_dim PE n -> { B : 'E^n | is_basis PE B }.
-Proof.
-move=>> H; apply constructive_indefinite_description.
-induction H as [B]; exists B; easy.
-Qed.
+Proof. move=>> H; apply ex_EX; induction H as [B]; exists B; easy. Qed.
 
 Lemma has_dim_ex:
   forall (PE : E -> Prop) n,
@@ -2870,7 +2880,7 @@ Variable B : 'E^n.
 Hypothesis HB : is_basis PE B.
 
 Definition dual_basis : '(E -> R)^n := fun i x =>
-  match (excluded_middle_informative (PE x)) with
+  match (classic_dec (PE x)) with
   | left Hx (* in PE *) =>
       let (L, _) :=
         span_EX _ _ (eq_ind_r (@^~ x) Hx (eq_sym (proj1 HB))) in
@@ -2880,7 +2890,7 @@ Definition dual_basis : '(E -> R)^n := fun i x =>
 
 (*
 Definition dual_basis : '(E -> R)^n := fun i x =>
-   match (excluded_middle_informative (PE x)) with
+   match (classic_dec (PE x)) with
      | left Hx => let (L,_) :=
              (span_EX _ _ (proj1 (proj1 HB x) Hx)) in
                  L i
@@ -2891,7 +2901,7 @@ Definition dual_basis : '(E -> R)^n := fun i x =>
 Proof.
 intros i x.
 destruct HB as [HB1 HB2].
-destruct (excluded_middle_informative (PE x)) as [Hx | Hx].
+destruct (classic_dec (PE x)) as [Hx | Hx].
 2: apply 0. (*not in PE *)
 specialize (proj1 (HB1 x) Hx); intros H1.
 destruct (span_EX _ _ H1) as [L HL].
@@ -2911,7 +2921,7 @@ Proof.
 destruct HB as [HB1 HB2].
 intros x L H k.
 unfold dual_basis.
-destruct (excluded_middle_informative _) as [Hx | Hx].
+destruct (classic_dec _) as [Hx | Hx].
 destruct (span_EX _ _ _) as [L' HL'].
 assert (T:L=L'); [idtac| rewrite T; easy].
 apply (is_free_uniq_decomp HB2); try easy.
@@ -2926,7 +2936,7 @@ Lemma dual_basis_out : forall x, ~ PE x ->
 Proof.
 intros x H k.
 unfold dual_basis.
-destruct (excluded_middle_informative _) as [Hx | Hx]; easy.
+destruct (classic_dec _) as [Hx | Hx]; easy.
 Qed.
 
 Lemma dual_basis_is_linear_mapping :
@@ -3110,8 +3120,8 @@ Lemma aff_span_EX :
   forall {n} (A : 'E^n) G,
     aff_span A G -> { L | sum L = 1 /\ G = barycenter L A }.
 Proof.
-move=>> Hx; apply constructive_indefinite_description.
-induction Hx as [L HL]; eexists; apply (barycenter_normalized _ _ _ HL); easy.
+move=>> Hx; apply ex_EX; induction Hx as [L HL];
+    eexists; apply (barycenter_normalized _ _ _ HL); easy.
 Qed.
 
 Lemma aff_span_ex :
@@ -3170,10 +3180,7 @@ Inductive has_aff_dim (PE : E -> Prop) n : Prop :=
 
 Lemma has_aff_dim_EX :
   forall (PE : E -> Prop) n, has_aff_dim PE n -> { A : 'E^n.+1 | is_aff_basis PE A }.
-Proof.
-move=>> H; apply constructive_indefinite_description.
-induction H as [A]; exists A; easy.
-Qed.
+Proof. move=>> H; apply ex_EX; induction H as [A]; exists A; easy. Qed.
 
 Lemma has_aff_dim_ex:
   forall (PE : E -> Prop) n,
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index caf258e4..729849f0 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -55,9 +55,9 @@ Section FF_Def1a.
 Context {n : nat}.
 Variable P : 'Prop^n.
 
-Lemma PF_dec : {PAF P} + {PEF (notF P)}.
+Lemma PF_dec : { PAF P } + { PEF (notF P) }.
 Proof.
-destruct (excluded_middle_informative (PAF P));
+destruct (classic_dec (PAF P));
     [left | right; apply not_all_ex_not_equiv]; easy.
 Qed.
 
@@ -373,7 +373,7 @@ Definition unfunF {n1 n2} (f : 'I_{n1,n2}) (A1 : 'E^n1) (x0 : E) : 'E^n2 :=
     end.
 
 Definition maskPF {n} (P : 'Prop^n) (A : 'E^n) (x0 : E) : 'E^n :=
-  fun i => match (excluded_middle_informative (P i)) with
+  fun i => match (classic_dec (P i)) with
     | left _ => A i
     | right _ => x0
     end.
@@ -644,15 +644,11 @@ Qed.
 
 Lemma maskPF_correct_l :
   forall {n} {P : 'Prop^n} {A : 'E^n} x0 i, P i -> maskPF P A x0 i = A i.
-Proof.
-intros; unfold maskPF; destruct (excluded_middle_informative _); easy.
-Qed.
+Proof. intros; unfold maskPF; destruct (classic_dec _); easy. Qed.
 
 Lemma maskPF_correct_r :
   forall {n} {P : 'Prop^n} (A : 'E^n) {x0} i, ~ P i -> maskPF P A x0 i = x0.
-Proof.
-intros; unfold maskPF; destruct (excluded_middle_informative _); easy.
-Qed.
+Proof. intros; unfold maskPF; destruct (classic_dec _); easy. Qed.
 
 Lemma funF_unfunF :
   forall {n1 n2} {f : 'I_{n1,n2}} (x0 : E),
@@ -1509,8 +1505,7 @@ Lemma injF_extend_bij_EX :
   forall {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
     { p2 | bijective p2 /\ forall i1, f i1 = widenF (injF_leq Hf) p2 i1 }.
 Proof.
-intros n1 n2 f Hf; apply constructive_indefinite_description;
-    induction n1 as [|n1 Hn1].
+intros n1 n2 f Hf; apply ex_EX; induction n1 as [|n1 Hn1].
 exists id; repeat split; [apply bij_id | now intros [i Hi]].
 pose (f' := fun i1 => f (widen_S i1)).
 assert (Hf' : injective f') by now move=> i1 j1 /Hf /widen_ord_inj.
@@ -5033,7 +5028,7 @@ Lemma filter_neqF_gen_unfunF :
         (filter_neqF_gen (permutF q1 A1) x0 (permutF q1 B1))).
 Proof.
 intros F n1 n2 f Hf A1 x0 B1 y0 q1 Hq1a Hq1b.
-destruct (excluded_middle_informative (forall i1, A1 i1 = x0)) as [HA1 | HA1].
+destruct (classic_dec (forall i1, A1 i1 = x0)) as [HA1 | HA1].
 apply eqAF_nil; left; apply lenPF0_alt; intuition.
 move: HA1 => /not_all_ex_not_equiv [i0 Hi0].
 move: (extendPF_unfunF_neqF A1 x0 Hf) => HP.
diff --git a/FEM/Algebra/Finite_table.v b/FEM/Algebra/Finite_table.v
index 0b018917..5e307028 100644
--- a/FEM/Algebra/Finite_table.v
+++ b/FEM/Algebra/Finite_table.v
@@ -46,8 +46,8 @@ Variable M N : 'E^{m,n}.
 Definition brT : Prop := forall i j, R (M i j) (N i j).
 Definition nbrT : Prop := exists i j, ~ R (M i j) (N i j).
 
-Lemma brT_dec : {brT} + {~ brT}.
-Proof. apply excluded_middle_informative. Qed.
+Lemma brT_dec : { brT } + { ~ brT }.
+Proof. apply classic_dec. Qed.
 
 End FT_Def0.
 
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index 4ba06af1..227e82b0 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -53,7 +53,7 @@ Proof. intros; apply iff_sym, not_all_ex_not_equiv. Qed.
 
 Lemma zero_struct_dec : forall G, { zero_struct G } + { nonzero_struct G }.
 Proof.
-intros; destruct (excluded_middle_informative (zero_struct G));
+intros; destruct (classic_dec (zero_struct G));
     [left | right; apply nonzero_not_zero_struct_equiv]; easy.
 Qed.
 
diff --git a/FEM/Algebra/Ring_compl.v b/FEM/Algebra/Ring_compl.v
index 2339d01c..36b6085b 100644
--- a/FEM/Algebra/Ring_compl.v
+++ b/FEM/Algebra/Ring_compl.v
@@ -85,13 +85,10 @@ Lemma invertible_ex : forall {x}, (exists y, is_inverse x y) -> invertible x.
 Proof. intros x [y Hy]; apply (Invertible _ _ Hy). Qed.
 
 Lemma invertible_EX : forall {x}, invertible x -> { y | is_inverse x y }.
-Proof.
-move=>> Hx; apply constructive_indefinite_description.
-destruct Hx as [y Hy]; exists y; easy.
-Defined.
+Proof. move=>> Hx; apply ex_EX; destruct Hx as [y Hy]; exists y; easy. Defined.
 
 Lemma invertible_dec : forall x, { invertible x } + { ~ invertible x }.
-Proof. intros; apply excluded_middle_informative. Qed.
+Proof. intros; apply classic_dec. Qed.
 
 Definition inv (x : K) : K :=
   match invertible_dec x with
@@ -718,9 +715,8 @@ Proof.
 intros; pose (P n := n <> 0%nat /\ plusn1 K n = 0).
 destruct (LPO P (fun=> classic _)) as [[N HN] | H]; [left | right].
 (* *)
-apply constructive_indefinite_description.
-destruct (dec_inh_nat_subset_has_unique_least_element P) as [n [[Hn1 Hn2] _]];
-    [intros; apply classic | exists N; easy | ].
+apply ex_EX; destruct (dec_inh_nat_subset_has_unique_least_element P)
+    as [n [[Hn1 Hn2] _]]; [intros; apply classic | exists N; easy |].
 exists n; repeat split; try apply Hn1.
 intros p Hp0; rewrite contra_not_r_equiv Nat.nlt_ge; intros Hp1.
 apply Hn2; easy.
diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index 284e51e4..2a3abcda 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -2880,8 +2880,8 @@ Lemma bc_len_EX :
         sum L = 1 /\ (forall i, L i <> 0) /\
         inclF B gen /\ A = barycenter L B }.
 Proof.
-intros gen A; apply constructive_indefinite_description.
-destruct (excluded_middle_informative (barycenter_closure gen A)) as [HA | HA].
+intros gen A; apply ex_EX.
+destruct (classic_dec (barycenter_closure gen A)) as [HA | HA].
 destruct (barycenter_closure_ex_rev _ _ HA) as [n [L [B HLB]]].
 exists n; intros _; exists L, B; easy.
 exists 0; intros HA'; easy.
@@ -2896,8 +2896,8 @@ Lemma bc_EX :
       sum LB.1 = 1 /\ (forall i, LB.1 i <> 0) /\
       inclF LB.2 gen /\ A = barycenter LB.1 LB.2 }.
 Proof.
-intros gen A; apply constructive_indefinite_description.
-destruct (excluded_middle_informative (barycenter_closure gen A)) as [HA | HA].
+intros gen A; apply ex_EX.
+destruct (classic_dec (barycenter_closure gen A)) as [HA | HA].
 destruct (proj2_sig (bc_len_EX gen A)) as [L [B HLB]]; try easy.
 exists (L, B); intros _; easy.
 destruct (inhabited_as E) as [O].
diff --git a/FEM/Compl/Compl.v b/FEM/Compl/Compl.v
index 9fac6b03..af0e99b3 100644
--- a/FEM/Compl/Compl.v
+++ b/FEM/Compl/Compl.v
@@ -22,6 +22,7 @@ COPYING file for more details.
 
   Provides 'propositional_extensionality' as 'prop_ext',
            'proof_irrelevance' as 'proof_irrel',
+           'excluded_middle_informative' as 'classic_dec',
            'constructive_indefinite_description' as 'ex_EX'.
  *)
 
diff --git a/FEM/Compl/logic_compl.v b/FEM/Compl/logic_compl.v
index b926fef8..6152c1df 100644
--- a/FEM/Compl/logic_compl.v
+++ b/FEM/Compl/logic_compl.v
@@ -14,9 +14,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(* We need propositional extensionality, classical logic, and a constructive
- form of indefinite description. *)
-From Coq Require Import PropExtensionality Classical IndefiniteDescription.
+(* We need propositional extensionality, classical logic, excluded-middle in Set,
+ and a constructive form of indefinite description. *)
+From Coq Require Import PropExtensionality ClassicalDescription IndefiniteDescription.
 
 
 (** Additional definitions and results about classical logic.
@@ -26,6 +26,7 @@ From Coq Require Import PropExtensionality Classical IndefiniteDescription.
 
   'prop_ext' is an alias for 'propositional_extensionality'.
   'proof_irrel' is an alias for 'proof_irrelevance'.
+  'classic_dec' is an alias for 'excluded_middle_informative'.
 
   Provide equivalence results to enable the use of the rewrite tactic.
   All names use the "_equiv" prefix. These are for:
@@ -65,6 +66,9 @@ Proof. exact propositional_extensionality. Qed.
 Lemma proof_irrel : forall (H : Prop) (P Q : H), P = Q.
 Proof. exact proof_irrelevance. Qed.
 
+Lemma classic_dec : forall (P : Prop), { P } + { ~ P }.
+Proof. exact excluded_middle_informative. Qed.
+
 End Classical_propositional_Facts1.
 
 
diff --git a/FEM/FE.v b/FEM/FE.v
index e098da06..b9114960 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -218,7 +218,7 @@ Proof.
 generalize (choice (fun (j : 'I_(ndof fe)) p => (P_approx fe p) 
   /\ (forall i : 'I_(ndof fe), (Sigma fe) i p = kronecker i j))).
 intros T.
-apply constructive_indefinite_description in T.
+apply ex_EX in T.
 (* *)
 destruct T as [x Hx].
 apply x.
@@ -236,7 +236,7 @@ Defined.
 Lemma shape_fun_correct : is_local_shape_fun shape_fun.
 Proof.
 unfold shape_fun.
-destruct (constructive_indefinite_description _) as [x Hx].
+destruct (ex_EX _) as [x Hx].
 split; try apply Hx.
 intros; apply Hx.
 Qed.
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index 7c51115f..dcc86ca2 100644
--- a/FEM/multi_index.v
+++ b/FEM/multi_index.v
@@ -856,7 +856,7 @@ Qed.
 Definition A_d_k_inv (d k:nat) (b:'nat^d) : 'I_((pbinom d k).+1) :=
    match (le_dec (sum b) k) with
      | left H => 
-        proj1_sig (constructive_indefinite_description _ (A_d_k_surj d k b H))
+        proj1_sig (ex_EX _ (A_d_k_surj d k b H))
      | right _ => ord0
    end.
 
@@ -867,7 +867,7 @@ Proof.
 intros d k b H; unfold A_d_k_inv.
 case (le_dec (sum b) k); try easy.
 intros H'.
-destruct (constructive_indefinite_description _ _) as (i,Hi); easy.
+destruct (ex_EX _ _) as (i,Hi); easy.
 Qed.
 
 Lemma A_d_k_inv_correct_l : forall d k i, 
@@ -875,7 +875,7 @@ Lemma A_d_k_inv_correct_l : forall d k i,
 Proof.
 intros d k i; unfold A_d_k_inv.
 case (le_dec _ k); intros H; simpl.
-destruct (constructive_indefinite_description _ _) as (j,Hj); try easy.
+destruct (ex_EX _ _) as (j,Hj); try easy.
 simpl; apply A_d_k_inj; easy.
 contradict H; apply A_d_k_sum.
 Qed.
-- 
GitLab