From 4ad3c323f591179902a000bf3aee3c1e93bb2536 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 22 Apr 2024 02:11:58 +0900 Subject: [PATCH] less warnings, CI --- .github/workflows/docker-action.yml | 13 ++++++------- README.md | 2 +- coq-infotheo.opam | 14 +++++++------- ecc_classic/decoding.v | 20 +++++++++---------- ecc_classic/hamming_code.v | 10 +++++----- ecc_classic/linearcode.v | 18 ++++++++--------- ecc_classic/repcode.v | 4 ++-- ecc_modern/degree_profile.v | 2 +- information_theory/entropy.v | 2 +- information_theory/shannon_fano.v | 6 +++--- information_theory/typ_seq.v | 2 +- lib/Reals_ext.v | 4 ++-- lib/bigop_ext.v | 2 +- lib/dft.v | 4 ++-- lib/hamming.v | 2 +- meta.yml | 30 ++++++++++++++--------------- probability/bayes.v | 2 +- probability/convex.v | 6 +++--- probability/convex_equiv.v | 8 ++++---- probability/fdist.v | 2 +- probability/fsdist.v | 8 ++++---- 21 files changed, 79 insertions(+), 82 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index a2a581e6..8b840348 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,13 +17,12 @@ 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.0.0-coq-8.17' + - 'mathcomp/mathcomp:2.0.0-coq-8.18' + - 'mathcomp/mathcomp:2.0.0-coq-8.19' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.1.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/coq-infotheo.opam b/coq-infotheo.opam index 98e18bac..b0d9fef8 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.0.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" & < "1.20.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/decoding.v b/ecc_classic/decoding.v index 351d21f5..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,7 +130,7 @@ 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. +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. @@ -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,7 +286,7 @@ 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 R (vspace_not_empty C). @@ -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/hamming_code.v b/ecc_classic/hamming_code.v index d0f34929..e5136c4b 100644 --- a/ecc_classic/hamming_code.v +++ b/ecc_classic/hamming_code.v @@ -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. @@ -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. @@ -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'). diff --git a/ecc_classic/linearcode.v b/ecc_classic/linearcode.v index e0fa83a8..f5692e5b 100644 --- a/ecc_classic/linearcode.v +++ b/ecc_classic/linearcode.v @@ -489,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. @@ -658,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. @@ -671,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 @@ -741,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. @@ -774,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. @@ -859,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. @@ -1018,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. @@ -1036,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/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/degree_profile.v b/ecc_modern/degree_profile.v index 9256b446..84f1a516 100644 --- a/ecc_modern/degree_profile.v +++ b/ecc_modern/degree_profile.v @@ -444,7 +444,7 @@ HB.instance Definition _ n l := @isFinite.Build (fintree n l) _ (@fintree_enumP 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. diff --git a/information_theory/entropy.v b/information_theory/entropy.v index a99951cb..063186d9 100644 --- a/information_theory/entropy.v +++ b/information_theory/entropy.v @@ -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/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/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/lib/Reals_ext.v b/lib/Reals_ext.v index 2430364b..ad13510c 100644 --- a/lib/Reals_ext.v +++ b/lib/Reals_ext.v @@ -298,9 +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 ler_addl. +by rewrite lerDl. Qed. Definition Prob_invp (p : {prob R}) := Prob.mk (prob_invp_subproof p). diff --git a/lib/bigop_ext.v b/lib/bigop_ext.v index 856b67a4..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. diff --git a/lib/dft.v b/lib/dft.v index 1f220d6d..bea351fd 100644 --- a/lib/dft.v +++ b/lib/dft.v @@ -131,8 +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 /sub/=(_ : Ordinal jn = j) //. -by apply/val_inj. +rewrite /Sub/= (_ : Ordinal jn = j) //. +exact/val_inj. Qed. End frequency_domain_coordinates. diff --git a/lib/hamming.v b/lib/hamming.v index 5c98b430..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. diff --git a/meta.yml b/meta.yml index f456a6af..f4aaa8a2 100644 --- a/meta.yml +++ b/meta.yml @@ -41,54 +41,52 @@ 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.0.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.17' +- version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.19.0-coq-8.17' +- version: '2.0.0-coq-8.19' repo: 'mathcomp/mathcomp' -- version: '1.17.0-coq-8.18' +- version: '2.1.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.18' +- version: '2.1.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.1.0-coq-8.19' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.16.0" & < "1.20.0") | (= "dev") }' + version: '{ (>= "2.0.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" & < "1.20.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 +96,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 8e724f3c..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 *) diff --git a/probability/convex.v b/probability/convex.v index 6971b703..1f1b75ec 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -1970,16 +1970,16 @@ Let avgA p q (d0 d1 d2 : R) : Proof. by rewrite /avg convA. Qed. #[export] -(* TODO(rei): attributed needed? *) +(* 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. diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index c2d89875..065798f6 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -44,7 +44,7 @@ HB.mixin Record isNaryConv (T : Type) of Choice 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. @@ -529,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/fdist.v b/probability/fdist.v index 3de9bcba..b90b3b96 100644 --- a/probability/fdist.v +++ b/probability/fdist.v @@ -1379,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. diff --git a/probability/fsdist.v b/probability/fsdist.v index 5a68b562..507b91d3 100644 --- a/probability/fsdist.v +++ b/probability/fsdist.v @@ -444,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) /=. @@ -452,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. @@ -532,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. @@ -556,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.