From 58d8e62307887db54b4a0b344679c9c84d2e328f Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 24 Oct 2024 15:49:34 +0900 Subject: [PATCH] compatibility with Coq 8.20 (#131) * compatibility with Coq 8.20 --- .github/workflows/docker-action.yml | 2 +- README.md | 2 +- changelog.txt | 4 +++- coq-infotheo.opam | 4 ++-- information_theory/jtypes.v | 10 +++++----- information_theory/types.v | 26 +++++++++++++------------- meta.yml | 10 +++++----- probability/convex_equiv.v | 7 +++++-- robust/weightedmean.v | 2 +- 9 files changed, 36 insertions(+), 31 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index edc24fd9..90e3c33a 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,8 +17,8 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.2.0-coq-8.18' - 'mathcomp/mathcomp:2.2.0-coq-8.19' + - 'mathcomp/mathcomp:2.2.0-coq-8.20' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index c01bb18f..9cfc7bdb 100644 --- a/README.md +++ b/README.md @@ -32,7 +32,7 @@ information theory, and linear error-correcting codes. - Naruomi Obata, Titech (M2) - Alessandro Bruni, IT-University of Copenhagen - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.18--8.19 +- Compatible Coq versions: Coq 8.19--8.20 - 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 c688fe5a..946b68f3 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,4 +1,6 @@ - +------------------- +from 0.7.2 to 0.7.3 +------------------- - lemma `conv_pt_cset_is_convex` changed into a `Let` diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 97f0969e..6d20793e 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -21,13 +21,13 @@ build: [ ] install: [make "install"] depends: [ - "coq" { (>= "8.18" & < "8.20~") | (= "dev") } + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } "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.2.0") } + "coq-mathcomp-analysis" { (>= "1.5.0") } "coq-hierarchy-builder" { >= "1.5.0" } "coq-mathcomp-algebra-tactics" { >= "1.2.0" } "coq-interval" { >= "4.10.0"} diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v index 2207417f..4a87c90b 100644 --- a/information_theory/jtypes.v +++ b/information_theory/jtypes.v @@ -654,13 +654,13 @@ Local Open Scope nat_scope. Definition type_of_row (a : A) (Ha : N(a | ta) != 0) : P_ N(a | ta) ( B ). pose f := [ffun b => Ordinal (ctyp_element_ub Hrow_num_occ Hta a b)]. pose d := [ffun b => ((f b)%:R / N(a | ta)%:R)%R]. -have d0 : forall b, (0 <= d b)%mcR. +assert (d0 : forall b, (0 <= d b)%mcR). move=> b. apply/RleP. rewrite /d /= ffunE. apply mulR_ge0; first exact/leR0n. apply/invR_ge0/ltR0n; by rewrite lt0n. -have d1 : (\sum_(b : B) d b)%R = 1%R. +assert (d1 : (\sum_(b : B) d b)%R = 1%R). under eq_bigr do rewrite ffunE /=. rewrite -big_distrl /= -big_morph_natRD. set lhs := \sum_i _. @@ -1240,17 +1240,17 @@ Hypothesis Bnot0 : (0 < #|B|)%nat. Definition num_co_occ_jtype (ta : n.-tuple A) (tb : n.-tuple B) : P_ n (A , B). set f := [ffun a => [ffun b => Ordinal (num_co_occ_ub a b ta tb)]]. -have Hf : \sum_(a in A) \sum_(b in B) f a b == n. +assert (Hf : \sum_(a in A) \sum_(b in B) f a b == n). rewrite /f. apply/eqP. transitivity (\sum_a \sum_b N(a, b|ta, tb)); last by rewrite num_co_occ_sum. apply eq_big => a //= _. apply eq_big => b //= _. by rewrite 2!ffunE. -have Htmp' : (forall a b, +assert (Htmp' : (forall a b, (chan_of_jtype Anot0 Bnot0 f) a b = (let ln := (\sum_(b0 in B) (f a) b0)%nat in - if ln == O then / #|B|%:R else (((f a) b)%:R / ln%:R))%R). + if ln == O then / #|B|%:R else (((f a) b)%:R / ln%:R))%R)). by move=> a b; rewrite ffunE. exact (@JType.mk _ _ _ (chan_of_jtype Anot0 Bnot0 f) f Hf Htmp'). Defined. diff --git a/information_theory/types.v b/information_theory/types.v index f3969f1a..c8b2c9d0 100644 --- a/information_theory/types.v +++ b/information_theory/types.v @@ -90,10 +90,10 @@ Definition type_of_tuple (A : finType) n (ta : n.+1.-tuple A) : P_ n.+1 ( A ). set f := [ffun a => N(a | ta)%:R / n.+1%:R]. assert (H1 : forall a, (0%mcR <= f a)%mcR). move=> a; rewrite ffunE; apply/RleP/divR_ge0; by [apply leR0n | apply ltR0n]. -have H2 : \sum_(a in A) f a = 1%R. +assert (H2 : \sum_(a in A) f a = 1%R). under eq_bigr do rewrite ffunE /=. by rewrite -big_distrl /= -big_morph_natRD sum_num_occ_alt mulRV // INR_eq0'. -have H : forall a, (N(a | ta) < n.+2)%nat. +assert (H : forall a, (N(a | ta) < n.+2)%nat). move=> a; rewrite ltnS; by apply num_occ_leq_n. refine (@type.mkType _ n.+1 (FDist.make H1 H2) [ffun a => @Ordinal n.+2 (N(a | ta)) (H a)] _). @@ -141,22 +141,22 @@ Qed. Definition fdist_of_ffun (A : finType) n (f : {ffun A -> 'I_n.+2}) (Hf : (\sum_(a in A) f a)%nat == n.+1) : {fdist A}. set pf := [ffun a : A => INR (f a) / INR n.+1]. -have H : (\sum_(a in A) pf a)%mcR = 1 :> R. +assert (pf_ge0 : forall a, (0 <= pf a)%mcR). + move=> a; apply/RleP. + rewrite /pf/= ffunE; apply: divR_ge0 => //. + apply/RleP. + rewrite INRE. + by rewrite Num.Theory.ler0n. + apply/RltP. + rewrite INRE. + by rewrite Num.Theory.ltr0n. +assert (H : (\sum_(a in A) pf a)%mcR = 1 :> R). rewrite /pf; under eq_bigr do rewrite ffunE /=. rewrite /Rdiv -big_distrl /= -big_morph_natRD. move/eqP : Hf => ->. rewrite -RmultE. by rewrite mulRV// INR_eq0'. -apply: (FDist.make _ H). -move=> a. -apply/RleP. -rewrite /pf/= ffunE; apply: divR_ge0 => //. - apply/RleP. - rewrite INRE. - by rewrite Num.Theory.ler0n. -apply/RltP. -rewrite INRE. -by rewrite Num.Theory.ltr0n. +exact: (FDist.make pf_ge0 H). Defined. Lemma fdist_of_ffun_prop (A : finType) n (f : {ffun A -> 'I_n.+2}) diff --git a/meta.yml b/meta.yml index 1911d312..ac8b8431 100644 --- a/meta.yml +++ b/meta.yml @@ -43,14 +43,14 @@ license: nix: true supported_coq_versions: - text: Coq 8.18--8.19 - opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }' + text: Coq 8.19--8.20 + opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }' tested_coq_opam_versions: -- version: '2.2.0-coq-8.18' - repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-8.20' + repo: 'mathcomp/mathcomp' dependencies: - opam: @@ -80,7 +80,7 @@ dependencies: [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "1.2.0") }' + version: '{ (>= "1.5.0") }' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index 065798f6..8663b5fd 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -295,10 +295,13 @@ 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. +#[local] +Definition 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. +#[local] +Definition T' := NaryConv_sort__canonical__convex_ConvexSpace. Lemma equiv_conv p (a b : C.T) : a <| p |> b = a <& p &> b. Proof. diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 4338d8a0..75e978bb 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -407,7 +407,7 @@ by move=> *; exact/sq_dev_ge0. Qed. Lemma sq_dev_max_ge0 : 0 <= sq_dev_max. -Proof. by rewrite /sq_dev_max; apply/topology.bigmax_geP; left. Qed. +Proof. by rewrite /sq_dev_max; apply/boolp.bigmax_geP; left. Qed. Lemma sq_dev_max_ge u : C u != 0 -> sq_dev u <= sq_dev_max. Proof. by move=> Cu0; rewrite /sq_dev_max; apply/le_bigmax_cond. Qed.