diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index a2a581e6..0e80a934 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,13 +17,9 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.17.0-coq-8.17' - - 'mathcomp/mathcomp:1.18.0-coq-8.17' - - 'mathcomp/mathcomp:1.19.0-coq-8.17' - - 'mathcomp/mathcomp:1.17.0-coq-8.18' - - 'mathcomp/mathcomp:1.18.0-coq-8.18' - - 'mathcomp/mathcomp:1.19.0-coq-8.18' - - 'mathcomp/mathcomp:1.19.0-coq-8.19' + - 'mathcomp/mathcomp:2.2.0-coq-8.17' + - 'mathcomp/mathcomp:2.2.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 759c3fb4..96e45c48 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ information theory, and linear error-correcting codes. - Takafumi Saikawa, Nagoya U. - Naruomi Obata, Titech (M2) - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.17 +- Compatible Coq versions: Coq 8.17--8.19 - Additional dependencies: - [MathComp ssreflect](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) diff --git a/changelog.txt b/changelog.txt index dd8f0e9a..8260dafe 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,3 +1,15 @@ +------------------- +from 0.6.1 to 0.7.0 +------------------- + +Port to MathComp 2 + +------------------- +from 0.6.0 to 0.6.1 +------------------- + +compatibility release + ------------------- from 0.5.2 to 0.6.0 ------------------- diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 98e18bac..1013b748 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -22,14 +22,14 @@ build: [ install: [make "install"] depends: [ "coq" { (>= "8.17" & < "8.20~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.20.0") | (= "dev") } - "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.20.0") | (= "dev") } - "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.20.0") | (= "dev") } - "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.20.0") | (= "dev") } - "coq-mathcomp-field" { (>= "1.16.0" & < "1.20.0") | (= "dev") } - "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.8~")} + "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-analysis" { (>= "1.0.0") } "coq-hierarchy-builder" { >= "1.5.0" } - "coq-mathcomp-algebra-tactics" { = "1.1.1" } + "coq-mathcomp-algebra-tactics" { >= "1.2.0" } ] tags: [ diff --git a/ecc_classic/alternant.v b/ecc_classic/alternant.v index b9a66562..03c6d748 100644 --- a/ecc_classic/alternant.v +++ b/ecc_classic/alternant.v @@ -54,7 +54,7 @@ Section injection_into_extension_field. Variables (F0 : finFieldType) (F1 : fieldExtType F0). -Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg_rmorphism F0 F1. +Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg F1. Definition ext_inj_tmp : {rmorphism F0 -> (FinFieldExtType F1)} := ext_inj. diff --git a/ecc_classic/bch.v b/ecc_classic/bch.v index 2f35bdc0..f0fcb430 100644 --- a/ecc_classic/bch.v +++ b/ecc_classic/bch.v @@ -158,7 +158,7 @@ Section BCH_def. Variables (n : nat) (m : nat). Definition code (a : 'rV_n) t := - Rcode.t (@GF2_of_F2_rmorphism m) (kernel (PCM a t)). + Rcode.t (@GF2_of_F2 m) (kernel (PCM a t)). End BCH_def. diff --git a/ecc_classic/cyclic_code.v b/ecc_classic/cyclic_code.v index 0d6f54f3..69716df8 100644 --- a/ecc_classic/cyclic_code.v +++ b/ecc_classic/cyclic_code.v @@ -122,10 +122,12 @@ Lemma rcs'_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : rcs' x = rcs x. Proof. rewrite /rcs' /rcs; apply/rowP => i; rewrite !mxE. case: ifPn => [/eqP -> |i0]. - congr (x _ _); apply val_inj => /=. - by rewrite PermDef.fun_of_permE ffunE /= inordK. + congr (x _ _). + rewrite /rcs_perm/= unlock/= ffunE eqxx. + apply/val_inj => /=. + by rewrite inordK. congr (x _ _); apply val_inj => /=. -rewrite PermDef.fun_of_permE ffunE /= inordK. +rewrite unlock ffunE /= inordK. by rewrite (negPf i0) inordK // (ltn_trans _ (ltn_ord i)) // prednK // lt0n. by rewrite (ltn_trans _ (ltn_ord i)) // prednK // lt0n. Qed. @@ -138,7 +140,7 @@ rewrite coef_add_poly coefXM coefCM coef_add_poly coefXn 2!coef_opp_poly coefC. case: ifPn => [/eqP ->|i0]; last rewrite subr0. rewrite 2!add0r mulrN1 coef_rVpoly /=. case: insubP => //= j _ j0. - rewrite mxE PermDef.fun_of_permE ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _). + rewrite mxE unlock ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _). by apply val_inj => /=; rewrite inordK. case/boolP : (i == n.+1) => [/eqP ->|in0]. rewrite mulr1 2!coef_rVpoly /=. @@ -148,7 +150,7 @@ case/boolP : (i == n.+1) => [/eqP ->|in0]. rewrite mulr0 2!coef_rVpoly; case: insubP => /= [j|]. rewrite ltnS => in0' ji; case: insubP => /= [k _ ki|]. apply/eqP; rewrite subr_eq0; apply/eqP. - rewrite mxE PermDef.fun_of_permE ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _). + rewrite mxE unlock ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _). apply/val_inj => /=; by rewrite inordK. rewrite ltnS -ltnNge => n0i; exfalso. rewrite -ltnS prednK // in in0'; last by rewrite lt0n. @@ -234,20 +236,20 @@ rewrite (reindex_onto (@rcs_perm n) (perm_inv (@rcs_perm n))) /=; last first. move=> i1 _; by rewrite permKV. rewrite (eq_bigl xpredT); last by move=> i1; rewrite permK eqxx. apply eq_bigr => i1 _. -rewrite coef_rVpoly PermDef.fun_of_permE ffunE. +rewrite coef_rVpoly unlock ffunE. case: ifPn => [/eqP ->|]. case: insubP => [j _ jn0|]; last by rewrite ltnS leqnn. rewrite /= in jn0. rewrite coef_rVpoly; case: insubP => // k _ k0. rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly. - rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE k0 /= expr0 mulr1. + rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE k0 /= expr0 mulr1. by rewrite exprAC an1 expr1n mulr1; congr (x _ _); apply val_inj => /=. case: insubP => /= [j|]. rewrite ltnS => i1n0 ji1 i10; rewrite coef_rVpoly. case: insubP => /= [k|]. rewrite ltnS => i1n0' ki1. rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly. - rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10). + rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10). rewrite inordK; last by rewrite ltnW // ltnS prednK // lt0n. rewrite prednK // ?lt0n //; congr (x _ _ * _). by apply/val_inj. diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v index 01d1c89c..67d498b3 100644 --- a/ecc_classic/decoding.v +++ b/ecc_classic/decoding.v @@ -114,7 +114,7 @@ Section maximum_likelihood_decoding. Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)). Variables (n : nat) (C : {vspace 'rV[A]_n}). -Variable f : decT B [finType of 'rV[A]_n] n. +Variable f : decT B ('rV[A]_n) n. Variable P : {fdist 'rV[A]_n}. Local Open Scope reals_ext_scope. @@ -130,8 +130,8 @@ Section maximum_likelihood_decoding_prop. Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)). Variables (n : nat) (C : {vspace 'rV[A]_n}). -Variable repair : decT B [finType of 'rV[A]_n] n. -Let P := fdist_uniform_supp real_realType (vspace_not_empty C). +Variable repair : decT B ('rV[A]_n) n. +Let P := fdist_uniform_supp R (vspace_not_empty C). Hypothesis ML_dec : ML_decoding W C repair P. Local Open Scope channel_code_scope. @@ -216,11 +216,11 @@ Let card_F2 : #| 'F_2 | = 2%nat. Proof. by rewrite card_Fp. Qed. Let W := BSC.c card_F2 p. Variables (n : nat) (C : {vspace 'rV['F_2]_n}). -Variable f : repairT [finType of 'F_2] [finType of 'F_2] n. +Variable f : repairT 'F_2 'F_2 n. Variable f_img : oimg f \subset C. Variable M : finType. -Variable discard : discardT [finType of 'F_2] n M. -Variable enc : encT [finType of 'F_2] M n. +Variable discard : discardT 'F_2 n M. +Variable enc : encT 'F_2 M n. Hypothesis compatible : cancel_on C enc discard. Variable P : {fdist 'rV['F_2]_n}. @@ -273,7 +273,7 @@ Section MAP_decoding. Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)). Variables (n : nat) (C : {vspace 'rV[A]_n}). -Variable dec : decT B [finType of 'rV[A]_n] n. +Variable dec : decT B ('rV[A]_n) n. Variable P : {fdist 'rV[A]_n}. Definition MAP_decoding := forall y : P.-receivable W, @@ -286,9 +286,9 @@ Section MAP_decoding_prop. Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)). Variables (n : nat) (C : {vspace 'rV[A]_n}). -Variable dec : decT B [finType of 'rV[A]_n] n. +Variable dec : decT B ('rV[A]_n) n. Variable dec_img : oimg dec \subset C. -Let P := fdist_uniform_supp real_realType (vspace_not_empty C). +Let P := fdist_uniform_supp R (vspace_not_empty C). Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P. Proof. @@ -332,13 +332,13 @@ End MAP_decoding_prop. Section MPM_decoding. (* in the special case of a binary code... *) -Variable W : `Ch('F_2, [finType of 'F_2]). +Variable W : `Ch('F_2, 'F_2). Variable n : nat. Variable C : {vspace 'rV['F_2]_n}. Hypothesis C_not_empty : (0 < #|[set cw in C]|)%nat. Variable m : nat. -Variable enc : encT [finFieldType of 'F_2] [finType of 'rV['F_2]_(n - m)] n. -Variable dec : decT [finFieldType of 'F_2] [finType of 'rV['F_2]_(n - m)] n. +Variable enc : encT 'F_2 'rV['F_2]_(n - m) n. +Variable dec : decT 'F_2 'rV['F_2]_(n - m) n. Local Open Scope vec_ext_scope. diff --git a/ecc_classic/grs.v b/ecc_classic/grs.v index 5508c5d5..7a2e42e0 100644 --- a/ecc_classic/grs.v +++ b/ecc_classic/grs.v @@ -72,7 +72,7 @@ Qed. Definition syndromep r y := \poly_(l < r) (syndrome_coord l y). -Lemma syndomepE r y : +Lemma syndromepE r y : syndromep r y = \sum_(i in supp y) (y ``_ i * b ``_ i)%:P * (\sum_(l < r) (a ``_ i ^+ l)%:P * 'X^l). Proof. @@ -221,11 +221,14 @@ case/boolP : (r == O) => r0. rewrite -scalerAl mulrC mul_polyC; congr (_ *: (_ *: _)). apply eq_bigl => k; by rewrite in_setD1 andbC. rewrite /GRS_mod big_distrl /= /Omega /erreval -big_split /=. -rewrite GRS.syndomepE big_distrr /=. +rewrite GRS.syndromepE big_distrr /=. apply eq_bigr => i iy. rewrite -3!scalerAl -scalerA -scalerDr. rewrite polyCM -!mulrA mulrCA !mulrA mul_polyC -!scalerAl; congr (_ *: _). -rewrite /Sigma /errloc (bigD1 i) //= mulrC -!mulrA mulrBl mul1r. +rewrite /Sigma /errloc. +rewrite (bigD1 i) //=. +rewrite (mulrC (1 - a ``_ i *: 'X)). +rewrite -!mulrA mulrBl mul1r. set x := (X in _ * X = _). rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first. rewrite /x mulrCA -mulrBr big_distrr /= -sumrB. @@ -241,7 +244,7 @@ rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first. rewrite -!scalerAl mulrCA -exprS !scalerAl; congr (_ * _). by rewrite -mul_polyC -polyCM -exprS. by rewrite -mulrCA -scalerAl -exprS 2!mul_polyC scalerA -exprSr. -rewrite mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _). +rewrite [in LHS]mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _). apply/eq_bigl => j; by rewrite in_setD1 andbC. rewrite -mulNr !mulrA; congr (_ * _). by rewrite -mulNr -mulrA mulrC -!mulrA. diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v index 3cafee7e..e5136c4b 100644 --- a/ecc_classic/hamming_code.v +++ b/ecc_classic/hamming_code.v @@ -1,8 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp. +From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp. From mathcomp Require Import matrix mxalgebra vector. -From mathcomp Require Import Rstruct. +From mathcomp Require Import Rstruct reals. Require Import realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming. Require Import bigop_ext fdist proba channel channel_code decoding. Require Import binary_symmetric_channel. @@ -59,7 +59,7 @@ Let n := (2 ^ m.-1).-1.*2.+1. Definition PCM := \matrix_(i < m, j < n) (cV_of_nat m j.+1 i 0). -Definition code : Lcode0.t [finFieldType of 'F_2] n := kernel PCM. +Definition code : Lcode0.t 'F_2 n := kernel PCM. End hamming_code_definition. @@ -78,13 +78,13 @@ rewrite /n /len !expnS -subn1 doubleB -muln2 -subSn; last first. by rewrite -muln2 mul1n subn2 /= mulnC. Qed. -Lemma two_len : 2 < n. +Lemma two_len : (2 < n)%N. Proof. by rewrite len_dim -subn1 ltn_subRL (@leq_exp2l 2 2). Qed. -Lemma dim_len : m <= n. +Lemma dim_len : (m <= n)%N. Proof. by rewrite len_dim -ltnS prednK ?expn_gt0 // ltn_expl. Qed. -Lemma len_two_m (i : 'I_n) : i.+1 < 2 ^ m. +Lemma len_two_m (i : 'I_n) : (i.+1 < 2 ^ m)%N. Proof. by rewrite (leq_ltn_trans (ltn_ord i)) // len_dim -ltnS prednK // expn_gt0. Qed. @@ -216,9 +216,9 @@ Proof. move: (min_dist_is_min hamming_not_trivial) => Hforall. move: (min_dist_achieved hamming_not_trivial) => Hexists. move: (min_dist_neq0) => H3. -suff : min_dist hamming_not_trivial <> 1%N /\ - min_dist hamming_not_trivial <> 2%N /\ - min_dist hamming_not_trivial <= 3%N. +suff : (min_dist hamming_not_trivial <> 1 /\ + min_dist hamming_not_trivial <> 2 /\ + min_dist hamming_not_trivial <= 3)%N. move : H3. move/(_ _ _ _ hamming_not_trivial). destruct (min_dist hamming_not_trivial) as [|p]=> //. @@ -253,7 +253,7 @@ Definition hamming_err y := let i := nat_of_rV (syndrome (Hamming.PCM m) y) in if i is O then 0 else rV_of_nat n (2 ^ (n - i)). -Lemma wH_hamming_err_ub y : wH (hamming_err y) <= 1. +Lemma wH_hamming_err_ub y : (wH (hamming_err y) <= 1)%N. Proof. rewrite /hamming_err. move Hy : (nat_of_rV _) => [|p /=]. @@ -266,13 +266,13 @@ Definition alt_hamming_err (y : 'rV_n) : 'rV['F_2]_n := let n0 := nat_of_rV s in if n0 is O then 0 else (\row_(j < n) if n0.-1 == j then 1 else 0). -Lemma alt_hamming_err_ub y : wH (alt_hamming_err y) <= 1. +Lemma alt_hamming_err_ub y : (wH (alt_hamming_err y) <= 1)%N. Proof. rewrite /alt_hamming_err. destruct (nat_of_rV _); first by rewrite wH0. clearbody n; clear. rewrite wH_sum. -case/boolP : (n0 < n) => n0n. +case/boolP : (n0 < n)%N => n0n. rewrite (bigD1 (Ordinal n0n)) //= mxE eqxx (eq_bigr (fun x => O)); last first. move=> i Hi; rewrite mxE ifF //. apply: contraNF Hi => /eqP Hi; by apply/eqP/val_inj. @@ -291,7 +291,7 @@ case/boolP : (s == 0) => [/eqP ->|s0]. have [k ks] : exists k : 'I_n, nat_of_rV s = k.+1. move: s0; rewrite -nat_of_rV_eq0 -lt0n => s0. move: (nat_of_rV_up s) => sup. - have sn1up : (nat_of_rV s).-1 < n. + have sn1up : ((nat_of_rV s).-1 < n)%N. by rewrite /n Hamming.len_dim -ltnS prednK // prednK // expn_gt0. exists (Ordinal sn1up); by rewrite /= prednK. rewrite ks /= /syndrome. @@ -369,13 +369,13 @@ Variable m' : nat. Let m := m'.+2. Let n := Hamming.len m'. -Lemma cols_PCM : [set c | wH c^T >= 1] = [set col i (Hamming.PCM m) | i : 'I_n]. +Lemma cols_PCM : [set c | (wH c^T >= 1)%N] = [set col i (Hamming.PCM m) | i : 'I_n]. Proof. apply/setP => i. rewrite in_set. -case Hi : (0 < wH i^T). +case Hi : (0 < wH i^T)%N. apply/esym/imsetP. - have H0 : nat_of_rV i^T - 1 < n. + have H0 : (nat_of_rV i^T - 1 < n)%N. have iup := nat_of_rV_up i^T. rewrite /n Hamming.len_dim -subn1 ltn_sub2r //. by rewrite -{1}(expn0 2) ltn_exp2l // ltnW. @@ -436,14 +436,14 @@ rewrite !mxE eqxx /=. by case Hji : (j == i) => // _; apply/esym/eqP. Qed. -Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1]. +Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1]%N. Definition unit_cols := [set c : 'cV['F_2]_m | wH c^T == 1%nat]. Lemma card_all_cols : #|non_unit_cols :|: unit_cols| = n. Proof. rewrite /non_unit_cols /unit_cols. -transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|. +transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1]%N|. apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt. by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj. Qed. @@ -521,7 +521,7 @@ Qed. Lemma idsA_ids1 (i : 'I_(n - m)) (j : 'I_m) : idsA `_ i <> sval (ids1 j). Proof. destruct (ids1 j) => /= Hij. -have Hlti : i < size idsA by rewrite size_idsA. +have Hlti : (i < size idsA)%N by rewrite size_idsA. move: (mem_nth 0 Hlti). rewrite Hij => Hi. move: (imset_f (fun i => col i (Hamming.PCM m)) Hi). @@ -571,7 +571,7 @@ Lemma PCM_A_1 : PCM = castmx (erefl, subnK (Hamming.dim_len m')) (row_mx CSM 1). Proof. apply/matrixP => i j. rewrite mxE castmxE /=. -case/boolP : (j < n - m) => Hcond. +case/boolP : (j < n - m)%N => Hcond. have -> : cast_ord (esym (subnK (Hamming.dim_len m'))) j = lshift m (Ordinal Hcond) by apply val_inj. rewrite row_mxEl [in X in _ = X]mxE. @@ -602,7 +602,7 @@ Definition GEN' : 'M_(n - m, n) := castmx (erefl, subnK (Hamming.dim_len m')) (row_mx 1%:M (- CSM)^T). Program Definition GEN'' : 'M_(n - m, n) := - @Syslcode.GEN [finFieldType of 'F_2] _ _ _ (castmx (_, erefl (n - m)%nat) CSM). + @Syslcode.GEN 'F_2 _ _ _ (castmx (_, erefl (n - m)%nat) CSM). Next Obligation. exact: leq_subr. Qed. Next Obligation. by rewrite (subnBA _ (Hamming.dim_len m')) addnC addnK. Qed. @@ -676,7 +676,7 @@ Definition mx_discard : 'M['F_2]_(n - m, n) := (* castmx _ (@Syslcode.DIS _ _ _ _).*) Definition mx_discard' : 'M_(n - m, n) := - @Syslcode.DIS [finFieldType of 'F_2] _ _ (leq_subr _ _). + @Syslcode.DIS 'F_2 _ _ (leq_subr _ _). Lemma mx_discardE : mx_discard = mx_discard'. Proof. @@ -792,7 +792,7 @@ rewrite -mulmxA. have [Y1 [Y2 HY]] : exists (Y1 : 'cV_ _) Y2, (row_perm systematic y^T) = castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 Y2). exists (\matrix_(j < 1, i < n - m) (y j (systematic (widen_ord (leq_subr m n) i))))^T. - have dim_len_new i (Hi : i < m) : n - m + i < n. + have dim_len_new i (Hi : (i < m)%N) : (n - m + i < n)%N. by rewrite -ltn_subRL subnBA ?Hamming.dim_len // addnC addnK. exists (\matrix_(j < 1, i < m) (y j (systematic (Ordinal (dim_len_new _ (ltn_ord i))))))^T. apply/colP => a /=. @@ -842,7 +842,7 @@ apply/eqP => /=; rewrite ffunE /syndrome. by rewrite trmx_mul trmxK -mulmxA -(trmxK GEN) -trmx_mul PCM_GEN trmx0 mulmx0. Qed. -Lemma enc_img_is_code : (enc channel_code) @: [finType of 'rV_(n - m)] \subset Hamming.code m. +Lemma enc_img_is_code : (enc channel_code) @: 'rV_(n - m) \subset Hamming.code m. Proof. apply/subsetP => /= t /imsetP[/= x _] ->. by rewrite mem_kernel_syndrome0 (syndrome_enc x). @@ -866,7 +866,7 @@ Variable r' : nat. Let r := r'.+2. Let n := Hamming.len r'. -Definition lcode : Lcode.t [finFieldType of 'F_2] [finFieldType of 'F_2] n _ := +Definition lcode : Lcode.t 'F_2 'F_2 n _ := @Lcode.mk _ _ _ _ _ (Encoder.mk (@Hamming'.encode_inj r') (@Hamming'.enc_img_is_code r')) (Decoder.mk (@hamming_repair_img r') (@Hamming'.discard r')) (@Hamming'.enc_discard_is_id r'). @@ -910,7 +910,7 @@ move=> ->. Defined. Lemma encode_decode c y : c \in lcode -> - repair y != None -> dH c y <= 1 -> repair y = Some c. + repair y != None -> (dH c y <= 1)%N -> repair y = Some c. Proof. move=> Hc Hy cy. apply: (@mddP _ _ lcode _ decoder (hamming_not_trivial r')) => //. @@ -919,7 +919,7 @@ by rewrite /mdd_err_cor hamming_min_dist. Qed. Lemma repair_failure2 e c : c \in lcode -> - ~~ (if repair e is Some y0 then y0 != c else true) -> wH (c + e) <= 1. + ~~ (if repair e is Some y0 then y0 != c else true) -> (wH (c + e) <= 1)%N. Proof. move=> Hc H. suff : dH e c = O \/ dH e c = 1%N by rewrite dHE F2_mx_opp addrC; case=> ->. @@ -933,7 +933,7 @@ rewrite dH_wH leq_eqVlt ?ltnS ?leqn0 => /orP[|] /eqP ->; by auto. Qed. Lemma repair_failure1 e c : c \in lcode -> - (if repair e is Some x then x != c else true) -> 1 < wH (c + e). + (if repair e is Some x then x != c else true) -> (1 < wH (c + e))%N. Proof. move=> Hc. move xc : (repair e) => [x ex |]; last first. @@ -947,7 +947,7 @@ rewrite leq_eqVlt ltnS leqn0 orbC => /orP[|/eqP cy1]. Qed. Lemma repair_failure e c : c \in lcode -> - (if repair e is Some x then x != c else true) = (1 < wH (c + e)). + (if repair e is Some x then x != c else true) = (1 < wH (c + e))%N. Proof. move=> Hc. apply/idP/idP; first by move/repair_failure1; apply. @@ -963,7 +963,7 @@ Require Import Reals Reals_ext. Section hamming_code_error_rate. Variable M : finType. -Hypothesis M_not_0 : 0 < #|M|. +Hypothesis M_not_0 : (0 < #|M|)%nat. Variable p : {prob R}. Let card_F2 : #| 'F_2 | = 2%N. by rewrite card_Fp. Qed. Let W := BSC.c card_F2 p. diff --git a/ecc_classic/linearcode.v b/ecc_classic/linearcode.v index 31fa4028..f5692e5b 100644 --- a/ecc_classic/linearcode.v +++ b/ecc_classic/linearcode.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg poly polydiv fingroup perm. From mathcomp Require Import finalg zmodp matrix mxalgebra mxpoly vector. Require Import ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code. @@ -117,18 +118,23 @@ Proof. by rewrite /syndrome trmx0 mulmx0 trmx0. Qed. Lemma additive_syndrome : additive syndrome. Proof. move=> x y; by rewrite syndromeD syndromeN. Qed. -Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} := - GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ). +HB.instance Definition _ := + GRing.isAdditive.Build _ _ _ additive_syndrome. +HB.instance Definition _ := + GRing.isScalable.Build _ _ _ _ _ syndromeZ. -Definition hom_syndrome : 'Hom(matrix_vectType F 1 n, matrix_vectType F 1 m) := - linfun lin_syndrome. +(*Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} := + GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).*) + +Definition hom_syndrome : 'Hom('rV[F]_n, 'rV[F]_m) := + linfun syndrome. Definition kernel : Lcode0.t F n := lker hom_syndrome. Lemma dim_hom_syndrome_ub : \dim (limg hom_syndrome) <= m. Proof. rewrite [in X in _ <= X](_ : m = \dim (fullv : {vspace 'rV[F]_m})); last first. - by rewrite dimvf /Vector.dim /= mul1n. + by rewrite dimvf/= /dim/= mul1n. by rewrite dimvS // subvf. Qed. @@ -139,7 +145,7 @@ Lemma dim_kernel (Hm : \rank H = m) (mn : m <= n) : \dim kernel = (n - m)%N. Proof. move: (limg_ker_dim hom_syndrome fullv). rewrite (_ : (fullv :&: _)%VS = kernel); last by apply/capv_idPr/subvf. -rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n. +rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n. move=> H0; rewrite -{}[in RHS]H0. suff -> : \dim (limg hom_syndrome) = m by rewrite addnK. set K := castmx (erefl, Hm) (col_base H). @@ -190,14 +196,14 @@ Section dual_code. Variables (F : finFieldType) (m n : nat) (H : 'M[F]_(m, n)). Definition dual_code : {vspace 'rV[F]_n} := - (linfun (mulmxr_linear _ H) @: fullv)%VS. + (linfun (mulmxr H) @: fullv)%VS. Lemma dim_dual_code : (\dim (kernel H) + \dim dual_code = n)%N. Proof. -move: (limg_ker_dim (linfun (lin_syndrome H)) fullv). +move: (limg_ker_dim (linfun (syndrome H)) fullv). rewrite -/(kernel H). rewrite (_ : (fullv :&: _)%VS = kernel H); last by apply/capv_idPr/subvf. -rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n. +rewrite (_ : \dim fullv = n); last by rewrite dimvf /dim /= mul1n. rewrite (_ : \dim (limg _) = \dim dual_code) // /dual_code. rewrite /dimv. Abort. @@ -390,9 +396,14 @@ Proof. by apply/rowP => i; rewrite !mxE. Qed. Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H). Proof. by move=> x y; rewrite sbound_f'D sbound_f'N. Qed. -Definition sbound_f_linear k (H : k.-1 <= n) : +HB.instance Definition _ k (H : k.-1 <= n) := + GRing.isAdditive.Build _ _ _ (additive_sbound_f' H). +HB.instance Definition _ k (H : k.-1 <= n) := + GRing.isScalable.Build _ _ _ _ _ (sbound_f'Z H). + +(*Definition sbound_f_linear k (H : k.-1 <= n) : {linear 'rV[F]_n -> 'rV[F]_k.-1} := - GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)). + GRing.Linear.Pack _ (GRing.Linear.Class (additive_sbound_f' H) (sbound_f'Z H)).*) (* McEliece, theorem 9.8, p.255 *) Lemma singleton_bound : min_dist <= n - \dim C + 1. @@ -400,18 +411,18 @@ Proof. set k := \dim C. have dimCn : k.-1 < n. have /dimvS := subvf C. - rewrite dimvf /Vector.dim /= mul1n. + rewrite dimvf /dim /= mul1n. by apply: leq_trans; rewrite prednK // not_trivial_dim. -set f := linfun (sbound_f_linear (ltnW dimCn)). +set f := linfun (sbound_f' (ltnW dimCn)). have H1 : \dim (f @: C) <= k.-1. suff : \dim (f @: C) <= \dim (fullv : {vspace 'rV[F]_k.-1}). - by rewrite dimvf /= /Vector.dim /= mul1n. + by rewrite dimvf /= /dim /= mul1n. by apply/dimvS/subvf. have H2 : (\dim (f @: C) + \dim (C :&: lker f) = \dim (fullv : {vspace 'rV[F]_k}))%N. - by rewrite dimvf /= /Vector.dim /= mul1n -[RHS](limg_ker_dim f C) addnC. + by rewrite dimvf /= /dim /= mul1n -[RHS](limg_ker_dim f C) addnC. have H3 : 1 <= \dim (C :&: lker f). rewrite lt0n; apply/eqP => abs; move: H2. - rewrite abs addn0 dimvf /Vector.dim /= mul1n -/k. + rewrite abs addn0 dimvf /dim /= mul1n -/k. apply/eqP. move: H1; rewrite leqNgt; apply: contra => /eqP ->. by rewrite prednK // not_trivial_dim. @@ -478,7 +489,7 @@ End minimum_distance. Section not_trivial_binary_codes. -Variable (n : nat) (C : Lcode0.t [finFieldType of 'F_2] n). +Variable (n : nat) (C : Lcode0.t 'F_2 n). Hypothesis C_not_trivial : not_trivial C. @@ -647,7 +658,7 @@ Section hamming_bound. Definition ball q n x r := [set y : 'rV['F_q]_n | dH x y <= r]. -Lemma min_dist_ball_disjoint n q (C : Lcode0.t [finFieldType of 'F_q] n) +Lemma min_dist_ball_disjoint n q (C : Lcode0.t 'F_q n) (C_not_trivial : not_trivial C) t : min_dist C_not_trivial = t.*2.+1 -> forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0. @@ -660,7 +671,7 @@ move: (min_dist_prop C_not_trivial xC yC xy). rewrite Hmin => /(leq_ltn_trans xyt); by rewrite ltnn. Qed. -Lemma ball_disjoint_min_dist_lb n q (C : Lcode0.t [finFieldType of 'F_q] n) +Lemma ball_disjoint_min_dist_lb n q (C : Lcode0.t 'F_q n) (C_not_trivial : not_trivial C) t : (forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0) -> forall x : 'rV_n, x \in C -> x != 0 -> t.*2 < wH x @@ -730,7 +741,7 @@ apply eq_bigr => i _. rewrite card_sphere // (leq_trans _ rn) //; move: (ltn_ord i); by rewrite ltnS. Qed. -Lemma hamming_bound q n (C : Lcode0.t [finFieldType of 'F_q] n) +Lemma hamming_bound q n (C : Lcode0.t 'F_q n) (C_not_trivial : not_trivial C) t (tn : t <= n) : prime q -> min_dist C_not_trivial = t.*2.+1 -> #| C | * card_ball q n t <= q^n. Proof. @@ -763,7 +774,7 @@ rewrite big_imset /=; last first. move=> <-; apply subset_leq_card; apply/subsetP => x; by rewrite inE. Qed. -Definition perfect n q (C : Lcode0.t [finFieldType of 'F_q] n) +Definition perfect n q (C : Lcode0.t 'F_q n) (C_not_trivial : not_trivial C) := exists r, min_dist C_not_trivial = r.*2.+1 /\ (#| C | * card_ball q n r = q^n)%N. @@ -848,7 +859,7 @@ Section lcode_prop. Variables (A B : finFieldType) (n : nat). -Lemma dimlen (k : nat) (C : t A B n [finType of 'rV[A]_k]) : 1 < #|A| -> k <= n. +Lemma dimlen (k : nat) (C : t A B n 'rV[A]_k) : 1 < #|A| -> k <= n. Proof. move=> F1. case : C => cws [] /= f. @@ -1007,7 +1018,7 @@ Qed. Lemma H_G_T : 'H *m 'G ^T = 0. Proof. by rewrite -trmx0 -G_H_T trmx_mul trmxK. Qed. -Definition encode : encT F [finType of 'rV[F]_k] n := [ffun x => x *m 'G]. +Definition encode : encT F 'rV[F]_k n := [ffun x => x *m 'G]. Lemma encode_inj : injective encode. Proof. @@ -1025,11 +1036,11 @@ Definition DIS : 'M[F]_(k, n) := castmx (erefl, subnKC dimlen) (row_mx 1%:M 0). Local Notation "'D" := DIS. -Definition discard : discardT F n [finType of 'rV_k] := [ffun x => x *m 'D^T]. +Definition discard : discardT F n 'rV_k := [ffun x => x *m 'D^T]. Definition t (repair : repairT F F n) (repair_img : oimg repair \subset kernel 'H) - (H : cancel_on (kernel 'H) encode discard) : Lcode.t F F n [finType of 'rV[F]_k]. + (H : cancel_on (kernel 'H) encode discard) : Lcode.t F F n 'rV[F]_k. apply: (@Lcode.mk _ _ _ _ (kernel 'H) (Encoder.mk encode_inj _) (Decoder.mk repair_img discard) diff --git a/ecc_classic/reed_solomon.v b/ecc_classic/reed_solomon.v index 90119417..6ef1dfd3 100644 --- a/ecc_classic/reed_solomon.v +++ b/ecc_classic/reed_solomon.v @@ -167,7 +167,7 @@ rewrite {}/tmp (exchange_big_dep xpredT) //=; apply eq_bigr => j _; rewrite !mxE have @i' : 'I_d. by apply (@Ordinal _ i); rewrite (leq_trans (ltn_ord i)). rewrite (bigD1 i') //= coefXn insubT //= => Hj. -rewrite eqxx mulr1 (_ : Ordinal Hj = j); last by apply val_inj. +rewrite eqxx mulr1 (_ : Sub _ _ = j); last by apply val_inj. rewrite mxE inordK; last by rewrite ltnS (leq_trans (ltn_ord i)). rewrite mulrC; apply/eqP. rewrite addrC -subr_eq subrr; apply/eqP/esym. @@ -444,10 +444,10 @@ Proof. move=> an c0 Hc. have a_neq0 := primitive_uroot_neq0 an. rewrite -(wH_phase_shift a_neq0 _ d). -apply: (@BCH_argument_lemma _ _ (@GRing.idfun_rmorphism F) _ RS_Hchar _ an +apply: (@BCH_argument_lemma _ _ idfun _ RS_Hchar _ an (phase_shift a c d.+1) _ dn). by rewrite -wH_eq0 wH_phase_shift // wH_eq0. -rewrite (_ : \row_i0 (GRing.idfun_rmorphism F) ((phase_shift a c d.+1) ``_ i0) = +rewrite (_ : \row_i0 idfun ((phase_shift a c d.+1) ``_ i0) = phase_shift a c d.+1); last by apply/rowP => i; rewrite !mxE. apply (dft_shifting a_neq0 (prim_expr_order an) dn) => i /andP[ir1 ir2]. have {Hc} : c \in RS.codebook a n' d by rewrite -(RS.lcode0_codebook a dn) inE. @@ -467,7 +467,7 @@ move/poly_rV_0_inv; apply; by rewrite size_rs_gen. Qed. Lemma PCM_lin1_mx : - RS.PCM a n d = (lin1_mx (linfun (lin_syndrome (RS.PCM a n d))))^T. + RS.PCM a n d = (lin1_mx (linfun (syndrome (RS.PCM a n d))))^T. Proof. apply/matrixP => i j. rewrite !(mxE,lfunE) (bigD1 j) //= !mxE !eqxx mulr1 (eq_bigr (fun=> 0)). @@ -892,7 +892,7 @@ by rewrite -RS.lcode0_codebook // ?inE. Qed. Definition RS_as_lcode (an1 : a ^+ n = 1) (Hchar : ([char F]^').-nat n) : - Lcode.t _ _ _ [finType of 'rV_(n - d.+1).+1] := + Lcode.t _ _ _ 'rV_(n - d.+1).+1 := @Lcode.mk _ _ _ _ _ (Encoder.mk RS_enc_injective RS_enc_img) (Decoder.mk (RS_repair_img an1 Hchar) RS_discard) diff --git a/ecc_classic/repcode.v b/ecc_classic/repcode.v index f729975b..a27c796f 100644 --- a/ecc_classic/repcode.v +++ b/ecc_classic/repcode.v @@ -183,7 +183,7 @@ Section minimum_distance_decoding. Variable r : nat. (* we assume a repair function *) -Variable f : repairT [finType of 'F_2] [finType of 'F_2] r.+1. +Variable f : repairT 'F_2 'F_2 r.+1. Hypothesis Hf : oimg f \subset Rep.code r. Let RepLcode := Rep.Lcode_wo_repair Hf. @@ -236,7 +236,7 @@ Definition majority_vote r (s : seq 'F_2) : option 'rV['F_2]_r := else if (r./2 == cnt) && ~~ odd r then None else Some 0. -Definition repair r : repairT [finFieldType of 'F_2] [finFieldType of 'F_2] r.+1 := +Definition repair r : repairT 'F_2 'F_2 r.+1 := [ffun l => majority_vote r.+1 (tuple_of_row l)]. Lemma repair_odd (r : nat) (Hr : odd r.+1) x : @repair r x != None. diff --git a/ecc_modern/checksum.v b/ecc_modern/checksum.v index 1b4ca63c..bf408140 100644 --- a/ecc_modern/checksum.v +++ b/ecc_modern/checksum.v @@ -1,8 +1,9 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp. +From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp. From mathcomp Require Import matrix vector. Require Import Reals. +From mathcomp Require Import Rstruct. Require Import ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode. Require Import pproba. @@ -171,7 +172,7 @@ Qed. Local Close Scope R_scope. Let C := kernel H. -Hypothesis HC : 0 < #| [set cw in C] |. +Hypothesis HC : (0 < #| [set cw in C] |)%nat. Local Open Scope proba_scope. Variable y : (`U HC).-receivable W. diff --git a/ecc_modern/degree_profile.v b/ecc_modern/degree_profile.v index 5167a9ff..c3aa6791 100644 --- a/ecc_modern/degree_profile.v +++ b/ecc_modern/degree_profile.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum. From mathcomp Require Import matrix perm. From mathcomp Require boolp. @@ -55,7 +56,7 @@ End Lambda_definition. End DegreeDistribution. Definition degdistp := DegreeDistribution.p. -Coercion degdistp : DegreeDistribution.Lambda >-> poly_of. +Coercion degdistp : DegreeDistribution.Lambda >-> polynomial. Lemma sum_coef_pos (K : numFieldType) (p : DegreeDistribution.Lambda K) : p.[1] > 0. Proof. @@ -99,7 +100,7 @@ Coercion Lambda_of_L : NormalizedDegreeDistribution.L >-> DegreeDistribution.Lambda. Definition nzdegdist_coerce := NormalizedDegreeDistribution.p. -Coercion nzdegdist_coerce : NormalizedDegreeDistribution.L >-> poly_of. +Coercion nzdegdist_coerce : NormalizedDegreeDistribution.L >-> polynomial. Module TreeEnsemble. @@ -119,8 +120,7 @@ Proof. by move=> [] []; constructor. Qed. -Canonical kind_eqMixin := EqMixin kind_eqP. -Canonical kind_eqType := Eval hnf in EqType _ kind_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ kind_eqP. Definition negk k := if k is kv then kf else kv. Lemma negk_involution k : negk (negk k) = k. @@ -189,11 +189,9 @@ elim: l k => [|l IH] k t. Qed. End EncodeDecode. -Definition tree_eqMixin l k := CanEqMixin (@cancel_tree l k). -Canonical tree_eqType l k := Eval hnf in EqType _ (@tree_eqMixin l k). -Definition tree_choiceMixin l k := CanChoiceMixin (@cancel_tree l k). -Canonical tree_choiceType l k := - Eval hnf in ChoiceType _ (tree_choiceMixin l k). +HB.instance Definition _ l k := Equality.copy (tree l k) (can_type (@cancel_tree l k)). + +HB.instance Definition _ l k := Choice.copy (tree l k) (can_type (@cancel_tree l k)). (* For finite types we need to limit the branching degree *) Fixpoint max_deg (l : nat) k (t : tree l k) : nat := @@ -267,17 +265,13 @@ congr mkFintree. by apply eq_irrelevance. Qed. -Definition fintree_eqMixin n l := CanEqMixin (@cancel_fintree n l). -Canonical fintree_eqType n l := Eval hnf in EqType _ (@fintree_eqMixin n l). -Definition fintree_choiceMixin n l := CanChoiceMixin (@cancel_fintree n l). -Canonical fintree_choiceType n l := Eval hnf in - ChoiceType _ (fintree_choiceMixin n l). +HB.instance Definition _ n l := Equality.copy (fintree n l) (can_type (@cancel_fintree n l)). + +HB.instance Definition _ n l := Choice.copy (fintree n l) (can_type (@cancel_fintree n l)). -Definition tree_countMixin l k := CanCountMixin (@cancel_tree l k). -Canonical tree_countType l k := Eval hnf in CountType _ (tree_countMixin l k). -Definition fintree_countMixin n l := CanCountMixin (@cancel_fintree n l). -Canonical fintree_countType n l := Eval hnf in - CountType _ (fintree_countMixin n l). +HB.instance Definition _ l k := Countable.copy (tree l k) (can_type (@cancel_tree l k)). + +HB.instance Definition _ n l := Countable.copy (fintree n l) (can_type (@cancel_fintree n l)). Section count_allpairs. @@ -446,13 +440,11 @@ have /mapP [x Hx1 Hx2] : ft t \in [seq ft i | i <- s]. by rewrite (can_inj (@cancel_fintree n l) Hx2) Hx1. Qed. -Definition fintree_finMixin n l := Eval hnf in FinMixin (@fintree_enumP n l). - -Canonical fintree_finType n l := Eval hnf in FinType _ (fintree_finMixin n l). +HB.instance Definition _ n l := @isFinite.Build (fintree n l) _ (@fintree_enumP n l). Local Open Scope fdist_scope. -Definition ensemble {K : numDomainType} n l := @FDist.t K [finType of (@fintree n l)]. +Definition ensemble {K : numDomainType} n l := @FDist.t K (@fintree n l). End ensemble. @@ -638,8 +630,7 @@ Qed. Lemma f1 l : \sum_(t : @fintree tw l) (@fintree_dist l t) = 1. Proof. rewrite /index_enum /=. -have ->: Finite.enum (fintree_finType tw l) - = fintree_enum tw l. +have ->: Finite.enum (fintree tw l) = fintree_enum tw l. by rewrite unlock /=. rewrite /fintree_enum. destruct (fintree_enum_dep _ _) => /=. @@ -1117,9 +1108,7 @@ apply ReflectF => [] []. by move/Hp. Qed. -Definition hemi_comp_graph_eqMixin := EqMixin hemi_comp_graph_eqP. -Canonical hemi_comp_graph_eqType := - Eval hnf in EqType _ hemi_comp_graph_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ hemi_comp_graph_eqP. Definition comp_graph_eqb (c1 c2 : comp_graph) := [&& nodes c1 == nodes c2, conodes c1 == conodes c2 & edges c1 == edges c2]. @@ -1147,9 +1136,7 @@ apply ReflectF => [] []. by move/Hn. Qed. -Definition comp_graph_eqMixin := EqMixin comp_graph_eqP. -Canonical comp_graph_eqType := - Eval hnf in EqType _ comp_graph_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ comp_graph_eqP. End pcomp_graph_def. @@ -1195,7 +1182,7 @@ case: ifP => Hend. by rewrite (subsetP (border_p (conodes c)) _ Hx2) orbT. apply/orP; left. apply/bigcupP; exists end_node; last by []. - by rewrite in_set eqxx. + by rewrite inE eqxx. Qed. Definition step_conodes : hemi_comp_graph port := diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v index 539f9f76..dfdf1463 100644 --- a/ecc_modern/ldpc_algo.v +++ b/ecc_modern/ldpc_algo.v @@ -1,7 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. Require Import Init.Wf Recdef Reals. -From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg. +From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum. From mathcomp Require Import Rstruct. Require Import ssrR Reals_ext f2 subgraph_partition tanner. Require Import fdist channel pproba linearcode ssralg_ext. @@ -79,7 +80,18 @@ Definition alpha_op (out inp : R2) := (o*i + o'*i', o*i' + o'*i). Definition alpha := foldr alpha_op (1,0). -Program Definition alpha_op_monoid_law : Monoid.law (R1, R0) := @Monoid.Law _ _ alpha_op _ _ _. +Lemma alphaA : associative alpha_op. +Proof. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed. + +Lemma alphaC : commutative alpha_op. +Proof. by move=> -[a0 a1] [b0 b1]/=; f_equal; ring. Qed. + +Lemma alpha0x : left_id (R1, R0) alpha_op. +Proof. by move=> -[a0 a1] /=; f_equal; ring. Qed. + +HB.instance Definition _ := @Monoid.isComLaw.Build _ _ _ alphaA alphaC alpha0x. + +(*Program Definition alpha_op_monoid_law : Monoid.law (R1, R0) := @Monoid.Law _ _ alpha_op _ _ _. Next Obligation. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed. Next Obligation. by move=> -[a0 a1] /=; f_equal; ring. Qed. Next Obligation. by move=> -[a0 a1] /=; f_equal; ring. Qed. @@ -87,7 +99,7 @@ Canonical alpha_op_monoid_law. Program Definition alpha_op_monoid_com_law := @Monoid.ComLaw R2 _ alpha_op_monoid_law _. Next Obligation. by move=> -[a0 a1] [b0 b1] /=; f_equal; ring. Qed. -Canonical alpha_op_monoid_com_law. +Canonical alpha_op_monoid_com_law.*) (** β[m0,n0](x) = W(y_n0|x) Π_{m1 ∈ F(n0)\{m0}} α[m1,n0](x) *) @@ -96,7 +108,18 @@ Definition beta_op (out inp : R2) := let (o,o') := out in let (i,i') := inp in (o*i, o'*i'). Definition beta := foldl beta_op. -Program Definition beta_op_monoid_law : Monoid.law (R1, R1) := @Monoid.Law _ _ beta_op _ _ _. +Lemma betaA : associative beta_op. +Proof. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; f_equal; ring. Qed. + +Lemma betaC : commutative beta_op. +Proof. by move=> -[a0 a1] [b0 b1]/=; f_equal; ring. Qed. + +Lemma beta0x : left_id (R1, R1) beta_op. +Proof. by move=> -[a0 a1] /=; f_equal; ring. Qed. + +HB.instance Definition _ := @Monoid.isComLaw.Build _ _ _ betaA betaC beta0x. + +(*Program Definition beta_op_monoid_law : Monoid.law (R1, R1) := @Monoid.Law _ _ beta_op _ _ _. Next Obligation. by move=> -[a0 a1] [b0 b1] [c0 c1] /=; rewrite !mulRA. Qed. Next Obligation. by move=> -[a0 a1]; rewrite /beta_op !mul1R. Qed. Next Obligation. by move=> -[a0 a1]; rewrite /beta_op !mulR1. Qed. @@ -104,7 +127,7 @@ Canonical beta_op_monoid_law. Program Definition beta_op_monoid_com_law : Monoid.com_law (R1, R1) := @Monoid.ComLaw _ _ beta_op_monoid_law _. Next Obligation. by move=> -[a0 a1] [b0 b1]; rewrite /beta_op /= (mulRC a0) (mulRC a1). Qed. -Canonical beta_op_monoid_com_law. +Canonical beta_op_monoid_com_law.*) (** Select α or β according to node kind *) Definition alpha_beta {b} (t : tag b) := diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v index c185c8da..d2e5bd87 100644 --- a/ecc_modern/ldpc_algo_proof.v +++ b/ecc_modern/ldpc_algo_proof.v @@ -1,7 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. Require Import Wf_nat Init.Wf Recdef Reals. -From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg. +From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg ssrnum. From mathcomp Require Import Rstruct. Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2. Require Import fdist channel pproba linearcode subgraph_partition tanner. @@ -45,8 +46,7 @@ Proof. by move=> [] []; constructor. Qed. -Canonical kind_eqMixin := EqMixin kind_eqP. -Canonical kind_eqType := Eval hnf in EqType _ kind_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ kind_eqP. Definition tag_eq_bool k (t1 t2 : tag k) : bool := match t1, t2 with @@ -71,8 +71,7 @@ Section EqTag. Variable k : kind. -Canonical tag_eqMixin := EqMixin (@tag_eqP k). -Canonical tag_eqType := Eval hnf in EqType _ tag_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ (@tag_eqP k). End EqTag. @@ -126,8 +125,7 @@ Section EqTnTree. Variable k : kind. -Canonical tn_tree_eqMixin := EqMixin (@tn_tree_eqP k). -Canonical tn_tree_eqType := Eval hnf in EqType _ tn_tree_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ (@tn_tree_eqP k). End EqTnTree. @@ -299,7 +297,7 @@ move/(_ (eqxx true)) => Hcy. by rewrite (eqP Hcy) Hy in Hch. Qed. -Lemma seq_full {A:finType} (s : seq A) a : #|A| - #|s| <= 0 -> a \in s. +Lemma seq_full {A:finType} (s : seq A) a : (#|A| - #|s| <= 0)%N -> a \in s. Proof. move=> Hh. have Hs: finset (mem s) = [set: A]. @@ -313,7 +311,7 @@ Qed. Definition lastE := (last_cat, last_rcons, last_cons). Lemma card_uniq_seq_decr {T : finType} x (s : seq T) h : - #|T| - #|s| <= h.+1 -> uniq (x :: s) -> #|T| - #|x :: s| <= h. + (#|T| - #|s| <= h.+1)%N -> uniq (x :: s) -> (#|T| - #|x :: s| <= h)%N. Proof. move=> Hh Hun. move /card_uniqP: (Hun) => ->. @@ -324,7 +322,7 @@ by move /andP/proj2/card_uniqP: Hun => <-. Qed. Lemma build_tree_rec_ok h k i s : - #|id'| - #|s| <= h -> + (#|id'| - #|s| <= h)%N -> uniq_path (tanner_rel H) (id_of_kind k i) s -> let l := labels (build_tree_rec H rW h s k i) in forall a b, a \in l -> b \in l -> @@ -469,7 +467,7 @@ by move /norP/proj2: Hc. Qed. Lemma build_tree_rec_full h k i s : - #|id'| - #|s| <= h -> + (#|id'| - #|s| <= h)%N -> uniq_path (tanner_rel H) (id_of_kind k i) s -> mem (labels (build_tree_rec H rW h s k i)) =i connect (tanner_split s) (id_of_kind k i). @@ -485,7 +483,7 @@ case Hai: (a == id_of_kind k i); simpl. apply /connectP. by exists [::]. move/andP: Hc => [] /= Hc Hun. -have Hh': #|id'| - #|id_of_kind k i :: s| <= h. +have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%N. by apply card_uniq_seq_decr. have Hchild o: o \in select_children H s k i -> uniq_path (tanner_rel H) (id_of_kind (negk k) o) (id_of_kind k i :: s). @@ -638,7 +636,7 @@ Fixpoint mypath (h : nat) : seq (seq id') := end. Theorem test_acyclic : forall p, p \in [::] :: mypath (m+n) -> - (size p > 2) ==> ~~ ucycleb myrel p. + (size p > 2)%N ==> ~~ ucycleb myrel p. Proof. by apply /allP. Qed. Lemma myrel_ok : myrel =2 tanner_rel H. @@ -656,7 +654,7 @@ elim: h a => [|h Hh] a. by rewrite ltn0. rewrite /= in_cons. case/boolP : (_ == _) => //= a_not_h. -suff a_ltn_h : a < h. +suff a_ltn_h : (a < h)%N. apply/mapP. exists (Ordinal a_ltn_h) => //. by apply val_inj. @@ -670,7 +668,7 @@ destruct a; [left | right]; apply /map_f/my_ord_enum_ok. Qed. Lemma mypath_ok_rec h a p : - (size p) < h -> path myrel a p -> (a :: p \in mypath h). + (size p < h)%N -> path myrel a p -> (a :: p \in mypath h). Proof. elim: h a p => [//|h IHh] a p Hp Hun. suff : a :: p \in flatten [seq [seq i :: l | @@ -692,7 +690,7 @@ Lemma mypath_ok a p : uniq (a :: p) -> path myrel a p -> (a :: p) \in mypath (m+n). Proof. move /card_uniqP => Hsz Hp. -have Hc: #|a::p| <= #|id'| by apply max_card. +have Hc : (#|a::p| <= #|id'|)%N by apply max_card. rewrite Hsz card_sum !card_ord in Hc. by apply mypath_ok_rec. Qed. @@ -1835,11 +1833,14 @@ case Hid: (node_id t == inr n0). rewrite set1F -imset_set1 (kind_filter (k:=kv)). rewrite !beta_map -Monoid.mulmA; congr beta_op. rewrite big_filter (eq_bigr (fun j => msg_spec' (inl j) (inr i))) //. - rewrite Monoid.mulmC -big_filter. + set tmp := alpha_beta _ _. + rewrite /=. + rewrite Monoid.mulmC -big_filter/=. + rewrite /tmp. rewrite -msg_spec_alpha_beta; last first. rewrite sym_tanner_rel. by move/andP/proj1: Hun => /= /andP/proj1. - rewrite -(big_seq1 beta_op_monoid_law o (fun j => msg_spec' (inl j) (inr i))). + rewrite -(big_seq1 beta_op o (fun j => msg_spec' (inl j) (inr i))). rewrite -big_cat. apply/perm_big/uniq_perm. - rewrite /= filter_uniq. diff --git a/ecc_modern/ldpc_erasure.v b/ecc_modern/ldpc_erasure.v index 458c6933..c03525cf 100644 --- a/ecc_modern/ldpc_erasure.v +++ b/ecc_modern/ldpc_erasure.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. Require Program.Wf. From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp. From mathcomp Require Import matrix. @@ -57,8 +58,7 @@ case: a b; [|by case|by case]. by move=> a'; case => //= b' /eqP ->. Qed. -Canonical letter_eqMixin := EqMixin eqlP. -Canonical letter_eqType := Eval hnf in EqType letter letter_eqMixin. +HB.instance Definition _ := hasDecEq.Build _ eqlP. CoInductive letter_spec : letter -> bool -> bool -> bool -> bool -> Prop := | letter_spec0 : letter_spec (Bit 0) true false false false @@ -91,17 +91,12 @@ Definition letter_unpickle (n : nat) := Lemma letter_count : pcancel letter_pickle letter_unpickle. Proof. by case/letterP. Qed. -Definition letter_choiceMixin := PcanChoiceMixin letter_count. -Canonical letter_choiceType := Eval hnf in ChoiceType letter letter_choiceMixin. - -Definition letter_countMixin := PcanCountMixin letter_count. -Canonical letter_countType := Eval hnf in CountType letter letter_countMixin. +HB.instance Definition _ := @PCanIsCountable _ _ _ _ letter_count. Lemma letter_enumP : Finite.axiom [::Bit 0; Bit 1; Star; Blank]. Proof. by case => //; case/F2P. Qed. -Definition letter_finMixin := Eval hnf in FinMixin letter_enumP. -Canonical letter_finType := Eval hnf in FinType letter letter_finMixin. +HB.instance Definition _ := @isFinite.Build letter _ letter_enumP. Definition F2_of_letter (l : letter) : 'F_2 := if l is Bit a then a else 0. diff --git a/ecc_modern/summary.v b/ecc_modern/summary.v index f678a699..197cc138 100644 --- a/ecc_modern/summary.v +++ b/ecc_modern/summary.v @@ -208,12 +208,13 @@ transitivity (\sum_(f in {ffun 'I_n -> bool} | freeon s d (\row_i F2_of_bool (f by rewrite 2!tnth_fgraph ffunE. transitivity (\sum_(f in {set 'I_n} | freeon s d (\row_i F2_of_bool (i \in f))) e (\row_k0 (if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0)))%R. - rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [set x | f x ]) - (@finfun_of_set [finType of 'I_n])). + have @f' : {set 'I_n} -> {ffun 'I_n -> bool} := (fun x => [ffun i => i \in x]). + rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [set x | f x ]) f'). apply eq_big => /= f. rewrite -[LHS]andbT; congr (freeon s d _ && _). - apply/rowP => i; by rewrite !mxE inE. - apply/esym/eqP/ffunP => /= i; by rewrite SetDef.finsetE ffunE. + by apply/rowP => i; rewrite !mxE inE. + apply/esym/eqP/ffunP => /= i. + by rewrite /f' ffunE inE. move=> Hf. congr e. apply/rowP => b; rewrite !mxE. @@ -221,8 +222,7 @@ transitivity (\sum_(f in {set 'I_n} | freeon s d (\row_i F2_of_bool (i \in f))) by rewrite inE tnth_fgraph -enum_rank_ord enum_rankK. move=> /= f Hf. apply/setP => /= k0. - rewrite inE. - by rewrite SetDef.pred_of_setE. + by rewrite inE /f' ffunE. transitivity (\sum_(f in {set 'I_n} | f \subset s) e (\row_(k0 < n) if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0))%R; last first. apply eq_bigl => /= s0. by rewrite powersetE. diff --git a/ecc_modern/summary_tanner.v b/ecc_modern/summary_tanner.v index b7462b33..42465fb5 100644 --- a/ecc_modern/summary_tanner.v +++ b/ecc_modern/summary_tanner.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg zmodp matrix. Require Import Reals. From mathcomp Require Import Rstruct. Require Import ssr_ext ssralg_ext ssrR Reals_ext f2 summary. diff --git a/ecc_modern/tanner.v b/ecc_modern/tanner.v index 48772264..73d57a27 100644 --- a/ecc_modern/tanner.v +++ b/ecc_modern/tanner.v @@ -121,9 +121,9 @@ Lemma Vgraph_set1 m1 n1 : n1 \notin 'V m1 -> 'V(m1, n1) = [set n1]. Proof. move=> m1n1. apply/setP => n2. -rewrite inE in_set1 /=. +rewrite !inE. case/boolP: (n2 == n1) => //= n2n1. -by rewrite 2!inE -VnextE (negbTE m1n1). +by rewrite -VnextE (negbTE m1n1). Qed. (** Function nodes *) diff --git a/ecc_modern/tanner_partition.v b/ecc_modern/tanner_partition.v index 0f1e9386..95b390ce 100644 --- a/ecc_modern/tanner_partition.v +++ b/ecc_modern/tanner_partition.v @@ -975,8 +975,7 @@ move/negbT : Hlhs; apply contra. case/andP. rewrite 2!inE. move=> n1n0. -rewrite in_set1 (negbTE n1n0) orFb. -rewrite inE. +rewrite !inE (negbTE n1n0) orFb. case/andP => _ Hn1. apply/bigcupP => /=. case/connectP : Hn1 => /= p. @@ -1013,7 +1012,7 @@ exists m1. by apply: contra Hun => /eqP ->. rewrite !inE (negbTE n1n2) /= -VnextE -FnextE. case/andP : H2 => -> H2 /=. -apply/connectP; exists p' => //. +apply/connectP; exists p'; last by []. apply: sub_path_except H3 => //. apply/negP => n2p'. move: Hun. diff --git a/information_theory/binary_symmetric_channel.v b/information_theory/binary_symmetric_channel.v index 805080db..7fb19997 100644 --- a/information_theory/binary_symmetric_channel.v +++ b/information_theory/binary_symmetric_channel.v @@ -108,15 +108,9 @@ transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ). set l2Pb := Log 2 (P b). set l21p := Log 2 (1 - p). set l2p := Log 2 p. - ring_simplify. (* TODO *) - congr (_ + _). - rewrite [RHS]addRC !addRA; congr (_ + _). - rewrite [RHS]addRC !addRA; congr (_ + _). - rewrite [RHS]addRC !addRA; congr (_ + _ + _). - rewrite !mulNR; congr (- _). - by rewrite [RHS]mulRC mulRA. - by rewrite [RHS]mulRC mulRA. - by rewrite mulRC. + set Pa := P a. + set Pb := P b. + ring. move: (FDist.f1 P). rewrite Set2sumE /= -/a -/b. rewrite -RplusE => ->. @@ -335,8 +329,7 @@ case/boolP: (p == 0%:pr). move/eqP->; rewrite !coqRE; apply/RleP. rewrite probpK subr0 !expr1n !mul1r !expr0n. move: d1d2; case: d2; first by rewrite leqn0 => /andP [] ->. - case: (d1 == 0%nat) => //=. - move=> ? ?; exact:ler01. + by case: (d1 == 0%nat). move/prob_gt0 => p1. rewrite !coqRE. apply/RleP/expr_conv_mono => //. @@ -366,7 +359,7 @@ Let p_01 : {prob R} := Eval hnf in Prob.mk_ p_01'_. Let p_01 := Eval hnf in Prob.mk_ (ltR2W p_01'). *) -Let P := fdist_uniform (R:=R_numFieldType) card_A. +Let P := fdist_uniform (R:=R) card_A. Variable a' : A. Hypothesis Ha' : receivable_prop (P `^ 1) (BSC.c card_A p_01) (\row_(i < 1) a'). diff --git a/information_theory/channel.v b/information_theory/channel.v index edbda8c3..30557a04 100644 --- a/information_theory/channel.v +++ b/information_theory/channel.v @@ -240,7 +240,7 @@ Lemma Pr_DMC_fst (Q : 'rV_n -> bool) : Proof. rewrite {1}/Pr big_rV_prod /= -(pair_big_fst _ _ [pred x | Q x]) //=; last first. move=> t /=. - rewrite SetDef.pred_of_setE /= SetDef.finsetE /= ffunE. (* TODO: clean? *) + set X := (X in X _ = _); transitivity (prod_rV t \in X) => //; rewrite inE/=. congr (Q _). by apply/rowP => a; rewrite !mxE. transitivity (\sum_(i | Q i) P `^ n i * (\sum_(y in 'rV[B]_n) W ``(y | i))). @@ -259,7 +259,7 @@ Lemma Pr_DMC_out m (S : {set 'rV_m}) : Proof. rewrite {1}/Pr big_rV_prod /= -(pair_big_snd _ _ [pred x | x \notin S]) //=; last first. move=> tab /=. - rewrite SetDef.pred_of_setE /= SetDef.finsetE /= ffunE. (* TODO: clean *) + set X := (X in X _ = _); transitivity (prod_rV tab \in X) => //; rewrite inE/=. do 2 f_equal. by apply/rowP => a; rewrite !mxE. rewrite /= /Pr /= exchange_big /=; apply: eq_big => tb; first by rewrite !inE. diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v index fc58c527..00434e75 100644 --- a/information_theory/channel_coding_direct.v +++ b/information_theory/channel_coding_direct.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix perm. Require Import Reals Lra Classical. From mathcomp Require Import Rstruct classical_sets. @@ -445,7 +446,7 @@ elim: m n F => [m2 F /=|m IH n F]. apply eq_bigr => // i _; congr F. exact/val_inj. - symmetry. - transitivity (\sum_(p in tuple_finType (m + n).+1 C) F p)%R; first by apply congr_big. + transitivity (\sum_(p in [the finType of (m + n).+1.-tuple C]) F p)%R; first by apply congr_big. rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). apply eq_bigr => i _. @@ -749,7 +750,7 @@ have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | pro case=> H1; by rewrite {1}H1. rewrite cardsE. apply eq_card => m_. - by rewrite -!topredE /= !finset.in_set andbC. + by rewrite -!topredE /= !finset.in_set andbC/= inE. by apply eq_big => //; exact: second_summand. rewrite card_ord /=. apply (@leR_ltR_trans (epsilon0 + k%:R * diff --git a/information_theory/conditional_divergence.v b/information_theory/conditional_divergence.v index 719cff4b..0deb15eb 100644 --- a/information_theory/conditional_divergence.v +++ b/information_theory/conditional_divergence.v @@ -1,8 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg finset matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum finset matrix. Require Import Reals. -From mathcomp Require Import Rstruct. +From mathcomp Require Import Rstruct reals. Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts. Require Import num_occ fdist entropy channel divergence types jtypes. Require Import proba jfdist_cond. @@ -139,7 +139,12 @@ have [H'|H'] := eqVneq ((R `X Q) (a, b)) 0. by move/eqP : H; tauto. rewrite -RmultE. by rewrite !(mulR0,mul0R,div0R). -by rewrite 2!fdist_prod1 /=; field; split; exact/eqP. +rewrite 2!fdist_prod1 /=. +set x := R _. +set y := (R `X P _). +set z := (R `X Q _). +field. +split; exact/eqP. Qed. End conditional_divergence_vs_conditional_relative_entropy. diff --git a/information_theory/entropy.v b/information_theory/entropy.v index 936e61f8..063186d9 100644 --- a/information_theory/entropy.v +++ b/information_theory/entropy.v @@ -1,8 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect all_algebra fingroup perm matrix. +From mathcomp Require Import all_ssreflect all_algebra fingroup perm. Require Import Reals. -From mathcomp Require Import Rstruct. +From mathcomp Require Import Rstruct reals. Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext. Require Import logb ln_facts fdist jfdist_cond proba binary_entropy_function. Require Import divergence. @@ -386,8 +386,8 @@ move=> j; rewrite /put_back /put_front; case: (ifPn (j == i)) => [ji|]. rewrite neq_ltn => /orP[|] ji. rewrite ji ifF; last first. apply/negbTE/eqP => /(congr1 val) => /=. - by rewrite inordK // ltnS (leq_trans ji) // -ltnS. - rewrite inordK; last by rewrite ltnS (leq_trans ji) // -ltnS. + by rewrite inordK // ltnS (leq_trans ji) // -ltnS/=. + rewrite inordK; last by rewrite ltnS (leq_trans ji) // -ltnS/=. by rewrite ji /=; apply val_inj => /=; rewrite inordK. rewrite ltnNge (ltnW ji) /= ifF; last first. by apply/negbTE; rewrite -lt0n (leq_trans _ ji). @@ -418,7 +418,7 @@ transitivity (\sum_(x : A) P move: ji; rewrite neq_ltn => /orP[|] ji. apply val_inj => /=. rewrite inordK; last first. - by rewrite /unbump (ltnNge i j) (ltnW ji) subn0 (leq_trans ji) // -ltnS. + by rewrite /unbump (ltnNge i j) (ltnW ji) subn0 (leq_trans ji) // -ltnS/=. by rewrite unbumpK //= inE ltn_eqF. apply val_inj => /=. rewrite inordK; last first. @@ -442,12 +442,12 @@ rewrite neq_ltn => /orP[|] ki. rewrite (_ : inord _ = rshift 1 (inord k)); last first. apply/val_inj => /=. rewrite add1n inordK /=. - by rewrite inordK // (leq_trans ki) // -ltnS. - by rewrite ltnS (leq_trans ki) // -ltnS. + by rewrite inordK // (leq_trans ki) // -ltnS/=. + by rewrite ltnS (leq_trans ki) // -ltnS/=. rewrite (@row_mxEr _ _ 1); congr (v ``_ _). apply val_inj => /=. rewrite /unbump ltnNge (ltnW ki) subn0 inordK //. - by rewrite (leq_trans ki) // -ltnS. + by rewrite (leq_trans ki) // -ltnS/=. rewrite ltnNge (ltnW ki) /=; move: ki. have [/eqP -> //|k0] := boolP (k == ord0). rewrite (_ : k = rshift 1 (inord k.-1)); last first. @@ -691,7 +691,8 @@ Lemma cdiv1_ge0 z : 0 <= cdiv1 z. Proof. have [z0|z0] := eqVneq (PQR`2 z) 0. apply/RleP/sumr_ge0 => -[a b] _; apply/RleP. - by rewrite {1}/jcPr setX1 Pr_set1 (dom_by_fdist_snd _ z0) div0R mul0R. + rewrite {1}/jcPr setX1 [X in X / _ * _]Pr_set1/= (dom_by_fdist_snd (a, b) z0). + by rewrite div0R mul0R. have Hc : (fdistX PQR)`1 z != 0 by rewrite fdistX1. have Hc1 : (fdistX (fdist_proj13 PQR))`1 z != 0. by rewrite fdistX1 fdist_proj13_snd. @@ -1088,15 +1089,14 @@ have -> : cond_entropy PY = \sum_(j < n.+1) rewrite 2!fdist_sndE; congr (_ * _). apply eq_bigr => a _. rewrite -H2. - congr (fdistX _ (a, castmx (_, _) _)). - exact: eq_irrelevance. + by rewrite (_ : esym H1 = H1). rewrite /cond_entropy1; congr (- _). apply eq_bigr => a _. rewrite /jcPr /Pr !big_setX /= !big_set1. rewrite !H2 //=. congr (_ / _ * log (_ / _)). - + rewrite 2!fdist_sndE; apply eq_bigr => a' _; by rewrite H2. - + rewrite 2!fdist_sndE; apply eq_bigr => a' _; by rewrite H2. + + by rewrite 2!fdist_sndE; apply eq_bigr => a' _; rewrite H2. + + by rewrite 2!fdist_sndE; apply eq_bigr => a' _; rewrite H2. rewrite -addR_opp big_morph_oppR -big_split /=; apply eq_bigr => j _ /=. case: ifPn => j0. - rewrite mutual_infoE addR_opp; congr (`H _ - _). @@ -1234,7 +1234,7 @@ transitivity (Pr PRQ [set x] / Pr Q [set x.2]). transitivity (Pr PQ [set (x.1.1,x.2)] * \Pr_RQ[[set x.1.2]|[set x.2]] / Pr Q [set x.2]). congr (_ / _). case: x H0 => [[a c] b] H0 /=. - rewrite /PRQ Pr_set1 fdistACE /= mc; congr (_ * _). + rewrite /PRQ [LHS]Pr_set1 fdistACE /= mc; congr (_ * _). rewrite /jcPr {2}/QP fdistX2 -/P Pr_set1 mulRCA mulRV ?mulR1; last first. apply dom_by_fdist_fstN with b. apply dom_by_fdist_fstN with c. @@ -1337,7 +1337,7 @@ have H2 : cond_entropy (fdistA (fdistAC Q)) = cond_entropy (fdist_prod_of_rV P). cond_entropy1 (fdistA Q) (a1, a2))%R) /=. apply eq_bigr => v _. (* TODO: lemma yyy *) - rewrite (@reindex_onto _ _ _ [finType of 'rV[A]_n'] [finType of 'rV[A]_(n' - i)] + rewrite (@reindex_onto _ _ _ 'rV[A]_n' 'rV[A]_(n' - i) (fun w => (castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w))) (@row_drop A _ i)) /=; last first. move=> w wv; apply/rowP => j. diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v index ad4b4eca..d4957147 100644 --- a/information_theory/entropy_convex.v +++ b/information_theory/entropy_convex.v @@ -50,7 +50,7 @@ Import Order.POrderTheory GRing.Theory Num.Theory. Section entropy_log_div. Variables (A : finType) (p : {fdist A}) (n : nat) (An1 : #|A| = n.+1). -Let u := @fdist_uniform R_numFieldType _ _ An1. +Let u := @fdist_uniform R _ _ An1. Local Open Scope divergence_scope. @@ -85,6 +85,10 @@ Implicit Types p q : {prob R}. Definition dom_pair := {d : {fdist A} * {fdist A} | d.1 `<< d.2}. +(* TODO: wouldn't be needed if dominates were on bool *) +HB.instance Definition _ := boolp.gen_eqMixin dom_pair. +HB.instance Definition _ := boolp.gen_choiceMixin dom_pair. + Lemma dom_conv p (x y u v : {fdist A}) : x `<< y -> u `<< v -> x <| p |> u `<< y <| p |> v. Proof. @@ -123,7 +127,7 @@ Let avgA p q x y z : Proof. by rewrite /avg /=; exact/boolp.eq_exist/convA. Qed. HB.instance Definition _ := @isConvexSpace.Build dom_pair - (Choice.class (choice_of_Type dom_pair)) avg avg1 avgI avgC avgA. + avg avg1 avgI avgC avgA. End dominated_pair. @@ -146,14 +150,16 @@ have [y2a0|y2a0] := eqVneq (y.2 a) 0. have [p0|p0] := eqVneq p 0%:pr. by rewrite p0 -!RmultE -!RplusE ?(mul0R,mulR0,addR0). apply/Req_le; rewrite -!RmultE -!RplusE mulRA ?(mulR0,addR0); congr (_ * _ * log _). - simpl. + set u := x.1 a. + set v := x.2 a. by field; split; exact/eqP. have [x2a0|x2a0] := eqVneq (x.2 a) 0. rewrite x2a0 (_ : x.1 a = 0)// -?RplusE -?RmultE ?(mulR0,add0R,mul0R); last first. by move/dominatesP : Hx; exact. have [->|t0] := eqVneq (Prob.p p).~ 0; first by rewrite !mul0R. apply/Req_le; rewrite mulRA; congr (_ * _ * log _). - simpl. + set u := y.1 a. + set v := y.2 a. by field; split; exact/eqP. set h : {fdist A} -> {fdist A} -> {ffun 'I_2 -> R} := fun p1 p2 => [ffun i => [eta (fun=> 0) with ord0 |-> Prob.p p * p1 a, lift ord0 ord0 |-> (Prob.p p).~ * p2 a] i]. @@ -203,7 +209,7 @@ Hypothesis cardA_gt0 : (0 < #|A|)%nat. Let cardApredS : #|A| = #|A|.-1.+1. Proof. by rewrite prednK. Qed. -Lemma entropy_concave : concave_function (fun P : choice_of_Type {fdist A} => `H P). +Lemma entropy_concave : concave_function (fun P : {fdist A} => `H P). Proof. apply RNconcave_function => p q t; rewrite /convex_function_at. rewrite !(entropy_log_div _ cardApredS) /= /leconv /= [in X in _ <= X]avgRE. @@ -219,7 +225,7 @@ End entropy_concave. Module entropy_concave_alternative_proof_binary_case. -Lemma pderivable_H2 : pderivable H2 (CSet.car open_unit_interval). +Lemma pderivable_H2 : pderivable H2 uniti. Proof. move=> x /= [Hx0 Hx1]. apply derivable_pt_plus. @@ -264,10 +270,10 @@ move=> ? ? ? x [? ?]; split; Qed. Lemma concavity_of_entropy_x_le_y x y (t : {prob R}) : - x \in open_unit_interval -> y \in open_unit_interval -> x < y -> + uniti x -> uniti y -> x < y -> concave_function_at H2 x y t. Proof. -rewrite !classical_sets.in_setE => -[H0x Hx1] [H0y Hy1] Hxy. +move=> -[H0x Hx1] [H0y Hy1] Hxy. apply RNconcave_function_at. set Df := fun z : R => log z - log (1 - z). have @f_derive : pderivable (fun x0 => - H2 x0) (fun z => x <= z <= y). @@ -325,7 +331,7 @@ have DDf_nonneg : forall z, x <= z <= y -> 0 <= DDf z. exact: (@second_derivative_convexf_pt _ _ _ _ Df _ _ DDf). Qed. -Lemma concavity_of_entropy : concave_function_in open_unit_interval H2. +Lemma concavity_of_entropy : concave_function_in uniti H2. Proof. rewrite /concave_function_in => x y t Hx Hy. apply: RNconcave_function_at. @@ -342,7 +348,7 @@ wlog : x y Hx Hy Hxy / x < y. apply: convex_function_sym => // t0. by apply H => //; left. move=> Hxy' t. -exact/R_convex_function_atN /concavity_of_entropy_x_le_y. +by apply/R_convex_function_atN /concavity_of_entropy_x_le_y => //; apply/classical_sets.set_mem. Qed. End entropy_concave_alternative_proof_binary_case. @@ -353,10 +359,10 @@ Variables (A B : finType) (W : A -> {fdist B}). Hypothesis B_not_empty : (0 < #|B|)%nat. Lemma mutual_information_concave : - concave_function (fun P : choice_of_Type {fdist A} => mutual_info (P `X W)). + concave_function (fun P : {fdist A} => mutual_info (P `X W)). Proof. suff : concave_function - (fun P : choice_of_Type {fdist A} => let PQ := fdistX (P `X W) in `H PQ`1 - cond_entropy PQ). + (fun P : {fdist A} => let PQ := fdistX (P `X W) in `H PQ`1 - cond_entropy PQ). set f := fun _ => _. set g := fun _ => _. suff -> : f = g by []. by rewrite boolp.funeqE => d; rewrite {}/f {}/g /= -mutual_infoE -mutual_info_sym. @@ -367,7 +373,7 @@ apply: R_concave_functionB. apply: leR_trans (concave_H (p `X W)`2 (q `X W)`2 t). under eq_bigr do rewrite fdist_prod2_conv. by apply/RleP; rewrite lexx. -suff : affine (fun x : choice_of_Type {fdist A} => cond_entropy (fdistX (x `X W))). +suff : affine (fun x : {fdist A} => cond_entropy (fdistX (x `X W))). by move=> /affine_functionP[]. move=> t p q. rewrite /= avgRE /cond_entropy /cond_entropy1. diff --git a/information_theory/error_exponent.v b/information_theory/error_exponent.v index c878b080..0bbf8dcb 100644 --- a/information_theory/error_exponent.v +++ b/information_theory/error_exponent.v @@ -54,8 +54,7 @@ apply/RleP; rewrite -(@ler_pM2r _ (/ 2)); last first. by rewrite RinvE' invr_gt0// (_ : 2%coqR = 2%:R)// INRE ltr0n. rewrite RmultE -mulrA mulrCA RinvE' (_ : 2%coqR = 2%:R)// INRE. rewrite mulfV ?mulr1 ?gt_eqF//. - by apply/RleP; rewrite -RdivE'. -exact/RltP. +by apply/RleP; rewrite -RdivE'. Qed. Local Open Scope variation_distance_scope. diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v index 3e6c8443..024b1ae8 100644 --- a/information_theory/joint_typ_seq.v +++ b/information_theory/joint_typ_seq.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssrnum ssralg matrix. Require Import Reals Lra. From mathcomp Require Import Rstruct. Require Import ssrZ ssrR Reals_ext ssr_ext logb ssralg_ext bigop_ext. @@ -48,7 +48,7 @@ Local Open Scope R_scope. Section joint_typ_seq_definition. Variables A B : finType. -Variable P : {fdist A}. +Variable P : R.-fdist A. Variable W : `Ch(A, B). Variable n : nat. Variable epsilon : R. diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v index 1a24fdc7..41887e9d 100644 --- a/information_theory/jtypes.v +++ b/information_theory/jtypes.v @@ -1,3 +1,4 @@ +From HB Require Import structures. (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup perm. @@ -90,8 +91,7 @@ have ? : d1 = d2. subst d2; congr JType.mk; exact/boolp.Prop_irrelevance. Qed. -Definition jtype_eqMixin A B n := EqMixin (@jtype_eqP A B n). -Canonical jtype_eqType A B n := Eval hnf in EqType _ (@jtype_eqMixin A B n). +HB.instance Definition _ A B n := @hasDecEq.Build _ _ (@jtype_eqP A B n). Definition nneg_fun_of_pre_jtype (A B : finType) (Bnot0 : (0 < #|B|)%nat) n (f : {ffun A -> {ffun B -> 'I_n.+1}}) : A -> nneg_finfun B. @@ -182,10 +182,7 @@ destruct Sumbool.sumbool_of_bool; last by rewrite Hf in e1. congr Some; by apply/jtype_eqP => /=. Qed. -Lemma jtype_choiceMixin A B n : choiceMixin (P_ n ( A , B )). -Proof. apply (PcanChoiceMixin (@jtype_choice_pcancel A B n)). Qed. - -Canonical jtype_choiceType A B n := Eval hnf in ChoiceType _ (jtype_choiceMixin A B n). +HB.instance Definition _ A B n := @PCanIsCountable _ _ _ _ (@jtype_choice_pcancel A B n). Definition jtype_pickle (A B : finType) n (P : P_ n (A , B)) : nat. destruct P as [d t H]. @@ -240,10 +237,7 @@ destruct Sumbool.sumbool_of_bool; last by rewrite Hf in e1. congr Some; by apply/jtype_eqP => /=. Qed. -Definition jtype_countMixin A B n := CountMixin (@jtype_count_pcancel A B n). - -Canonical jtype_countType (A B : finType) n := - Eval hnf in CountType (P_ n ( A , B )) (@jtype_countMixin A B n). +HB.instance Definition _ A B n := @PCanIsCountable _ _ _ _ (@jtype_count_pcancel A B n). Definition jtype_enum_f (A B : finType) n (f : { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat}) : @@ -312,8 +306,7 @@ rewrite count_map. by apply eq_count. Qed. -Definition jtype_finMixin A B n := Eval hnf in FinMixin (@jtype_enumP A B n). -Canonical jtype_finType A B n := Eval hnf in FinType _ (@jtype_finMixin A B n). +HB.instance Definition _ A B n := @isFinite.Build (P_ n (A , B)) _ (@jtype_enumP A B n). Section jtype_facts. Variables (A B : finType) (n : nat) (ta : n.-tuple A). @@ -346,7 +339,7 @@ Qed. 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. -apply (@leq_trans (size (map (@ffun_of_jtype A B n) (Finite.enum (jtype_finType A B n))))). +apply (@leq_trans (size (map (@ffun_of_jtype A B n) (Finite.enum (P_ n (A, B)))))). by rewrite 2!size_map. rewrite cardE. apply: uniq_leq_size. @@ -697,7 +690,7 @@ rewrite /split_tuple /= in_setX; apply/andP; split. apply/val_inj => /=. rewrite eq_tcast /=. by rewrite -tb's sum_num_occ_rec take_takel// leq_addr. -- rewrite in_set. +- rewrite inE. apply/eqP/val_inj => /=. by rewrite eq_tcast -Ha take0. Qed. @@ -1279,7 +1272,7 @@ Variable ta : n.-tuple A. Variable P : P_ n ( A ). Hypothesis Hta : ta \in T_{P}. -Definition shell_partition : {set set_of_finType [finType of n.-tuple B]} := +Definition shell_partition (*: {set set_of_finType [finType of n.-tuple B]}*) := (fun V => V.-shell ta) @: \nu^{B}(P). Lemma cover_shell : cover shell_partition = [set: n.-tuple B]. diff --git a/information_theory/kraft.v b/information_theory/kraft.v index 9428de7f..4895cd4b 100644 --- a/information_theory/kraft.v +++ b/information_theory/kraft.v @@ -129,6 +129,7 @@ Section ary_of_nat. Variable t' : nat. Let t := t'.+2. +Local Obligation Tactic := idtac. Program Definition ary_of_nat' (n : nat) (f : forall n', (n' < n)%coq_nat -> seq 'I_t) : seq 'I_t := match n with @@ -139,7 +140,7 @@ Program Definition ary_of_nat' else rcons (f (n %/ t) _) (inord (n %% t)) end. -Next Obligation. exact/ltP/ltn_Pdiv. Qed. +Next Obligation. by move=> n ? ? <-; apply/ltP/ltn_Pdiv. Qed. Definition ary_of_nat := Fix Wf_nat.lt_wf (fun _ => seq 'I_t) ary_of_nat'. @@ -387,7 +388,7 @@ Section example_of_code. Variable (n' : nat) (t' : nat). Let n := n'.+1. Let t := t'.+2. -Let T := [finType of 'I_t]. +Let T := 'I_t. Variable l : seq nat. Hypothesis l_n : size l = n. Hypothesis sorted_l : sorted leq l. @@ -490,9 +491,11 @@ Definition kraft_cond (T : finType) (l : seq nat) := End kraft_condition. +Local Obligation Tactic := idtac. Program Definition prepend (T : finType) (lmax : nat) (c : seq T) (t : (lmax - size c).-tuple T) : lmax.-tuple T := @Tuple _ _ (take lmax c ++ t) _. Next Obligation. +move=> T lmax c t. rewrite size_cat size_take size_tuple. case: ifPn. move/ltnW; rewrite -subn_eq0 => /eqP ->; by rewrite addn0. @@ -582,7 +585,7 @@ rewrite (eq_bigr (fun i : 'I_n => #|suffixes C``_i|%:R)%R); last first. by apply/leq_lmax/nthP; exists i. by rewrite unitfE pnatr_eq0 -lt0n. (*\color{comment}{\framebox{the goal is now $\sum_{i < n} | \{ x | \prefix{c_i}{x} \} | \leq |T|^{\ell_{\mathrm{max}}}$}} *) -apply (@le_trans _ _ (#|\bigcup_(i < n) suffixes (C ``_ i)|%:R)%R). +apply: (@le_trans _ _ (#|\bigcup_(i < n) suffixes (C ``_ i)|%:R)%R). rewrite -sum1_card. rewrite partition_disjoint_bigcup /=. rewrite natr_sum ler_sum // => i _. @@ -603,7 +606,7 @@ Section kraft_code. Variable (n' : nat) (t' : nat). Let n := n'.+1. Let t := t'.+2. -Let T := [finType of 'I_t]. +Let T := 'I_t. Variable l : seq nat. Hypothesis l_n : size l = n. Hypothesis sorted_l : sorted leq l. @@ -674,7 +677,7 @@ Section kraft_cond_implies_prefix. Variable (n' : nat) (t' : nat). Let n := n'.+1. Let t := t'.+2. -Let T := [finType of 'I_t]. +Let T := 'I_t. Variable l : seq nat. Hypothesis l_n : size l = n. Hypothesis sorted_l : sorted leq l. diff --git a/information_theory/shannon_fano.v b/information_theory/shannon_fano.v index 29b2b2ce..21495e93 100644 --- a/information_theory/shannon_fano.v +++ b/information_theory/shannon_fano.v @@ -57,7 +57,7 @@ Let a : A. by move/card_gt0P: (fdist_card_neq0 P) => /sigW [i]. Qed. Variable t' : nat. Let t := t'.+2. -Let T := [finType of 'I_t]. +Let T := 'I_t. Variable (f : Encoding.t A T). Let sizes := [seq (size \o f) a| a in A]. @@ -107,7 +107,7 @@ Section shannon_fano_suboptimal. Variables (A : finType) (P : {fdist A}). Hypothesis Pr_pos : forall s, P s != 0. -Let T := [finType of 'I_2]. +Let T := 'I_2. Variable f : Encoding.t A T. Local Open Scope entropy_scope. @@ -150,7 +150,7 @@ Variables (A : finType) (P : {fdist A}). Variable (t' : nat). Let n := #|A|.-1.+1. Let t := t'.+2. -Let T := [finType of 'I_t]. +Let T := 'I_t. Variable l : seq nat. Hypothesis l_n : size l = n. Hypothesis sorted_l : sorted leq l. diff --git a/information_theory/source_code.v b/information_theory/source_code.v index e167c2b1..bb9146e5 100644 --- a/information_theory/source_code.v +++ b/information_theory/source_code.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. Require Import Reals. From mathcomp Require Import Rstruct. Require Import ssrR Reals_ext logb fdist proba. @@ -40,7 +40,7 @@ Variables (A : finType) (k n : nat). Definition scode_vl := scode A (seq bool) k. -Variables (P : {fdist A}) (f : {RV (P `^ n) -> seq bool}). +Variables (P : R.-fdist A) (f : {RV (P `^ n) -> seq bool}). Definition E_leng_cw := `E ((INR \o size) `o f). diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v index eb3edf4a..e15eba93 100644 --- a/information_theory/source_coding_fl_direct.v +++ b/information_theory/source_coding_fl_direct.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. Require Import Reals Lra. From mathcomp Require Import Rstruct. Require Import ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist. @@ -24,7 +24,7 @@ Local Open Scope ring_scope. Local Open Scope fdist_scope. Section encoder_and_decoder. -Variables (A : finType) (P : {fdist A}) (n k : nat). +Variables (A : finType) (P : R.-fdist A) (n k : nat). Variable S : {set 'rV[A]_k.+1}. @@ -208,7 +208,7 @@ rewrite inE /=; apply/negPn/negPn. rewrite -exp2_0; apply Exp_le_increasing => //. apply mulR_ge0; first exact: leR0n. apply addR_ge0; first exact: entropy_ge0. - apply Rlt_le; exact: lambda2_gt0. + by apply Rlt_le; exact: lambda2_gt0. + rewrite addRR -{1}(logK Rlt_0_2) -ExpD {1}/log Log_n //. by apply/RleP; rewrite Order.POrderTheory.lexx. Qed. diff --git a/information_theory/source_coding_vl_direct.v b/information_theory/source_coding_vl_direct.v index d00b6d96..4e0e266b 100644 --- a/information_theory/source_coding_vl_direct.v +++ b/information_theory/source_coding_vl_direct.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. Require Import Reals Lra. From mathcomp Require Import Rstruct. Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext. @@ -67,7 +67,7 @@ End R_lemma. Section Length. Variable (X : finType) (n' : nat). Let n := n'.+1. -Variable P : {fdist X}. +Variable P : R.-fdist X. Variable epsilon : R. Hypothesis eps_pos : 0 < epsilon. @@ -145,7 +145,7 @@ Definition enc_typ x := in Tuple (size_bitseq_of_nat i (Z.abs_nat L_typ)). Lemma card_le_Xn_Lnt : - (#|[finType of n.-tuple X] | <= #|[finType of (Z.abs_nat L_not_typ).-tuple bool]|)%nat. + (#|[the finType of n.-tuple X] | <= #|[the finType of (Z.abs_nat L_not_typ).-tuple bool]|)%nat. Proof. rewrite -!cardsT. apply/leP. diff --git a/information_theory/string_entropy.v b/information_theory/string_entropy.v index bb57752e..ec5c4877 100644 --- a/information_theory/string_entropy.v +++ b/information_theory/string_entropy.v @@ -2,7 +2,7 @@ (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum. Require Import Reals. -From mathcomp Require Import Rstruct. +From mathcomp Require Import Rstruct classical_sets. Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb. Require Import fdist entropy convex ln_facts jensen num_occ. diff --git a/information_theory/success_decode_bound.v b/information_theory/success_decode_bound.v index 92665419..ba135f11 100644 --- a/information_theory/success_decode_bound.v +++ b/information_theory/success_decode_bound.v @@ -140,7 +140,7 @@ apply/le_INR/leP/subset_leq_card/setIidPl/setP => tb. by rewrite in_set in_set andbC andbA andbb. Qed. -Let partition_pre_image : {set set_of_finType [finType of n.-tuple B]} := +Let partition_pre_image (*: {set set_of_finType [finType of n.-tuple B]}*) := [set T_{ `tO( V ) } :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m])) | m in M & [exists y, y \in T_{`tO( V )} :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m]))]]. diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v index 57ad937a..ba16be68 100644 --- a/information_theory/typ_seq.v +++ b/information_theory/typ_seq.v @@ -220,7 +220,7 @@ rewrite Heq Pr_set0 in H. lra. Qed. -Definition TS_0 (H : aep_bound P epsilon <= n.+1%:R) : [finType of 'rV[A]_n.+1]. +Definition TS_0 (H : aep_bound P epsilon <= n.+1%:R) : 'rV[A]_n.+1. apply (@enum_val _ (pred_of_set (`TS P n.+1 epsilon))). have -> : #| `TS P n.+1 epsilon| = #| `TS P n.+1 epsilon|.-1.+1. rewrite prednK //. diff --git a/information_theory/types.v b/information_theory/types.v index d2c6ddec..861e1f0f 100644 --- a/information_theory/types.v +++ b/information_theory/types.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum perm. From mathcomp Require Import matrix. From mathcomp Require boolp. @@ -54,7 +55,7 @@ End type_def. End type. Definition type_coercion := type.d. -Coercion type_coercion : type.type >-> fdist_of. +Coercion type_coercion : type.type >-> FDist.t. Notation "'P_' n '(' A ')'" := (type.type A n) : types_scope. @@ -120,8 +121,7 @@ suff ? : d1 = d2 by subst d2; congr type.mkType; exact: boolp.Prop_irrelevance. apply fdist_ext => /= a; by rewrite H1 H2. Qed. -Definition type_eqMixin A n := EqMixin (@type_eqP A n). -Canonical type_eqType A n := Eval hnf in EqType _ (@type_eqMixin A n). +HB.instance Definition _ A n := hasDecEq.Build _ (@type_eqP A n). Lemma type_ffunP A n (P Q : P_ n.+1 ( A )) : (forall c, type.d P c = type.d Q c) -> P = Q. @@ -197,10 +197,7 @@ suff ? : d1 = d by subst d; congr type.mkType; apply boolp.Prop_irrelevance. apply fdist_ext => /= a; by rewrite ffunE H. Qed. -Lemma type_choiceMixin A n : choiceMixin (P_ n ( A )). -Proof. apply (PcanChoiceMixin (@type_choice_pcancel A n)). Qed. - -Canonical type_choiceType A n := Eval hnf in ChoiceType _ (type_choiceMixin A n). +HB.instance Definition _ A n := @PCanIsCountable _ _ _ _ (@type_choice_pcancel A n). Definition type_pickle A n (P : P_ n (A)) : nat. destruct P as [d f H]. @@ -237,9 +234,7 @@ suff ? : d1 = d by subst d; congr type.mkType; apply boolp.Prop_irrelevance. apply/fdist_ext => a; by rewrite ffunE H. Qed. -Definition type_countMixin A n := CountMixin (@type_count_pcancel A n). -Canonical type_countType A n := - Eval hnf in CountType (P_ n ( A )) (@type_countMixin A n). +HB.instance Definition _ A n := @PCanIsCountable _ _ _ _ (@type_count_pcancel A n). Definition type_enum_f (A : finType) n (f : { f : {ffun A -> 'I_n.+1} | (\sum_(a in A) f a)%nat == n} ) : option (P_ n ( A )). destruct n. @@ -250,7 +245,7 @@ Defined. Definition type_enum A n := pmap (@type_enum_f A n) (enum [finType of {f : {ffun A -> 'I_n.+1} | (\sum_(a in A) f a)%nat == n}]). -Lemma type_enumP A n : Finite.axiom (@type_enum A n). +Lemma type_enumP A n : finite_axiom (@type_enum A n). Proof. destruct n. case=> d t H /=; by move: (no_0_type H). @@ -263,8 +258,7 @@ rewrite /type_enum /= /type_enum_f /= count_map. by apply eq_count. Qed. -Definition type_finMixin A n := Eval hnf in FinMixin (@type_enumP A n). -Canonical type_finType A n := Eval hnf in FinType _ (@type_finMixin A n). +HB.instance Definition _ A n := @isFinite.Build (P_ n (A)) _ (@type_enumP A n). Section type_facts. Variable A : finType. @@ -274,12 +268,12 @@ Lemma type_counting n : #| P_ n ( A ) | <= expn (n.+1) #|A|. Proof. rewrite -(card_ord n.+1) -card_ffun /=. rewrite cardE /enum_mem. -apply (@leq_trans (size (map (@ffun_of_type A n) (Finite.enum (type_finType A n))))). +apply (@leq_trans (size (map (@ffun_of_type A n) (Finite.enum _)))). by rewrite 2!size_map. rewrite cardE. apply: uniq_leq_size. rewrite map_inj_uniq //. - move: (enum_uniq (type_finType A n)). + move: (enum_uniq (P_ n (A))). by rewrite enumT. case=> d f Hd [] d2 f2 Hd2 /= ?; subst f2. have ? : d = d2 by apply/fdist_ext => a; rewrite Hd Hd2. @@ -595,15 +589,15 @@ Lemma sum_messages_types' f : \sum_ (S | S \in enc_pre_img_partition c) \sum_(m in S) f m. Proof. rewrite (bigID (fun P => [exists m, m \in enc_pre_img c P] )). -rewrite (_ : forall a b, Radd_comoid a b = a + b) //. +rewrite /=. rewrite Rplus_comm big1 ; last first. - move=> P ; rewrite andTb negb_exists => HP. + move=> P; rewrite negb_exists => HP. apply big_pred0 => m /=. - apply/negP/negPn; by move:HP => /forallP/(_ m) ->. + by apply/negP/negPn; move:HP => /forallP/(_ m) ->. rewrite /= add0R big_imset. apply eq_big => [P|P _] //=. rewrite in_set. - case: set0Pn => [/existsP //| ?]; exact/existsP. + by case: set0Pn => [/existsP //| ?]; exact/existsP. move=> P Q; rewrite 2!in_set => HP HQ HPQ /=. move: (enc_pre_img_injective HP HPQ) => {HP HQ} {}HPQ. case: P HPQ => /= Pd Pf HP HPQ. @@ -613,7 +607,7 @@ apply/eqP. apply ffunP => a. apply/val_inj/INR_eq. move: {HPQ}(HPQ a); rewrite HP HQ eqR_mul2r //. -apply/invR_neq0; by rewrite INR_eq0. +by apply/invR_neq0; rewrite INR_eq0. Qed. Lemma sum_messages_types f : diff --git a/lib/Reals_ext.v b/lib/Reals_ext.v index d4cc9191..ad13510c 100644 --- a/lib/Reals_ext.v +++ b/lib/Reals_ext.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import all_algebra vector reals normedtype. From mathcomp Require Import mathcomp_extra boolp. @@ -241,9 +242,8 @@ Record nneg_finfun := mkNNFinfun { nneg_ff :> {ffun T -> R} ; _ : [forall a, (0 <= nneg_ff a)%mcR] }. -Canonical nneg_finfun_subType := Eval hnf in [subType for nneg_ff]. -Definition nneg_finfun_eqMixin := [eqMixin of nneg_finfun by <:]. -Canonical nneg_finfun_eqType := Eval hnf in EqType _ nneg_finfun_eqMixin. +HB.instance Definition _ := [isSub for nneg_ff]. +HB.instance Definition _ := [Equality of nneg_finfun by <:]. End nneg_finfun. Record nneg_fun (T : Type) := mkNNFun { @@ -298,10 +298,9 @@ Proof. apply/andP; split. by rewrite RdivE' mul1r invr_ge0 ?addr_ge0. rewrite RdivE' mul1r invf_le1//. - by rewrite ler_addl. + by rewrite lerDl. rewrite (@lt_le_trans _ _ 1)//. - by rewrite ltr01. -by rewrite ler_addl. +by rewrite lerDl. Qed. Definition Prob_invp (p : {prob R}) := Prob.mk (prob_invp_subproof p). @@ -336,7 +335,7 @@ Export OProb.Exports. Coercion OProb.p : oprob >-> prob. Canonical oprobcplt (p : oprob) := Eval hnf in OProb.mk (onem_oprob (OProb.O1 p)). *) -Coercion OProb.p : oprob >-> prob_of. +Coercion OProb.p : oprob >-> prob. Section oprob_lemmas. Implicit Types p q : {oprob R}. @@ -392,7 +391,7 @@ by rewrite mulr_ilt1//; apply/RltP/oprob_lt1. Qed. Canonical oprobmulR (p q : {oprob R}) := - Eval hnf in @OProb.mk _ (Prob.p (OProb.p p) * q)%:pr (oprob_mulR_subproof p q). + Eval hnf in @OProb.mk R (probmulR p q) (oprob_mulR_subproof p q). Lemma s_of_pq_oprob_subproof (p q : {oprob R}) : (0 < Prob.p [s_of p, q] < 1)%O. Proof. @@ -417,7 +416,7 @@ rewrite r_of_pqE; apply/andP; split. rewrite divr_gt0////. exact/RltP/oprob_gt0. rewrite s_of_pqE//. - have := OProb.O1 (((oprob_to_real p).~ * (oprob_to_real q).~).~)%:opr. + have := OProb.O1 (oprobcplt (oprobmulR (oprobcplt p) (oprobcplt q))). by move/andP=> [] /=. apply/RltP. rewrite -RdivE'. @@ -426,7 +425,7 @@ rewrite ltR_neqAle; split; last exact/RleP/ge_s_of. rewrite s_of_pqE; apply/eqP/ltR_eqF. rewrite onemM !onemK -!RplusE -RoppE -addRA. apply/ltR_addl. -have := oprob_gt0 ((oprob_to_real p).~ * oprob_to_real q)%:opr. +have := oprob_gt0 (oprobmulR (oprobcplt p) q). by rewrite /= onemE mulrBl mul1r -RminusE//. Qed. @@ -456,13 +455,10 @@ End Exports. End Rpos. Export Rpos.Exports. -Canonical Rpos_subType := [subType for Rpos.v]. -Definition Rpos_eqMixin := Eval hnf in [eqMixin of Rpos by <:]. -Canonical Rpos_eqType := Eval hnf in EqType Rpos Rpos_eqMixin. -Definition Rpos_choiceMixin := Eval hnf in [choiceMixin of Rpos by <:]. -Canonical Rpos_choiceType := Eval hnf in ChoiceType Rpos Rpos_choiceMixin. +HB.instance Definition _ := [isSub for Rpos.v]. +HB.instance Definition _ := [Choice of Rpos by <:]. -Definition rpos_coercion (p : Rpos) : Real.sort real_realType := Rpos.v p. +Definition rpos_coercion (p : Rpos) : Real.sort R := Rpos.v p. Coercion rpos_coercion : Rpos >-> Real.sort. Definition mkRpos x H := @Rpos.mk x (introT (RltP _ _) H). @@ -547,11 +543,8 @@ End Exports. End Rnng. Export Rnng.Exports. -Canonical Rnng_subType := [subType for Rnng.v]. -Definition Rnng_eqMixin := Eval hnf in [eqMixin of Rnng by <:]. -Canonical Rnng_eqType := Eval hnf in EqType Rnng Rnng_eqMixin. -Definition Rnng_choiceMixin := Eval hnf in [choiceMixin of Rnng by <:]. -Canonical Rnng_choiceType := Eval hnf in ChoiceType Rnng Rnng_choiceMixin. +HB.instance Definition _ := [isSub for Rnng.v]. +HB.instance Definition _ := [Choice of Rnng by <:]. Section Rnng_theory. Local Open Scope R_scope. diff --git a/lib/bigop_ext.v b/lib/bigop_ext.v index 9530e74b..7958f0cd 100644 --- a/lib/bigop_ext.v +++ b/lib/bigop_ext.v @@ -92,7 +92,7 @@ under eq_bigr=> i. over. rewrite bigA_distr_bigA big_mkord (partition_big (fun i : {ffun I -> bool} => inord #|[set x | i x]|) - (fun j : [finType of 'I_#|I|.+1] => true)) //=. + (fun j : 'I_#|I|.+1 => true)) //=. { eapply eq_big =>// i _. rewrite (reindex (fun s : {set I} => [ffun x => x \in s])); last first. { apply: onW_bij. @@ -503,15 +503,15 @@ Section big_tuple_ffun. Import Monoid.Theory. Variable R : Type. Variable V : zmodType. -Variable times : Monoid.mul_law (GRing.zero V). +Variable times : Monoid.mul_law (@GRing.zero V). Local Notation "*%M" := times (at level 0). -Variable plus : Monoid.add_law (GRing.zero V) *%M. +Variable plus : Monoid.add_law (@GRing.zero V) *%M. Local Notation "+%M" := plus (at level 0). Lemma big_tuple_ffun (I J : finType) (F : {ffun I -> J} -> R) (G : R -> J -> V) (jdef : J) (idef : I) : - \big[+%M/GRing.zero V]_(j : #|I|.-tuple J) G (F [ffun x => tnth j (enum_rank x)]) (nth jdef j 0) - = \big[+%M/GRing.zero V]_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)). + \big[+%M/@GRing.zero V]_(j : #|I|.-tuple J) G (F [ffun x => tnth j (enum_rank x)]) (nth jdef j 0) + = \big[+%M/@GRing.zero V]_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)). Proof. rewrite (reindex_onto (fun y => fgraph y) (fun p => [ffun x => tnth p (enum_rank x)])); last first. move=> t _; by apply/eq_from_tnth => i; rewrite tnth_fgraph ffunE enum_valK. diff --git a/lib/dft.v b/lib/dft.v index 6c87b7e5..bea351fd 100644 --- a/lib/dft.v +++ b/lib/dft.v @@ -131,7 +131,8 @@ Proof. by rewrite /fdcoor linearZ /= hornerZ. Qed. Lemma fdcoorE y i : y ^`_ i = \sum_(j < n) (y ``_ j) * (u ``_ i) ^+ j. Proof. rewrite /fdcoor horner_poly; apply eq_bigr => j _; rewrite insubT //= => jn. -rewrite (_ : Ordinal jn = j) //; by apply/val_inj. +rewrite /Sub/= (_ : Ordinal jn = j) //. +exact/val_inj. Qed. End frequency_domain_coordinates. diff --git a/lib/euclid.v b/lib/euclid.v index b21b4eb5..06112170 100644 --- a/lib/euclid.v +++ b/lib/euclid.v @@ -126,7 +126,7 @@ transitivity ((- q k.+2 * v k.+1) * u k.+1 + v k * u k.+1 + rewrite mulrDl -3!addrA; congr (_ + (_ + _)). rewrite mulrDr opprD; congr (_ - _). by rewrite mulNr mulrN opprK. -rewrite exprS -IH mulNr mul1r opprD opprK [in RHS]addrC; congr (_ - _). +rewrite exprS -IH [in RHS]mulNr mul1r opprD opprK [in RHS]addrC; congr (_ - _). rewrite addrC addrA -[RHS]add0r; congr (_ + _). by rewrite mulrC -mulrA (mulrC (v k.+1)) mulrA 2!mulNr subrr. Qed. diff --git a/lib/hamming.v b/lib/hamming.v index b58a2e49..118d0fab 100644 --- a/lib/hamming.v +++ b/lib/hamming.v @@ -192,7 +192,7 @@ Qed. Section wH_num_occ_bitstring. -Lemma wH_col_1 n (i : 'I_n) : @wH [fieldType of 'F_2] _ (col i 1%:M)^T = 1%N. +Lemma wH_col_1 n (i : 'I_n) : @wH 'F_2 _ (col i 1%:M)^T = 1%N. Proof. rewrite wH_sum (bigD1 i) //= !mxE eqxx /= add1n (eq_bigr (fun=> O)). by rewrite big_const iter_addn mul0n. @@ -850,7 +850,7 @@ Lemma hamming_01 m p : (1 - p) ^ m + m%:R * p * (1 - p) ^ (m - 1). Proof. rewrite (bigID [pred i | wH i == O]) /=. -rewrite (big_pred1 (GRing.zero _)) /=; last first. +rewrite (big_pred1 (@GRing.zero _)) /=; last first. by move=> i /=; rewrite !inE -wH_eq0 andb_idl // => /eqP ->. rewrite wH0 pow_O subn0 mulR1; congr (_ + _). transitivity (\sum_(i | wH (i : 'rV['F_2]_m) == 1%nat) ((1 - p) ^ (m - 1) * p ^ 1)). diff --git a/lib/realType_ext.v b/lib/realType_ext.v index f6829473..7aebdc25 100644 --- a/lib/realType_ext.v +++ b/lib/realType_ext.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp Require Import reals normedtype. From mathcomp Require Import mathcomp_extra boolp. @@ -131,37 +132,31 @@ Definition mk_ (R : realType) (q : R) (Oq1 : (0 <= q <= 1)%R) := mk Oq1. Module Exports. Notation prob := t. Notation "q %:pr" := (@mk _ q (@O1 _ _)). -Canonical prob_subType (R : realType) := Eval hnf in [subType for @p R]. -Definition prob_eqMixin (R : realType) := [eqMixin of (prob R) by <:]. -Canonical prob_eqType (R : realType) := Eval hnf in EqType _ (prob_eqMixin R). +HB.instance Definition _ (R : realType) := [isSub for @p R]. +HB.instance Definition _ (R : realType) := [Choice of t R by <:]. End Exports. End Prob. Export Prob.Exports. Coercion Prob.p : prob >-> Real.sort. Lemma probpK R p H : Prob.p (@Prob.mk R p H) = p. Proof. by []. Qed. -Definition prob_of (R : realType) := - fun phT : phant (Num.NumDomain.sort (*Real.sort*)R) => @prob R. -Notation "{ 'prob' T }" := (@prob_of _ (Phant T)). +Notation "{ 'prob' T }" := (@prob T). -Definition to_porder (R : realType) (p : {prob R}) : Order.POrder.sort _ := - (p : R). -Coercion to_porder : prob_of >-> Order.POrder.sort. -Arguments to_porder /. +HB.instance Definition _ (R : realType) := [Order of {prob R} by <:]. Definition to_numdomain (R : realType) (p : {prob R}) : Num.NumDomain.sort _ := (p : R). -Coercion to_numdomain : prob_of >-> Num.NumDomain.sort. +Coercion to_numdomain : prob >-> Num.NumDomain.sort. Arguments to_numdomain /. Definition to_zmodule (R : realType) (p : {prob R}) : GRing.Zmodule.sort _ := (p : R). -Coercion to_zmodule : prob_of >-> GRing.Zmodule.sort. +Coercion to_zmodule : prob >-> GRing.Zmodule.sort. Arguments to_zmodule /. Definition to_ring (R : realType) (p : {prob R}) : GRing.Ring.sort _ := (p : R). -Coercion to_ring : prob_of >-> GRing.Ring.sort. +Coercion to_ring : prob >-> GRing.Ring.sort. Arguments to_ring /. Section prob_lemmas. @@ -252,9 +247,9 @@ End prob_lemmas. Global Hint Resolve prob_ge0 : core. Global Hint Resolve prob_le1 : core. -#[export] Hint Extern 0 (is_true (Prob.p _ <= 1)%R) => +#[export] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) => exact/prob_le1 : core. -#[export] Hint Extern 0 (is_true (0 <= Prob.p _)%R) => +#[export] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) => exact/prob_ge0 : core. Arguments prob0 {R}. @@ -275,9 +270,8 @@ End def. Module Exports. Notation oprob := t. Notation "q %:opr" := (@mk _ q%:pr (@O1 _ _)). -Canonical oprob_subType (R: realType) := Eval hnf in [subType for @p R]. -Definition oprob_eqMixin (R: realType) := [eqMixin of (oprob R) by <:]. -Canonical oprob_eqType (R : realType) := Eval hnf in EqType _ (oprob_eqMixin R). +HB.instance Definition _ (R : realType) := [isSub for @p R]. +HB.instance Definition _ (R : realType) := [Equality of t R by <:]. End Exports. End OProb. Export OProb.Exports. @@ -286,9 +280,7 @@ Canonical oprobcplt [R: realType] (p : oprob R) := Eval hnf in OProb.mk (onem_oprob (OProb.O1 p)). Reserved Notation "{ 'oprob' T }" (at level 0, format "{ 'oprob' T }"). -Definition oprob_of (R : realType) := - fun phT : phant (Num.NumDomain.sort R) => @oprob R. -Notation "{ 'oprob' T }" := (@oprob_of _ (Phant T)). +Notation "{ 'oprob' T }" := (@oprob T). Definition oprob_coercion (R: realType) (p : {oprob R}) : R := OProb.p p. Notation oprob_to_real o := (Prob.p (OProb.p o)). (*(R: realType) (o : {oprob R}) := Prob.p (OProb.p o).*) @@ -362,7 +354,7 @@ Proof. move=> p0; rewrite s_of_pqE; apply: onem_gt0. have [->/=|q0] := eqVneq q 0%:pr. by rewrite onem0 mulr1 onem_lt1// lt0r p0/=. -rewrite mulr_ilte1 => //. +rewrite mulr_ilte1 => //=. by rewrite onem_lt1// lt0r p0/=. by rewrite onem_lt1// lt0r q0/=. Qed. @@ -376,8 +368,7 @@ rewrite -lerBlDr. rewrite -opprB. rewrite lerNl opprK. rewrite -/(Prob.p p).~. -rewrite ler_piMr//. -by apply: onem_le1. +by rewrite ler_piMr. Qed. End s_of_pq_lemmas. diff --git a/lib/ssrR.v b/lib/ssrR.v index 76104f8c..7304d8a7 100644 --- a/lib/ssrR.v +++ b/lib/ssrR.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum. Require Import Reals. From mathcomp Require Import lra. @@ -913,7 +914,7 @@ Lemma bigmaxRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) : \rmax_(i <- r | P i) F i = \big[Order.max/0]_(i <- r | P i) F i. Proof. rewrite /Rmax /Order.max/=. -congr BigOp.bigop. +congr bigop.body. apply: boolp.funext=> i /=. congr BigBody. apply: boolp.funext=> x /=. diff --git a/lib/ssrZ.v b/lib/ssrZ.v index bf5eae8b..24dce60b 100644 --- a/lib/ssrZ.v +++ b/lib/ssrZ.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Import ZArith Lia. @@ -32,8 +33,7 @@ Local Open Scope zarith_ext_scope. Lemma eqZP : Equality.axiom Zeq_bool. Proof. by move=> x y; apply: (iffP idP) => H; apply/Zeq_is_eq_bool. Qed. -Canonical Z_eqMixin := EqMixin eqZP. -Canonical Z_eqType := Eval hnf in EqType Z Z_eqMixin. +HB.instance Definition _ := hasDecEq.Build Z eqZP. Arguments eqZP {x y}. diff --git a/lib/ssr_ext.v b/lib/ssr_ext.v index 10d72b64..90607d87 100644 --- a/lib/ssr_ext.v +++ b/lib/ssr_ext.v @@ -1078,3 +1078,27 @@ destruct boolP. by move=> x y; have:= Bool.bool_dec x y => -[]; [left | right]. Qed. End boolP. + +Section fintype_extra. + +Lemma index_enum_cast_ord n m (e : n = m) : + index_enum 'I_m = [seq cast_ord e i | i <- index_enum 'I_n]. +Proof. +subst m; rewrite -{1}(map_id (index_enum 'I_n)). +apply eq_map=> [[x xlt]]. +by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance. +Qed. + +Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f -> + perm_eq (index_enum T) [seq f i | i <- index_enum T]. +Proof. +rewrite /index_enum; case: index_enum_key => /= fbij. +rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. +case: fbij => g fg gf. +rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _ + (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))). + by rewrite size_filter enumP. +by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//]. +Qed. + +End fintype_extra. diff --git a/lib/ssralg_ext.v b/lib/ssralg_ext.v index 054c0266..c6b5920a 100644 --- a/lib/ssralg_ext.v +++ b/lib/ssralg_ext.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp. From mathcomp Require Import matrix mxalgebra vector. Require Import ssr_ext f2. @@ -474,7 +475,6 @@ Lemma full_rank_inj m n (A : 'M[F]_(m, n)) : m <= n -> \rank A = m -> Proof. move=> Hmn Hrank a b Hab. move: Hrank. -rewrite /mxrank. destruct m => //= [_|]. by rewrite (empty_rV a) (empty_rV b). destruct n => //=. @@ -487,9 +487,7 @@ have {}Hab : b *m col_ebase A *m pid_mx (\rank A) *m row_ebase A *m (invmx (row_ebase A)). by rewrite Hab. rewrite -!mulmxA mulmxV in Hab; last by exact: row_ebase_unit. -rewrite mulmx1 !mulmxA /mxrank /= in Hab. -unlock in Hab. -rewrite !Htmp in Hab. +rewrite !Htmp mulmx1 !mulmxA /mxrank /= in Hab. move: {Heq}(@pid_mx_inj _ _ _ (a *m col_ebase A) (b *m col_ebase A) Hmn Hab) => Heq. have {}Hab : a *m col_ebase A *m (invmx (col_ebase A)) = b *m col_ebase A *m (invmx (col_ebase A)) by rewrite Heq. @@ -614,9 +612,6 @@ case: ifPn => [/eqP -> /=|]; first by rewrite mul0r. rewrite -F2_eq1 => /eqP -> /=; by rewrite !mul1r. Qed. -Definition rmorphism_GF2_of_F2 : rmorphism GF2_of_F2. -Proof. split; [exact: additive_GF2_of_F2|exact: multiplicative_GF2_of_F2]. Qed. - Lemma GF2_of_F2_eq0 x : (GF2_of_F2 x == 0) = (x == 0). Proof. apply/idP/idP => [|/eqP -> //]. @@ -628,15 +623,15 @@ End GF2m. Arguments GF2_of_F2 [_] _. -Canonical GF2_of_F2_additive m := Additive (additive_GF2_of_F2 m). -Canonical GF2_of_F2_rmorphism m := RMorphism (rmorphism_GF2_of_F2 m). +HB.instance Definition _ m := GRing.isAdditive.Build _ _ (@GF2_of_F2 m) (additive_GF2_of_F2 m). +HB.instance Definition _ m := GRing.isMultiplicative.Build _ _ _ (multiplicative_GF2_of_F2 m). Definition F2_to_GF2 (m : nat) n (y : 'rV['F_2]_n) := map_mx (@GF2_of_F2 m) y. Lemma supp_F2_to_GF2 n m (e : 'rV['F_2]_n) : supp (F2_to_GF2 m e) = supp e. Proof. apply/setP => i; rewrite !inE !mxE; apply/idP/idP; apply: contra. - move/eqP => ->; by rewrite rmorph0. + by move/eqP => ->; rewrite /= rmorph0. by rewrite GF2_of_F2_eq0. Qed. diff --git a/meta.yml b/meta.yml index f456a6af..f7609c34 100644 --- a/meta.yml +++ b/meta.yml @@ -41,54 +41,46 @@ license: nix: true supported_coq_versions: - text: Coq 8.17 + text: Coq 8.17--8.19 opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }' tested_coq_opam_versions: -- version: '1.17.0-coq-8.17' +- version: '2.2.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.17' +- version: '2.2.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.19.0-coq-8.17' - repo: 'mathcomp/mathcomp' -- version: '1.17.0-coq-8.18' - repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.18' - repo: 'mathcomp/mathcomp' -- version: '1.19.0-coq-8.18' - repo: 'mathcomp/mathcomp' -- version: '1.19.0-coq-8.19' +- version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "0.6.6") & (< "0.8~")}' + version: '{ (>= "1.0.0") }' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: @@ -98,7 +90,7 @@ dependencies: [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - opam: name: coq-mathcomp-algebra-tactics - version: '{ = "1.1.1" }' + version: '{ >= "1.2.0" }' description: |- MathComp algebra tactics diff --git a/probability/bayes.v b/probability/bayes.v index 029b17e2..4d79586e 100644 --- a/probability/bayes.v +++ b/probability/bayes.v @@ -107,7 +107,7 @@ Section univ_types. (* heterogeneous types *) Variable n : nat. Variable types : 'I_n -> eqType. -Definition univ_types := [eqType of {dffun forall i, types i}]. +Definition univ_types : eqType := [eqType of {dffun forall i, types i}]. Section prod_types. (* sets of indices *) @@ -115,7 +115,7 @@ Variable I : {set 'I_n}. Definition prod_types := [eqType of - {dffun forall i : 'I_n, if i \in I then types i else unit_finType}]. + {dffun forall i : 'I_n, if i \in I then types i else unit}]. Lemma prod_types_app i (A B : prod_types) : A = B -> A i = B i. Proof. by move=> ->. Qed. diff --git a/probability/convex.v b/probability/convex.v index 811d84d2..1e602740 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -140,7 +140,7 @@ Local Open Scope fdist_scope. Import Order.POrderTheory GRing.Theory Num.Theory. -Local Notation "{ 'fdist' T }" := (fdist_of _ (Phant T)) : fdist_scope. +Local Notation "{ 'fdist' T }" := (_ .-fdist T) : fdist_scope. #[export] Hint Extern 0 (0 <= _)%coqR => solve [apply/RleP/(FDist.ge0 _)] : core. @@ -156,170 +156,33 @@ Local Notation "{ 'fdist' T }" := (fdist_of _ (Phant T)) : fdist_scope. #[export] Hint Extern 0 (0 <= onem _)%coqR => exact/RleP/onem_ge0 : core. -(* TODO: the following lemmas are currently not in use. Maybe remove? *) -Section tmp. -Local Open Scope ring_scope. - -Lemma fdist_convn_Add (R : realType) - (n m : nat) (d1 : {fdist 'I_n}) (d2 : {fdist 'I_m}) (p : {prob R}) - (A : finType) (g : 'I_n -> {fdist A}) (h : 'I_m -> {fdist A}) : - fdist_convn (fdist_add d1 d2 p) - [ffun i => match fintype.split i with inl a => g a | inr a => h a end] = - (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist. -Proof. -apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE. -rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _); - apply eq_bigr => i _; rewrite fdist_addE ffunE. -case: splitP => /= j ij. -rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj. -move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0. -case: splitP => /= j ij. -move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0. -move/eqP : ij; rewrite eqn_add2l => /eqP ij. -rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj. -Qed. - -Import realType_ext. -Lemma fdist_convn_del - (R : realType) - (A : finType) (n : nat) (g : 'I_n.+1 -> {fdist A}) (P : {fdist 'I_n.+1}) - (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) : - let g' := fun i : 'I_n => g (fdist_del_idx j i) in - fdist_convn P g = - (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist. -Proof. -move=> g' /=; apply/fdist_ext => a. -rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _). -rewrite fdist_convnE big_distrr /=. -rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=. -rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _). - rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW. - move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS. - move=> jn'. - apply/eq_big. - by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. - move=> /= i _. - rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first. - by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. - rewrite mulrA mulrCA mulrV ?mulr1; last first. -rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //. - congr (P _ * _); first exact/val_inj. - by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj. -rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first. - move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle. -rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first. - move=> i; by rewrite -leqNgt. -rewrite big_mkcond. -rewrite big_ord_recl ltn0 /= add0r. -rewrite [in RHS]big_mkcond. -apply eq_bigr => i _. -rewrite /bump add1n ltnS; case: ifPn => // ji. -rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first. - apply/eqP => /(congr1 val) => /=. - rewrite /bump add1n => ij. - by move: ji; apply/negP; rewrite -ij ltnn. - rewrite -mulrAC [in RHS]mulrC 3!mulrA divrr ?mul1r ?unitfE ?onem_neq0 //. -by rewrite /g' /fdist_del_idx ltnNge ji. -Qed. -End tmp. - -(* TODO: move*) -Section fintype_extra. - -Lemma index_enum_cast_ord n m (e : n = m) : - index_enum (ordinal_finType m) = [seq cast_ord e i | i <- index_enum (ordinal_finType n)]. -Proof. -subst m; rewrite -{1}(map_id (index_enum (ordinal_finType n))). -apply eq_map=> [[x xlt]]. -by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance. -Qed. - -Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f -> - perm_eq (index_enum T) [seq f i | i <- index_enum T]. -Proof. -rewrite /index_enum; case: index_enum_key => /= fbij. -rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. -case: fbij => g fg gf. -rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _ - (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))). - by rewrite size_filter enumP. -by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//]. -Qed. - -End fintype_extra. - -Module CodomDFDist. -Section def. -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. -Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A). -Variables (e : fdist_of R (Phant 'I_n)) (y : set A). -Definition f := [ffun i : 'I_n => if g i \in y then e i else 0]. -Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed. -Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) : - (\sum_(i < n) f i = 1). -Proof. -rewrite /f -(FDist.f1 e) /=. -apply eq_bigr => i _; rewrite ffunE. -case: ifPn => // /negP; rewrite in_setE => ygi. -rewrite ge //. -have : (x `|` y) (g i) by apply/gX; by exists i. -by case. -Qed. -Definition d (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) : {fdist 'I_n} := - locked (FDist.make f0 (f1 gX ge)). -Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) i : - d gX ge i = if g i \in y then e i else 0. -Proof. by rewrite /d; unlock; rewrite ffunE. Qed. -Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) : - (\sum_(i < n) f i = 1). -Proof. -rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE. -case: ifPn => // /negP; rewrite in_setE => giy. -rewrite ge //. -have : (x `|` y) (g i) by apply/gX; by exists i. -by case. -Qed. -Definition d' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) := - locked (FDist.make f0 (f1' gX ge)). -Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i : - d' gX ge i = if g i \in y then e i else 0. -Proof. by rewrite /d'; unlock; rewrite ffunE. Qed. -End def. -End CodomDFDist. -Module isConvexSpace_. +Fixpoint Convn (A : Type) (f : {prob R} -> A -> A -> A) 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 Bool.bool_dec (e ord0 == 1%coqR) true with + | left _ => g ord0 + | right H => let G := fun i => g (fdist_del_idx ord0 i) in + f (probfdist e ord0) (g ord0) (Convn f (fdist_del (Bool.eq_true_not_negb _ H)) G) + end + end. -HB.mixin Record isConvexSpace (T : Type) := { - convexspacechoiceclass : Choice.class_of T ; +HB.mixin Record isConvexSpace0 T of Choice T := { conv : {prob R} -> T -> T -> T ; + convn : forall n, {fdist 'I_n} -> ('I_n -> T) -> T ; + convnE : forall n d g, convn n d g = Convn conv d g ; conv1 : forall a b, conv 1%:pr a b = a ; convmm : forall p a, conv p a a = a ; convC : forall p a b, conv p a b = conv (onem (Prob.p p))%:pr b a ; convA : forall (p q : {prob R}) (a b c : T), conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c }. -#[short(type=convType)] -HB.structure Definition ConvexSpace := {T of isConvexSpace T }. -End isConvexSpace_. -Export -(coercions) isConvexSpace_. - -Coercion ConvexSpace.isConvexSpace__isConvexSpace_mixin : - ConvexSpace.axioms_ >-> isConvexSpace.axioms_. -Canonical conv_eqType (T : convType) := - Eval hnf in EqType (ConvexSpace.sort T) convexspacechoiceclass. -Canonical conv_choiceType (T : convType) := - Eval hnf in ChoiceType (ConvexSpace.sort T) convexspacechoiceclass. -Coercion conv_choiceType : convType >-> choiceType. +#[short(type=convType)] +HB.structure Definition ConvexSpace := {T of isConvexSpace0 T & }. +Arguments convn {s n}. Notation "a <| p |> b" := (conv p a b) : convex_scope. - Local Open Scope convex_scope. Section convex_space_lemmas. @@ -327,13 +190,71 @@ Variables A : convType. Implicit Types a b : A. Import Reals_ext. - Lemma conv0 a b : a <| 0%:pr |> b = b. Proof. by rewrite convC /= (_ : _ %:pr = 1%:pr) ?conv1 //; apply/val_inj/onem0. Qed. + +Let Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> A) : + convn (fdist1 j) g = g j. +Proof. +elim: n j g => [[] [] //|n IH j g /=]. +rewrite convnE {1}/Convn. +case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01]. + rewrite fdist1E; case j0 : (_ == _) => /=. + by move=> _; rewrite (eqP j0). + by move/eqP; rewrite eq_sym R1E oner_eq0. +rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last first. + apply val_inj => /=; move: b01; rewrite !fdist1E => j0. + by case j0' : (_ == _) => //; rewrite j0' eqxx in j0. +have j0 : ord0 != j by apply: contra b01 => /eqP <-; rewrite fdist1xx. +have j0' : 0 < j by rewrite lt0n; apply: contra j0 => /eqP j0; apply/eqP/val_inj. +move=> [:H]; have @j' : 'I_n. + by apply: (@Ordinal _ j.-1 _); abstract: H; rewrite prednK // -ltnS. +rewrite (_ : fdist_del b01 = fdist1 j'); last first. + apply/fdist_ext => /= k. + rewrite fdist_delE fdistD1E /= !fdist1E /= (negbTE j0) subr0 divr1. + congr (GRing.natmul _ (nat_of_bool _)). + move R : (k == _) => [|]. + - apply/eqP/val_inj; rewrite /= /bump leq0n add1n. + by move/eqP : R => -> /=; rewrite prednK // lt0n. + - apply: contraFF R => /eqP. + move/(congr1 val) => /=; rewrite /bump leq0n add1n => kj. + by apply/eqP/val_inj; rewrite /= -kj. +rewrite -/(Convn _ _) -convnE IH /fdist_del_idx ltn0; congr g. +by apply val_inj; rewrite /= /bump leq0n add1n prednK // lt0n. +Qed. + +Let ConvnIE n (g : 'I_n.+1 -> A) (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%coqR) : + convn d g = (g ord0) <| probfdist d ord0 |> + (convn (fdist_del i1) (fun x => g (fdist_del_idx ord0 x))). +Proof. +rewrite !convnE /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H. +exfalso; by rewrite (eqP H) eqxx in i1. +by rewrite (eq_irrelevance H i1). +Qed. + +Let ConvnI1E (g : 'I_1 -> A) (e : {fdist 'I_1}) : convn e g = g ord0. +Proof. +rewrite convnE /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H. +exfalso; move/eqP: H; apply. +by apply/eqP; rewrite fdist1E1 (fdist1I1 e). +Qed. + +Let ConvnI2E (g : 'I_2 -> A) (d : {fdist 'I_2}) : + convn d g = (g ord0) <| probfdist d ord0 |> (g (lift ord0 ord0)). +Proof. +have [/eqP|i1] := eqVneq (d ord0) 1%coqR. + rewrite fdist1E1 => /eqP ->; rewrite Convn_fdist1. + rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //. + by apply val_inj; rewrite /= fdist1xx. +rewrite ConvnIE; congr (conv _ _ _). +by rewrite ConvnI1E /fdist_del_idx ltnn. +Qed. + End convex_space_lemmas. + Section segment. Variable A : convType. Definition segment (x y : A) : set A := (fun p => conv p x y) @` [set: {prob R}]. @@ -351,20 +272,6 @@ Lemma segmentR x y : segment x y y. Proof. by exists 0%:pr; rewrite ?conv0. Qed. End segment. -Fixpoint Convn (A : convType) 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 Bool.bool_dec (e ord0 == 1%coqR) true with - | left _ => g ord0 - | right H => let G := fun i => g (fdist_del_idx ord0 i) in - g ord0 <| probfdist e ord0 |> Convn (fdist_del (Bool.eq_true_not_negb _ H)) G - end - end. - - -Notation "'<|>_' d f" := (Convn d f) : convex_scope. - Definition affine (U V : convType) (f : U -> V) := forall p, {morph f : a b / a <| p |> b >-> a <| p |> b}. @@ -450,14 +357,8 @@ Arguments point {A} pt. Arguments weight {A}. Notation "p *: a" := (Scaled p a) : scaled_scope. -Definition scaled_eqMixin (A : eqType) := CanEqMixin (@sum_of_scaledK A). -Canonical scaled_eqType (A : eqType) := - Eval hnf in EqType (scaled A) (@scaled_eqMixin A). -Definition scaled_choiceMixin (A : choiceType) := - CanChoiceMixin (@sum_of_scaledK A). -Canonical scaled_choiceType (A : choiceType) := - Eval hnf in ChoiceType (scaled A) (@scaled_choiceMixin A). -Canonical scaled_pointedType (A : choiceType) := PointedType _ (@Zero A). +HB.instance Definition _ (A : eqType) := Equality.copy (scaled A) (can_type (@sum_of_scaledK A)). +HB.instance Definition _ (A : choiceType) := Choice.copy (scaled A) (can_type (@sum_of_scaledK A)). Section scaled_eqType. Variable A : eqType. @@ -490,8 +391,7 @@ Notation "[ 'point' 'of' x ]" := (@point _ _ (@weight_gt0 _ _ x)) Notation "[ 'weight' 'of' x ]" := (weight_neq0 x) (at level 0, format "[ 'weight' 'of' x ]"). -HB.mixin Record isQuasiRealCone A := { - quasirealconechoiceclass : Choice.class_of A ; +HB.mixin Record isQuasiRealCone A of Choice A := { addpt : A -> A -> A ; zero : A ; addptC : commutative addpt ; @@ -505,13 +405,7 @@ HB.mixin Record isQuasiRealCone A := { scalept p (scalept q x) = scalept (p * q)%coqR x }. #[short(type=quasiRealCone)] -HB.structure Definition QuasiRealCone := { A & isQuasiRealCone A}. - -Canonical quasirealcone_eqType (T : quasiRealCone) := - Eval hnf in EqType (QuasiRealCone.sort T) quasirealconechoiceclass. -Canonical quasirealcone_choiceType (T : quasiRealCone) := - Eval hnf in ChoiceType (QuasiRealCone.sort T) quasirealconechoiceclass. -Coercion quasirealcone_choiceType : quasiRealCone >-> choiceType. +HB.structure Definition QuasiRealCone := { A of isQuasiRealCone A & }. Section quasireal_cone_theory. Variable A : quasiRealCone. @@ -524,8 +418,8 @@ Proof. by move=> p0; rewrite -[in LHS](scale0pt zero) scaleptA// mulR0 scale0pt. Qed. -Canonical addpt_monoid := Monoid.Law (@addptA A) add0pt addpt0. -Canonical addpt_comoid := Monoid.ComLaw (@addptC A). +HB.instance Definition _ := + Monoid.isComLaw.Build A (@zero A) (@addpt A) addptA addptC add0pt. Definition big_morph_scalept q := @big_morph _ _ (@scalept A q) zero addpt zero _ (@scaleptDr A q). @@ -563,12 +457,13 @@ Notation "\ssum_ ( i | P ) F" := (\big[addpt/@zero _]_(i | P) F). Notation "\ssum_ ( i < n | P ) F" := (\big[addpt/@zero _]_(i < n | P%B) F). Notation "\ssum_ ( i < n ) F" := (\big[addpt/@zero _]_(i < n) F). -HB.mixin Record isRealCone (A : Type) of isQuasiRealCone A := { - scaleptDl : forall p q x, (0 <= p)%coqR -> (0 <= q)%coqR -> - @scalept [the quasiRealCone of A] (p + q)%coqR x = addpt (scalept p x) (scalept q x) }. +HB.mixin Record isRealCone A of QuasiRealCone A := { + scaleptDl : forall (p q : R) (x : A), (0 <= p)%coqR -> (0 <= q)%coqR -> + scalept (p + q)%coqR x = addpt (scalept p x) (scalept q x) +}. #[short(type=realCone)] -HB.structure Definition RealCone := { A of isQuasiRealCone A & isRealCone A }. +HB.structure Definition RealCone := { A of isRealCone A & }. Section real_cone_theory. Variable A : realCone. @@ -586,8 +481,8 @@ Qed. Section barycenter_fdist_convn. Variables (n : nat) (B : finType). -Variable p : real_realType.-fdist 'I_n. -Variable q : 'I_n -> real_realType.-fdist B. +Variable p : R.-fdist 'I_n. +Variable q : 'I_n -> R.-fdist B. Variable h : B -> A. Lemma ssum_fdist_convn : @@ -684,9 +579,8 @@ case: x => [r x|]; rewrite ?scalept0 // !scalept_gt0; first exact: mulR_gt0. by move=> Hpq; congr (_ *: _); apply val_inj => /=; rewrite mulRA. Qed. -HB.instance Definition _ := @isQuasiRealCone.Build (scaled A) - (Choice.class (@scaled_choiceType A)) addpt Zero addptC' addptA' addpt0 - scalept scale0pt scale1pt scaleptDr scaleptA. +HB.instance Definition _ := + isQuasiRealCone.Build (scaled A) addptC' addptA' addpt0 scale0pt scale1pt scaleptDr scaleptA. Let scaleptDl p q x : 0 <= p -> 0 <= q -> scalept (p + q) x = addpt (scalept p x) (scalept q x). @@ -731,9 +625,10 @@ rewrite RmultE pq_is_rs mulrC -RmultE. by rewrite s_of_pqE onemK RmultE. Qed. -HB.instance Definition __cone := @isConvexSpace.Build (scaled A) - (Choice.class [the choiceType of scaled A]) convpt convpt1 convptmm convptC - convptA. +Let convn := Convn convpt. + +HB.instance Definition _ := + @isConvexSpace0.Build (scaled A) convpt convn (fun _ _ _ => erefl) convpt1 convptmm convptC convptA. Lemma convptE p (a b : scaled A) : a <| p |> b = convpt p a b. Proof. by []. Qed. @@ -812,6 +707,8 @@ End adjunction. End scaled_convex. +Notation "'<|>_' d f" := (Convn (@conv _) d f) : convex_scope. + Section convex_space_prop1. Variables T : convType. Implicit Types a b : T. @@ -825,16 +722,16 @@ have [r0|r0] := eqVneq r 0%:pr. rewrite r0 conv0 (_ : p = 0%:pr) ?conv0; last first. by apply/val_inj; rewrite /= H1 r0 mul0R. congr (_ <| _ |> _); move: H2; rewrite H1 r0 mul0R onem0 mul1R. - by move/(congr1 (@onem real_realType)); rewrite !onemK => ?; exact/val_inj. + by move/(congr1 (@onem R)); rewrite !onemK => ?; exact/val_inj. have [s0|s0] := eqVneq s 0%:pr. have p0 : p = 0%:pr by apply/val_inj; rewrite /= H1 s0 mulR0. rewrite s0 conv0 p0 // ?conv0. rewrite (_ : q = 0%:pr) ?conv0 //. - move: H2; rewrite p0 onem0 mul1R => /(congr1 (@onem real_realType)); rewrite !onemK => sq. + move: H2; rewrite p0 onem0 mul1R => /(congr1 (@onem R)); rewrite !onemK => sq. by rewrite -s0; exact/val_inj. rewrite convA; congr ((_ <| _ |> _) <| _ |> _). apply val_inj; rewrite /= s_of_pqE. - move/(congr1 (@onem real_realType)) : H2. + move/(congr1 (@onem R)) : H2. by rewrite onemK => ->. exact: (@r_of_pq_is_r _ _ _ _ s). Qed. @@ -1038,7 +935,7 @@ exfalso; by rewrite (eqP H) eqxx in i1. by rewrite (eq_irrelevance H i1). Qed. -Lemma ConvnI2E (g : 'I_2 -> T) (d : {fdist 'I_2}) : +Lemma ConvnI2E' (g : 'I_2 -> T) (d : {fdist 'I_2}) : <|>_d g = g ord0 <| probfdist d ord0 |> g (lift ord0 ord0). Proof. have [/eqP|i1] := eqVneq (d ord0) 1%coqR. @@ -1049,6 +946,105 @@ rewrite ConvnIE; congr (_ <| _ |> _). by rewrite ConvnI1E /fdist_del_idx ltnn. Qed. +Lemma ConvnI2E (g : 'I_2 -> T) (d : {fdist 'I_2}) : + convn d g = (g ord0) <| probfdist d ord0 |> (g (lift ord0 ord0)). +Proof. +have [/eqP|i1] := eqVneq (d ord0) 1%coqR. + rewrite fdist1E1 convnE => /eqP ->; rewrite Convn_fdist1. + rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //. + by apply val_inj; rewrite /= fdist1xx. +rewrite convnE ConvnIE; congr (conv _ _ _). +by rewrite ConvnI1E /fdist_del_idx ltnn. +Qed. +End convex_space_prop2. + +HB.factory Record isConvexSpace T of Choice T := { + conv : {prob R} -> T -> T -> T ; + conv1 : forall a b, conv 1%:pr a b = a ; + convmm : forall p a, conv p a a = a ; + convC : forall p a b, conv p a b = conv (onem (Prob.p p))%:pr b a ; + convA : forall (p q : {prob R}) (a b c : T), + conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c }. + +HB.builders Context T of isConvexSpace T. + +Definition convn := Convn conv. + +Let conv0 a b : conv 0%:pr a b = b. +Proof. +by rewrite convC /= (_ : _ %:pr = 1%:pr) ?conv1 //; apply/val_inj/onem0. +Qed. + +Let Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> T) : + convn (fdist1 j) g = g j. +Proof. +elim: n j g => [[] [] //|n IH j g /=]. +rewrite /convn {1}/Convn. +case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01]. + rewrite fdist1E; case j0 : (_ == _) => /=. + by move=> _; rewrite (eqP j0). + by move/eqP; rewrite eq_sym R1E oner_eq0. +rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last first. + apply val_inj => /=; move: b01; rewrite !fdist1E => j0. + by case j0' : (_ == _) => //; rewrite j0' eqxx in j0. +have j0 : ord0 != j by apply: contra b01 => /eqP <-; rewrite fdist1xx. +have j0' : 0 < j by rewrite lt0n; apply: contra j0 => /eqP j0; apply/eqP/val_inj. +move=> [:H]; have @j' : 'I_n. + by apply: (@Ordinal _ j.-1 _); abstract: H; rewrite prednK // -ltnS. +rewrite (_ : fdist_del b01 = fdist1 j'); last first. + apply/fdist_ext => /= k. + rewrite fdist_delE fdistD1E /= !fdist1E /= (negbTE j0) subr0 divr1. + congr (GRing.natmul _ (nat_of_bool _)). + move R : (k == _) => [|]. + - apply/eqP/val_inj; rewrite /= /bump leq0n add1n. + by move/eqP : R => -> /=; rewrite prednK // lt0n. + - apply: contraFF R => /eqP. + move/(congr1 val) => /=; rewrite /bump leq0n add1n => kj. + by apply/eqP/val_inj; rewrite /= -kj. +rewrite -/Convn. +rewrite -/convn. +rewrite IH /fdist_del_idx ltn0; congr g. +by apply val_inj; rewrite /= /bump leq0n add1n prednK // lt0n. +Qed. + +Let ConvnIE n (g : 'I_n.+1 -> T) (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%coqR) : + convn d g = conv (probfdist d ord0) (g ord0) + (convn (fdist_del i1) (fun x => g (fdist_del_idx ord0 x))). +Proof. +rewrite /convn /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H. +exfalso; by rewrite (eqP H) eqxx in i1. +by rewrite (eq_irrelevance H i1). +Qed. + +Let ConvnI1E (g : 'I_1 -> T) (e : {fdist 'I_1}) : convn e g = g ord0. +Proof. +rewrite /convn /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H. +exfalso; move/eqP: H; apply. +by apply/eqP; rewrite fdist1E1 (fdist1I1 e). +Qed. + +Let ConvnI2E : forall (g : 'I_2 -> T) (d : {fdist 'I_2}), + convn d g = conv (probfdist d ord0) (g ord0) (g (lift ord0 ord0)). +Proof. +move=> g d. +have [/eqP|i1] := eqVneq (d ord0) 1%coqR. + rewrite fdist1E1 => /eqP ->. + rewrite Convn_fdist1. + rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //. + by apply val_inj; rewrite /= fdist1xx. +rewrite ConvnIE; congr conv. +by rewrite ConvnI1E /fdist_del_idx ltnn. +Qed. + +HB.instance Definition _ := @isConvexSpace0.Build T + conv convn (fun _ _ _ => erefl) conv1 convmm convC convA. + +HB.end. + +Section convex_space_prop3. +Variables T U : convType. +Implicit Types a b : T. + (* ref: M.H.Stone, postulates for the barycentric calculus, lemma 2 *) Lemma Convn_perm (n : nat) (d : {fdist 'I_n}) (g : 'I_n -> T) (s : 'S_n) : <|>_d g = <|>_(fdistI_perm d s) (g \o s). @@ -1127,7 +1123,7 @@ congr addpt; apply: congr_big => //= i _; rewrite scaleptA// fdist_addE. by have := ltn_ord j; by rewrite -nij -ltn_subRL subnn. Qed. -End convex_space_prop2. +End convex_space_prop3. Section hull_def. Local Open Scope classical_set_scope. @@ -1189,6 +1185,84 @@ Qed. End hull_prop. +Module ErealConvex. +Section ereal_convex. +Local Open Scope ereal_scope. + +Let conv_ereal (p : {prob R}) x y := (Prob.p p : R)%:E * x + (Prob.p p).~%:E * y. + +Let conv_ereal_conv1 a b : conv_ereal 1%:pr a b = a. +Proof. by rewrite /conv_ereal probpK onem1 /= mul1e mul0e adde0. Qed. + +Let conv_ereal_convmm p a : conv_ereal p a a = a. +Proof. +rewrite /conv_ereal; case/boolP : (a \is a fin_num) => [?|]. + by rewrite -muleDl// -EFinD probKC mul1e. +rewrite fin_numE negb_and !negbK => /predU1P[-> | /eqP->]. +- rewrite -ge0_muleDl. + + by rewrite -EFinD probKC mul1e. + + by rewrite lee_fin; apply/prob_ge0. + + by rewrite lee_fin; apply/prob_ge0. +- rewrite -ge0_muleDl. + + by rewrite -EFinD probKC mul1e. + + by rewrite lee_fin; apply/prob_ge0. + + by rewrite lee_fin; apply/prob_ge0. +Qed. + +Let conv_ereal_convC p a b : conv_ereal p a b = conv_ereal ((Prob.p p).~)%:pr b a. +Proof. by rewrite [in RHS]/conv_ereal onemK addeC. Qed. + +Lemma oprob_sg1 (p : {oprob R}) : Num.sg (oprob_to_real p) = 1%mcR. +Proof. +have /andP[] := OProb.O1 p; move=> /[swap] _. rewrite -sgr_cp0. +by move/eqP. +Qed. + +Let conv_ereal_convA (p q: {prob R}) a b c : + conv_ereal p a (conv_ereal q b c) = + conv_ereal [s_of p, q] (conv_ereal [r_of p, q] a b) c. +Proof. +rewrite /conv_ereal. +apply (prob_trichotomy' p); + [ by rewrite s_of_0q r_of_0q !mul0e !add0e !onem0 !mul1e + | by rewrite s_of_1q r_of_1q !mul1e !onem1 !mul0e !adde0 + | rewrite {p}=> p]. +apply (prob_trichotomy' q); + [ by rewrite s_of_p0 Reals_ext.r_of_p0_oprob onem1 onem0 mul0e !mul1e add0e adde0 + | by rewrite s_of_p1 r_of_p1 onem1 !mul1e mul0e !adde0 + | rewrite {q}=> q]. +have sgp := oprob_sg1 p. +have sgq := oprob_sg1 q. +have sgonemp := oprob_sg1 (Prob.p (OProb.p p)).~%:opr. +have sgonemq := oprob_sg1 (Prob.p (OProb.p q)).~%:opr. +have sgrpq := oprob_sg1 [r_of OProb.p p, OProb.p q]%:opr. +have sgspq := oprob_sg1 [s_of OProb.p p, OProb.p q]%:opr. +have sgonemrpq := oprob_sg1 (Prob.p [r_of OProb.p p, OProb.p q]).~%:opr. +have sgonemspq := oprob_sg1 (Prob.p [s_of OProb.p p, OProb.p q]).~%:opr. +Ltac mulr_infty X := do ! (rewrite mulr_infty X mul1e). +set sg := (sgp,sgq,sgonemp,sgonemq,sgrpq,sgspq,sgonemrpq,sgonemspq). +case: a=> [a | | ]; case: b=> [b | | ]; case: c=> [c | | ]; + try by mulr_infty sg. +rewrite muleDr // addeA. +congr (_ + _)%E; last by rewrite s_of_pqE onemK EFinM muleA. +rewrite muleDr //. +congr (_ + _)%E. + by rewrite (p_is_rs (OProb.p p) (OProb.p q)) mulrC EFinM muleA. +rewrite muleA -!EFinM. +rewrite (pq_is_rs (OProb.p p) (OProb.p q)). +rewrite mulrA. +by rewrite (mulrC (Prob.p [r_of OProb.p p, OProb.p q]).~). +Qed. + +#[export] HB.instance Definition _ := @isConvexSpace.Build (\bar R) conv_ereal conv_ereal_conv1 conv_ereal_convmm conv_ereal_convC conv_ereal_convA. + +Lemma conv_erealE p (a b : \bar R) : a <| p |> b = conv_ereal p a b. +Proof. by []. Qed. + +End ereal_convex. +End ErealConvex. +HB.export ErealConvex. + (* Convex sets in a convex space *) Section is_convex_set. @@ -1258,6 +1332,18 @@ Qed. End is_convex_set. +(* TODO: +Record ConvexSet (A : convType) := { convset_set :> set A ; _ : is_convex_set convset_set }. +HB.instance Definition _ A := [isSub of ConvexSet A for @convset_set A ]. +*) +HB.mixin Record isConvexSet (A : convType) (X : set A) := { is_convex : is_convex_set X }. +HB.structure Definition ConvexSet A := { X of isConvexSet A X }. +Notation "{ 'convex_set' T }" := (ConvexSet.type T) : convex_scope. + +Canonical cset_predType A := Eval hnf in + PredType (fun t : {convex_set A} => (fun x => x \in ConvexSet.sort t)). + +(* Module CSet. Section cset. Variable A : convType. @@ -1286,16 +1372,19 @@ Canonical cset_predType := Eval hnf in Canonical cset_eqType := Equality.Pack (@gen_eqMixin (convex_set A)). Canonical cset_choiceType := choice_of_Type (convex_set A). End cset_canonical. +*) + +HB.instance Definition _ A := @gen_eqMixin {convex_set A}. Section CSet_interface. Variable (A : convType). Implicit Types X Y : {convex_set A}. Lemma convex_setP X : is_convex_set X. -Proof. by case: X => X []. Qed. +Proof. by case: X => X [[]] /=. Qed. Lemma cset_ext X Y : X = Y :> set _ -> X = Y. Proof. -move: X Y => -[X HX] [Y HY] /= ?; subst Y. -congr (CSet.Pack _); exact/Prop_irrelevance. +move: X Y => -[X [[HX]]] [Y [[HY]]] /= ?; subst Y. +do! [f_equal]; exact/Prop_irrelevance. Qed. End CSet_interface. @@ -1308,32 +1397,30 @@ Implicit Types x y : scaled A. Lemma mem_convex_set a1 a2 p X : a1 \in X -> a2 \in X -> a1 <|p|> a2 \in X. Proof. -case: X => X [convX]; move: (convX) => convX_save. -move/asboolP : convX => convX Hx Hy. -by rewrite in_setE; apply: convX; rewrite -in_setE. +have /asboolP C := @is_convex A X. +by rewrite !inE; apply: C. Qed. -Definition cset0 : {convex_set A} := CSet.Pack (CSet.Mixin (is_convex_set0 A)). +HB.instance Definition _ := isConvexSet.Build A set0 (is_convex_set0 A). -Lemma cset0P X : (X == cset0) = (X == set0 :> set _). +Lemma cset0P X : (X == set0) = (X == set0 :> set _). Proof. case: X => x [Hx] /=; apply/eqP/eqP => [-[] //| ?]; subst x; exact: cset_ext. Qed. -Lemma cset0PN X : X != cset0 <-> X !=set0. +Lemma cset0PN X : X != set0 <-> X !=set0. Proof. rewrite cset0P; case: X => //= x Hx; split; last first. case=> a xa; apply/eqP => x0; move: xa; by rewrite x0. by case/set0P => /= d dx; exists d. Qed. -Definition cset1 a : {convex_set A} := CSet.Pack (CSet.Mixin (is_convex_set1 a)). +HB.instance Definition _ a := isConvexSet.Build A [set a] (is_convex_set1 a). -Lemma cset1_neq0 a : cset1 a != cset0. +Lemma cset1_neq0 a : [set a] != set0 :> {convex_set A}. Proof. by apply/cset0PN; exists a. Qed. -Definition convex_set_of_segment (x y : A) : convex_set A := - CSet.Pack (CSet.Mixin (segment_is_convex x y)). +HB.instance Definition _ x y := isConvexSet.Build _ (segment x y) (segment_is_convex x y). End CSet_prop. @@ -1366,15 +1453,16 @@ by rewrite fdist_convn_add; congr (_ <| _ |> _); apply eq_Convn => i //=; rewrite ffunE (split_lshift,split_rshift). Qed. -Canonical hull_is_convex_set (Z : set A) : convex_set A := - CSet.Pack (CSet.Mixin (hull_is_convex Z)). +HB.instance Definition _ (Z : set A) := isConvexSet.Build _ (hull Z) (hull_is_convex Z). Lemma segment_hull (x y : A) : segment x y = hull [set x; y]. Proof. rewrite eqEsubset; split. by have := hull_is_convex [set x; y] => /is_convex_segmentP/(_ x y); apply; apply subset_hull; [left | right]. -pose h := convex_set_of_segment x y. +(* BUG in HB: HB.pack only accepts types as subjects + pose h : {convex_set A} := HB.pack _ (isConvexSet.Build _ _ (segment_is_convex x y)).*) +pose h : {convex_set A} := @ConvexSet.Pack _ _ (@ConvexSet.Class _ _ (isConvexSet.Build _ _ (segment_is_convex x y))). by have := @hull_sub_convex [set x; y] h; apply => z -[] ->; [exact: segmentL|exact: segmentR]. Qed. @@ -1389,7 +1477,9 @@ Implicit Types X Y Z : set A. Lemma is_convex_hullE X : is_convex_set X = (hull X == X). Proof. apply/idP/idP => [conv|/eqP <-]; last exact: hull_is_convex. -exact/eqP/(hull_cset {| CSet.car := X; CSet.class := CSet.Mixin conv |}). +(* BUG in HB *) +pose X' : {convex_set A} := @ConvexSet.Pack _ _ (@ConvexSet.Class _ _ (isConvexSet.Build _ _ conv)). +exact/eqP/(hull_cset X'). Qed. Lemma hull_eqEsubset X Y : @@ -1554,6 +1644,7 @@ Qed. End split_prod. +Module LmoduleConvex. Section lmodR_convex_space. Variable E : lmodType R. Implicit Type p q : {prob R}. @@ -1590,17 +1681,18 @@ have ->: (Prob.p p).~ * Prob.p q = ((Prob.p p).~ * Prob.p q)%coqR by []. by rewrite RmultE pq_is_rs -/r -/s mulrC. Qed. -HB.instance Definition _ := - @isConvexSpace.Build E (Choice.class _) avg avg1 avgI avgC avgA. +#[non_forgetful_inheritance] HB.instance Definition _ := + isConvexSpace.Build E avg1 avgI avgC avgA. Lemma avgrE p (x y : E) : x <| p |> y = avg p x y. Proof. by []. Qed. - End lmodR_convex_space. +End LmoduleConvex. Section lmodR_convex_space_prop. Variable E : lmodType R. Implicit Type p q : {prob R}. Local Open Scope ring_scope. +Import LmoduleConvex. Lemma avgr_addD p (a b c d : E) : (a + b) <|p|> (c + d) = (a <|p|> c) + (b <|p|> d). @@ -1619,7 +1711,7 @@ by move=> x ? ?; rewrite 2!avgrE scalerDr !scalerA; congr +%R; congr (_ *: _); Qed. Lemma avgr_scalerDl p : - left_distributive *:%R (fun x y : GRing.regular_lmodType R_ringType => x <|p|> y). + left_distributive *:%R (fun x y : (R^o : lmodType R) => x <|p|> y). Proof. by move=> x ? ?; rewrite avgrE scalerDl -2!scalerA. Qed. (* Introduce morphisms to prove avgnE *) @@ -1730,17 +1822,18 @@ Import ssrnum vector. Variable E : vectType R. Local Open Scope ring_scope. Local Open Scope classical_set_scope. +Import LmoduleConvex. (* TODO: move? *) Import Order.TotalTheory. -Lemma caratheodory (A : set (Vector.lmodType E)) x : x \in hull A -> - exists (n : nat) (g : 'I_n -> Vector.lmodType E) (d : {fdist 'I_n}), - [/\ (n <= (dimv (@fullv R_fieldType E)).+1)%nat, range g `<=` A & x = <|>_d g]. +Lemma caratheodory (A : set (E : lmodType R)) x : x \in hull A -> + exists (n : nat) (g : 'I_n -> (E : lmodType R)) (d : {fdist 'I_n}), + [/\ (n <= (dimv (@fullv R E)).+1)%nat, range g `<=` A & x = <|>_d g]. Proof. move=> /set_mem[n [g [d [gA ->]]]]. elim: n => [|n IHn] in g d gA *; first by case: (fdistI0_False d). -have [nsgt|nsgt] := leqP n (dimv (@fullv R_fieldType E)). +have [nsgt|nsgt] := leqP n (dimv (@fullv R E)). by exists n.+1, g, d. have [mu [muR muE [i mui]]] : exists mu : 'I_n.+1 -> R, [/\ \sum_(i < n.+1) mu i = 0, \sum_(i < n.+1) (mu i) *: g i = 0 & @@ -1786,17 +1879,17 @@ wlog: g d gA mu muR muE im muip muim / (im == ord0)%N. by move=>y [i _ <-]; apply gA; eexists. move=>/(_ gA' (fun i => mu (f' i))). have mu'R : \sum_(i0 < n.+1) mu (f' i0) = 0. - rewrite (perm_big _ (perm_map_bij _ fbij)); [| exact nil ]. - by rewrite big_map -{4}muR; apply congr_big=>// [[j jlt]] _; congr mu; apply fcan'. + rewrite (perm_big _ (perm_map_bij _ fbij)) /=; [| exact nil ]. + by rewrite big_map -[in RHS]muR; apply congr_big=>// [[j jlt]] _; congr mu; apply fcan'. move=>/(_ mu'R). have mu'E: \sum_(i0 < n.+1) mu (f' i0) *: g (f' i0) = 0. - rewrite (perm_big _ (perm_map_bij _ fbij)); [| exact nil ]. - rewrite big_map -{4}muE; apply congr_big=>// j _. + rewrite (perm_big _ (perm_map_bij _ fbij)) /=; [| exact nil ]. + rewrite big_map -[in RHS]muE; apply congr_big=>// j _. by congr (mu _ *: g _); exact/fcan'. move=>/(_ mu'E (f' im)). have muip' : 0 < mu (f' (f' im)) by rewrite fcan'. move=>/(_ muip'). - have muim' (j : ordinal_finType n.+1) : + have muim' (j : 'I_n.+1) : 0 < mu (f' j) -> fdistmap f' d (f' im) / mu (f' (f' im)) <= fdistmap f' d j / mu (f' j). move=> /muim. @@ -1843,22 +1936,26 @@ Qed. End caratheodory. +Module LinearAffine. Section linear_affine. Open Scope ring_scope. Variables (E F : lmodType R) (f : {linear E -> F}). - +Import LmoduleConvex. Let linear_is_affine: affine f. Proof. by move=>p x y; rewrite linearD 2!linearZZ. Qed. -HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine. +#[export] HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine. End linear_affine. +End LinearAffine. +HB.export LinearAffine. (* TOTHINK: Should we keep this section, only define R_convType, or something else ? *) +Module RConvex. Section R_convex_space. Implicit Types p q : {prob R}. - -Let avg p (a b : [the lmodType R of R^o]) := a <| p |> b. +Import LmoduleConvex. +Let avg p (a b : (R^o : lmodType R)) := a <| p |> b. Let avgE p a b : avg p a b = (Prob.p p * a + (Prob.p p).~ * b)%coqR. Proof. by []. Qed. @@ -1873,16 +1970,17 @@ Let avgA p q (d0 d1 d2 : R) : avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2. Proof. by rewrite /avg convA. Qed. -HB.instance Definition _ := @isConvexSpace.Build R - (Choice.class _) _ avg1 avgI avgC avgA. +#[export] +(* TODO(rei): attribute needed? *) +(*#[non_forgetful_inheritance]*) HB.instance Definition _ := @isConvexSpace.Build R _ avg1 avgI avgC avgA. Lemma avgRE p (x y : R) : x <| p |> y = (Prob.p p * x + (Prob.p p).~ * y)%coqR. Proof. by []. Qed. Lemma avgR_oppD p x y : (- x <| p |> - y = - (x <| p |> y))%coqR. -Proof. exact: (@avgr_oppD [lmodType R of R^o]). Qed. +Proof. exact: (@avgr_oppD R^o). Qed. Lemma avgR_mulDr p : right_distributive Rmult (fun x y => x <| p |> y). -Proof. exact: (@avgr_scalerDr [lmodType R of R^o]). Qed. +Proof. exact: (@avgr_scalerDr R^o). Qed. Lemma avgR_mulDl p : left_distributive Rmult (fun x y => x <| p |> y). Proof. exact: @avgr_scalerDl. Qed. @@ -1922,12 +2020,17 @@ by apply eq_bigr => i _; rewrite scaleR_scalept // Scaled1RK. Qed. End R_convex_space. +End RConvex. +HB.export RConvex. +Module FunConvexSpace. Section fun_convex_space. Variables (A : choiceType) (B : convType). -Let T := A -> B. +Definition funT := A -> B. +Local Notation T := funT. +HB.instance Definition _ := Choice.on T. Implicit Types p q : {prob R}. -Let avg p (x y : T) := fun a : A => (x a <| p |> y a). +Definition avg p (x y : T) := fun a : A => (x a <| p |> y a). Let avg1 (x y : T) : avg 1%:pr x y = x. Proof. rewrite funeqE => a; exact/conv1. Qed. Let avgI p (x : T) : avg p x x = x. @@ -1937,13 +2040,15 @@ Proof. rewrite funeqE => a; exact/convC. Qed. Let avgA p q (d0 d1 d2 : T) : avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2. Proof. move=> *; rewrite funeqE => a; exact/convA. Qed. -HB.instance Definition _ := @isConvexSpace.Build T (Choice.class _) _ - avg1 avgI avgC avgA. +#[export] HB.instance Definition _ := @isConvexSpace.Build T avg avg1 avgI avgC avgA. End fun_convex_space. +End FunConvexSpace. +HB.export FunConvexSpace. +Module DepfunConvexSpace. Section depfun_convex_space. Variables (A : choiceType) (B : A -> convType). -Let T := dep_arrow_choiceType B. +Let T := forall x : A, B x. Implicit Types p q : {prob R}. Let avg p (x y : T) := fun a : A => (x a <| p |> y a). Let avg1 (x y : T) : avg 1%:pr x y = x. @@ -1968,10 +2073,14 @@ move => *. apply FunctionalExtensionality.functional_extensionality_dep => a. exact/convA. Qed. -HB.instance Definition _ := @isConvexSpace.Build _ (Choice.class _) - _ avg1 avgI avgC avgA. + +#[export] HB.instance Definition _ := isConvexSpace.Build (forall x : A, B x) avg1 avgI avgC avgA. + End depfun_convex_space. +End DepfunConvexSpace. +HB.export DepfunConvexSpace. +Module PairConvexSpace. Section pair_convex_space. Variables (A B : convType). Let T := (A * B)%type. @@ -1987,14 +2096,16 @@ Let avgA p q (d0 d1 d2 : T) : avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2. Proof. move => *; congr (pair _ _); by apply convA. Qed. -HB.instance Definition _ := - @isConvexSpace.Build T (Choice.class _) avg avg1 avgI avgC avgA. +#[export] HB.instance Definition _ := + isConvexSpace.Build (A * B)%type avg1 avgI avgC avgA. End pair_convex_space. +End PairConvexSpace. +HB.export PairConvexSpace. Section fdist_convex_space. Variable A : finType. -Implicit Types a b c : real_realType.-fdist A. +Implicit Types a b c : R.-fdist A. Let conv1 a b : (a <| 1%:pr |> b)%fdist = a. Proof. @@ -2017,7 +2128,7 @@ Proof. apply/fdist_ext => a0 /=; rewrite 4!fdist_convE /=. set r := r_of_pq p q. set s := s_of_pq p q. transitivity (Prob.p p * a a0 + (Prob.p p).~ * Prob.p q * b a0 + (Prob.p p).~ * (Prob.p q).~ * c a0). - by rewrite /onem /=; lra. + by rewrite mulrDr !mulrA !addrA. transitivity (Prob.p r * Prob.p s * a a0 + (Prob.p r).~ * Prob.p s * b a0 + (Prob.p s).~ * c a0); last first. by rewrite 2!(mulrC _ (Prob.p s)) -2!mulrA -mulrDr. rewrite -!RmultE. @@ -2026,14 +2137,13 @@ congr (_ + _ + _); by rewrite !RmultE pq_is_rs. Qed. -HB.instance Definition _ := @isConvexSpace.Build (real_realType.-fdist A) - (Choice.class (choice_of_Type (real_realType.-fdist A))) - (@fdist_conv _ A) conv1 convmm convC convA. +HB.instance Definition _ := isConvexSpace.Build (R.-fdist A) conv1 convmm convC convA. + End fdist_convex_space. Section scaled_convex_lemmas_depending_on_T_convType. Local Open Scope R_scope. - +Import RConvex. Lemma scalept_conv (T : convType) (x y : R) (s : scaled T) (p : {prob R}): 0 <= x -> 0 <= y -> scalept (x <|p|> y) s = scalept x s <|p|> scalept y s. @@ -2087,7 +2197,7 @@ Module Convn_finType. Section def. Local Open Scope ring_scope. -Variables (A : convType) (T : finType) (d' : real_realType.-fdist T) (f : T -> A). +Variables (A : convType) (T : finType) (d' : R.-fdist T) (f : T -> A). Let n := #| T |. Definition t0 : T. @@ -2103,7 +2213,7 @@ Lemma d_enum0 : forall b, 0 <= d_enum b. Proof. by move=> ?; rewrite ffunE. Qed. Lemma d_enum1 : \sum_(b in 'I_n) d_enum b = 1. Proof. -rewrite -(@FDist.f1 real_realType T d') (eq_bigr (d' \o enum)); last by move=> i _; rewrite ffunE. +rewrite -(@FDist.f1 R T d') (eq_bigr (d' \o enum)); last by move=> i _; rewrite ffunE. rewrite (@reindex _ _ _ _ _ enum_rank) //; last first. by exists enum_val => i; [rewrite enum_rankK | rewrite enum_valK]. apply eq_bigr => i _; congr (d' _); by rewrite -[in RHS](enum_rankK i). @@ -2121,7 +2231,7 @@ End Convn_finType. Export Convn_finType.Exports. Section S1_Convn_finType. -Variables (A : convType) (T : finType) (d : real_realType.-fdist T) (f : T -> A). +Variables (A : convType) (T : finType) (d : R.-fdist T) (f : T -> A). Lemma S1_Convn_finType : S1 (<$>_d f) = \ssum_i scalept (d i) (S1 (f i)). Proof. @@ -2136,7 +2246,7 @@ End S1_Convn_finType. Section S1_proj_Convn_finType. Variables (A B : convType) (prj : {affine A -> B}). -Variables (T : finType) (d : real_realType.-fdist T) (f : T -> A). +Variables (T : finType) (d : R.-fdist T) (f : T -> A). Lemma S1_proj_Convn_finType : S1 (prj (<$>_d f)) = \ssum_i scalept (d i) (S1 (prj (f i))). @@ -2144,8 +2254,12 @@ Proof. by rewrite Convn_comp; exact: S1_Convn_finType. Qed. End S1_proj_Convn_finType. -HB.mixin Record isOrdered (T : Type) := { - orderedchoiceclass : Choice.class_of T ; +(*Check convex_isConvexSpace__to__convex_isConvexSpace0.*) +(*convex_isConvexSpace__to__convex_isConvexSpace0 + : forall (A : choiceType) (B : convType), + isConvexSpace0.axioms_ (A -> B) (HB_unnamed_mixin_131 A B) (HB_unnamed_mixin_130 A B)*) + +HB.mixin Record isOrdered T of Choice T := { leconv : T -> T -> Prop ; leconvR : forall a, leconv a a; leconv_trans : forall b a c, leconv a b -> leconv b c -> leconv a c ; @@ -2154,17 +2268,14 @@ HB.mixin Record isOrdered (T : Type) := { #[short(type=orderedConvType)] HB.structure Definition OrderedConvexSpace := {T of isOrdered T & ConvexSpace T}. -Canonical ordered_eqType (T : orderedConvType) := EqType T orderedchoiceclass. -Canonical ordered_choiceType (T : orderedConvType) := - ChoiceType T orderedchoiceclass. - Arguments leconv_trans {s b a c}. Notation "x <= y" := (leconv x y) : ordered_convex_scope. Notation "x <= y <= z" := (leconv x y /\ leconv y z) : ordered_convex_scope. +Import RConvex. HB.instance Definition _ := - @isOrdered.Build R (Choice.class _) Rle Rle_refl leR_trans eqR_le. + isOrdered.Build R Rle_refl leR_trans eqR_le. Module FunLe. Section lefun. @@ -2193,33 +2304,28 @@ Section fun_ordered_convex_space. Variables (T : convType) (U : orderedConvType). Import FunLe. -HB.instance Definition _ := @isOrdered.Build (T -> U) - (Choice.class _) (@lefun T U) (@lefunR T U) (@lefun_trans T U) (@eqfun_le T U). +HB.instance Definition _ := isOrdered.Build (T -> U) (@lefunR T U) (@lefun_trans T U) (@eqfun_le T U). End fun_ordered_convex_space. + Module OppositeOrderedConvexSpace. Section def. Variable A : orderedConvType. -CoInductive T := mkOpp : A -> T. +CoInductive oppT := mkOpp : A -> oppT. Lemma A_of_TK : cancel (fun t => let: mkOpp a := t in a) mkOpp. Proof. by case. Qed. -Definition A_of_T_eqMixin := CanEqMixin A_of_TK. - -Canonical A_of_T_eqType := Eval hnf in EqType T A_of_T_eqMixin. - -Definition A_of_T_choiceMixin := CanChoiceMixin A_of_TK. +HB.instance Definition _ := Choice.copy oppT (can_type A_of_TK). -Canonical A_of_T_choiceType := Eval hnf in ChoiceType T A_of_T_choiceMixin. End def. Section leopp. Local Open Scope ordered_convex_scope. Variable A : orderedConvType. -Notation T := (T A). +Notation T := (oppT A). Definition leopp (x y : T) := match (x, y) with (mkOpp x', mkOpp y') => y' <= x' end. @@ -2240,7 +2346,7 @@ End leopp. Section convtype. Local Open Scope convex_scope. Variable A : orderedConvType. -Notation T := (T A). +Notation T := (oppT A). Implicit Types p q : {prob R}. Definition unbox (x : T) := match x with mkOpp x' => x' end. @@ -2261,8 +2367,7 @@ Lemma avgA p q d0 d1 d2 : Proof. by case d0;case d1;case d2=>d2' d1' d0';rewrite/avg/unbox/=convA. Qed. #[export] -HB.instance Definition _ := @isConvexSpace.Build T (Choice.class _) _ - avg1 avgI avgC avgA. +HB.instance Definition _ := isConvexSpace.Build T avg1 avgI avgC avgA. End convtype. End OppositeOrderedConvexSpace. @@ -2272,8 +2377,7 @@ Section opposite_ordered_convex_space. Import OppositeOrderedConvexSpace. Variable A : orderedConvType. -HB.instance Definition _ := @isOrdered.Build (T A) - (Choice.class _) (@leopp A) (@leoppR A) (@leopp_trans A) (@eqopp_le A). +HB.instance Definition _ := isOrdered.Build (oppT A) (@leoppR A) (@leopp_trans A) (@eqopp_le A). End opposite_ordered_convex_space. @@ -2291,11 +2395,12 @@ Proof. by []. Qed. Lemma unboxK (a : A) : unbox (\opp{a}) = a. Proof. reflexivity. Qed. -Lemma leoppP (a b : T A) : a <= b <-> unbox b <= unbox a. +Lemma leoppP (a b : oppT A) : a <= b <-> unbox b <= unbox a. Proof. by case a;case b=>*;rewrite !unboxK. Qed. End opposite_ordered_convex_space_prop. + Section convex_function_def. Local Open Scope ordered_convex_scope. Variables (T : convType) (U : orderedConvType). @@ -2403,9 +2508,10 @@ End definition. Section counterexample. Local Open Scope R_scope. +Import RConvex. Example biconvex_is_not_convex_in_both : - exists f : R -> R -> R, biconvex_function f /\ ~ convex_in_both f. + exists f : R -> R -> R, @biconvex_function R R R f /\ ~ convex_in_both f. Proof. exists Rmult; split. by split => [a b0 b1 t | b a0 a1 t]; @@ -2636,30 +2742,33 @@ Section linear_function_image. Local Open Scope classical_set_scope. Local Open Scope ring_scope. Variables (T U : lmodType R). - +Import LmoduleConvex. (* TODO: find how to speak about multilinear maps. *) Lemma hull_add (A B : set T) : hull [set a + b | a in A & b in B] = [set a + b | a in hull A & b in hull B]. Proof. rewrite eqEsubset; split. -- have conv : is_convex_set [set a + b | a in hull A & b in hull B]. +set xx := [set a + b | a in hull A & b in hull B]. +- have conv : is_convex_set xx. apply/asboolP=>x y p [ax axA] [bx bxB] <- [ay ayA] [by' byB] <-. rewrite avgr_addD; exists (ax <|p|> ay). by move: (hull_is_convex A)=>/asboolP; apply. exists (bx <|p|> by')=>//. by move: (hull_is_convex B)=>/asboolP; apply. - apply (@hull_sub_convex _ _ (CSet.Pack (CSet.Mixin conv))), image2_subset; - exact (@subset_hull _ _). -- move=>x [a [na [ga [da [gaA ->]]]]] [b [nb [gb [db [gbB ->]]]]] <-. - rewrite avgnr_add. - exists (na * nb)%nat, - (fun i => let (i, j) := split_prod i in ga i + gb j), - (fdistmap (unsplit_prod (n:=nb)) da `x db); split=>// y [i _ <-]. - by case: split_prod=>ia ib; exists (ga ia); [by apply gaA; exists ia |]; - exists (gb ib)=>//; apply gbB; exists ib. -Qed. - + pose xx' : {convex_set T} := @ConvexSet.Pack T xx (@ConvexSet.Class _ _ (isConvexSet.Build _ _ conv)). + apply: (@hull_sub_convex _ _ xx'). + by apply/image2_subset; exact (@subset_hull _ _). +move=>x [a [na [ga [da [gaA ->]]]]] [b [nb [gb [db [gbB ->]]]]] <-. +rewrite avgnr_add. +exists (na * nb)%nat, + (fun i => let (i, j) := split_prod i in ga i + gb j), + (fdistmap (unsplit_prod (n:=nb)) da `x db); split=>// y [i _ <-]. +by case: split_prod => ia ib; exists (ga ia); [by apply gaA; exists ia |]; + exists (gb ib)=>//; apply gbB; exists ib. +Qed. + +Import LinearAffine. Proposition preimage_preserves_convex_hull (f : {linear T -> U}) (Z : set U) : Z `<=` range f -> f @^-1` (hull Z) = hull (f @^-1` Z). Proof. @@ -2686,7 +2795,7 @@ Qed. End R_affine_function_prop. Section convex_function_in_def. -Variables (T : convType) (U : orderedConvType) (D : convex_set T) (f : T -> U). +Variables (T : convType) (U : orderedConvType) (D : {convex_set T}) (f : T -> U). Definition convex_function_in := forall a b p, a \in D -> b \in D -> convex_function_at f a b p. @@ -2720,7 +2829,9 @@ TODO: see convex_type.v Section convex_set_R. -Lemma Rpos_convex : is_convex_set (fun x => 0 < x)%coqR. +Definition Rpos_interval : set R := (fun x => 0 < x)%coqR. + +Lemma Rpos_convex : is_convex_set Rpos_interval. Proof. apply/asboolP => x y t Hx Hy. have [->|Ht0] := eqVneq t 0%:pr; first by rewrite conv0. @@ -2728,12 +2839,16 @@ apply addR_gt0wl; first by apply mulR_gt0 => //; exact/RltP/prob_gt0. apply mulR_ge0 => //; exact: ltRW. Qed. -Definition Rpos_interval : {convex_set R} := CSet.Pack (CSet.Mixin Rpos_convex). +(*#[local]*) +HB.instance Definition _ := isConvexSet.Build R Rpos_interval Rpos_convex. -Lemma Rnonneg_convex : is_convex_set (fun x => 0 <= x)%coqR. +Definition Rnonneg_interval : set R := (fun x => 0 <= x)%coqR. + +Lemma Rnonneg_convex : is_convex_set Rnonneg_interval. Proof. apply/asboolP=> x y t Hx Hy; apply addR_ge0; exact/mulR_ge0. Qed. -Definition Rnonneg_interval := CSet.Pack (CSet.Mixin Rnonneg_convex). +(*#[local]*) +HB.instance Definition _ := isConvexSet.Build R Rnonneg_interval Rnonneg_convex. Lemma open_interval_convex a b (Hab : (a < b)%coqR) : is_convex_set (fun x => a < x < b)%coqR. @@ -2752,10 +2867,12 @@ rewrite mulrDl. apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1]. Qed. -Lemma open_unit_interval_convex : is_convex_set (fun x => 0 < x < 1)%coqR. +Definition uniti : set R := (fun x => 0 < x < 1)%coqR. + +Lemma open_unit_interval_convex : is_convex_set uniti. Proof. exact: open_interval_convex. Qed. -Definition open_unit_interval := CSet.Pack (CSet.Mixin open_unit_interval_convex). +HB.instance Definition _ := isConvexSet.Build R uniti open_unit_interval_convex. End convex_set_R. @@ -2955,79 +3072,3 @@ by apply/mulR_ge0; rewrite subR_ge0; exact/ltRW. Qed. End twice_derivable_convex. - -Section ereal_convex. -Local Open Scope ereal_scope. - -Let conv_ereal (p : {prob R}) x y := (Prob.p p : R)%:E * x + (Prob.p p).~%:E * y. - -Let conv_ereal_conv1 a b : conv_ereal 1%:pr a b = a. -Proof. by rewrite /conv_ereal probpK onem1 /= mul1e mul0e adde0. Qed. - -Let conv_ereal_convmm p a : conv_ereal p a a = a. -Proof. -rewrite /conv_ereal; case/boolP : (a \is a fin_num) => [?|]. - by rewrite -muleDl// -EFinD probKC mul1e. -rewrite fin_numE negb_and !negbK => /predU1P[-> | /eqP->]. -- rewrite -ge0_muleDl. - + by rewrite -EFinD probKC mul1e. - + by rewrite lee_fin; apply/prob_ge0. - + by rewrite lee_fin; apply/prob_ge0. -- rewrite -ge0_muleDl. - + by rewrite -EFinD probKC mul1e. - + by rewrite lee_fin; apply/prob_ge0. - + by rewrite lee_fin; apply/prob_ge0. -Qed. - -Let conv_ereal_convC p a b : conv_ereal p a b = conv_ereal ((Prob.p p).~)%:pr b a. -Proof. by rewrite [in RHS]/conv_ereal onemK addeC. Qed. - -Lemma oprob_sg1 (p : {oprob R}) : Num.sg (oprob_to_real p) = 1%mcR. -Proof. -have /andP[] := OProb.O1 p; move=> /[swap] _. rewrite -sgr_cp0. -by move/eqP. -Qed. - -Let conv_ereal_convA (p q: {prob R}) a b c : - conv_ereal p a (conv_ereal q b c) = - conv_ereal [s_of p, q] (conv_ereal [r_of p, q] a b) c. -Proof. -rewrite /conv_ereal. -apply (prob_trichotomy' p); - [ by rewrite s_of_0q r_of_0q !mul0e !add0e !onem0 !mul1e - | by rewrite s_of_1q r_of_1q !mul1e !onem1 !mul0e !adde0 - | rewrite {p}=> p]. -apply (prob_trichotomy' q); - [ by rewrite s_of_p0 Reals_ext.r_of_p0_oprob onem1 onem0 mul0e !mul1e add0e adde0 - | by rewrite s_of_p1 r_of_p1 onem1 !mul1e mul0e !adde0 - | rewrite {q}=> q]. -have sgp := oprob_sg1 p. -have sgq := oprob_sg1 q. -have sgonemp := oprob_sg1 (Prob.p (OProb.p p)).~%:opr. -have sgonemq := oprob_sg1 (Prob.p (OProb.p q)).~%:opr. -have sgrpq := oprob_sg1 [r_of OProb.p p, OProb.p q]%:opr. -have sgspq := oprob_sg1 [s_of OProb.p p, OProb.p q]%:opr. -have sgonemrpq := oprob_sg1 (Prob.p [r_of OProb.p p, OProb.p q]).~%:opr. -have sgonemspq := oprob_sg1 (Prob.p [s_of OProb.p p, OProb.p q]).~%:opr. -Ltac mulr_infty X := do ! (rewrite mulr_infty X mul1e). -set sg := (sgp,sgq,sgonemp,sgonemq,sgrpq,sgspq,sgonemrpq,sgonemspq). -case: a=> [a | | ]; case: b=> [b | | ]; case: c=> [c | | ]; - try by mulr_infty sg. -rewrite muleDr // addeA. -congr (_ + _)%E; last by rewrite s_of_pqE onemK EFinM muleA. -rewrite muleDr //. -congr (_ + _)%E. - by rewrite (p_is_rs (OProb.p p) (OProb.p q)) mulrC EFinM muleA. -rewrite muleA -!EFinM. -rewrite (pq_is_rs (OProb.p p) (OProb.p q)). -rewrite mulrA. -by rewrite (mulrC (Prob.p [r_of OProb.p p, OProb.p q]).~). -Qed. - -HB.instance Definition _ := @isConvexSpace.Build (\bar R) (Choice.class _) _ - conv_ereal_conv1 conv_ereal_convmm conv_ereal_convC conv_ereal_convA. - -Lemma conv_erealE p (a b : \bar R) : a <| p |> b = conv_ereal p a b. -Proof. by []. Qed. - -End ereal_convex. diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index 01ebc90a..065798f6 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -39,19 +39,15 @@ Local Open Scope convex_scope. Module NaryConvexSpace. -HB.mixin Record isNaryConv (T : Type) := { - narychoice : Choice.class_of T ; +HB.mixin Record isNaryConv (T : Type) of Choice T := { convn : forall n, {fdist 'I_n} -> ('I_n -> T) -> T }. #[short(type=naryConvType)] -HB.structure Definition NaryConv := {T & isNaryConv T}. +HB.structure Definition NaryConv := {T of isNaryConv T &}. Notation "'<&>_' d f" := (convn _ d f) : convex_scope. -Canonical naryconv_eqType (T : naryConvType) := EqType T narychoice. -Canonical conv_choiceType (T : naryConvType) := ChoiceType T narychoice. - End NaryConvexSpace. Module NaryConvexSpaceEquiv. @@ -60,70 +56,6 @@ Import NaryConvexSpace. (* In this module we use funext to avoid explicitly handling the congruence of convn (cf. eq_convn in convex_choice.v for the iterated version). *) -(* These definitions about distributions should probably be elsewhere *) -Definition fdistE := - (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE). - -Module FDistPart. -Section fdistpart. -Local Open Scope fdist_scope. -Variables (n m : nat) (K : 'I_m -> 'I_n) (e : {fdist 'I_m}) (i : 'I_n). - -Definition d := (fdistX (e `X (fun j => fdist1 (K j)))) `(| i). -Definition den := (fdistX (e `X (fun j => fdist1 (K j))))`1 i. - -Lemma denE : den = fdistmap K e i. -Proof. -rewrite /den !fdistE [RHS]big_mkcond /=. -under eq_bigl do rewrite inE. -apply/eq_bigr => a _. -rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=; - last by case=> x y; rewrite /swap /= !xpair_eqE andbC. -rewrite eq_sym 2!inE. -by case: eqP => // _; rewrite (mulr0,mulr1). -Qed. - -Lemma dE j : fdistmap K e i != 0%coqR -> - d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR. -Proof. -rewrite -denE => NE. -rewrite jfdist_condE // {NE} /jcPr /proba.Pr. -rewrite (big_pred1 (j,i)); last first. - by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE. -rewrite (big_pred1 i); last by move=> k; rewrite !inE. -rewrite !fdistE big_mkcond [in RHS]big_mkcond /=. -rewrite -RmultE -INRE. -congr (_ / _)%R. -under eq_bigr => k do rewrite {2}(surjective_pairing k). -rewrite -(pair_bigA _ (fun k l => - if l == i - then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l) - else R0))%R /=. -apply eq_bigr => k _. -rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym. -by case: ifP; rewrite (mulr1,mulr0). -Qed. -End fdistpart. - -Lemma dK n m K (e : {fdist 'I_m}) j : - e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R. -Proof. -under eq_bigr => /= a _. - have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R. - rewrite Ka0 mul0R. - have <- : (e j * (a == K j)%:R = 0)%R. - have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0. - move: Ka0; rewrite fdistE /=. - by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym. - over. - rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1; - last by rewrite fdistE in Ka0. -over. -move=> /=. -rewrite (bigD1 (K j)) //= eqxx mulR1. -by rewrite big1 ?addR0 // => i /negbTE ->; rewrite mulR0. -Qed. -End FDistPart. Section Axioms. Variable T : naryConvType. @@ -183,10 +115,10 @@ Module Type ConvSpace. Axiom T : convType. End ConvSpace. Module BinToNary(C : ConvSpace) <: NaryConvSpace. Import NaryConvexSpace. -HB.instance Definition _ := @isNaryConv.Build _ (Choice.class _) (@Convn C.T). +HB.instance Definition _ := @isNaryConv.Build C.T (@Convn C.T conv). (* NB: is that ok? *) -Definition T : naryConvType := Choice_sort__canonical__NaryConvexSpace_NaryConv. +Definition T : naryConvType := C.T. Definition axbary := @Convn_fdist_convn C.T. Definition axproj := @Convn_fdist1 C.T. End BinToNary. @@ -264,7 +196,7 @@ rewrite /binconv. set g := fun i : 'I_3 => if i <= 0 then a else if i <= 1 then b else c. rewrite [X in <&>_(fdistI2 q) X](_ : _ = g \o lift ord0); last first. by apply funext => i; case/orP: (ord2 i) => /eqP ->. -rewrite [X in <&>_(_ [r_of p, q]) X](_ : _ = g \o (widen_ord (leqnSn 2))); last first. +rewrite [X in <&>_(fdistI2 [r_of p, q]) X](_ : _ = g \o (widen_ord (leqnSn 2))); last first. by apply funext => i; case/orP: (ord2 i) => /eqP ->. rewrite 2!axmap. set d1 := fdistmap _ _. @@ -298,29 +230,18 @@ Qed. Lemma binconvmm p a : binconv p a a = a. Proof. by apply axidem => i; case: ifP. Qed. -#[export] -HB.instance Definition _ := @isConvexSpace.Build A.T (Choice.class _) binconv +HB.instance Definition _ := @isConvexSpace.Build A.T binconv binconv1 binconvmm binconvC binconvA. End NaryToBin. +(*HB.export NaryToBin. +Error: Anomaly "Uncaught exception Not_found." +Please report at http://coq.inria.fr/bugs/. +*) (* Then prove BinToN and NToBin cancel each other: operations should coincide on both sides *) -Module Equiv1(C : ConvSpace). -Module A := BinToNary(C). -Module B := NaryToBin(A). -Import A B. - -Lemma equiv_conv p (a b : T) : a <| p |> b = a <& p &> b. -Proof. -apply: S1_inj. -rewrite [LHS](@affine_conv NaryConv_sort__canonical__isConvexSpace__ConvexSpace)/=. -by rewrite [RHS](@affine_conv NaryConv_sort__canonical__isConvexSpace__ConvexSpace). -Qed. - -End Equiv1. - Module Equiv2(A : NaryConvSpace). Module B := NaryToBin(A). Import A B. @@ -352,8 +273,48 @@ apply/eqP => /(congr1 (Rplus (d ord0))). rewrite addRCA addRN !addR0 => b'. by elim b; rewrite -b' eqxx. Qed. + +(* +Lemma equiv_conv p x y : x <& p &> y = x <| p |> y. +Proof. +rewrite /binconv. +set g := fun (o : 'I_2) => if o == ord0 then x else y. +set d := fdistI2 p. +change x with (g ord0). +change y with (g (lift ord0 ord0)). +have -> : p = probfdist d ord0 by apply: val_inj=> /=; rewrite fdistI2E eqxx. +by rewrite -ConvnI2E -equiv_convn. +Qed. +*) + End Equiv2. +Module Equiv1(C : ConvSpace). +Module A := BinToNary(C). +Module B := NaryToBin(A). +Module EA := Equiv2(A). +Import A B. + +Let equiv_convn n (d : {fdist 'I_n}) (g : 'I_n -> A.T) : <&>_d g = <|>_d g. +Proof. by []. Qed. + +Let T' := NaryConv_sort__canonical__convex_ConvexSpace. + +Lemma equiv_conv p (a b : C.T) : a <| p |> b = a <& p &> b. +Proof. +change (a <& p &> b) with (@conv T' p a b). +pose g := fun (x : 'I_2) => if x == ord0 then a else b. +change a with (g ord0). +change b with (g (lift ord0 ord0)). +pose d := fdistI2 p. +have -> : p = probfdist d ord0 by apply: val_inj=> /=; rewrite fdistI2E eqxx. +rewrite -!ConvnI2E. +rewrite convnE -equiv_convn. +by rewrite EA.equiv_convn. +Qed. + +End Equiv1. + Module Type MapConst. Parameter T : naryConvType. Parameter axmap : ax_map T. @@ -568,15 +529,15 @@ Qed. Lemma axbary : ax_bary T. Proof. move=> n m d e g. -set f : 'I_n * 'I_m -> 'I_#|[finType of 'I_n * 'I_m]| := enum_rank. -set f' : 'I_#|[finType of 'I_n * 'I_m]| -> 'I_n * 'I_m := enum_val. +set f : 'I_n * 'I_m -> 'I_#|{: 'I_n * 'I_m}| := enum_rank. +set f' : 'I_#|{: 'I_n * 'I_m}| -> 'I_n * 'I_m := enum_val. set h := fun k i => f (k, i). set h' := fun i => snd (f' i). rewrite (_ : (fun i => _) = (fun i => <&>_(fdistmap (h i) (e i)) (g \o h'))); last first. apply funext => i. have {1}-> : g = (g \o h') \o h i. - apply funext => j; by rewrite /h' /h /= /f' /f enum_rankK. + by apply funext => j; rewrite /h' /h /= /f' /f enum_rankK. rewrite axinjmap //. by move=> x y; rewrite /h => /enum_rank_inj []. rewrite axbarypart; first last. diff --git a/probability/convex_stone.v b/probability/convex_stone.v index dbe54591..e4c28d35 100644 --- a/probability/convex_stone.v +++ b/probability/convex_stone.v @@ -211,7 +211,7 @@ by move /(@perm_inj _ s)/lift_inj. Qed. Lemma swap_asaE n (s : 'S_n.+2) (K : s ord0 != ord0) : - s = (lift_perm ord0 ord0 (PermDef.perm (swap_asa_inj K)) * tperm (ord0) (s ord0))%g. + s = (lift_perm ord0 ord0 (perm (swap_asa_inj K)) * tperm (ord0) (s ord0))%g. Proof. apply/permP => i. rewrite [in RHS]permE /=. @@ -549,7 +549,7 @@ Qed. Lemma Convn_perm_1 n (d : {fdist 'I_n}) (g : 'I_n -> A) : <|>_d g = <|>_(fdistI_perm d 1%g) (g \o (1%g : 'S_n)). Proof. -rewrite fdistI_perm1; congr (Convn d _). +rewrite fdistI_perm1; congr (Convn _ d _). by rewrite boolp.funeqE => i /=; rewrite perm1. Qed. @@ -707,6 +707,8 @@ congr (_ <| _ |> _). rewrite s_of_pqE /= /onem. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. rewrite -R1E -!RminusE -!RdivE'// -!RmultE. + set tmp1 := d _. + set tmp2 := d _. field. split; first by rewrite subR_eq0; exact/nesym. rewrite -addR_opp oppRB -addR_opp oppRB addRC addRA subRK. @@ -719,6 +721,8 @@ congr (_ <| _ |> _). rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. rewrite -[RHS]RdivE'. rewrite -R1E -!RminusE -!RdivE' // -!RmultE. + set tmp1 := d _. + set tmp2 := d _. field. split. rewrite subR_eq0. @@ -879,7 +883,7 @@ Lemma Convn_perm_projection n (d : {fdist 'I_n.+2}) Proof. transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdist_del dmax1) (fun x => g (fdist_del_idx ord0 x)))). by rewrite convnE. -set s' : 'S_n.+1 := PermDef.perm (Sn.proj0_inj H). +set s' : 'S_n.+1 := perm (Sn.proj0_inj H). transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))). by rewrite -IH. transitivity (g (s ord0) <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))). @@ -995,7 +999,7 @@ pose G : 'I_3 -> A := [eta (fun=>g ord0) with ord0 |-> g ord0, lift ord0 ord0 |-> g (lift ord0 ord0), ord_max |-> <|>_(fdist_del H1) (fun i : 'I_n.+1 => g (lift ord0 (lift ord0 i)))]. -transitivity (Convn D G). +transitivity (Convn conv D G). erewrite convn3E. rewrite convnE. congr (_ <| _ |> _). @@ -1123,7 +1127,9 @@ apply/fdist_ext => a. rewrite fdist_convE fdist_convnE /= big_ord_recl; congr (_ + _)%coqR. rewrite IH fdist_convnE big_distrr /=; apply eq_bigr => i _. rewrite fdist_delE fdistD1E eq_sym (negbTE (neq_lift _ _)). -by rewrite mulrAC mulrC !mulrA mulrV ?mul1r //; exact/onem_neq0. +rewrite mulrAC mulrC -!mulrA; congr (_ * _)%mcR. +rewrite /fdist_del_idx ltn0 /onem mulVr ?mulr1//. +exact/onem_neq0. Qed. End convn_convnfdist. diff --git a/probability/fdist.v b/probability/fdist.v index eca6a780..b90b3b96 100644 --- a/probability/fdist.v +++ b/probability/fdist.v @@ -1,5 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg fingroup perm matrix. From mathcomp Require Import all_algebra vector reals normedtype. From mathcomp Require Import mathcomp_extra boolp. @@ -133,17 +134,15 @@ End Exports. End FDist. Export FDist.Exports. Coercion FDist.f : fdist >-> finfun_of. -Canonical fdist_subType R A := Eval hnf in [subType for @FDist.f R A]. -Definition fdist_eqMixin R A := [eqMixin of fdist R A by <:]. -Canonical fdist_eqType R A := Eval hnf in EqType _ (fdist_eqMixin R A). + +HB.instance Definition _ R A := [isSub for @FDist.f R A]. +HB.instance Definition _ R A := [Choice of fdist R A by <:]. #[global] Hint Extern 0 (is_true (0 <= _)%R) => solve [exact: FDist.ge0] : core. #[global] Hint Extern 0 (is_true (_ <= 1)%R) => solve [exact: FDist.le1] : core. -Definition fdist_of (R : realType) (A : finType) := - fun phT : phant (Finite.sort A) => fdist R A. -Notation "R '.-fdist' T" := (fdist_of R (Phant T)) : fdist_scope. -Notation "{ 'fdist' T }" := (fdist_of real_realType (Phant T)) : fdist_scope. +Notation "R '.-fdist' T" := (fdist R T%type) : fdist_scope. +Notation "{ 'fdist' T }" := (fdist Rdefinitions.R T%type) : fdist_scope. Lemma fdist_ge0_le1 (R : numDomainType) (A : finType) (d : fdist R A) a : (0 <= d a <= 1)%R. @@ -764,8 +763,7 @@ rewrite (bigID (pred1 j)) /= [X in _ = X + _](_ : _ = 0) ?add0r; last first. rewrite (big_pred1 j). by rewrite /D fdistD1E eqxx. by move=> /= i; rewrite -leqNgt andbC andb_idr // => /eqP ->. -rewrite [in RHS]big_mkcond big_ord_recl. -set X := (X in _ = GRing.add_monoid R _ X). +rewrite [in RHS]big_mkcond big_ord_recl /=. rewrite /= -leqNgt leqn0 eq_sym andbN add0r. rewrite big_mkcond; apply eq_bigr => i _. rewrite -2!leqNgt andbC eq_sym -ltn_neqAle ltnS. @@ -784,7 +782,7 @@ End fdist_del. Section fdist_belast. Local Open Scope ring_scope. Variable R : realType. -Variables (n : nat) (P : fdist_of R (Phant 'I_n.+1)) (Pmax_neq1 : P ord_max != 1). +Variables (n : nat) (P : fdist R 'I_n.+1) (Pmax_neq1 : P ord_max != 1). Let D : R.-fdist 'I_n.+1 := fdistD1 Pmax_neq1. @@ -1073,7 +1071,7 @@ Section fdistX_prop. Local Open Scope ring_scope. Variable T : realType. Variables (A B : finType) (P : fdist T A) (Q : fdist T B) - (R S : fdist_of T (Phant (A * B))). + (R S : T .-fdist (A * B)). Lemma fdistXI : fdistX (fdistX R) = R. Proof. by rewrite /fdistX fdistmap_comp swapK fdistmap_id. Qed. @@ -1090,10 +1088,17 @@ Qed. End fdistX_prop. +Section fdistX_prop_ext. Lemma fdistX_prod2 {R: realType} (A B : finType) (P : fdist R A) (W : A -> fdist R B) : (fdistX (P `X W))`2 = P. Proof. by rewrite fdistX2 fdist_prod1. Qed. +End fdistX_prop_ext. + +Section fdist_prop_ext. +Definition fdistE := + (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE). +End fdist_prop_ext. Section fdist_rV. Local Open Scope ring_scope. @@ -1172,7 +1177,7 @@ End wolfowitz_counting. Section fdist_prod_of_rV. Local Open Scope ring_scope. Variable R : realType. -Variables (A : finType) (n : nat) (P : fdist_of R (Phant 'rV[A]_n.+1)). +Variables (A : finType) (n : nat) (P : R .-fdist 'rV[A]_n.+1). Let f (v : 'rV[A]_n.+1) : A * 'rV[A]_n := (v ord0 ord0, rbehead v). @@ -1374,7 +1379,7 @@ Lemma fdist_takeE i v : fdist_take i v = \sum_(w in 'rV[A]_(n - i)) P (castmx (erefl, subnKC (ltnS' (ltn_ord i))) (row_mx v w)). Proof. rewrite fdistmapE /=. -rewrite (@reindex_onto _ _ _ [finType of 'rV[A]_n] [finType of 'rV[A]_(n - i)] +rewrite (@reindex_onto _ _ _ 'rV[A]_n 'rV[A]_(n - i) (fun w => castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w)) (@row_drop A n i)) /=; last first. move=> w wv; apply/rowP => j. @@ -1857,3 +1862,119 @@ Defined. *) End tuple_prod_cast.*) + +(* TODO: the following lemmas are currently not in use. Maybe remove? *) +Section moved_from_convex. +Local Open Scope ring_scope. + +Lemma fdist_convn_Add (R : realType) + (n m : nat) (d1 : R.-fdist 'I_n) (d2 : R.-fdist 'I_m) (p : {prob R}) + (A : finType) (g : 'I_n -> R.-fdist A) (h : 'I_m -> R.-fdist A) : + fdist_convn (fdist_add d1 d2 p) + [ffun i => match fintype.split i with inl a => g a | inr a => h a end] = + (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist. +Proof. +apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE. +rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _); + apply eq_bigr => i _; rewrite fdist_addE ffunE. +case: splitP => /= j ij. +rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj. +move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0. +case: splitP => /= j ij. +move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0. +move/eqP : ij; rewrite eqn_add2l => /eqP ij. +rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj. +Qed. + +Import realType_ext. +Lemma fdist_convn_del + (R : realType) + (A : finType) (n : nat) (g : 'I_n.+1 -> R.-fdist A) (P : R.-fdist 'I_n.+1) + (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) : + let g' := fun i : 'I_n => g (fdist_del_idx j i) in + fdist_convn P g = + (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist. +Proof. +move=> g' /=; apply/fdist_ext => a. +rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _). +rewrite fdist_convnE big_distrr /=. +rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=. +rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _). + rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW. + move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS. + move=> jn'. + apply/eq_big. + by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. + move=> /= i _. + rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first. + by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. + rewrite mulrA mulrCA mulrV ?mulr1; last first. +rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //. + congr (P _ * _); first exact/val_inj. + by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj. +rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first. + move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle. +rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first. + move=> i; by rewrite -leqNgt. +rewrite big_mkcond. +rewrite big_ord_recl ltn0 /= add0r. +rewrite [in RHS]big_mkcond. +apply eq_bigr => i _. +rewrite /bump add1n ltnS; case: ifPn => // ji. +rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first. + apply/eqP => /(congr1 val) => /=. + rewrite /bump add1n => ij. + by move: ji; apply/negP; rewrite -ij ltnn. +rewrite -[1 - P j]/(P j).~. +rewrite [_ / _]mulrC !mulrA divrr ?unitfE ?onem_neq0 // mul1r. +by rewrite /g' /fdist_del_idx ltnNge ji. +Qed. +End moved_from_convex. + + +Module CodomDFDist. +Import classical_sets. +Section def. +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A). +Variables (e : R .-fdist 'I_n) (y : set A). +Definition f := [ffun i : 'I_n => if g i \in y then e i else 0]. +Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed. +Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) : + (\sum_(i < n) f i = 1). +Proof. +rewrite /f -(FDist.f1 e) /=. +apply eq_bigr => i _; rewrite ffunE. +case: ifPn => // /negP; rewrite in_setE => ygi. +rewrite ge //. +have : (x `|` y) (g i) by apply/gX; by exists i. +by case. +Qed. +Definition d (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) : R.-fdist 'I_n := + locked (FDist.make f0 (f1 gX ge)). +Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) i : + d gX ge i = if g i \in y then e i else 0. +Proof. by rewrite /d; unlock; rewrite ffunE. Qed. +Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) : + (\sum_(i < n) f i = 1). +Proof. +rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE. +case: ifPn => // /negP; rewrite in_setE => giy. +rewrite ge //. +have : (x `|` y) (g i) by apply/gX; by exists i. +by case. +Qed. +Definition d' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) := + locked (FDist.make f0 (f1' gX ge)). +Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i : + d' gX ge i = if g i \in y then e i else 0. +Proof. by rewrite /d'; unlock; rewrite ffunE. Qed. +End def. +End CodomDFDist. diff --git a/probability/fsdist.v b/probability/fsdist.v index 29554ed3..507b91d3 100644 --- a/probability/fsdist.v +++ b/probability/fsdist.v @@ -57,10 +57,10 @@ Local Open Scope fdist_scope. Import Order.POrderTheory Num.Theory. -Lemma fdist_Rgt0 (A : finType) (d : real_realType.-fdist A) a : +Lemma fdist_Rgt0 (A : finType) (d : R.-fdist A) a : (d a != 0) <-> (0 < d a)%coqR. Proof. by rewrite fdist_gt0; split=> /RltP. Qed. -Lemma fdist_Rge0 (A : finType) (d : real_realType.-fdist A) a : +Lemma fdist_Rge0 (A : finType) (d : R.-fdist A) a : 0 <= d a. Proof. by apply/RleP; rewrite FDist.ge0. Qed. @@ -95,7 +95,7 @@ Section fsdist. Variable A : choiceType. Record t := mk { - f :> {fsfun A -> real_realType with 0} ; + f :> {fsfun A -> R with 0} ; _ : all (fun x => (0 < f x)%mcR) (finsupp f) && \sum_(a <- finsupp f) f a == 1}. @@ -145,16 +145,15 @@ Global Hint Resolve FSDist.ge0 : core. Section FSDist_canonical. Variable A : choiceType. -Canonical FSDist_subType := Eval hnf in [subType for @FSDist.f A]. -Definition FSDist_eqMixin := [eqMixin of fsdist A by <:]. -Canonical FSDist_eqType := Eval hnf in EqType _ FSDist_eqMixin. -Definition FSDist_choiceMixin := [choiceMixin of fsdist A by <:]. -Canonical FSDist_choiceType := Eval hnf in ChoiceType _ FSDist_choiceMixin. +HB.instance Definition _ := [isSub for @FSDist.f A]. +HB.instance Definition _ := [Equality of fsdist A by <:]. +HB.instance Definition _ := [Choice of fsdist A by <:]. End FSDist_canonical. -Definition FSDist_to_Type (A : choiceType) := +(*Definition FSDist_to_Type (A : choiceType) := fun phT : phant (Choice.sort A) => fsdist A. -Local Notation "{ 'dist' T }" := (FSDist_to_Type (Phant T)). +Local Notation "{ 'dist' T }" := (FSDist_to_Type (Phant T)).*) +Local Notation "{ 'dist' T }" := (fsdist T). Section fsdist_prop. Variable A : choiceType. @@ -416,14 +415,14 @@ Definition FSDist_prob (C : choiceType) (d : {dist C}) (x : C) : {prob R} := Eval hnf in Prob.mk_ (andb_true_intro (conj (FSDist.ge0' d x) (FSDist.le1' d x))). Canonical FSDist_prob. -Definition fsdistjoin A (D : {dist (FSDist_choiceType A)}) : {dist A} := +Definition fsdistjoin A (D : {dist {dist A}}) : {dist A} := D >>= ssrfun.id. -Lemma fsdistjoinE A (D : {dist (FSDist_choiceType A)}) x : +Lemma fsdistjoinE A (D : {dist {dist A}}) x : fsdistjoin D x = \sum_(d <- finsupp D) D d * d x. Proof. by rewrite /fsdistjoin fsdistbindE. Qed. -Lemma fsdistjoin1 (A : choiceType) (D : {dist (FSDist_choiceType A)}) : +Lemma fsdistjoin1 (A : choiceType) (D : {dist {dist A}}) : fsdistjoin (fsdist1 D) = D. Proof. apply/fsdist_ext => d. @@ -445,7 +444,7 @@ Qed. Lemma f1 : \sum_(a <- finsupp f) f a = 1. Proof. rewrite -(FSDist.f1 P) !big_seq_fsetE /=. -have hP (a : [finType of finsupp P]) : a \in finsupp f. +have hP (a : finsupp P) : a \in finsupp f. by rewrite mem_finsupp fsfunE ffunE inE -mem_finsupp fsvalP. pose h a := FSetSub (hP a). rewrite (reindex h) /=. @@ -453,7 +452,7 @@ rewrite (reindex h) /=. by exists (@fsval _ _) => //= -[a] *; exact: val_inj. Qed. -Definition d : {dist [finType of finsupp P]} := FSDist.make f0 f1. +Definition d : {dist finsupp P} := FSDist.make f0 f1. End def. End FSDist_crop0. @@ -503,7 +502,7 @@ End FSDist_lift_supp. Module FSDist_of_fdist. Section def. -Variable (A : finType) (P : real_realType.-fdist A). +Variable (A : finType) (P : R.-fdist A). Let D := [fset a0 : A | P a0 != 0]. Definition f : {fsfun A -> R with 0} := [fsfun a in D => P a | 0]. @@ -533,7 +532,7 @@ End FSDist_of_fdist. Module fdist_of_FSDist. Section def. Variable (A : choiceType) (P : {dist A}). -Definition D := [finType of finsupp P] : finType. +Definition D := finsupp P : finType. Definition f := [ffun d : D => P (fsval d)]. Lemma f0 b : 0 <= f b. Proof. by rewrite ffunE. Qed. Lemma f1 : \sum_(b in D) f b = 1. @@ -543,7 +542,7 @@ Qed. Lemma f0' b : (0 <= f b)%O. (* TODO: we shouldn't see %O *) Proof. exact/RleP/f0. Qed. -Definition d : real_realType.-fdist D := locked (FDist.make f0' f1). +Definition d : R.-fdist D := locked (FDist.make f0' f1). End def. Module Exports. Notation fdist_of_fs := d. @@ -557,7 +556,7 @@ Variable (A : choiceType) (d : {dist A}). Lemma fdist_of_fsE i : fdist_of_fs d i = d (fsval i). Proof. by rewrite /fdist_of_fs; unlock; rewrite ffunE. Qed. -Lemma fdist_of_FSDistDE : fdist_of_FSDist.D d = [finType of finsupp d]. +Lemma fdist_of_FSDistDE : fdist_of_FSDist.D d = finsupp d. Proof. by []. Qed. End fdist_of_FSDist_lemmas. @@ -579,7 +578,7 @@ rewrite [X in (_ + X = _)%coqR](_ : _ = 0) ?addR0. by rewrite big1 // => a; rewrite mem_finsupp negbK ffunE => /eqP. Qed. -Definition d : real_realType.-fdist A := locked (FDist.make f0' f1). +Definition d : R.-fdist A := locked (FDist.make f0' f1). Lemma dE a : d a = P a. Proof. by rewrite /d; unlock; rewrite ffunE. Qed. @@ -592,7 +591,7 @@ End fdist_of_finFSDist. Export fdist_of_finFSDist.Exports. Section fsdist_conv_def. -Variables (A : choiceType) (p : {prob real_realType}) (d1 d2 : {dist A}). +Variables (A : choiceType) (p : {prob R}) (d1 d2 : {dist A}). Local Open Scope reals_ext_scope. Local Open Scope convex_scope. @@ -628,8 +627,7 @@ Proof. move => /[dup]; rewrite {1}supp => aD. rewrite /f ltR_neqAle mem_finsupp eq_sym => /eqP ?; split => //. rewrite /f fsfunE avgRE aD. -by apply/RleP; rewrite RplusE !RmultE addr_ge0// mulr_ge0//; - [exact/RleP|exact/onem_ge0|exact/RleP]. +by apply/RleP; rewrite RplusE !RmultE addr_ge0// mulr_ge0//. Qed. Let f1 : \sum_(a <- finsupp f) f a = 1. @@ -668,7 +666,7 @@ End fsdist_conv_def. Section fsdist_convType. Variables (A : choiceType). -Implicit Types (p q : {prob real_realType}) (a b c : {dist A}). +Implicit Types (p q : {prob R}) (a b c : {dist A}). Local Open Scope reals_ext_scope. Local Notation "x <| p |> y" := (fsdist_conv p x y) : fsdist_scope. @@ -690,14 +688,14 @@ Let convA p q a b c : Proof. by apply/fsdist_ext=> ?; rewrite !fsdist_convE convA. Qed. HB.instance Definition _ := - @isConvexSpace.Build (FSDist.t _) (Choice.class _) (@fsdist_conv A) + @isConvexSpace.Build (FSDist.t _) (@fsdist_conv A) conv1 convmm convC convA. End fsdist_convType. Section fsdist_conv_prop. Variables (A : choiceType). -Implicit Types (p : {prob real_realType}) (a b c : {dist A}). +Implicit Types (p : {prob R}) (a b c : {dist A}). Local Open Scope reals_ext_scope. Local Open Scope convex_scope. @@ -734,15 +732,16 @@ Lemma supp_fsdist_conv p (p0 : p != 0%:pr) (p1 : p != 1%:pr) a b : finsupp (a <|p|> b) = finsupp a `|` finsupp b. Proof. by rewrite supp_fsdist_conv' (negPf p0) (negPf p1). Qed. -Lemma fsdist_scalept_conv (C : convType) (x y : {dist C}) (p : {prob real_realType}) (i : C) : +Lemma fsdist_scalept_conv (C : convType) (x y : {dist C}) (p : {prob R}) (i : C) : scalept ((x <|p|> y) i) (S1 i) = scalept (x i) (S1 i) <|p|> scalept (y i) (S1 i). Proof. by rewrite fsdist_convE scalept_conv. Qed. End fsdist_conv_prop. -Definition FSDist_to_convType (A : choiceType) := +(*Definition FSDist_to_convType (A : choiceType) := fun phT : phant (Choice.sort A) => conv_choiceType [the convType of FSDist.t A]. -Notation "{ 'dist' T }" := (FSDist_to_convType (Phant T)) : proba_scope. +Notation "{ 'dist' T }" := (FSDist_to_convType (Phant T)) : proba_scope.*) +Notation "{ 'dist' T }" := (FSDist.t T) : proba_scope. Local Open Scope reals_ext_scope. Local Open Scope proba_scope. diff --git a/probability/graphoid.v b/probability/graphoid.v index 5df9e479..9a41c2d9 100644 --- a/probability/graphoid.v +++ b/probability/graphoid.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. Require Import Reals. From mathcomp Require Import Rstruct. Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist. diff --git a/probability/jensen.v b/probability/jensen.v index 425c6d90..abfb7a52 100644 --- a/probability/jensen.v +++ b/probability/jensen.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. From mathcomp Require Import boolp Rstruct. Require Import Reals. Require Import ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb. diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v index bb2e58e1..c41cb4e4 100644 --- a/probability/jfdist_cond.v +++ b/probability/jfdist_cond.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. From mathcomp Require boolp. From mathcomp Require Import Rstruct. Require Import Reals. @@ -220,7 +220,7 @@ Lemma jproduct_rule E F : Pr P (E `* F) = \Pr_P[E | F] * Pr (P`2) F. Proof. have [/eqP PF0|PF0] := boolP (Pr (P`2) F == 0). rewrite jcPrE /cPr -{1}(setIT E) -{1}(setIT F) -setIX. - rewrite Pr_domin_setI; last by rewrite -Pr_fdistX Pr_domin_setX // fdistX1. + rewrite [LHS]Pr_domin_setI; last by rewrite -Pr_fdistX Pr_domin_setX // fdistX1. by rewrite setIC Pr_domin_setI ?(div0R,mul0R) // setTE Pr_setTX. rewrite -{1}(setIT E) -{1}(setIT F) -setIX product_rule. rewrite -EsetT setTT cPrET Pr_setT mulR1 jcPrE. @@ -267,7 +267,9 @@ Arguments jcPr_fdistmap_l [A] [A'] [B] [f] [d] [E] [F] _. Lemma Pr_jcPr_unit (A : finType) (E : {set A}) (P : {fdist A}) : Pr P E = \Pr_(fdistmap (fun a => (a, tt)) P) [E | setT]. Proof. -rewrite /jcPr (Pr_set1 _ tt). +rewrite /jcPr/= (_ : [set: unit] = [set tt]); last first. + by apply/setP => -[]; rewrite !inE eqxx. +rewrite (Pr_set1 _ tt). rewrite (_ : _`2 = fdist1 tt) ?fdist1xx ?divR1; last first. rewrite /fdist_snd fdistmap_comp; apply/fdist_ext; case. by rewrite fdistmapE fdist1xx (eq_bigl xpredT) // FDist.f1. @@ -393,3 +395,67 @@ by case ab. Qed. End fdist_split. + + +Import GRing.Theory Num.Theory. + +Module FDistPart. +Section fdistpart. +Local Open Scope fdist_scope. +Variables (n m : nat) (K : 'I_m -> 'I_n) (e : {fdist 'I_m}) (i : 'I_n). + +Definition d := (fdistX (e `X (fun j => fdist1 (K j)))) `(| i). +Definition den := (fdistX (e `X (fun j => fdist1 (K j))))`1 i. + +Lemma denE : den = fdistmap K e i. +Proof. +rewrite /den !fdistE [RHS]big_mkcond /=. +under eq_bigl do rewrite inE. +apply/eq_bigr => a _. +rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=; + last by case=> x y; rewrite /swap /= !xpair_eqE andbC. +rewrite eq_sym 2!inE. +by case: eqP => // _; rewrite (mulr0,mulr1). +Qed. + +Lemma dE j : fdistmap K e i != 0%coqR -> + d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR. +Proof. +rewrite -denE => NE. +rewrite jfdist_condE // {NE} /jcPr /proba.Pr. +rewrite (big_pred1 (j,i)); last first. + by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE. +rewrite (big_pred1 i); last by move=> k; rewrite !inE. +rewrite !fdistE big_mkcond [in RHS]big_mkcond /=. +rewrite -RmultE -INRE. +congr (_ / _)%R. +under eq_bigr => k do rewrite {2}(surjective_pairing k). +rewrite -(pair_bigA _ (fun k l => + if l == i + then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l) + else R0))%R /=. +apply eq_bigr => k _. +rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym. +by case: ifP; rewrite (mulr1,mulr0). +Qed. +End fdistpart. + +Lemma dK n m K (e : {fdist 'I_m}) j : + e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R. +Proof. +under eq_bigr => /= a _. + have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R. + rewrite Ka0 mul0R. + have <- : (e j * (a == K j)%:R = 0)%R. + have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0. + move: Ka0; rewrite fdistE /=. + by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym. + over. + rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1; + last by rewrite fdistE in Ka0. +over. +move=> /=. +rewrite (bigD1 (K j)) //= eqxx mulR1. +by rewrite big1 ?addR0 // => i /negbTE ->; rewrite mulR0. +Qed. +End FDistPart. diff --git a/probability/ln_facts.v b/probability/ln_facts.v index 2fc4870a..c5038fc9 100644 --- a/probability/ln_facts.v +++ b/probability/ln_facts.v @@ -1,8 +1,9 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp Require boolp. -From mathcomp Require Import Rstruct. +From mathcomp Require Import Rstruct reals. Require Import Reals Lra. Require Import ssrR realType_ext Reals_ext Ranalysis_ext logb convex. diff --git a/probability/necset.v b/probability/necset.v index 8317c561..e799ab3e 100644 --- a/probability/necset.v +++ b/probability/necset.v @@ -91,34 +91,31 @@ Local Open Scope reals_ext_scope. Local Open Scope fdist_scope. Local Open Scope convex_scope. -Module NESet. -Local Open Scope classical_set_scope. -Record mixin_of (T : Type) (X : set T) := Mixin {_ : X != set0 }. -Record t (T : Type) : Type := Pack { car : set T ; class : mixin_of car }. -Module Exports. -Notation neset := t. -Notation "s %:ne" := (@Pack _ s (class _)). -Coercion car : neset >-> set. -End Exports. -End NESet. -Export NESet.Exports. +HB.mixin Record isNESet (T : Type) (X : set T) := { is_nonempty : X != set0 }. +#[short(type=neset)] +HB.structure Definition NESet T := { X of isNESet T X }. +Notation "s %:ne" := ((s : neset _)%classic). (*(@Pack _ s (class _)).*) Section neset_canonical. Variable A : Type. Canonical neset_predType := Eval hnf in PredType (fun t : neset A => (fun x => x \in (t : set _))). -Canonical neset_eqType := Equality.Pack (@gen_eqMixin (neset A)). -Canonical neset_choiceType := choice_of_Type (neset A). +HB.instance Definition _ := gen_eqMixin (neset A). +HB.instance Definition _ := gen_choiceMixin (neset A). +(* +Canonical neset_eqType := Equality.Pack (Equality.Class (@gen_eqMixin (neset A))). +Canonical neset_choiceType := Choice.Pack (Choice.Class (@choice_of_Type (neset A). +*) End neset_canonical. Section NESet_interface. Variables (A : Type). Lemma neset_neq0 (a : neset A) : a != set0 :> set _. -Proof. by case: a => [? []]. Qed. +Proof. by case: a => [? [[]]]. Qed. Lemma neset_ext (a b : neset A) : a = b :> set _ -> a = b. Proof. -move: a b => -[a Ha] -[b Hb] /= ?; subst a. -congr NESet.Pack; exact/Prop_irrelevance. +move: a b => -[a [[Ha]]] -[b [[Hb]]] /= ?; subst a. +congr NESet.Pack; congr NESet.Class; f_equal; exact/Prop_irrelevance. Qed. End NESet_interface. @@ -130,11 +127,11 @@ Proof. by apply/set0P; exists a. Qed. Definition neset_repr A (X : neset A) : A. Proof. -case: X => X [] /set0P /boolp.constructive_indefinite_description [x _]; exact x. +case: X => X [[]] /set0P /boolp.constructive_indefinite_description [x _]; exact x. Defined. Lemma repr_in_neset A (X : neset A) : (X : set A) (neset_repr X). -Proof. by case: X => X [] X0 /=; case: cid. Qed. +Proof. by case: X => X [[]] X0 /=; case: cid. Qed. Global Opaque neset_repr. Local Hint Resolve repr_in_neset : core. @@ -154,24 +151,31 @@ Proof. apply/set0P; eexists; exact/imageP. Qed. Lemma neset_setU_neq0 A (X Y : neset A) : X `|` Y != set0. Proof. by apply/set0P; eexists; left. Qed. -Canonical neset1 {A} (a : A) := - @NESet.Pack A [set a] (NESet.Mixin (set1_neq0 a)). -Canonical bignesetU {A} I (S : neset I) (F : I -> neset A) := - NESet.Pack (NESet.Mixin (neset_bigsetU_neq0 S F)). -Canonical image_neset {A B} (f : A -> B) (X : neset A) := - NESet.Pack (NESet.Mixin (neset_image_neq0 f X)). -Canonical nesetU {T} (X Y : neset T) := - NESet.Pack (NESet.Mixin (neset_setU_neq0 X Y)). +(* Canonical neset1 *) +HB.instance Definition neset1 {A} (a : A) := isNESet.Build _ _ (set1_neq0 a). +(* Canonical bignesetU *) +HB.instance Definition _ {A} I (S : neset I) (F : I -> neset A) := + isNESet.Build _ _ (neset_bigsetU_neq0 S F). +(* Canonical image_neset *) +HB.instance Definition _ {A B} (f : A -> B) (X : neset A) := + isNESet.Build _ _ (neset_image_neq0 f X). +(* Canonical nesetU *) +HB.instance Definition _ {T} (X Y : neset T) := + isNESet.Build _ _ (neset_setU_neq0 X Y). Lemma neset_hull_neq0 (T : convType) (F : neset T) : hull F != set0. Proof. by rewrite hull_eq0 neset_neq0. Qed. -Canonical neset_hull (T : convType) (F : neset T) := - NESet.Pack (NESet.Mixin (neset_hull_neq0 F)). +(* Canonical neset_hull *) +HB.instance Definition _ (T : convType) (F : neset T) := + isNESet.Build _ _ (neset_hull_neq0 F). End neset_lemmas. Local Hint Resolve repr_in_neset : core. -Arguments image_neset : simpl never. +(*Arguments image_neset : simpl never.*) + +#[short(type=necset)] +HB.structure Definition NECSet (A : convType) := {X of @isConvexSet A X & @isNESet A X}. Section conv_set_def. Local Open Scope classical_set_scope. @@ -196,7 +200,6 @@ Lemma conv_pt_setE p x Y : x <| p |>: Y = (fun y => x <| p |> y) @` Y. Proof. by rewrite /conv_pt_set; unlock. Qed. Definition conv_set p (X Y : set L) := \bigcup_(x in X) (x <| p |>: Y). -Local Notation "X :<| p |>: Y" := (conv_set p X Y). End conv_set_def. Notation "x <| p |>: Y" := (conv_pt_set p x Y) : convex_scope. @@ -325,20 +328,27 @@ Proof. apply/set0P; eexists; exists 1%:pr => //; by rewrite conv1_set. Qed. Fixpoint iter_conv_set_neq0 (X : neset A) (n : nat) : iter_conv_set X n != set0 := if n is n'.+1 then - oplus_conv_set_neq0 X (NESet.Pack (NESet.Mixin (iter_conv_set_neq0 X n'))) + oplus_conv_set_neq0 X (NESet.Pack (NESet.Class (isNESet.Build _ _ (iter_conv_set_neq0 X n')))) else neset_neq0 X. -Canonical probset_neset := NESet.Pack (NESet.Mixin probset_neq0). -Canonical natset_neset := NESet.Pack (NESet.Mixin natset_neq0). -Canonical conv_pt_set_neset (p : {prob R}) (x : A) (Y : neset A) := - NESet.Pack (NESet.Mixin (conv_pt_set_neq0 p x Y)). -Canonical conv_set_neset (p : {prob R}) (X Y : neset A) := - NESet.Pack (NESet.Mixin (conv_set_neq0 p X Y)). -Canonical oplus_conv_set_neset (X Y : neset A) := - NESet.Pack (NESet.Mixin (oplus_conv_set_neq0 X Y)). -Canonical iter_conv_set_neset (X : neset A) (n : nat) := - NESet.Pack (NESet.Mixin (iter_conv_set_neq0 X n)). - +(*Canonical probset_neset*) +HB.instance Definition _ := isNESet.Build _ _ probset_neq0. +(*Canonical natset_neset*) +HB.instance Definition _ := isNESet.Build _ _ natset_neq0. +(*Canonical conv_pt_set_neset*) +HB.instance Definition _ (p : {prob R}) (x : A) (Y : neset A) := + isNESet.Build _ _ (conv_pt_set_neq0 p x Y). +(*Canonical conv_set_neset*) +HB.instance Definition _ (p : {prob R}) (X Y : neset A) := + isNESet.Build _ _ (conv_set_neq0 p X Y). +(*Canonical oplus_conv_set_neset*) +HB.instance Definition _ (X Y : neset A) := + isNESet.Build _ _ (oplus_conv_set_neq0 X Y). +(*Canonical iter_conv_set_neset*) +HB.instance Definition _ (X : neset A) (n : nat) := + isNESet.Build _ _ (iter_conv_set_neq0 X n). + +(* TODO: Let insteaad of Lemma *) Lemma conv_pt_cset_is_convex (p : {prob R}) (x : A) (Y : {convex_set A}) : is_convex_set (conv_pt_set p x Y). Proof. @@ -348,8 +358,9 @@ rewrite -convDr; apply/imageP. by move/asboolP: (convex_setP Y); apply. Qed. -Canonical conv_pt_cset (p : {prob R}) (x : A) (Y : {convex_set A}) := - CSet.Pack (CSet.Mixin (conv_pt_cset_is_convex p x Y)). +(*Canonical conv_pt_cset*) +HB.instance Definition _ (p : {prob R}) (x : A) (Y : {convex_set A}) := + isConvexSet.Build _ _ (conv_pt_cset_is_convex p x Y). Lemma conv_cset_is_convex (p : {prob R}) (X Y : {convex_set A}) : is_convex_set (conv_set p X Y). @@ -361,8 +372,8 @@ by rewrite convACA; apply/conv_in_conv_set; [move/asboolP: (convex_setP X); apply | move/asboolP: (convex_setP Y); apply]. Qed. -Canonical conv_cset (p : {prob R}) (X Y : {convex_set A}) := - CSet.Pack (CSet.Mixin (conv_cset_is_convex p X Y)). +HB.instance Definition _ (p : {prob R}) (X Y : {convex_set A}) := + isConvexSet.Build _ _ (conv_cset_is_convex p X Y). Lemma oplus_conv_cset_is_convex (X Y : {convex_set A}) : is_convex_set (oplus_conv_set X Y). @@ -387,19 +398,21 @@ apply (prob_trichotomy' q) => [| |oq]. move/asboolP: (convex_setP Y); apply]. Qed. -Canonical oplus_conv_cset (X Y : {convex_set A}) := - CSet.Pack (CSet.Mixin (oplus_conv_cset_is_convex X Y)). +HB.instance Definition _ (X Y : {convex_set A}) := + isConvexSet.Build _ _ (oplus_conv_cset_is_convex X Y). Fixpoint iter_conv_cset_is_convex (X : {convex_set A}) (n : nat) : is_convex_set (iter_conv_set X n) := match n with | 0 => convex_setP X | n'.+1 => oplus_conv_cset_is_convex - X (CSet.Pack (CSet.Mixin (iter_conv_cset_is_convex X n'))) + X (ConvexSet.Pack + (ConvexSet.Class + (isConvexSet.Build _ _ (iter_conv_cset_is_convex X n')))) end. -Canonical iter_conv_cset (X : {convex_set A}) (n : nat) := - CSet.Pack (CSet.Mixin (iter_conv_cset_is_convex X n)). +HB.instance Definition _ (X : {convex_set A}) (n : nat) := + isConvexSet.Build _ _ (iter_conv_cset_is_convex X n). Lemma conv_pt_set_monotone (p : {prob R}) (x : A) (Y Y' : set A) : Y `<=` Y' -> x <| p |>: Y `<=` x <| p |>: Y'. @@ -443,7 +456,7 @@ Proof. elim: n => [g d|n IHn g d X]; first by have := fdistI0_False d. have [/eqP ->|Xneq0 gX] := boolP (X == set0). by move=> /(_ (g ord0)) H; exfalso; apply/H/imageP. -set X' := NESet.Pack (NESet.Mixin Xneq0). +set X' := NESet.Pack (NESet.Class (isNESet.Build _ _ Xneq0)). have gXi : forall i : 'I_n.+1, X (g i). by move=> i; move/subset_image : gX; apply. have [/eqP d01|d0n1] := boolP (d ord0 == 1). @@ -526,19 +539,14 @@ Local Close Scope classical_set_scope. lattice. For now, I write down the following definition of semilattice independently of the two, as it seems hard to insert a new layer in the mathcomp hierarchy. *) -HB.mixin Record isSemiLattice (T : Type) := { - slchoice : Choice.class_of T ; +HB.mixin Record isSemiLattice (T : Type) of Choice T := { lub : T -> T -> T ; lubC : commutative lub; lubA : associative lub; lubxx : idempotent lub }. #[short(type=semiLattType)] -HB.structure Definition SemiLattice := { T & isSemiLattice T }. - -Canonical semilattice_eqType (T : semiLattType) := EqType T slchoice. -Canonical semilattice_choiceType (T : semiLattType) := ChoiceType T slchoice. -Coercion semilattice_choiceType : semiLattType >-> choiceType. +HB.structure Definition SemiLattice := { T of isSemiLattice T & }. Notation "x [+] y" := (lub x y) : latt_scope. @@ -571,8 +579,7 @@ Proof. by rewrite lubAC lubC lubxx. Qed. End semilattice_lemmas. -HB.mixin Record isSemiCompSemiLatt T of isSemiLattice T := { - scslchoice : Choice.class_of T ; +HB.mixin Record isSemiCompSemiLatt T of isSemiLattice T & Choice T := { biglub : neset T -> T ; (* [Reiterman] p.326, axiom 3 *) biglub1 : forall x : T, biglub [set x]%:ne = x ; @@ -581,13 +588,7 @@ HB.mixin Record isSemiCompSemiLatt T of isSemiLattice T := { lubE : forall x y, x [+] y = biglub [set x; y]%:ne }. #[short(type=semiCompSemiLattType)] -HB.structure Definition SemiCompSemiLatt := - { T of @isSemiCompSemiLatt T & isSemiLattice T }. - -Canonical semicompsemilatt_eqType (T : semiCompSemiLattType) := - EqType T scslchoice. -Canonical semicompsemilatt_choiceType (T : semiCompSemiLattType) := - ChoiceType T scslchoice. +HB.structure Definition SemiCompSemiLatt := { T of @isSemiCompSemiLatt T & }. Notation "|_| f" := (biglub f) : latt_scope. Local Open Scope latt_scope. @@ -822,7 +823,7 @@ Lemma biglub_oplus_conv_setE (X Y : neset L) : |_| (oplus_conv_set X Y)%:ne = |_| ((fun p => |_| X <|p|> |_| Y) @` probset)%:ne. Proof. -transitivity (|_| (\bigcup_(p in probset_neset) (X :<| p |>: Y))%:ne). +transitivity (|_| (\bigcup_(p in probset) (X :<| p |>: Y))%:ne). by congr (|_| _%:ne); apply/neset_ext. rewrite biglub_bigcup //; congr (|_| _%:ne); apply/neset_ext => /=. rewrite image_comp; congr image; apply funext => p /=. @@ -869,32 +870,12 @@ HB.instance Definition _ (*biglubDr_semiLattConvType*) := @isSemiLattConv.Build End semicompsemilattconvtype_lemmas. -Module NECSet. -Section def. -Variable A : convType. -Record class_of (X : set A) : Type := Class { - base : CSet.mixin_of X ; mixin : NESet.mixin_of X }. -Record t : Type := Pack { car : set A ; class : class_of car }. -Definition baseType (M : t) := CSet.Pack (base (class M)). -Definition mixinType (M : t) := NESet.Pack (mixin (class M)). -End def. -Module Exports. -Notation necset := t. -Canonical baseType. -Canonical mixinType. -Coercion baseType : necset >-> convex_set. -Coercion mixinType : necset >-> neset. -Coercion car : necset >-> set. -End Exports. -End NECSet. -Export NECSet.Exports. - Section necset_canonical. Variable (A : convType). Canonical necset_predType := Eval hnf in PredType (fun t : necset A => (fun x => x \in (t : set _))). -Canonical necset_eqType := Equality.Pack (@gen_eqMixin (necset A)). -Canonical necset_choiceType := choice_of_Type (necset A). +HB.instance Definition _ := gen_eqMixin (necset A). +HB.instance Definition _ := gen_choiceMixin (necset A). End necset_canonical. Section necset_lemmas. @@ -902,28 +883,44 @@ Variable A : convType. Lemma necset_ext (a b : necset A) : a = b :> set _ -> a = b. Proof. -move: a b => -[a Ha] -[b Hb] /= ?; subst a. -congr NECSet.Pack; exact/Prop_irrelevance. +move: a b => -[a [[?] [?]]] -[b [[?] [?]]] /= ?; subst a. +congr NECSet.Pack; congr NECSet.Class; f_equal; exact/Prop_irrelevance. Qed. -(* TODO: does the Canonical make sense? *) -Canonical neset_hull_necset (T : convType) (F : neset T) := - NECSet.Pack (NECSet.Class (CSet.Mixin (hull_is_convex F)) - (NESet.Mixin (neset_hull_neq0 F))). - -(* TODO: does the Canonical make sense? *) -Canonical necset1 (T : convType) (x : T) := Eval hnf in - @NECSet.Pack _ [set x] (NECSet.Class (CSet.Mixin (is_convex_set1 x)) - (NESet.Mixin (set1_neq0 x))). +(*Canonical neset_hull_necset*) +HB.instance Definition _ (T : convType) (F : neset T) := + isConvexSet.Build _ _ (hull_is_convex F). +HB.instance Definition _ (T : convType) (F : neset T) := + isNESet.Build _ _ (neset_hull_neq0 F). + +(*Canonical necset1*) +HB.instance Definition _ (T : convType) (x : T) := + isConvexSet.Build _ _ (is_convex_set1 x). +HB.instance Definition _ (T : convType) (x : T) := + isNESet.Build _ _ (set1_neq0 x). End necset_lemmas. +(*Definition necset_convType_conv {A : convType} p (X Y : necset A) := + X :<|p|>: Y. + +HB.instance Definition _ {A : convType} p (X Y : necset A) := + NESet.on (necset_convType_conv p X Y). + +HB.instance Definition _ {A : convType} p (X Y : necset A) := + ConvexSet.on (necset_convType_conv p X Y).*) + +HB.instance Definition _ {A : convType} (p : {prob R}) (X Y : necset A) := + isNESet.Build _ _ (conv_set_neq0 p X Y). + Module necset_convType. Section def. Variable A : convType. -Definition conv p (X Y : necset A) : necset A := locked - (NECSet.Pack (NECSet.Class (CSet.Mixin (conv_cset_is_convex p X Y)) - (NESet.Mixin (conv_set_neq0 p X Y)))). +Definition conv p (X Y : necset A) : necset A := X :<|p|>: Y. + +(*locked + (NECSet.Pack (NECSet.Class (isConvexSet.Build _ _ (conv_cset_is_convex p X Y)) + (isNESet.Build _ _ (conv_set_neq0 p X Y)))).*) Lemma convE p (X Y : necset A) : conv p X Y = conv_set p X Y :> set A. Proof. by rewrite /conv; unlock. Qed. @@ -939,7 +936,7 @@ Proof. by apply necset_ext; rewrite !convE convC_set. Qed. Lemma convA p q X Y Z : conv p X (conv q Y Z) = conv [s_of p, q] (conv [r_of p, q] X Y) Z. -Proof. by apply necset_ext; rewrite !convE convA_set. Qed. +Proof. by apply: necset_ext; rewrite 2!convE convA_set. Qed. End def. @@ -956,7 +953,7 @@ End lemmas. End necset_convType. HB.instance Definition necset_convType (A : convType) := - @isConvexSpace.Build (necset A) (Choice.class _) + @isConvexSpace.Build (necset A) (@necset_convType.conv A) (@necset_convType.conv1 A) (@necset_convType.convmm A) @@ -973,21 +970,19 @@ Local Open Scope classical_set_scope. Variable (A : convType). Definition pre_op (X : neset {necset A}) : {convex_set A} := - CSet.Pack (CSet.Mixin (hull_is_convex (\bigcup_(i in X) idfun i)%:ne)). + hull (\bigcup_(i in X) idfun i)%:ne. Lemma pre_op_neq0 X : pre_op X != set0 :> set _. Proof. by rewrite hull_eq0 neset_neq0. Qed. Definition biglub_necset (X : neset (necset A)) : necset A := - NECSet.Pack (NECSet.Class - (CSet.Mixin (hull_is_convex (\bigcup_(i in X) idfun i)%:ne)) - (NESet.Mixin (pre_op_neq0 X))). + hull (\bigcup_(i in X) idfun i)%:ne. Lemma biglub_necset1 x : biglub_necset [set x]%:ne = x. -Proof. by apply necset_ext => /=; rewrite bigcup_set1 hull_cset. Qed. +Proof. by apply: necset_ext => /=; rewrite bigcup_set1 hull_cset. Qed. Lemma biglub_necset_bigsetU (I : Type) (S : neset I) (F : I -> neset (necset A)) : - biglub_necset (bignesetU S F) = biglub_necset (biglub_necset @` (F @` S))%:ne. + biglub_necset (\bigcup_(i in S) F i) = biglub_necset (biglub_necset @` (F @` S))%:ne. Proof. apply necset_ext => /=. apply: hull_eqEsubset => a. @@ -1008,7 +1003,7 @@ Qed. Let lub_ (x y : necset A) : necset A := biglub_necset [set x; y]%:ne. -Let lub_E (x y : necset A) : lub_ x y = neset_hull_necset (x `|` y)%:ne. +Let lub_E (x y : necset A) : lub_ x y = hull (x `|` y)%:ne. Proof. by apply necset_ext; rewrite /= bigcup_setU !bigcup_set1. Qed. Let lub_C : commutative lub_. @@ -1027,7 +1022,7 @@ by move=> x; rewrite lub_E; apply necset_ext => /=; rewrite setUid hull_cset. Qed. #[export] -HB.instance Definition _ := @isSemiLattice.Build (necset A) (Choice.class _) +HB.instance Definition _ := @isSemiLattice.Build (necset A) lub_ lub_C lub_A lub_xx. Let lub_E' : forall x y, lub_ x y = biglub_necset [set x; y]%:ne. @@ -1035,7 +1030,7 @@ Proof. by []. Qed. #[export] HB.instance Definition _ (*necset_semiCompSemiLattType*) := - @isSemiCompSemiLatt.Build (necset A) (Choice.class _) + @isSemiCompSemiLatt.Build (necset A) biglub_necset biglub_necset1 biglub_necset_bigsetU lub_E'. End def. @@ -1052,7 +1047,9 @@ Let biglubDr' (p : {prob R}) (X : L) (I : neset L) : necset_convType.conv p X (|_| I) = |_| ((necset_convType.conv p X) @` I)%:ne. Proof. apply necset_ext => /=. -rewrite -hull_cset necset_convType.conv_conv_set /= hull_conv_set_strr. +rewrite -[LHS]hull_cset/=. +rewrite [X in hull X = _]necset_convType.conv_conv_set /=. +rewrite hull_conv_set_strr. congr hull; rewrite eqEsubset; split=> u /=. - case=> x Xx [] y []Y IY Yy <-. exists (necset_convType.conv p X Y); first by exists Y. @@ -1089,7 +1086,7 @@ Module necset_join. Section def. Local Open Scope classical_set_scope. Local Open Scope proba_scope. -Definition F (T : Type) := {necset {dist (choice_of_Type T)}}. +Definition F (T : Type) := {necset {dist {classic T}}}. Variable T : Type. Definition L := [the convType of F T]. @@ -1115,12 +1112,12 @@ Qed. Definition L' := necset L. Definition F1join0 : FFT -> L' := fun X => NECSet.Pack (NECSet.Class - (CSet.Mixin (F1join0'_convex X)) (NESet.Mixin (F1join0'_neq0 X))). + (isConvexSet.Build _ _ (F1join0'_convex X)) (isNESet.Build _ _ (F1join0'_neq0 X))). Definition join1' (X : L') - : convex_set [the convType of {dist (choice_of_Type T)}] := - CSet.Pack (CSet.Mixin (hull_is_convex - (\bigcup_(i in X) if i \in X then (i : set _) else cset0 _))). + : {convex_set [the convType of {dist {classic T}}]} := + ConvexSet.Pack (ConvexSet.Class (isConvexSet.Build _ _ (hull_is_convex + (\bigcup_(i in X) if i \in X then (i : set _) else set0)))). Lemma join1'_neq0 (X : L') : join1' X != set0 :> set _. Proof. @@ -1133,8 +1130,8 @@ by rewrite sy. Qed. Definition join1 : L' -> L := fun X => - NECSet.Pack (NECSet.Class (CSet.Mixin (hull_is_convex _)) - (NESet.Mixin (join1'_neq0 X))). + NECSet.Pack (NECSet.Class (isConvexSet.Build _ _ (hull_is_convex _)) + (isNESet.Build _ _ (join1'_neq0 X))). Definition join : FFT -> L := join1 \o F1join0. End def. Module Exports. @@ -1151,14 +1148,14 @@ Local Notation M := (necset_join.F). Section ret. Variable a : Type. -Definition necset_ret (x : a) : M a := necset1 (fsdist1 (x : choice_of_Type a)). +Definition necset_ret (x : a) : M a := [set (fsdist1 (x : {classic a}))]. End ret. Section fmap. Variables (a b : Type) (f : a -> b). Let necset_fmap' (ma : M a) := - (fsdistmap (f : choice_of_Type a -> choice_of_Type b)) @` ma. + (fsdistmap (f : {classic_ a} -> {classic b})) @` ma. Lemma necset_fmap'_convex ma : is_convex_set (necset_fmap' ma). Proof. @@ -1170,12 +1167,12 @@ Qed. Lemma necset_fmap'_neq0 ma : (necset_fmap' ma) != set0. Proof. case/set0P : (neset_neq0 ma) => x max; apply/set0P. -by exists (fsdistmap (f : choice_of_Type a -> choice_of_Type b) x), x. +by exists (fsdistmap (f : {classic a} -> {classic b}) x), x. Qed. Definition necset_fmap : M a -> M b := fun ma => - NECSet.Pack (NECSet.Class (CSet.Mixin (necset_fmap'_convex ma)) - (NESet.Mixin (necset_fmap'_neq0 ma))). + NECSet.Pack (NECSet.Class (isConvexSet.Build _ _ (necset_fmap'_convex ma)) + (isNESet.Build _ _ (necset_fmap'_neq0 ma))). End fmap. Section bind. @@ -1202,7 +1199,7 @@ rewrite lubE -[in LHS]biglub_hull; congr (|_| _); apply neset_ext => /=. rewrite eqEsubset; split=> i /=. - have /set0P x0 := set1_neq0 x. have /set0P y0 := set1_neq0 y. - move/(@hull_setU _ _ (necset1 x) (necset1 y) x0 y0). + move/(@hull_setU _ _ (set1 x) (set1 y) x0 y0). by move=> [a /asboolP ->] [b /asboolP ->] [p ->]; exists p. - by case=> p ? <-; exact/mem_hull_setU. Qed. diff --git a/probability/partition_inequality.v b/probability/partition_inequality.v index 8d13d3a2..a6cb0a11 100644 --- a/probability/partition_inequality.v +++ b/probability/partition_inequality.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssrnum. +From mathcomp Require Import all_ssreflect ssralg ssrnum. Require Import Reals Lra. From mathcomp Require Import Rstruct. Require Import ssrR realType_ext Reals_ext Ranalysis_ext ssr_ext logb ln_facts. @@ -36,7 +36,7 @@ Variable P : {fdist A}. Definition bipart_pmf := [ffun i => \sum_(a in A_ i) P a]. -Definition bipart : {fdist [finType of bool]}. +Definition bipart : {fdist bool}. apply (@FDist.make _ _ bipart_pmf). - by move=> a; rewrite ffunE; apply: sumr_ge0. - rewrite big_bool /= /bipart_pmf /= !ffunE. diff --git a/probability/proba.v b/probability/proba.v index eeb598de..9578e61c 100644 --- a/probability/proba.v +++ b/probability/proba.v @@ -137,7 +137,6 @@ Notation "E `*T" := ([set x | x.1 \in E]) : proba_scope. Notation "T`* F" := ([set x | x.2 \in F]) : proba_scope. Section TsetT. -Notation R := real_realType. Variables (A B : finType) (P : R.-fdist (A * B)). Implicit Types (E : {set A}) (F : {set B}). @@ -178,7 +177,6 @@ End TsetT. solve [apply/RleP; exact: FDist.le1] : core. Section probability. -Notation R := Rstruct.real_realType. Variables (A : finType) (P : R.-fdist A). Implicit Types E : {set A}. @@ -346,7 +344,6 @@ by move=> /(_ a); rewrite mem_index_enum => /(_ isT); rewrite aE implyTb. Qed. Section Pr_extra. -Notation R := real_realType. Variables (A B : finType) (P : R.-fdist (A * B)). Implicit Types (E : {set A}) (F : {set B}). @@ -390,7 +387,7 @@ Lemma Pr_domin_setXN (A B : finType) (P : {fdist A * B}) E F : Pr P (E `* F) != 0 -> Pr P`1 E != 0. Proof. by apply/contra => /eqP/Pr_domin_setX => ?; exact/eqP. Qed. -Lemma Pr_fdistmap (A B : finType) (f : A -> B) (d : real_realType.-fdist A) (E : {set A}) : +Lemma Pr_fdistmap (A B : finType) (f : A -> B) (d : R.-fdist A) (E : {set A}) : injective f -> Pr d E = Pr (fdistmap f d) (f @: E). Proof. @@ -486,7 +483,6 @@ Local Close Scope vec_ext_scope. Section random_variable. Variables (U : finType) (T : eqType). -Notation R := real_realType. Definition RV (P : R.-fdist U) := U -> T. @@ -501,7 +497,6 @@ End random_variable. Notation "{ 'RV' P -> T }" := (RV_of P (Phant _) (Phant T)) : proba_scope. Section random_variable_eqType. -Notation R := real_realType. Variables (U : finType) (A : eqType) (P : R.-fdist U). Definition pr_eq (X : {RV P -> A}) (a : A) := locked (Pr P (finset (X @^-1 a))). @@ -536,7 +531,6 @@ Notation "`Pr[ X = a ]" := (pr_eq X a) : proba_scope. Global Hint Resolve pr_eq_ge0 : core. Section random_variable_order. -Notation R := real_realType. Variables (U : finType) (d : unit) (T : porderType d) (P : R.-fdist U). Variables (X : {RV P -> T}). @@ -549,7 +543,6 @@ Notation "'`Pr[' X '>=' r ']'" := (pr_geq X r) : proba_scope. Notation "'`Pr[' X '<=' r ']'" := (pr_leq X r) : proba_scope. Section random_variable_finType. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (A : finType). Definition pr_eq_set (X : {RV P -> A}) (E : {set A}) := @@ -582,8 +575,6 @@ Notation "`Pr[ X '\in' E ]" := (pr_eq_set X E) : proba_scope. Notation "`p_ X" := (dist_of_RV X) : proba_scope. Section random_variables. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U). Definition const_RV (T : eqType) cst : {RV P -> T} := fun=> cst. @@ -618,7 +609,6 @@ Notation "'`--' P" := (neg_RV P) : proba_scope. Notation "'`log' P" := (log_RV P) : proba_scope. Section RV_lemmas. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Implicit Types X : {RV P -> R}. @@ -637,7 +627,6 @@ Proof. by rewrite sq_RV_pow2; exact: pow2_ge_0. Qed. End RV_lemmas. Section pair_of_RVs. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (A : eqType) (X : {RV P -> A}) (B : eqType) (Y : {RV P -> B}). Definition RV2 : {RV P -> A * B} := fun x => (X x, Y x). @@ -646,7 +635,6 @@ End pair_of_RVs. Notation "'[%' x , y , .. , z ']'" := (RV2 .. (RV2 x y) .. z). Section RV2_prop. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}). @@ -668,7 +656,6 @@ Proof. by []. Qed. End RV2_prop. Section RV3_prop. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (A B C D : finType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}). @@ -689,10 +676,10 @@ Proof. by rewrite /fdistC12 /dist_of_RV /fdistA fdistmap_comp. Qed. End RV3_prop. -Lemma pr_eq_unit (U : finType) (P : real_realType.-fdist U) : `Pr[ (unit_RV P) = tt ] = 1. +Lemma pr_eq_unit (U : finType) (P : R.-fdist U) : `Pr[ (unit_RV P) = tt ] = 1. Proof. by rewrite pr_eqE'; apply/eqP/fdist1P; case. Qed. -Lemma Pr_fdistmap_RV2 (U : finType) (P : real_realType.-fdist U) (A B : finType) +Lemma Pr_fdistmap_RV2 (U : finType) (P : R.-fdist U) (A B : finType) (E : {set A}) (F : {set B}) (X : {RV P -> A}) (Z : {RV P -> B}) : Pr `p_[% X, Z] (E `* F) = Pr P ([set x | preim X (mem E) x] :&: [set x | preim Z (mem F) x]). @@ -706,7 +693,6 @@ by rewrite fdistmapE. Qed. Section pr_pair. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (A B C : finType) (TA TB TC : eqType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}). @@ -777,7 +763,6 @@ by apply/imsetP/idP => [[a aE [] ->//]|XuE]; exists (X u). Qed. Section RV_domin. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (A B : finType) (TA TB : eqType). Variables (X : {RV P -> A}) (Y : {RV P -> B}). Variables (TX : {RV P -> A}) (TY : {RV P -> B}). @@ -798,11 +783,11 @@ End RV_domin. Local Open Scope vec_ext_scope. -Definition cast_RV_fdist_rV1 (U : finType) (P : real_realType.-fdist U) (T : eqType) (X : {RV P -> T}) +Definition cast_RV_fdist_rV1 (U : finType) (P : R.-fdist U) (T : eqType) (X : {RV P -> T}) : {RV (P `^ 1) -> T} := fun x => X (x ``_ ord0). -Definition cast_RV_fdist_rV10 (U : finType) (P : real_realType.-fdist U) (T : eqType) +Definition cast_RV_fdist_rV10 (U : finType) (P : R.-fdist U) (T : eqType) (Xs : 'rV[{RV P -> T}]_1) : {RV (P `^ 1) -> T} := cast_RV_fdist_rV1 (Xs ``_ ord0). @@ -815,7 +800,6 @@ Definition cast_fun_rV10 U (T : eqType) (Xs : 'rV[U -> T]_1) : 'rV[U]_1 -> T := Local Close Scope vec_ext_scope. Section expected_value_def. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}). Definition Ex := \sum_(u in U) X u * P u. @@ -830,7 +814,6 @@ Notation "'`E'" := (@Ex _ _) : proba_scope. (* Alternative definition of the expected value: *) Section Ex_alt. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}). Definition Ex_alt := \sum_(r <- fin_img X) r * `Pr[ X = r ]. @@ -847,8 +830,6 @@ Qed. End Ex_alt. Section expected_value_prop. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U) (X Y : {RV P -> R}). Lemma E_neg_RV : `E (`-- X) = - `E X. @@ -920,7 +901,7 @@ Proof. move=> H; by rewrite /comp_RV /= H. Qed. End expected_value_prop. -Lemma E_cast_RV_fdist_rV1 (A : finType) (P : real_realType.-fdist A) : +Lemma E_cast_RV_fdist_rV1 (A : finType) (P : R.-fdist A) : forall (X : {RV P -> R}), `E (cast_RV_fdist_rV1 X) = `E X. Proof. move=> f; rewrite /cast_RV_fdist_rV1 /=; apply big_rV_1 => // m. @@ -928,8 +909,6 @@ by rewrite -fdist_rV1. Qed. Section conditional_expectation_def. -Notation R := real_realType. - Variable (U : finType) (P : R.-fdist U) (X : {RV P -> R}) (F : {set U}). Definition cEx := @@ -939,8 +918,6 @@ End conditional_expectation_def. Notation "`E_[ X | F ]" := (cEx X F). Section conditional_expectation_prop. -Notation R := real_realType. - Variable (U I : finType) (P : R.-fdist U) (X : {RV P -> R}) (F : I -> {set U}). Hypothesis dis : forall i j, i != j -> [disjoint F i & F j]. Hypothesis cov : cover [set F i | i in I] = [set: U]. @@ -1025,7 +1002,6 @@ End Ind. contributed by Erik Martin-Dorel: the corresponding theorem is named [Pr_bigcup_incl_excl] and is more general than lemma [Pr_bigcup]. *) Section probability_inclusion_exclusion. -Notation R := real_realType. Variables (A : finType) (P : R.-fdist A). Let SumIndCap (n : nat) (S : 'I_n -> {set A}) (k : nat) (x : A) := @@ -1148,7 +1124,6 @@ Proof. by move=> r0; rewrite leR_pdivl_mulr // mulRC; exact/Ex_lb. Qed. End markov_inequality. Section thm61. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}) (phi : R -> R). Lemma Ex_comp_RV : `E (phi `o X) = \sum_(r <- fin_img X) phi r * `Pr[ X = r ]. @@ -1164,8 +1139,6 @@ Qed. End thm61. Section variance_def. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}). (* Variance of a random variable (\sigma^2(X) = V(X) = E (X^2) - (E X)^2): *) @@ -1185,8 +1158,6 @@ Arguments Var {U} _ _. Notation "'`V'" := (@Var _ _) : proba_scope. Section variance_prop. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}). (* The variance is not linear V (k X) = k^2 V (X) \cite[Theorem 6.7]{probook}: *) @@ -1219,8 +1190,6 @@ Qed. In any data sample, "nearly all" the values are "close to" the mean value: Pr[ |X - E X| \geq \epsilon] \leq V(X) / \epsilon^2 *) Section chebyshev. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}). Lemma chebyshev_inequality epsilon : 0 < epsilon -> @@ -1246,8 +1215,6 @@ Qed. End chebyshev. Section independent_events. -Notation R := real_realType. - Variables (A : finType) (d : R.-fdist A). Definition inde_events (E F : {set A}) := Pr d (E :&: F) = Pr d E * Pr d F. @@ -1268,8 +1235,6 @@ Qed. End independent_events. Section k_wise_independence. -Notation R := real_realType. - Variables (A I : finType) (k : nat) (d : R.-fdist A) (E : I -> {set A}). Definition kwise_inde := forall (J : {set I}), (#|J| <= k)%nat -> @@ -1278,8 +1243,6 @@ Definition kwise_inde := forall (J : {set I}), (#|J| <= k)%nat -> End k_wise_independence. Section pairwise_independence. -Notation R := real_realType. - Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}). Definition pairwise_inde := @kwise_inde A I 2%nat d E. @@ -1307,8 +1270,6 @@ Qed. End pairwise_independence. Section mutual_independence. -Notation R := real_realType. - Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}). Definition mutual_inde := (forall k, @kwise_inde A I k.+1 d E). @@ -1337,7 +1298,6 @@ Qed. End mutual_independence. Section conditional_probablity. -Notation R := real_realType. Variables (A : finType) (d : R.-fdist A). Implicit Types E F : {set A}. @@ -1458,7 +1418,6 @@ Notation "`Pr_ P [ E | F ]" := (cPr P E F) : proba_scope. Global Hint Resolve cPr_ge0 : core. Section fdist_cond. -Notation R := real_realType. Variables (A : finType) (P : R.-fdist A) (E : {set A}). Hypothesis E0 : Pr P E != 0. @@ -1484,7 +1443,6 @@ Definition fdist_cond : {fdist A} := locked (FDist.make f0 f1). End fdist_cond. Section fdist_cond_prop. -Notation R := real_realType. Variables (A : finType) (P : R.-fdist A) (E : {set A}). Hypothesis E0 : Pr P E != 0. @@ -1541,7 +1499,6 @@ by apply/fdist_proj23_domin/H; rewrite inE /= bF cG. Qed. Section conditionally_independent_events. -Notation R := real_realType. Variables (A : finType) (d : R.-fdist A). Definition cinde_events (E F G : {set A}) := @@ -1566,7 +1523,6 @@ Proof. by split; rewrite /cinde_events /inde_events !cPrET. Qed. End conditionally_independent_events. Section crandom_variable_eqType. -Notation R := real_realType. Variables (U : finType) (A B : eqType) (P : R.-fdist U). Definition cpr_eq (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) := @@ -1594,7 +1550,6 @@ by apply/setP => u; rewrite !inE xpair_eqE. Qed. Section crandom_variable_finType. -Notation R := real_realType. Variables (U A B : finType) (P : R.-fdist U). Implicit Types X : {RV P -> A}. @@ -1648,7 +1603,6 @@ by rewrite setTE Pr_fdistmap_RV2; congr Pr; apply/setP => u; rewrite !inE. Qed. Section cpr_pair. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (A B C D : finType) (TA TB TC TD : eqType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}). Variables (TX : {RV P -> TA}) (TY : {RV P -> TB}) (TZ : {RV P -> TC}) (TW : {RV P -> TD}). @@ -1811,8 +1765,6 @@ by apply eq_bigr => b _; rewrite pr_in_pairAC. Qed. Section conditionnally_independent_discrete_random_variables. -Notation R := real_realType. - Variables (U : finType) (P : R.-fdist U) (A B C : eqType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}). @@ -1836,8 +1788,6 @@ Notation "X _|_ Y | Z" := (cinde_rv X Y Z) : proba_scope. Section conditionnally_independent_discrete_random_variables_extra. -Notation R := real_realType. - Variables (U: finType) (P : R.-fdist U) (A B C: finType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}). @@ -1847,8 +1797,6 @@ Proof. move=>H a b c. by rewrite mulRC cpr_eq_pairC. Qed. End conditionnally_independent_discrete_random_variables_extra. Section independent_rv. -Notation R := real_realType. - Variables (A : finType) (P : R.-fdist A) (TA TB : eqType). Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). @@ -2025,7 +1973,6 @@ End sum_two_rand_var. Section expected_value_of_the_product. Section thm64. -Notation R := real_realType. Variables (A B : finType) (P : R.-fdist (A * B)). Variables (X : {RV (P`1) -> R}) (Y : {RV (P`2) -> R}). @@ -2072,8 +2019,6 @@ End thm64. End expected_value_of_the_product. Section sum_n_rand_var_def. -Notation R := real_realType. - Variables (A : finType) (P : R.-fdist A). Inductive sum_n : forall n, {RV (P `^ n) -> R} -> 'rV[{RV P -> R}]_n -> Prop := @@ -2087,8 +2032,6 @@ End sum_n_rand_var_def. Notation "X '\=sum' Xs" := (sum_n X Xs) : proba_scope. Section independent_rv_lemma. -Notation R := real_realType. - Variables (A B : finType) (P1 : R.-fdist A) (P2 : R.-fdist B) (TA TB : eqType). Variable (X : {RV P1 -> TA}) (Y : {RV P2 -> TB}). Let P := P1 `x P2. @@ -2134,8 +2077,6 @@ Qed. Local Close Scope vec_ext_scope. Section sum_n_rand_var. -Notation R := real_realType. - Variable (A : finType) (P : R.-fdist A). Local Open Scope vec_ext_scope. @@ -2202,8 +2143,6 @@ Qed. End sum_n_rand_var. Section weak_law_of_large_numbers. -Notation R := real_realType. - Local Open Scope vec_ext_scope. Variables (A : finType) (P : R.-fdist A) (n : nat). @@ -2235,7 +2174,6 @@ End weak_law_of_large_numbers. (* wip*) Section vector_of_RVs. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (A : finType) (n : nat) (X : 'rV[{RV P -> A}]_n). Local Open Scope ring_scope. @@ -2244,7 +2182,6 @@ Definition RVn : {RV P -> 'rV[A]_n} := fun x => \row_(i < n) (X ``_ i) x. End vector_of_RVs. Section prob_chain_rule. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U) (A : finType). Local Open Scope vec_ext_scope. @@ -2272,7 +2209,6 @@ End prob_chain_rule. Section more_rv_lemmas. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (TA TB UA UB : eqType) (f : TA -> UA) (g : TB -> UB). Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). @@ -2305,7 +2241,6 @@ End more_preimset. Section more_pr_lemmas. -Notation R := real_realType. Variables (U : finType) (P : R.-fdist U). Variables (TA UA : finType) (f : TA -> UA) (X : {RV P -> TA}). @@ -2336,7 +2271,6 @@ End more_fdist. Section more_inde_rv. -Notation R := real_realType. Variables (A : finType) (P : R.-fdist A) (TA TB : finType). Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). diff --git a/probability/smc.v b/probability/smc.v index bc0478ef..794953e0 100644 --- a/probability/smc.v +++ b/probability/smc.v @@ -1,8 +1,10 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg matrix. + +From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. +From mathcomp Require Import reals Rstruct zmodp. Require Import Reals. -From mathcomp Require Import Rstruct zmodp. + Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist. Require Import proba jfdist_cond graphoid. Import GRing.Theory. @@ -18,11 +20,13 @@ Unset Strict Implicit. Import Prenex Implicits. Local Open Scope R_scope. + +Local Open Scope reals_ext_scope. Local Open Scope proba_scope. Local Open Scope fdist_scope. Section more_independent_rv_lemmas. -Notation R := real_realType. + Variables (A : finType) (P : R.-fdist A) (TA TB TC TD : finType). Variables (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}). Variables (UA UB : finType) (f : TA -> UA) (g : TB -> UB). @@ -87,8 +91,6 @@ End more_independent_rv_lemmas. Section lemma_3_4. - -Notation R := real_realType. Lemma cpr_eqE_mul (U : finType) (P : {fdist U}) (TA TB : eqType) (X : {RV P -> TA}) (Y : {RV P -> TB}) a b : `Pr[ X = a | Y = b ] * `Pr[Y = b] = `Pr[ [% X, Y] = (a, b) ].