From 934ed6b9219b83c6f04838f62bba6b7590067ed2 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 15 Apr 2024 19:38:37 +0900 Subject: [PATCH] convex_equiv.v needs to be fixed --- probability/convex.v | 20 ++++----- probability/convex_equiv.v | 66 ++++++++++++++++++++++-------- probability/partition_inequality.v | 4 +- 3 files changed, 61 insertions(+), 29 deletions(-) diff --git a/probability/convex.v b/probability/convex.v index 95184d96..574b793a 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -307,7 +307,7 @@ HB.mixin Record isConvexSpace0 T of Choice 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 isConvexSpace0 T }. +HB.structure Definition ConvexSpace := {T of isConvexSpace0 T & }. Notation "a <| p |> b" := (conv p a b) : convex_scope. Local Open Scope convex_scope. @@ -485,7 +485,7 @@ HB.mixin Record isQuasiRealCone A of Choice A := { scalept p (scalept q x) = scalept (p * q)%coqR x }. #[short(type=quasiRealCone)] -HB.structure Definition QuasiRealCone := { A & isQuasiRealCone A}. +HB.structure Definition QuasiRealCone := { A of isQuasiRealCone A & }. Section quasireal_cone_theory. Variable A : quasiRealCone. @@ -543,7 +543,7 @@ HB.mixin Record isRealCone A of QuasiRealCone A := { }. #[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. @@ -2958,9 +2958,9 @@ TODO: see convex_type.v Section convex_set_R. -Let pos := (fun x => 0 < x)%coqR. +Definition Rpos_interval : set R := (fun x => 0 < x)%coqR. -Lemma Rpos_convex : is_convex_set pos. +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. @@ -2969,15 +2969,15 @@ apply mulR_ge0 => //; exact: ltRW. Qed. (*#[local]*) -HB.instance Definition Rpos_interval := isConvexSet.Build R pos Rpos_convex. +HB.instance Definition _ := isConvexSet.Build R Rpos_interval Rpos_convex. -Let nneg := (fun x => 0 <= x)%coqR. +Definition Rnonneg_interval : set R := (fun x => 0 <= x)%coqR. -Lemma Rnonneg_convex : is_convex_set nneg. +Lemma Rnonneg_convex : is_convex_set Rnonneg_interval. Proof. apply/asboolP=> x y t Hx Hy; apply addR_ge0; exact/mulR_ge0. Qed. (*#[local]*) -HB.instance Definition Rnonneg_interval := isConvexSet.Build R nneg Rnonneg_convex. +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. @@ -2996,7 +2996,7 @@ rewrite mulrDl. apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1]. Qed. -Let uniti := (fun x => 0 < x < 1)%coqR. +Let uniti : set R := (fun x => 0 < x < 1)%coqR. Lemma open_unit_interval_convex : is_convex_set uniti. Proof. exact: open_interval_convex. Qed. diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index 0a684362..0f984640 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -179,7 +179,7 @@ Module Type ConvSpace. Axiom T : convType. End ConvSpace. Module BinToNary(C : ConvSpace) <: NaryConvSpace. Import NaryConvexSpace. -HB.instance Definition _ := @isNaryConv.Build C.T (@Convn C.T). +HB.instance Definition _ := @isNaryConv.Build C.T (@Convn C.T conv). (* NB: is that ok? *) Definition T : naryConvType := C.T. @@ -295,7 +295,7 @@ 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 binconv +HB.instance Definition nary_to_bin := @isConvexSpace.Build A.T binconv binconv1 binconvmm binconvC binconvA. End NaryToBin. @@ -307,21 +307,6 @@ 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*))/=. -rewrite (_ : a <&p&> b = a <|p|> b)//. - by rewrite [RHS](@affine_conv (*NaryConv_sort__canonical__isConvexSpace__ConvexSpace*)_). -Admitted. - -End Equiv1. - Module Equiv2(A : NaryConvSpace). Module B := NaryToBin(A). Import A B. @@ -353,8 +338,55 @@ 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. +Lemma convnE (s : convType) (n : nat) (d : R.-fdist 'I_n) (g : 'I_n -> s) : + convex.convn n d g = <|>_d g. +Proof. Abort. + +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. + +STOP + +rewrite -equiv_convn. +by rewrite EA.equiv_convn. +Qed. + +End Equiv1. + Module Type MapConst. Parameter T : naryConvType. Parameter axmap : ax_map T. 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.