anticipate compatibility with mathcomp 1.9.0 and 1.10.0

information_theory/jtypes.v

@@ -6,6 +6,21 @@ Require Import Reals.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop fdist entropy.
 Require Import num_occ channel types.
 
+(******************************************************************************)
+(*                            Joint Types                                     *)
+(*                                                                            *)
+(* Definitions:                                                               *)
+(*   jtype == type of joint type, notation: P_n(A, B)                         *)
+(*   shell = shell, notation: V.-shell t                                      *)
+(*   cond_type == conditional type, notation: \nu{V}(P)                       *)
+(*                                                                            *)
+(* Lemmas:                                                                    *)
+(*   bound_card_jtype == upper-bound of the number of conditional types       *)
+(*    jtype_not_empty == joint types are not empty                            *)
+(*         occ_co_occ == Relation between the number of symbol occurrences    *)
+(*                       and the number of pairs of symbols occurrences       *)
+(******************************************************************************)
+
 Reserved Notation "'P_' n '(' A ',' B ')'" (at level 9,
   n at next level, A at next level, B at next level).
 Reserved Notation "V '.-shell' ta" (at level 5,
@@ -31,8 +46,6 @@ Variables A B : finType.
 Variable n : nat.
 Local Open Scope nat_scope.
 
-(** * Joint Types *)
-
 Record jtype : predArgType := mkJtype {
   c :> `Ch*(A, B) ;
   f : {ffun A -> {ffun B -> 'I_n.+1}} ;
@@ -315,8 +328,6 @@ exfalso.
 by apply/eqP : abs; apply/invR_neq0'; rewrite INR_eq0' H'.
 Qed.
 
-(** Upper-bound of the number of conditional types: *)
-
 Lemma bound_card_jtype : #| P_ n (A , B) | <= expn n.+1 (#|A| * #|B|).
 Proof.
 rewrite -(card_ord n.+1) mulnC expnM -2!card_ffun cardE /enum_mem.
@@ -336,8 +347,6 @@ apply/mapP.
 by exists f.
 Qed.
 
-(** As defined, channels are never empty: *)
-
 Lemma jtype_not_empty : 0 < #|A| -> 0 < #|B| -> 0 < #|P_ n (A , B)|.
 Proof.
 move=> Anot0 Bnot0.
@@ -373,8 +382,6 @@ Variable V : P_ n (A , B).
 
 Local Open Scope nat_scope.
 
-(** * Shells *)
-
 Definition shell :=
   [set tb : n.-tuple B | [forall a, [forall b, N(a, b |ta, tb) == (jtype.f V) a b]]].
 
@@ -392,8 +399,6 @@ Variable ta : n.-tuple A.
 Variable tb : n.-tuple B.
 Hypothesis Htb : tb \in V.-shell ta.
 
-(** Relation between the number of symbol occurrences and the number of pairs of symbols occurences (original lemma: N(a, b|ta, tb) = N(a | ta) V(b | a)) *)
-
 Lemma occ_co_occ : forall a b, N(a, b| ta, tb) = (jtype.f V) a b.
 Proof.
 move: Htb => Htb' x0 y0 ; rewrite /shell inE in Htb'.
@@ -600,8 +605,7 @@ Definition take_shell (k : nat) : {set (sum_num_occ ta k).-tuple B} :=
      tcast (minn_sum_num_occ_n ta k) [tuple of take (sum_num_occ ta k) b])
   @: (V.-shell ta).
 
-(** Same set modulo cast: *)
-
+(* Same set modulo cast: *)
 Lemma full_take_shell : #| take_shell #|A| | = #| V.-shell ta |.
 Proof.
 apply card_imset; rewrite /injective => /= v v' vv'.
@@ -745,10 +749,11 @@ eapply leq_trans; first by apply (subset_leq_card_split_tuple (card_take_shell_i
 by rewrite cardsX cards1 muln1.
 Qed.
 
-Definition card_type_of_row (i : 'I_#|A|) := match eqVneq N(enum_val i | ta) 0 with
-| left _ => 1
-| right Ha => #| T_{type_of_row Ha} |
-end.
+Definition card_type_of_row (i : 'I_#|A|) :=
+  match Bool.bool_dec (N(enum_val i | ta) == O) true with
+  | left _ => 1
+  | right Ha => #| T_{type_of_row (Bool.eq_true_not_negb _ Ha)} |
+  end.
 
 Lemma split_nocc_rec : forall k, k <= #|A| ->
   #|take_shell ta V k| <= \prod_ (i < #|A| | i < k) card_type_of_row i.
@@ -767,15 +772,14 @@ elim.
       by rewrite andbC /= ltnW.
     - rewrite andbC -ltn_neqAle.
       by move/negbTE : Hcase => ->.
-  rewrite /card_type_of_row; destruct eqVneq.
+  rewrite /card_type_of_row; case: Bool.bool_dec => [e|/Bool.eq_true_not_negb e].
     rewrite mul1n.
-    move/eqP in e.
     eapply leq_trans; [exact: (card_take_shell0 e) | by []].
-  apply (leq_trans (card_take_shell i)).
+  apply (leq_trans (card_take_shell e)).
   rewrite mulnC leq_pmul2l //.
   apply/card_gt0P.
-  set Q := type_of_row i.
-  case: (typed_tuples_not_empty_alt i Q) => tb Htb.
+  set Q := type_of_row e.
+  case: (typed_tuples_not_empty_alt e Q) => tb Htb.
   by exists tb.
 Qed.
 
@@ -820,7 +824,7 @@ apply (@leR_trans (\prod_ ( i < #|A|) card_type_of_row Hta Vctyp i)%:R).
   apply ler_rprod => a.
   split; first exact/leR0n.
   rewrite -exp2_pow mulRA.
-  rewrite /card_type_of_row; destruct eqVneq.
+  rewrite /card_type_of_row; case: Bool.bool_dec => [e|/Bool.eq_true_not_negb e].
     rewrite -[X in X <= _]exp2_0.
     apply Exp_le_increasing, mulR_ge0 => //.
       apply mulR_ge0 => //; exact: leR0n.
@@ -833,7 +837,7 @@ apply (@leR_trans (\prod_ ( i < #|A|) card_type_of_row Hta Vctyp i)%:R).
   + rewrite /entropy.
     apply Ropp_eq_compat, eq_bigr => b _.
     rewrite /pta0 (jtype.c_f V) /= (Vctyp Hta a) -{1 4}(enum_rankK a).
-    move/negbTE : (i) => ->; by rewrite !ffunE /= enum_rankK.
+    move/negbTE : (e) => ->; by rewrite !ffunE /= enum_rankK.
 Qed.
 
 End card_shell_ub.

probability/convex_choice.v

@@ -605,10 +605,10 @@ Fixpoint Convn n : {fdist 'I_n} -> ('I_n -> A) -> A :=
   match n return forall (e : {fdist 'I_n}) (g : 'I_n -> A), A with
   | O => fun e g => False_rect A (fdistI0_False e)
   | m.+1 => fun e g =>
-    match eqVneq (e ord0) 1%R with
+    match Bool.bool_dec (e ord0 == 1%R) true with
     | left _ => g ord0
     | right H => let G := fun i => g (DelFDist.f ord0 i) in
-      g ord0 <| probfdist e ord0 |> Convn (DelFDist.d H) G
+      g ord0 <| probfdist e ord0 |> Convn (DelFDist.d (Bool.eq_true_not_negb _ H)) G
     end
   end.
 
@@ -640,16 +640,15 @@ Proof.
 elim: n points d => [|n IH] points d.
   move: (FDist.f1 d); rewrite /= big_ord0 => /Rlt_not_eq; elim.
   exact: Rlt_0_1.
-rewrite /=.
-case: eqVneq => Hd.
-  rewrite (bigD1 ord0) ?inE // Hd big1 /=.
+rewrite /=; case: Bool.bool_dec => [/eqP|]Hd.
+  rewrite (bigD1 ord0) //= Hd big1 /=.
     rewrite addpt0 (scalept_gt0 _ _ Rlt_0_1).
     by congr Scaled; apply val_inj; rewrite /= mulR1.
   move=> i Hi; have := FDist.f1 d.
   rewrite (bigD1 ord0) ?inE // Hd /= addRC => /(f_equal (Rminus^~ R1)).
   rewrite addRK subRR => /prsumr_eq0P -> //.
   by rewrite scalept0.
-set d' := DelFDist.d Hd.
+set d' := DelFDist.d (Bool.eq_true_not_negb _ Hd).
 set points' := fun i => points (DelFDist.f ord0 i).
 rewrite /index_enum -enumT (bigD1_seq ord0) ?enum_uniq ?mem_enum //=.
 rewrite -big_filter (perm_big (map (lift ord0) (enum 'I_n)));
@@ -660,7 +659,7 @@ rewrite /barycenter 2!big_map [in RHS]big_map.
 apply eq_bigr => i _.
 rewrite scalept_comp // DelFDist.dE D1FDist.dE /=.
 rewrite /Rdiv (mulRC (d _)) mulRA mulRV ?mul1R //.
-by move: (Hd); apply contra => /eqP Hd'; rewrite -onem0 -Hd' onemK.
+by move: (Bool.eq_true_not_negb _ Hd); apply contra => /eqP Hd'; rewrite -onem0 -Hd' onemK.
 Qed.
 End with_affine_projection.
 
@@ -689,16 +688,16 @@ Proof. by apply convn_proj; rewrite FDist1.dE eqxx. Qed.
 
 Lemma convn1E g (e : {fdist 'I_1}) : \Conv_ e g = g ord0.
 Proof.
-rewrite /=; case: eqVneq => [//|H]; exfalso; move/eqP: H; apply.
+rewrite /=; case: Bool.bool_dec => // H; exfalso; move/eqP: (Bool.eq_true_not_negb _ H); apply.
 by apply/eqP; rewrite FDist1.dE1 (FDist1.I1 e).
 Qed.
 
 Lemma convnE n g (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%R) :
   \Conv_d g = g ord0 <| probfdist d ord0 |> \Conv_(DelFDist.d i1) (fun x => g (DelFDist.f ord0 x)).
 Proof.
-rewrite /=; case: eqVneq => /= H.
-exfalso; by rewrite H eqxx in i1.
-by rewrite (eq_irrelevance H i1).
+rewrite /=; case: Bool.bool_dec => /= H.
+exfalso; by rewrite (eqP H) eqxx in i1.
+by rewrite (eq_irrelevance (Bool.eq_true_not_negb _ H) i1).
 Qed.
 
 Lemma convn2E g (d : {fdist 'I_2}) :
@@ -843,16 +842,16 @@ exists 2, (fun i => if i == ord0 then a0 else a1), (I2FDist.d p); split => /=.
   move=> a2.
   case => i _ <-{a2} /=.
   case: ifPn => _; [by left | by right].
-case: eqVneq => [|H].
+case: Bool.bool_dec => [/eqP|H].
   rewrite I2FDist.dE eqxx /= => p1.
   suff -> : p = `Pr 1 by rewrite conv1.
   exact/prob_ext.
 congr (_ <| _ |> _); first by apply prob_ext => /=; rewrite I2FDist.dE eqxx.
-case: eqVneq => H' //.
+case: Bool.bool_dec => // H'.
 exfalso.
 move: H'; rewrite DelFDist.dE D1FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)).
 rewrite I2FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)) I2FDist.dE eqxx divRR ?eqxx //.
-by move: H; rewrite I2FDist.dE eqxx onem_neq0.
+by move: (Bool.eq_true_not_negb _ H); rewrite I2FDist.dE eqxx onem_neq0.
 Qed.
 End hull_prop.
 

probability/convex_stone.v

@@ -5,6 +5,12 @@ Require Import Reals Lra.
 Require Import ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb Rbigop.
 Require Import fdist convex_choice.
 
+(****************************************************************************)
+(* Direct formalization of the Lemma 2 from M. H. Stone. Postulates for the *)
+(* barycentric calculus. Ann. Mat. Pura Appl., 29(1):25–30, 1949. The files *)
+(* convex_{choice,type}.v contain a shorter proof.                          *)
+(****************************************************************************)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
@@ -429,26 +435,10 @@ Lemma distribute (x y z : A) (p q : prob) :
   x <| p |> (y <| q |> z) = (x <| p |> y) <| q |> (x <| p |> z).
 Proof. by rewrite -{1}(convmm x q) commute. Qed.
 
-(*Local Open Scope vec_ext_scope.
-
-Fixpoint Convn n : {dist 'I_n} -> ('I_n -> A) -> A :=
-  match n return forall (e : {dist 'I_n}) (g : 'I_n -> A), A with
-  | O => fun e g => False_rect A (distI0_False e)
-  | m.+1 => fun e g =>
-    match eqVneq (e ord0) 1%R with
-    | left _ => g ord0
-    | right H => let G := fun i => g (DelDist.h ord0 i) in
-      g ord0 <| probdist e ord0 |> Convn (DelDist.d H) G
-    end
-  end.
-
-Local Notation "'\Sum_' d f" := (Convn d f).
-*)
-
 Lemma ConvnFDist1 (n : nat) (j : 'I_n) (g : 'I_n -> A): \Conv_(FDist1.d j) g = g j.
 Proof.
 elim: n j g => [[] [] //|n IH j g /=].
-case: eqVneq => [|b01].
+case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01].
   rewrite FDist1.dE; case j0 : (_ == _) => /=.
   by move=> _; rewrite (eqP j0).
   rewrite (_ : (0%:R)%R = 0%R) //; lra.
@@ -475,15 +465,15 @@ Qed.
 
 Lemma convn1E a e : \Conv_ e (fun _ : 'I_1 => a) = a.
 Proof.
-rewrite /=; case: eqVneq => [//|H]; exfalso; move/eqP: H; apply.
+rewrite /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H; exfalso; move/eqP: H; apply.
 by apply/eqP; rewrite FDist1.dE1 (FDist1.I1 e).
 Qed.
 
 Lemma convnE n (g : 'I_n.+1 -> A) (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%R) :
   \Conv_d g = g ord0 <| probfdist d ord0 |> \Conv_(DelFDist.d i1) (fun x => g (DelFDist.f ord0 x)).
 Proof.
-rewrite /=; case: eqVneq => /= H.
-exfalso; by rewrite H eqxx in i1.
+rewrite /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H.
+exfalso; by rewrite (eqP H) eqxx in i1.
 by rewrite (boolp.Prop_irrelevance H i1).
 Qed.
 
@@ -1061,7 +1051,6 @@ by rewrite subR_eq0; apply/nesym/eqP.
 by rewrite boolp.funeqE => j; rewrite /= permE H permE.
 Qed.
 
-(* ref: M.H.Stone, postulates for the barycentric calculus, lemma 2*)
 Lemma Convn_perm (n : nat) (d : {fdist 'I_n}) (g : 'I_n -> A) (s : 'S_n) :
   \Conv_d g = \Conv_(PermFDist.d d s) (g \o s).
 Proof.
@@ -1100,14 +1089,14 @@ End convex_space_prop.
 Section R_convex_space.
 Lemma avgnE n (g : 'I_n -> R) e : \Conv_e g = avgn g e.
 elim: n g e => /= [g e|n IH g e]; first by move: (fdistI0_False e).
-case: eqVneq => H /=.
+case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb] H /=.
   rewrite /avgn big_ord_recl /= H mul1R big1 ?addR0 // => j _.
   by move/eqP/FDist1.P : H => ->; rewrite ?mul0R.
 rewrite /avgn big_ord_recl /=.
 rewrite /Conv /= /avg /=; congr (_ + _)%R.
 rewrite IH /avgn big_distrr /=; apply eq_bigr => j _.
 rewrite DelFDist.dE D1FDist.dE eq_sym (negbTE (neq_lift _ _)).
-by rewrite mulRAC mulRC -mulRA mulVR ?onem_neq0 // mulR1.
+rewrite mulRAC mulRC -mulRA mulVR ?mulR1 //; exact/onem_neq0.
 Qed.
 End R_convex_space.
 
@@ -1128,14 +1117,14 @@ Lemma convn_convnfdist (n : nat) (g : 'I_n -> fdist_convType A) (d : {fdist 'I_n
   \Conv_d g = ConvnFDist.d d g.
 Proof.
 elim: n g d => /= [g d|n IH g d]; first by move: (fdistI0_False d).
-case: eqVneq => H.
+case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb] H.
   apply/fdist_ext => a.
   rewrite ConvnFDist.dE big_ord_recl H mul1R big1 ?addR0 //= => j _.
   by move/eqP/FDist1.P : H => -> //; rewrite ?mul0R.
 apply/fdist_ext => a.
 rewrite ConvFDist.dE ConvnFDist.dE /= big_ord_recl; congr (_ + _)%R.
 rewrite IH ConvnFDist.dE big_distrr /=; apply eq_bigr => i _.
 rewrite DelFDist.dE D1FDist.dE eq_sym (negbTE (neq_lift _ _)).
-by rewrite /Rdiv mulRAC mulRC -mulRA mulVR ?onem_neq0 // mulR1.
+rewrite /Rdiv mulRAC mulRC -mulRA mulVR ?mulR1 //; exact/onem_neq0.
 Qed.
 End convn_convnfdist.

probability/convex_type.v

@@ -593,10 +593,10 @@ Fixpoint Convn n : {fdist 'I_n} -> ('I_n -> A) -> A :=
   match n return forall (e : {fdist 'I_n}) (g : 'I_n -> A), A with
   | O => fun e g => False_rect A (fdistI0_False e)
   | m.+1 => fun e g =>
-    match eqVneq (e ord0) 1%R with
+    match Bool.bool_dec (e ord0 == 1%R) true with
     | left _ => g ord0
     | right H => let G := fun i => g (DelFDist.f ord0 i) in
-      g ord0 <| probfdist e ord0 |> Convn (DelFDist.d H) G
+      g ord0 <| probfdist e ord0 |> Convn (DelFDist.d (Bool.eq_true_not_negb _ H)) G
     end
   end.
 
@@ -628,14 +628,14 @@ Proof.
 elim: n points d => [|n IH] points d.
   move: (FDist.f1 d); rewrite /= big_ord0 => /Rlt_not_eq; elim.
   exact: Rlt_0_1.
-rewrite /=.
-case: eqVneq => Hd.
-  rewrite (bigD1 ord0) ?inE // Hd big1 /=.
+rewrite /=; case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb]Hd.
+  rewrite (bigD1 ord0) //= Hd big1 /=.
     rewrite addpt0 (scalept_gt0 _ _ Rlt_0_1).
     by congr Scaled; apply val_inj; rewrite /= mulR1.
   move=> i Hi; have := FDist.f1 d.
   rewrite (bigD1 ord0) ?inE // Hd /= addRC => /(f_equal (Rminus^~ R1)).
-  by rewrite addRK subRR => /prsumr_eq0P -> //; rewrite scalept0.
+  rewrite addRK subRR => /prsumr_eq0P -> //.
+  by rewrite scalept0.
 set d' := DelFDist.d Hd.
 set points' := fun i => points (DelFDist.f ord0 i).
 rewrite /index_enum -enumT (bigD1_seq ord0) ?enum_uniq ?mem_enum //=.
@@ -677,15 +677,15 @@ Proof. by apply convn_proj; rewrite FDist1.dE eqxx. Qed.
 
 Lemma convn1E g (e : {fdist 'I_1}) : \Conv_ e g = g ord0.
 Proof.
-rewrite /=; case: eqVneq => [//|H]; exfalso; move/eqP: H; apply.
+rewrite /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H; exfalso; move/eqP: H; apply.
 by apply/eqP; rewrite FDist1.dE1 (FDist1.I1 e).
 Qed.
 
 Lemma convnE n g (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%R) :
   \Conv_d g = g ord0 <| probfdist d ord0 |> \Conv_(DelFDist.d i1) (fun x => g (DelFDist.f ord0 x)).
 Proof.
-rewrite /=; case: eqVneq => /= H.
-exfalso; by rewrite H eqxx in i1.
+rewrite /=; case: Bool.bool_dec => /= [H|/Bool.eq_true_not_negb H].
+exfalso; by rewrite (eqP H) eqxx in i1.
 by rewrite (eq_irrelevance H i1).
 Qed.
 
@@ -833,16 +833,15 @@ exists 2, (fun i => if i == ord0 then a0 else a1), (I2FDist.d p); split => /=.
   move=> a2.
   case => i _ <-{a2} /=.
   case: ifPn => _; [by left | by right].
-case: eqVneq => [|H].
+case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb H].
   rewrite I2FDist.dE eqxx /= => p1.
   suff -> : p = `Pr 1 by rewrite conv1.
   exact/prob_ext.
 congr (_ <| _ |> _); first by apply prob_ext => /=; rewrite I2FDist.dE eqxx.
-case: eqVneq => H' //.
+case: Bool.bool_dec => // H'.
 exfalso.
-move: H'; rewrite DelFDist.dE ltnn D1FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)).
-rewrite I2FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)).
-rewrite I2FDist.dE eqxx divRR ?eqxx //.
+move: H'; rewrite DelFDist.dE D1FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)).
+rewrite I2FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)) I2FDist.dE eqxx divRR ?eqxx //.
 by move: H; rewrite I2FDist.dE eqxx onem_neq0.
 Qed.
 End hull_prop.