From d123716013c0a2de33bac39aa1909e50c5655b5c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 16 Jan 2026 21:11:17 +0900 Subject: [PATCH 1/2] workaround for intrD1 --- information_theory/joint_typ_seq.v | 3 ++- information_theory/source_coding_vl_converse.v | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v index e19d44f59..2c643013d 100644 --- a/information_theory/joint_typ_seq.v +++ b/information_theory/joint_typ_seq.v @@ -110,7 +110,8 @@ Definition Nup (x : R) := `| Num.floor x |.+1. Lemma Nup_gt x : x < (Nup x)%:R. Proof. apply: (lt_le_trans (floorD1_gt x)). -by rewrite /Nup -intrD1 -natr1 lerD // natr_absz ler_int ler_norm. +rewrite /Nup [leLHS](_ : _ = (Num.Def.floor x)%:~R + 1%:~R) ?intrD1//. +by rewrite -natr1 lerD // natr_absz ler_int ler_norm. Qed. Definition JTS_1_bound := diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v index eb6ce626b..b0f46b113 100644 --- a/information_theory/source_coding_vl_converse.v +++ b/information_theory/source_coding_vl_converse.v @@ -2,6 +2,7 @@ (* Copyright (C) 2025 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix. From mathcomp Require Import archimedean lra ring. +From mathcomp Require Import mathcomp_extra. From mathcomp Require Import unstable contra reals normedtype sequences exp. Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln. Require Import fdist proba entropy divergence log_sum source_code. @@ -779,8 +780,9 @@ apply: (@le_trans _ _ ((x ^ 2 / 2 - 1) * eps * n%:R)); last first. rewrite /m /x. rewrite lerBlDr. rewrite (le_trans (ltW (floorD1_gt _)))//. - rewrite natr_absz intrD1 ler_int. - by rewrite lerD2r ler_norm. + rewrite natr_absz. + rewrite [leRHS](_ : _ = (`|floor (expR (m' eps))| + 1)%:~R) -?intrD1//. + by rewrite ler_int lerD2r ler_norm. rewrite logM//; last exact: mpos. rewrite -(ler_pM2r ln2_gt0). rewrite mulrDl -(mulrA (ln alp)) (mulVf ln2_neq0). From 87c2eb266fd75f20731f09b35b395a42e51e8e8f Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 16 Jan 2026 21:23:42 +0900 Subject: [PATCH 2/2] more tweaks --- information_theory/joint_typ_seq.v | 3 ++- information_theory/source_coding_vl_converse.v | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v index 2c643013d..3299d1e44 100644 --- a/information_theory/joint_typ_seq.v +++ b/information_theory/joint_typ_seq.v @@ -110,7 +110,8 @@ Definition Nup (x : R) := `| Num.floor x |.+1. Lemma Nup_gt x : x < (Nup x)%:R. Proof. apply: (lt_le_trans (floorD1_gt x)). -rewrite /Nup [leLHS](_ : _ = (Num.Def.floor x)%:~R + 1%:~R) ?intrD1//. +rewrite /Nup. +rewrite [leLHS](_ : _ = (Num.Def.floor x)%:~R + 1%:~R); last by rewrite intrD1. by rewrite -natr1 lerD // natr_absz ler_int ler_norm. Qed. diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v index b0f46b113..3e5262d6f 100644 --- a/information_theory/source_coding_vl_converse.v +++ b/information_theory/source_coding_vl_converse.v @@ -781,7 +781,7 @@ apply: (@le_trans _ _ ((x ^ 2 / 2 - 1) * eps * n%:R)); last first. rewrite lerBlDr. rewrite (le_trans (ltW (floorD1_gt _)))//. rewrite natr_absz. - rewrite [leRHS](_ : _ = (`|floor (expR (m' eps))| + 1)%:~R) -?intrD1//. + rewrite [leRHS](_ : _ = (`|floor (expR (m' eps))| + 1)%:~R); last by rewrite intrD1. by rewrite ler_int lerD2r ler_norm. rewrite logM//; last exact: mpos. rewrite -(ler_pM2r ln2_gt0).