Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

compatibility with Coq 8.20 #131

Merged
merged 3 commits into from
Oct 24, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
compatibility with Coq 8.20
affeldt-aist committed Oct 24, 2024
commit 5fe7f1da8c2493a95605af8845057b928622a5f8
1 change: 1 addition & 0 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -19,6 +19,7 @@ jobs:
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
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -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.18--8.20
- Additional dependencies:
- [MathComp ssreflect](https://math-comp.github.io)
- [MathComp fingroup](https://math-comp.github.io)
2 changes: 1 addition & 1 deletion coq-infotheo.opam
Original file line number Diff line number Diff line change
@@ -21,7 +21,7 @@ build: [
]
install: [make "install"]
depends: [
"coq" { (>= "8.18" & < "8.20~") | (= "dev") }
"coq" { (>= "8.18" & < "8.21~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
"coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
"coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") }
10 changes: 5 additions & 5 deletions information_theory/jtypes.v
Original file line number Diff line number Diff line change
@@ -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.
26 changes: 13 additions & 13 deletions information_theory/types.v
Original file line number Diff line number Diff line change
@@ -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})
6 changes: 4 additions & 2 deletions meta.yml
Original file line number Diff line number Diff line change
@@ -43,14 +43,16 @@ license:
nix: true

supported_coq_versions:
text: Coq 8.18--8.19
opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
text: Coq 8.18--8.20
opam: '{ (>= "8.18" & < "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:
7 changes: 5 additions & 2 deletions probability/convex_equiv.v
Original file line number Diff line number Diff line change
@@ -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.

Unchanged files with check annotations Beta

(* 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.

Check warning on line 4 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

Check warning on line 4 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "\pi ( _ )" defined at level 2 and "\pi"
Require Import Reals.
From mathcomp Require Import lra.
From mathcomp Require Import Rstruct.
(* *)
(******************************************************************************)
Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").

Check warning on line 63 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Postfix notations (i.e. starting with a nonterminal symbol and
Reserved Notation "'min(' x ',' y ')'" (format "'min(' x ',' y ')'").
Reserved Notation "'max(' x ',' y ')'" (format "'max(' x ',' y ')'").
Proof. by rewrite -{1}(addR0 x) ltR_add2l. Qed.
Lemma subR_gt0 x y : (0 < y - x) <-> (x < y).
Proof. by split; [exact: Rminus_gt_0_lt | exact: Rlt_Rminus]. Qed.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rminus_gt_0_lt is deprecated since 8.19.
Lemma subR_lt0 x y : (y - x < 0) <-> (y < x).
Proof. by split; [exact: Rminus_lt | exact: Rlt_minus]. Qed.
Lemma subR_ge0 x y : (0 <= y - x) <-> (x <= y).
(* 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.

Check warning on line 4 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

Check warning on line 4 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "\pi ( _ )" defined at level 2 and "\pi"
From mathcomp Require Import reals normedtype.

Check warning on line 5 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "{ ' _ | _ }" defined at level 0
From mathcomp Require Import mathcomp_extra boolp.
From mathcomp Require Import lra ring Rstruct.
Proof. by apply/dominatesP. Qed.
Let dominatesN A (Q P : A -> R) : P `<< Q -> forall a, P a != 0%R -> Q a != 0%R.
Proof. by move/dominatesP => H a; apply: contra => /eqP /H ->. Qed.

Check warning on line 102 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

dominatesN is declared opaque (Qed) but this is not fully respected
Lemma dominatesE A (Q P : A -> R) a : P `<< Q -> Q a = 0%R -> P a = 0%R.
Proof. move/dominatesP; exact. Qed.
End dominance.
Notation "P '`<<' Q" := (dominates Q P) : reals_ext_scope.

Check warning on line 121 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Declaring a scope implicitly is deprecated; use in advance an

Check warning on line 121 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Declaring a scope implicitly is deprecated; use in advance an
Notation "P '`<<b' Q" := (dominatesb Q P) : reals_ext_scope.
(* ---- Prob ---- *)
by apply/eqP/val_inj; rewrite inord_val.
- by apply/matrixP => i j; rewrite !mxE.
- by rewrite mul0r addr0 -det_tr.
Qed.

Check warning on line 673 in lib/ssralg_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

det_mlinear_rec is declared opaque (Qed) but this is not fully
Lemma det_mlinear (n: nat) (f : 'I_n -> 'I_n -> R) (g : 'I_n -> R) :
\det (\matrix_(i, j) (f i j * g j)) =
Proof.
have [/RleP ? /RleP ?] : (0 <= / IZR (Zpos p) <= 1)%coqR.
split; first exact/Rlt_le/Rinv_0_lt_compat/IZR_lt/Pos2Z.is_pos.
rewrite -[X in (_ <= X)%coqR]Rinv_1; apply Rle_Rinv => //.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
- exact/IZR_lt/Pos2Z.is_pos.
- exact/IZR_le/Pos2Z.pos_le_pos/Pos.le_1_l.
exact/andP.
rewrite mulRC mulRA mulRC; congr (_ * _).
rewrite factS natRM invRM ?INR_eq0' //; last by rewrite -lt0n fact_gt0.
by rewrite mulRC mulRA mulRV ?mul1R // INR_eq0'.
Qed.

Check warning on line 95 in lib/logb.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

exp_dev_rec is declared opaque (Qed) but this is not fully respected
Let exp_dev_gt0 : forall n r, 0 < r -> 0 < exp_dev n r.
Proof.
Section trivIset.
Import boolp classical_sets.
From mathcomp Require Import measure probability.

Check warning on line 964 in probability/fsdist.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Use of “Require” inside a section is fragile. It is not recommended
Local Open Scope classical_set_scope.
Context [T : Type] [I : eqType].
Variables (D : set I) (F : I -> set T)
Variable n : nat.
Variable types : 'I_n -> eqType.
Definition univ_types : eqType :=
[eqType of {dffun forall i, types i}].

Check warning on line 111 in probability/bayes.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation "[ eqType of _ ]" is deprecated since mathcomp 2.0.0.
Section prod_types.
(* sets of indices *)
Variable I : {set 'I_n}.
Definition prod_types :=
[eqType of

Check warning on line 118 in probability/bayes.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation "[ eqType of _ ]" is deprecated since mathcomp 2.0.0.
{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.
Qed.
Lemma sq_dev_max_ge0 : 0 <= sq_dev_max.
Proof. by rewrite /sq_dev_max; apply/topology.bigmax_geP; left. Qed.

Check failure on line 410 in robust/weightedmean.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

The reference topology.bigmax_geP was not found in the current

Check failure on line 410 in robust/weightedmean.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

The reference topology.bigmax_geP was not found in the current
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.
(* TODO: we should maybe extend mczify's ssrZ... *)
Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").

Check warning on line 15 in lib/ssrZ.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Postfix notations (i.e. starting with a nonterminal symbol and
Declare Scope zarith_ext_scope.