From 49c44066f29589f59b61ac218a6dc62d82b7994d Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 24 May 2024 16:20:01 +0900 Subject: [PATCH] porting to MathComp 2 (#131) Co-authored-by: Takafumi Saikawa --- .github/workflows/docker-action.yml | 7 +- README.md | 2 +- altprob_model.v | 22 ++-- array_lib.v | 6 +- coq-monae.opam | 18 ++-- example_iquicksort.v | 24 ++--- example_monty.v | 27 +++-- example_typed_store.v | 10 +- fail_lib.v | 65 +++++++++--- gcm_model.v | 70 ++++++------- hierarchy.v | 11 +- impredicative_set/ifmt_lifting.v | 2 +- impredicative_set/ihierarchy.v | 55 +++++----- impredicative_set/imonad_composition.v | 8 +- impredicative_set/imonad_lib.v | 28 ++--- impredicative_set/imonad_transformer.v | 10 +- meta.yml | 28 +++-- monad_model.v | 41 ++++---- monae_lib.v | 2 +- proba_lib.v | 140 ++++++++++++++----------- proba_monad_model.v | 9 +- smallstep.v | 2 +- state_lib.v | 4 +- 23 files changed, 309 insertions(+), 282 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0b4f3d91..8cfab4bc 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,10 +17,9 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.17.0-coq-8.17' - - 'mathcomp/mathcomp:1.18.0-coq-8.17' - - 'mathcomp/mathcomp:1.17.0-coq-8.18' - - 'mathcomp/mathcomp:1.18.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.17' + - 'mathcomp/mathcomp:2.2.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 2e3ab865..ef2f2d6f 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ in several examples of monadic equational reasoning. - Celestine Sauvage - Kazunari Tanaka - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.16-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/altprob_model.v b/altprob_model.v index e952a075..e7e410be 100644 --- a/altprob_model.v +++ b/altprob_model.v @@ -97,7 +97,7 @@ Proof. exact: scsl_hom_is_lubmorph. Qed. (* Local Notation F1o := necset_semiCompSemiLattConvType. *) -Local Notation F0o := FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *) +Local Notation F0o := FSDist.t. (*FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *)*) Local Notation FCo := choice_of_Type. Local Notation F1m := free_semiCompSemiLattConvType_mor. Local Notation F0m := free_convType_mor. @@ -130,7 +130,7 @@ Proof. by rewrite convC. Qed. Lemma choicemm A p : idempotent (@choice p A). Proof. by move=> m; rewrite /choice convmm. Qed. -Let choiceA A (p q r s : {prob [realType of R]}) (x y z : gcm A) : +Let choiceA A (p q r s : {prob R}) (x y z : gcm A) : x <| p |> (y <| q |> z) = (x <| [r_of p, q] |> y) <| [s_of p, q] |> z. Proof. exact: convA. Qed. @@ -156,7 +156,7 @@ Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left T))))) p : Proof. exact: scsl_hom_is_affine. Qed. (*Local Notation F1o := necset_semiCompSemiLattConvType.*) -Local Notation F0o := FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *) +Local Notation F0o := FSDist.t. Local Notation FCo := choice_of_Type. Local Notation F1m := free_semiCompSemiLattConvType_mor. Local Notation F0m := free_convType_mor. @@ -172,20 +172,20 @@ Qed. End bindchoiceDl. HB.instance Definition _ := - isMonadConvex.Build real_realType (Monad_of_category_monad.acto Mgcm) + isMonadConvex.Build R (Monad_of_category_monad.acto Mgcm) choice1 choiceC choicemm choiceA. HB.instance Definition _ := - isMonadProb.Build real_realType (Monad_of_category_monad.acto Mgcm) bindchoiceDl. + isMonadProb.Build R (Monad_of_category_monad.acto Mgcm) bindchoiceDl. -Lemma choicealtDr A (p : {prob real_realType}) : +Lemma choicealtDr A (p : {prob R}) : right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A). Proof. by move=> x y z; rewrite /choice lubDr. Qed. HB.instance Definition _ := - @isMonadAltProb.Build real_realType (Monad_of_category_monad.acto Mgcm) choicealtDr. + @isMonadAltProb.Build R (Monad_of_category_monad.acto Mgcm) choicealtDr. -Definition gcmAP := [the altProbMonad real_realType of gcm]. +Definition gcmAP := [the altProbMonad R of gcm]. End P_delta_altProbMonad. @@ -194,15 +194,15 @@ Local Open Scope proba_monad_scope. (* An example that probabilistic choice in this model is not trivial: we can distinguish different probabilities. *) -Example gcmAP_choice_nontrivial (p q : {prob real_realType}) : +Example gcmAP_choice_nontrivial (p q : {prob R}) : p <> q -> (* Ret = hierarchy.ret *) Ret true <|p|> Ret false <> Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool. Proof. apply contra_not. -rewrite !gcm_retE /Choice /= => /(congr1 (@NECSet.car _)). -rewrite !necset_convType.convE !conv_cset1 /=. +rewrite !gcm_retE /hierarchy.choice => /(congr1 (@NECSet.sort _)). +rewrite /= !necset_convType.convE !conv_cset1 /=. move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true). rewrite !fsdist_convE !fsdist1xx !fsdist10//; last exact/eqP. (*TODO: we should not need that*) by rewrite !avgRE !mulR1 ?mulR0 ?addR0 => /val_inj. diff --git a/array_lib.v b/array_lib.v index 11a9e684..e3614ec4 100644 --- a/array_lib.v +++ b/array_lib.v @@ -26,7 +26,7 @@ Require Import hierarchy monad_lib fail_lib. Local Open Scope monae_scope. Section marray. -Context {d : unit} {E : porderType d} {M : arrayMonad E nat_eqType}. +Context {d : unit} {E : porderType d} {M : arrayMonad E nat}. Implicit Type i j : nat. Import Order.POrderTheory. @@ -78,7 +78,7 @@ Qed. Lemma aput_writeListCR i j (x : E) (xs : seq E) : j + size xs <= i -> aput i x >> writeList j xs = writeList j xs >> aput i x. -Proof. by move=> ?; rewrite -writeList1 -writeListC. Qed. +Proof. by move=> jxsu; rewrite -writeList1 -[LHS]writeListC. Qed. Lemma writeList_cat i (s1 s2 : seq E) : writeList i (s1 ++ s2) = writeList i s1 >> writeList (i + size s1) s2. @@ -175,7 +175,7 @@ Fixpoint readList i (n : nat) : M (seq E) := End marray. Section refin_writeList_aswap. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). (* eqn 13 in mu2020flops, postulate introduce-swap in IQSort.agda *) Lemma refin_writeList_cons_aswap (i : nat) x (s : seq E) : diff --git a/coq-monae.opam b/coq-monae.opam index 9cfc7447..6aee4eff 100644 --- a/coq-monae.opam +++ b/coq-monae.opam @@ -18,16 +18,16 @@ in several examples of monadic equational reasoning.""" build: [make "-j%{jobs}%"] install: [make "install_full"] depends: [ - "coq" { (>= "8.16" & < "8.19~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.19~") | (= "dev") } - "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.19~") | (= "dev") } - "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.19~") | (= "dev") } - "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.19~") | (= "dev") } - "coq-mathcomp-field" { (>= "1.16.0" & < "1.19~") | (= "dev") } - "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.7~")} - "coq-infotheo" { >= "0.6.0" & < "0.7~"} + "coq" { (>= "8.17" & < "8.20~") | (= "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.1.0")} + "coq-infotheo" { >= "0.7.1"} "coq-paramcoq" { >= "1.1.3" & < "1.2~" } - "coq-hierarchy-builder" { = "1.5.0" } + "coq-hierarchy-builder" { >= "1.5.0" } "coq-equations" { >= "1.3" & < "1.4~" } ] diff --git a/example_iquicksort.v b/example_iquicksort.v index 4931e01b..10f0fdeb 100644 --- a/example_iquicksort.v +++ b/example_iquicksort.v @@ -42,7 +42,7 @@ Local Open Scope monae_scope. Local Open Scope tuple_ext_scope. Section partl. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types p : E. (* tail-recursive *) @@ -66,7 +66,7 @@ Proof. by rewrite partlE /=; case: partition. Qed. End partl. Section dispatch. -Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. Definition dispatch (x p : E) '(ys, zs) A (f : seq E -> seq E -> M A) : M A := @@ -93,7 +93,7 @@ Arguments dispatch_Ret {d E M}. solve[exact: dispatch_Ret_isNondet] : core. Section qperm_partl. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types p : E. Fixpoint qperm_partl p (ys zs xs : seq E) : M (seq E * seq E)%type := @@ -132,7 +132,7 @@ Section ipartl. Variables (d : unit) (T : orderType d). Section arrayMonad. -Variable M : arrayMonad T nat_eqType. +Variable M : arrayMonad T nat. Fixpoint ipartl p i ny nz nx : M (nat * nat)%type := if nx is k.+1 then @@ -147,7 +147,7 @@ End arrayMonad. Arguments ipartl {M}. Section plusArrayMonad. -Variable M : plusArrayMonad T nat_eqType. +Variable M : plusArrayMonad T nat. Lemma ipartl_guard p i ny nz nx : ipartl (M := M) p i ny nz nx = @@ -168,7 +168,7 @@ End ipartl. Arguments ipartl {d T M}. Section dipartl. -Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat_eqType). +Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat). Definition dipartlT y z x := {n : nat * nat | (n.1 <= x + y + z) && (n.2 <= x + y + z)}. @@ -220,7 +220,7 @@ Arguments dipartl {d T M}. (* top of page 11 *) Section derivation_qperm_partl_ipartl. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* page 11 step 4 *) @@ -274,7 +274,7 @@ Proof. move=> ih; rewrite qperm_partl_cons. apply: refin_trans; last exact: (refin_dispatch_Ret_write3L_ipartl ih). rewrite qperm_preserves_length. -rewrite bindA; apply refin_bindl => -[]. +rewrite bindA; apply: refin_bindl => -[]. rewrite if_bind; apply: refin_if => _; rewrite bindA; apply: refin_bindl => zs'. - by rewrite bindretf size_rcons -cats1 -catA /=; exact: refin_refl. @@ -284,7 +284,7 @@ Qed. End derivation_qperm_partl_ipartl. Section refin_qperm_partl. -Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Let refin_qperm_partl_helper a b p xs : (apply_triple_snd qperm >=> uncurry3 (qperm_partl p)) (a, b, xs) `<=` @@ -319,7 +319,7 @@ End refin_qperm_partl. (* specification of ipartl *) Section refin_ipartl. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* page 12, used in the proof of lemma 10 *) @@ -384,7 +384,7 @@ Qed. End refin_ipartl. Section iqsort_def. -Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat_eqType). +Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat). Local Obligation Tactic := idtac. @@ -492,7 +492,7 @@ End iqsort_def. Arguments iqsort {d T M}. Section iqsort_spec. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat_eqType). +Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* eqn 12 page 13 *) diff --git a/example_monty.v b/example_monty.v index a38821f5..a8e1f8eb 100644 --- a/example_monty.v +++ b/example_monty.v @@ -200,7 +200,7 @@ Qed. Local Open Scope proba_monad_scope. Local Open Scope mprog. -Lemma uniform_unfold {M : probMonad real_realType} (P : rel X) def d : +Lemma uniform_unfold {M : probMonad R} (P : rel X) def d : uniform def (enum X) >>= (fun p => Ret (P d p)) = Ret (P d a) <|(/ 3)%coqR%:pr|> (Ret (P d b) <|(/ 2)%coqR%:pr|> Ret (P d c)) :> M _. Proof. @@ -209,7 +209,7 @@ rewrite [LHS](_ : _ = fmap (fun p => P d p) (uniform def (enum X))); last first. by rewrite -(compE (fmap _)) -(uniform_naturality _ true) enumE. Qed. -Lemma uniform_unfold_pair {M : probMonad real_realType} def (P : rel X) : +Lemma uniform_unfold_pair {M : probMonad R} def (P : rel X) : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (P hp.1 hp.2)) = Ret (P a a) <|(/ 9)%coqR%:pr|> (Ret (P a b) <|(/ 8)%coqR%:pr|> (Ret (P a c) <|(/ 7)%coqR%:pr|> (Ret (P b a) <|(/ 6)%coqR%:pr|> (Ret (P b b) <|(/ 5)%coqR%:pr|> (Ret (P b c) <|(/ 4)%coqR%:pr|> @@ -222,7 +222,7 @@ Qed. (* matching choices: the elements h and p independently chosen at random will match one third of the time *) -Lemma bcoin13E_pair {M : probMonad real_realType} def (f : bool -> M bool) : +Lemma bcoin13E_pair {M : probMonad R} def (f : bool -> M bool) : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => f (hp.1 == hp.2)) = bcoin (/ 3)%coqR%:pr >>= f. Proof. @@ -237,7 +237,7 @@ rewrite (negbTE b_neq_c). by rewrite choiceA_compute /= -uFFTE. Qed. -Lemma bcoin23E_pair {M : probMonad real_realType} def : +Lemma bcoin23E_pair {M : probMonad R} def : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (hp.1 != hp.2)) = bcoin (/ 3)%coqR.~%:pr :> M _. Proof. @@ -281,18 +281,18 @@ Local Open Scope proba_monad_scope. Section monty_proba. Variable def : door. -Definition hide {M : probMonad real_realType} : M door := uniform def doors. +Definition hide {M : probMonad R} : M door := uniform def doors. -Definition pick {M : probMonad real_realType} : M door := uniform def doors. +Definition pick {M : probMonad R} : M door := uniform def doors. -Definition tease {M : probMonad real_realType} (h p : door) : M door := uniform def (doors \\ [:: h ; p]). +Definition tease {M : probMonad R} (h p : door) : M door := uniform def (doors \\ [:: h ; p]). Definition switch {N : monad} (p t : door) : N door := Ret (head def (doors \\ [:: p ; t])). Definition stick {N : monad} (p t : door) : N door := Ret p. -Context {M : probMonad [realType of R]}. +Context {M : probMonad R}. Definition play (strategy : door -> door -> M door) := monty hide pick tease strategy. @@ -380,7 +380,7 @@ Definition hide_n {M : altMonad} : M door := arbitrary def doors. Definition tease_n {M : altMonad} (h p : door) : M door := arbitrary def (doors \\ [:: h; p]). -Variable M : altProbMonad real_realType. +Variable M : altProbMonad R. Definition play_n (strategy : door -> door -> M door) : M bool := monty hide_n (pick def : M _) tease_n strategy. @@ -423,11 +423,8 @@ rewrite /doors Set3.enumE !inE => /or3P[] /eqP ->. rewrite -RmultE -RminusE -R1E; field. rewrite -RmultE -!RminusE -R1E; field. - rewrite eq_sym (negbTE (Set3.a_neq_b _)) eqxx (negbTE (Set3.b_neq_c _)). - congr (_ <| _ |> _). - rewrite choiceC (@choice_ext (/ 2)%coqR%:pr) //= /onem. - congr (Ret false <| _ |> Ret true). - apply/val_inj => /=. - by rewrite -RminusE -R1E; field. + congr (_ <| _ |> _); rewrite choiceC/=; congr (Ret false <| _ |> Ret true). + by apply/val_inj => /=; rewrite /onem -!coqRE; field. by rewrite eq_sym (negbTE (Set3.a_neq_c _)) eq_sym (negbTE (Set3.b_neq_c _)) eqxx. Qed. @@ -518,7 +515,7 @@ End monty_nondeter. Section forgetful_monty. -Variable M : exceptProbMonad real_realType. +Variable M : exceptProbMonad R. Variable def : door. Definition tease_f (h p : door) : M door := diff --git a/example_typed_store.v b/example_typed_store.v index a513c554..ad91c0ae 100644 --- a/example_typed_store.v +++ b/example_typed_store.v @@ -59,8 +59,8 @@ Inductive rlist (a : Type) (a_1 : ml_type) := | Nil | Cons (_ : a) (_ : loc (ml_rlist a_1)). -Definition ml_type_eq_mixin := EqMixin (comparePc MLTypes.ml_type_eq_dec). -Canonical ml_type_eqType := Eval hnf in EqType _ ml_type_eq_mixin. +Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec). +HB.instance Definition ml_type_eqType := ml_type_eq_mixin. End MLTypes. (******************************************************************************) @@ -82,8 +82,7 @@ Fixpoint coq_type_nat (T : ml_type) : Type := end. End with_monad. -HB.instance Definition _ := @isML_universe.Build ml_type - (Equality.class ml_type_eqType) coq_type_nat ml_unit val_nonempty. +HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty. Definition typedStoreMonad (N : monad) := typedStoreMonad ml_type N monad_model.locT_nat. @@ -724,8 +723,7 @@ Fixpoint coq_type63 (T : ml_type) : Type := End with_monad. (******************************************************************************) -HB.instance Definition _ := @isML_universe.Build ml_type - (Equality.class ml_type_eqType) coq_type63 ml_unit val_nonempty. +HB.instance Definition _ := @isML_universe.Build ml_type coq_type63 ml_unit val_nonempty. Section fact_for_int63. Variable N : monad. diff --git a/fail_lib.v b/fail_lib.v index 1d26923f..d06fa79d 100644 --- a/fail_lib.v +++ b/fail_lib.v @@ -90,8 +90,10 @@ Variable T : Type. Definition altCI_semiLattType := M T. +HB.instance Definition _ := boolp.gen_eqMixin altCI_semiLattType. +HB.instance Definition _ := boolp.gen_choiceMixin altCI_semiLattType. + HB.instance Definition _ := @isSemiLattice.Build altCI_semiLattType - (Choice.class (convex.choice_of_Type (M T))) (fun x y => x [~] y) (@altC M T) (@altA M T) (@altmm M T). @@ -1011,33 +1013,65 @@ Local Close Scope mprog. End splits_prePlusMonad. Section qperm. + Variables (M : altMonad) (A : UU0) (d : unit) (T : orderType d). -Equations? qperm (s : seq A) : M (seq A) by wf (size s) lt := +Local Obligation Tactic := idtac. +Program Definition qperm' (s : seq A) + (f : forall s' : seq A, size s' < size s -> M (seq A)) : M (seq A) := +match s with +| [::] => Ret [::] +| x :: xs => + splits_bseq xs >>= + (fun '(ys, zs) => liftM2 (fun a b => a ++ x :: b) ((*qperm ys*) f ys _ : M (seq A)) (f zs _) (*(qperm zs)*)) +end. +Next Obligation. +move=> s f x xs <- ? ys zs ?. +exact: (leq_ltn_trans (size_bseq ys)). +Defined. +Next Obligation. +move=> s f x xs <- ? ys zs ?. +exact: (leq_ltn_trans (size_bseq zs)). +Defined. + +(*Equations? qperm (s : seq A) : M (seq A) by wf (size s) lt := | [::] => Ret [::] | x :: xs => splits_bseq xs >>= (fun '(ys, zs) => liftM2 (fun a b => a ++ x :: b) (qperm ys : M (seq A)) (qperm zs)). Proof. -apply /ltP. +apply/ltP. exact: (leq_ltn_trans (size_bseq ys)). -apply /ltP. +apply/ltP. exact: (leq_ltn_trans (size_bseq zs)). -Defined. +(* +Error: Missing universe constraint declared for inductive type: Type <= Type + Type <= Type +*) +Defined.*) + +Definition qperm : seq A -> M (seq A) := + Fix (@well_founded_size _) (fun _ => M _) qperm'. Lemma qperm_nil : qperm [::] = Ret [::]. -Proof. by []. Qed. -(* by rewrite /qperm (Fix_eq _ _ _ qperm'_Fix). Qed. *) +(*Proof. by []. Qed.*) +Proof. +rewrite /qperm Init.Wf.Fix_eq // => -[//|h t f g H]. +rewrite /qperm'; bind_ext => -[s1 s2]. +by rewrite !H. +Qed. Lemma qperm_cons x xs : qperm (x :: xs) = splits xs >>= (fun '(ys, zs) => liftM2 (fun a b => a ++ x :: b) (qperm ys) (qperm zs)). Proof. -rewrite qperm_equation_2 splits_bseqE fmapE bindA; bind_ext => -[? ?]. +rewrite /qperm Init.Wf.Fix_eq //; last first. + move=> -[//|] h t f g fg. + rewrite /qperm'; bind_ext => -[s1 s2]. + by rewrite !fg. +rewrite {1}/qperm' /=. +rewrite splits_bseqE fmapE bindA; bind_ext => -[? ?]. by rewrite bindretf. -(* rewrite {1}/qperm {1}(Fix_eq _ _ _ qperm'_Fix) /=. -rewrite splitsE /= fmapE bindA; bind_ext => -[? ?]. -by rewrite bindretf. *) Qed. Definition qpermE := (qperm_nil, qperm_cons). @@ -1451,14 +1485,12 @@ Context {M : plusMonad} {A : eqType}. Lemma iperm_qperm : @iperm M A = @qperm M A. Proof. -rewrite boolp.funeqE => s. +(*rewrite boolp.funeqE => s. apply qperm_elim => [//|h t ihys ihzs]. rewrite iperm_cons_splits splits_bseqE fmapE bindA. bind_ext => -[a b]; rewrite bindretf. by rewrite (ihys (a, b) _ b) (ihzs (a, b) a). -Qed. - -(* (* old version *) +Qed.*) rewrite boolp.funeqE => s. have [n ns] := ubnP (size s); elim: n s ns => // n ih s ns. move: s ns => [na |h t]; first by rewrite qperm_nil. @@ -1468,7 +1500,8 @@ bind_ext => -[a b] /=; rewrite !bindA. apply: bind_ext_guard => /and3P[ta tb _]. rewrite !bindretf ih; last first. by rewrite (leq_trans _ ns)// ltnS; apply: size_subseq. -by rewrite ih // (leq_trans _ ns)// ltnS; apply: size_subseq. *) +by rewrite ih // (leq_trans _ ns)// ltnS; apply: size_subseq. +Qed. Lemma perm_eq_qperm (a b : seq A) : perm_eq a b -> qperm a = qperm b :> M _. Proof. by rewrite -!iperm_qperm; exact: perm_eq_iperm. Qed. diff --git a/gcm_model.v b/gcm_model.v index de71d0e0..53ccaf54 100644 --- a/gcm_model.v +++ b/gcm_model.v @@ -91,8 +91,9 @@ Definition hom_choiceType End choiceType_as_a_category. Notation CC := [the category of choiceType]. +Require monad_model. Section free_choiceType_functor. -Local Notation m := choice_of_Type. +Local Notation m := monad_model.choice_of_Type. Definition free_choiceType_mor (T U : CT) (f : {hom T, U}) : {hom m T, m U} := hom_choiceType (f : m T -> m U). @@ -219,7 +220,7 @@ Qed. (* free_convType_mor induces maps between supports *) Definition free_convType_mor_supp (A B : CC) (f : A -> B(*{hom A , B}*)) (d : {dist A}) (x : finsupp d) - : [finType of finsupp ((free_convType_mor (hom_choiceType f)) d)] := + : finsupp ((free_convType_mor (hom_choiceType f)) d) := FSetSub (mem_finsupp_free_convType_mor f x). Global Arguments free_convType_mor_supp [A B] f d. @@ -383,6 +384,7 @@ Proof. by split; move=> ?; case: f=> ? [] [] []. Qed. Fact scsl_hom_is_affine : affine f. Proof. by case: scsl_hom_is_biglub_affine. Qed. +(* NB(rei): this can actually maybe be removed *) HB.instance Definition SCSL_hom_affine := isAffine.Build _ _ _ scsl_hom_is_affine. (* Canonical SCSL_hom_affine (K L : CS) (f : {hom K , L}) := @@ -410,12 +412,14 @@ Let acto (a : CV) : CS := {necset a}. Section free_semiCompSemiLattConvType_mor. Variables (A B : convType) (f : {hom A , B}). -Definition free_semiCompSemiLattConvType_mor' (X : acto A) : acto B := - NECSet.Pack (NECSet.Class - (CSet.Mixin (is_convex_set_image - (Affine.Pack (Affine.Class (isAffine.Axioms_ _ _ (conv_hom_is_affine f)))) - X)) - (NESet.Mixin (neset_image_neq0 _ _))). +Local Notation affine_f := + (Affine.Pack (Affine.Class (isAffine.Build _ _ _ (conv_hom_is_affine f)))). + +Local Notation pack_imfx X := (NECSet.Pack (NECSet.Class + (isConvexSet.Build _ _ (is_convex_set_image affine_f X)) + (isNESet.Build _ _ (neset_image_neq0 _ _)))). + +Definition free_semiCompSemiLattConvType_mor' (X : acto A) : acto B := pack_imfx X. (* the results of free_semiCompSemiLattConvType_mor are semiLattConvType-morphisms, i.e., are @@ -424,11 +428,9 @@ Lemma free_semiCompSemiLattConvType_mor'_affine : affine free_semiCompSemiLattConvType_mor'. Proof. move=> p a0 a1; apply necset_ext => /=; rewrite predeqE => b0; split. -- rewrite !necset_convType.convE. - case=> a [] a0' a0a0'; rewrite conv_pt_setE=> -[] a1' a1a1' <- <- /=. +- case=> a [] a0' a0a0'; rewrite conv_pt_setE=> -[] a1' a1a1' <- <- /=. by rewrite affine_conv /=; exact: conv_in_conv_set. -- rewrite !necset_convType.convE. - move=> /conv_in_conv_set' [] x [] y [] [] a0' a0a0' <- [] [] a1' a1a1' <- ->. +- move=> /conv_in_conv_set' [] x [] y [] [] a0' a0a0' <- [] [] a1' a1a1' <- ->. rewrite affine_image_conv_set /=. by apply conv_in_conv_set; apply imageP. Qed. @@ -438,11 +440,7 @@ Lemma bigsetU_affine (X : neset (necset A)) : (f @` (\bigcup_(x in X) x) = Proof. rewrite funeqE => b; rewrite propeqE; split. - case => a [x Xx xa] <-{b}. - exists (NECSet.Pack (NECSet.Class - (CSet.Mixin (is_convex_set_image - (Affine.Pack (Affine.Class (isAffine.Axioms_ _ _ (conv_hom_is_affine f)))) - x)) - (NESet.Mixin (neset_image_neq0 f x)))) => /=; last by exists a. + exists (pack_imfx x) => /=; last by exists a. by exists x => //=; exact/necset_ext. - by case => b0 [a0 Xa0 <-{b0}] [a a0a <-{b}]; exists a => //; exists a0. Qed. @@ -462,14 +460,13 @@ Definition free_semiCompSemiLattConvType_mor : {hom acto A, acto B} := free_semiCompSemiLattConvType_mor'_affine)))). Lemma free_semiCompSemiLattConvType_morE (X : acto A) : - NECSet.mixinType (free_semiCompSemiLattConvType_mor X) = image_neset f X. + free_semiCompSemiLattConvType_mor X = f @` X :> neset _. Proof. by rewrite /free_semiCompSemiLattConvType_mor; unlock; apply neset_ext. Qed. Lemma free_semiCompSemiLattConvType_morE' (X : acto A) : - NESet.car (NECSet.mixinType (free_semiCompSemiLattConvType_mor X)) = - image_neset f X. + free_semiCompSemiLattConvType_mor X = f @` X :> set _. Proof. by rewrite /free_semiCompSemiLattConvType_mor; unlock. Qed. End free_semiCompSemiLattConvType_mor. @@ -549,8 +546,7 @@ Qed. Lemma eps1''_affine L : affine (@eps1'' L). Proof. move=> p X Y; rewrite -biglub_conv_setD. -congr (|_| _%:ne); apply/neset_ext => /=. -by rewrite necset_convType.convE. +by congr (|_| _%:ne); apply/neset_ext => /=. Qed. Let eps1' : F1 \O U1 ~~> FId := fun L => Hom.Pack (Hom.Class (isHom.Axioms_ @@ -572,17 +568,16 @@ Lemma eps1E (L : semiCompSemiLattConvType) : eps1 L = (fun X => |_| X) :> (_ -> _). Proof. by rewrite /eps1; unlock. Qed. -Lemma necset1_affine (C : convType) : affine (@necset1 C). +Lemma necset1_affine (C : convType) : affine (set1 : C -> necset C). Proof. move=> p a b /=; apply/necset_ext; rewrite eqEsubset; split=> x /=. - move->; rewrite necset_convType.convE. by apply conv_in_conv_set. -- rewrite necset_convType.convE /necset1 /=. - by case/conv_in_conv_set'=> a0 [] b0 [] -> [] -> ->. +- by case/conv_in_conv_set'=> a0 [] b0 [] -> [] -> ->. Qed. Let eta1' : FId ~~> U1 \O F1 := fun C => Hom.Pack (Hom.Class - (isHom.Axioms_ (FId C) ((U1 \O F1) C) (@necset1 C) (@necset1_affine C))). + (isHom.Axioms_ (FId C) ((U1 \O F1) C) set1 (@necset1_affine C))). Lemma eta1'_natural : naturality _ _ eta1'. Proof. @@ -594,22 +589,19 @@ HB.instance Definition _ := isNatural.Build _ _ _ _ _ eta1'_natural. Definition eta1 := locked [the _ ~> _ of eta1']. -Lemma eta1E (C : convType) : eta1 C = @necset1 _ :> (_ -> _). +Lemma eta1E (C : convType) : eta1 C = (set1 : C -> necset C) :> (_ -> _). Proof. by rewrite /eta1; unlock. Qed. Import comps_notation. -Lemma necset1E (T : convType) (t : T) : necset1 t = [set t] :> set T. -Proof. by []. Qed. - Lemma triL1 : TriangularLaws.left eta1 eps1. Proof. move=> c; apply funext => x /=; apply/necset_ext => /=. rewrite eps1E /= free_semiCompSemiLattConvType_morE' /=. rewrite -[in RHS](hull_cset x); congr hull. rewrite eqEsubset eta1E; split=> a. -- by case=> y [] b xb <-; rewrite necset1E => ->. -- by move=> xa; exists (necset1 a); [exists a | rewrite necset1E]. +- by case=> y [] b xb <- ->. +- by move=> xa; exists [set a]; [exists a | ]. Qed. Lemma triR1 : TriangularLaws.right eta1 eps1. @@ -623,9 +615,9 @@ Local Open Scope convex_scope. Local Open Scope classical_set_scope. Variable C : convType. -Definition join1' (s : necset {necset C}) : {convex_set C} := - CSet.Pack (CSet.Mixin - (hull_is_convex (\bigcup_(x in s) if x \in s then x : set _ else cset0 _))). +Definition join1' (s : necset (necset C)) : {convex_set C} := + ConvexSet.Pack (ConvexSet.Class (isConvexSet.Build C _ + (hull_is_convex (\bigcup_(x in s) if x \in s then x : set _ else set0)))). Lemma join1'_neq0 (s : necset {necset C}) : join1' s != set0 :> set _. Proof. @@ -636,8 +628,8 @@ by exists x; exists y => //; move: sy; rewrite -in_setE => ->. Qed. Definition join1 (s : necset {necset C}) : necset C := - NECSet.Pack (NECSet.Class (CSet.Mixin (hull_is_convex _)) - (NESet.Mixin (join1'_neq0 s))). + NECSet.Pack (NECSet.Class (isConvexSet.Build _ _ (hull_is_convex _)) + (isNESet.Build _ _ (join1'_neq0 s))). Lemma eps1_correct (s : necset {necset C}) : @eps1 _ s = join1 s. Proof. @@ -677,6 +669,8 @@ End P_delta_functor. Require monad_lib. Require Import hierarchy. +Local Notation choice_of_Type := monad_model.choice_of_Type. + Section P_delta_category_monad. Import category. Definition AC := AdjointFunctors.mk triLC triRC. @@ -692,7 +686,7 @@ Section gcm_opsE. Import hierarchy. Lemma gcm_retE (T : Type) (x : choice_of_Type T) : - Ret x = necset1 (fsdist1 x) :> gcm T. + Ret x = [set (fsdist1 x)] :> gcm T. Proof. rewrite /= /ret_ /Monad_of_category_monad.ret /=. rewrite !HCompId !HIdComp /=. diff --git a/hierarchy.v b/hierarchy.v index 7f53ea55..36e4a4f5 100644 --- a/hierarchy.v +++ b/hierarchy.v @@ -832,8 +832,8 @@ HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}. Section nondet_big. Variables (M : nondetMonad) (A : UU0). -Canonical alt_monoid := - Monoid.Law (@altA M A) (@altfailm _ _) (@altmfail _ _). +HB.instance Definition _ := + Monoid.isLaw.Build _ _ _ (@altA M A) (@altfailm _ _) (@altmfail _ _). Lemma test_bigop n : \big[(@alt _ _)/fail]_(i < n) (fail : M A) = fail. Proof. @@ -1085,16 +1085,13 @@ Variant loc (ml_type : Type) (locT : eqType) : ml_type -> Type := Definition loc_id (ml_type : Type) (locT : eqType) {T : ml_type} (l : loc locT T) : locT := let: mkloc _ n := l in n. -HB.mixin Structure isML_universe (ml_type : Type) := { - eqclass : Equality.class_of ml_type ; +HB.mixin Structure isML_universe (ml_type : Type) of Equality ml_type := { coq_type : forall M : Type -> Type, ml_type -> Type ; ml_nonempty : ml_type ; val_nonempty : forall M, coq_type M ml_nonempty }. #[short(type=ML_universe)] -HB.structure Definition ML_UNIVERSE := {ml_type & isML_universe ml_type}. - -Canonical isML_universe_eqType (T : ML_universe) := EqType T eqclass. +HB.structure Definition ML_UNIVERSE := {ml_type of isML_universe ml_type &}. HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType) (M : UU0 -> UU0) of Monad M := { diff --git a/impredicative_set/ifmt_lifting.v b/impredicative_set/ifmt_lifting.v index 055b63dc..fb688e9d 100644 --- a/impredicative_set/ifmt_lifting.v +++ b/impredicative_set/ifmt_lifting.v @@ -38,7 +38,7 @@ Definition MK (m : UU0 -> UU0) (A : UU0) := forall (B : UU0), (A -> m B) -> m B. Section codensity. Variable (M : monad). -Definition retK : FId ~~> MK M := +Definition retK : idfun ~~> MK M := fun (A : UU0) (a : A) (B : UU0) (k : A -> M B) => k a. Definition bindK (A B : UU0) (m : MK M A) f : MK M B := diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v index c8130281..6d4b02e3 100644 --- a/impredicative_set/ihierarchy.v +++ b/impredicative_set/ihierarchy.v @@ -19,7 +19,6 @@ From HB Require Import structures. (* Module FunctorLaws == map laws of a functor *) (* functor == type of functors *) (* F # g == application of the functor F to the morphism g *) -(* FId == notation for the identity functor *) (* F ~> G == natural transformation from functor F to functor G *) (* f ~~> g == forall A, f A -> g A, notation used for the *) (* components of a natural transformation *) @@ -30,7 +29,7 @@ From HB Require Import structures. (* >>= == notation for the standard bind operator *) (* m >> f := m >>= (fun _ => f) *) (* monad == type of monads *) -(* Ret == natural transformation FId ~> M for a monad M *) +(* Ret == natural transformation idfun ~> M for a monad M *) (* Join == natural transformation M \o M ~> M for a monad M *) (* Module BindLaws == bind laws of a monad *) (* *) @@ -97,14 +96,14 @@ Reserved Notation "m >> f" (at level 49). Reserved Notation "'fmap' f" (at level 4). Reserved Notation "x '[~]' y" (at level 50). -Notation "f ~~> g" := (forall A, f A -> g A) - (at level 51, only parsing) : monae_scope. - Local Open Scope monae_scope. Notation UU1 := Type. Notation UU0 := Set. +Notation "f ~~> g" := (forall A : UU0, f A -> g A) + (at level 51, only parsing) : monae_scope. + (* NB: not putting M in Set -> Set because of expressions like: M (A * (size s).-1.-tuple A)%type *) Module FunctorLaws. @@ -134,10 +133,7 @@ Let id_comp : FunctorLaws.comp id_actm. Proof. by []. Qed. HB.instance Definition _ := isFunctor.Build idfun id_id id_comp. End functorid. -(* NB: consider eliminating? *) -Notation FId := [the functor of idfun]. - -Lemma FIdE (A B : UU0) (f : A -> B) : FId # f = f. Proof. by []. Qed. +Lemma FIdE (A B : UU0) (f : A -> B) : idfun # f = f. Proof. by []. Qed. Section functor_composition. Variables f g : functor. @@ -270,20 +266,22 @@ Qed.*) Module JoinLaws. Section join_laws. Context {F : functor}. -Variables (ret : FId ~> F) (join : F \o F ~~> F). +Variables (ret : idfun ~~> F) (join : F \o F ~~> F). +Arguments ret {_}. +Arguments join {A}. -Definition left_unit := forall A, @join A \o ret (F A) = id :> (F A -> F A). +Definition left_unit := forall A, join \o ret = id :> (F A -> F A). -Definition right_unit := forall A, @join A \o F # ret A = id :> (F A -> F A). +Definition right_unit := forall A, join \o F # ret = id :> (F A -> F A). -Definition associativity := - forall A, @join A \o F # @join A = @join A \o @join (F A) :> (F (F (F A)) -> F A). +Definition associativity := forall A, + join \o F # join = join \o join :> (F (F (F A)) -> F A). End join_laws. End JoinLaws. HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := { - ret : FId ~> F ; + ret : idfun ~> F ; join : F \o F ~> F ; bind : forall (A B : UU0), F A -> (A -> F B) -> F B ; bindE : forall (A B : UU0) (f : A -> F B) (m : F A), @@ -364,7 +362,7 @@ Definition bind_of_join (F : functor) (j : F \o F ~~> F) j B ((F # f) m). Section from_join_laws_to_bind_laws. -Variable (F : functor) (ret : FId ~> F) (join : F \o F ~> F). +Variable (F : functor) (ret : idfun ~> F) (join : F \o F ~> F). Hypothesis joinretM : JoinLaws.left_unit ret join. Hypothesis joinMret : JoinLaws.right_unit ret join. @@ -391,7 +389,7 @@ Qed. End from_join_laws_to_bind_laws. HB.factory Record isMonad_ret_join (F : UU0 -> UU0) of isFunctor F := { - ret : FId ~> F ; + ret : idfun ~> F ; join : F \o F ~> F ; joinretM : JoinLaws.left_unit ret join ; joinMret : JoinLaws.right_unit ret join ; @@ -412,15 +410,15 @@ HB.instance Definition _ := isMonad.Build M bindE joinretM joinMret joinA. HB.end. HB.factory Record isMonad_ret_bind (F : UU0 -> UU0) := { - ret' : forall (A : UU0), A -> F A ; + ret : forall (A : UU0), A -> F A ; bind : forall (A B : UU0), F A -> (A -> F B) -> F B ; - bindretf : BindLaws.left_neutral bind ret' ; - bindmret : BindLaws.right_neutral bind ret' ; + bindretf : BindLaws.left_neutral bind ret ; + bindmret : BindLaws.right_neutral bind ret ; bindA : BindLaws.associative bind }. HB.builders Context M of isMonad_ret_bind M. -Let actm (a b : UU0) (f : a -> b) m := bind m (@ret' _ \o f). +Let actm (a b : UU0) (f : a -> b) m := bind m (@ret _ \o f). Let actm_id : FunctorLaws.id actm. Proof. @@ -443,7 +441,7 @@ HB.instance Definition _ := isFunctor.Build M actm_id actm_comp. Let F := [the functor of M]. Local Notation FF := [the functor of F \o F]. -Let ret'_naturality : naturality FId F ret'. +Let ret_naturality : naturality idfun F ret. Proof. move=> a b h. rewrite FIdE /ihierarchy.actm /= /actm; apply: funext => m /=. @@ -451,8 +449,7 @@ by rewrite bindretf. Qed. HB.instance Definition _ := - isNatural.Build FId F (ret' : FId ~~> F) ret'_naturality. -Let ret := [the FId ~> F of ret']. + isNatural.Build idfun F (ret : idfun ~~> F) ret_naturality. Let join' : FF ~~> F := fun _ m => bind m idfun. @@ -500,7 +497,7 @@ move=> a; apply: funext => m. rewrite /join /= /join'. rewrite /ihierarchy.actm /= /actm /=. rewrite bindA /=. -rewrite [X in bind m X](_ : _ = fun x => ret' x) ?bindmret //=; apply: funext => ?. +rewrite [X in bind m X](_ : _ = fun x => ret x) ?bindmret //=; apply: funext => ?. by rewrite bindretf. Qed. @@ -690,9 +687,9 @@ Notation "m <=< n" := (kleisli m n) : monae_scope. Notation "m >=> n" := (kleisli n m) : monae_scope. HB.mixin Record isMonadFail (M : UU0 -> UU0) of Monad M := { - fail : forall A : UU0, M A; + fail : forall A : UU0, M A ; (* exceptions are left-zeros of sequential composition *) - bindfailf : BindLaws.left_zero (@bind [the monad of M]) fail + bindfailf : BindLaws.left_zero (@bind M) fail (* fail A >>= f = fail B *) }. #[short(type=failMonad)] @@ -815,8 +812,8 @@ HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}. Section nondet_big. Variables (M : nondetMonad) (A : UU0). -Canonical alt_monoid := - Monoid.Law (@altA M A) (@altfailm _ _) (@altmfail _ _). +HB.instance Definition _ := + Monoid.isLaw.Build _ _ _ (@altA M A) (@altfailm _ _) (@altmfail _ _). Lemma test_bigop n : \big[(@alt _ _)/fail]_(i < n) (fail : M A) = fail. Proof. diff --git a/impredicative_set/imonad_composition.v b/impredicative_set/imonad_composition.v index aff8a5a3..6ef83d65 100644 --- a/impredicative_set/imonad_composition.v +++ b/impredicative_set/imonad_composition.v @@ -20,13 +20,13 @@ Local Open Scope monae_scope. Section comp. Variables (M N : monad). -Definition ret_comp : FId ~~> M \o N := (@ret M) \h (@ret N). -Lemma naturality_ret : naturality FId [the functor of M \o N] ret_comp. +Definition ret_comp : idfun ~~> M \o N := (@ret M) \h (@ret N). +Lemma naturality_ret : naturality idfun [the functor of M \o N] ret_comp. Proof. by move=> A B h; rewrite -(natural ((@ret M) \h (@ret N))). Qed. HB.instance Definition _ := isNatural.Build - FId [the functor of (M \o N)] ret_comp naturality_ret. + idfun [the functor of (M \o N)] ret_comp naturality_ret. End comp. -Definition CRet (M N : monad) := [the FId ~> [the functor of M \o N] of ret_comp M N]. +Definition CRet (M N : monad) := [the idfun ~> [the functor of M \o N] of ret_comp M N]. Module Prod. Section prod. diff --git a/impredicative_set/imonad_lib.v b/impredicative_set/imonad_lib.v index e03a8b00..1899d6d9 100644 --- a/impredicative_set/imonad_lib.v +++ b/impredicative_set/imonad_lib.v @@ -35,6 +35,8 @@ Require Import ihierarchy. (* (fun v => (Ret (u, v))) *) (* commute m n f := (m >>= n >>= f) = (n >>= m >>= f) *) (* (ref: definition 4.2, mu2019tr3) *) +(* preserves f g := the monadic function f : A -> M A preserves *) +(* the value of the function g : A -> B *) (* rep n mx == mx >> mx >> ... >> mx, n times *) (* forloop n1 n2 (b : nat -> M unit) : M unit := for-loop *) (* *) @@ -219,7 +221,7 @@ Proof. by rewrite functor_o. Qed. Section id_natural_transformation. Variables C : functor. -Definition NId := fun A => @id (C A). +Definition NId := fun A => @idfun (C A). Let natural_id : naturality C C NId. Proof. by []. Qed. HB.instance Definition _ := isNatural.Build C C NId natural_id. @@ -310,18 +312,18 @@ Lemma functor_app_natural_hcomp (S F G : functor) (nt : F ~> G) : Proof. by apply nattrans_ext => a; rewrite functor_app_naturalE. Qed. Section natural_transformation_example. -Definition fork' : FId ~~> squaring := fun (A : UU0) (a : A) => (a, a). +Definition fork' : idfun ~~> squaring := fun (A : UU0) (a : A) => (a, a). Lemma fork_natural : naturality _ _ fork'. Proof. by []. Qed. -HB.instance Definition _ := isNatural.Build FId squaring fork' fork_natural. +HB.instance Definition _ := isNatural.Build idfun squaring fork' fork_natural. -Definition fork : FId ~> squaring := [the _ ~> _ of fork']. +Definition fork : idfun ~> squaring := [the _ ~> _ of fork']. End natural_transformation_example. -Definition eta_type (f g : functor) := FId ~> g \o f. -Definition eps_type (f g : functor) := f \o g ~> FId. +Definition eta_type (f g : functor) := idfun ~> g \o f. +Definition eps_type (f g : functor) := f \o g ~> idfun. Module TriangularLaws. Section triangularlaws. Variables (F G : functor) (eps : eps_type F G) (eta : eta_type F G). @@ -353,14 +355,14 @@ Section adjoint_example. Variable (X : UU0). Definition curry_fun : curry_F X \o uncurry_F X ~~> idfun := fun (A : UU0) (af : X * (X -> A)) => af.2 af.1. -Lemma curry_naturality : naturality (curry_F X \o uncurry_F X) FId curry_fun. +Lemma curry_naturality : naturality (curry_F X \o uncurry_F X) idfun curry_fun. Proof. by []. Qed. HB.instance Definition _ := isNatural.Build - (curry_F X \o uncurry_F X) FId curry_fun curry_naturality. + (curry_F X \o uncurry_F X) idfun curry_fun curry_naturality. Definition curry_eps : eps_type (curry_F X) (uncurry_F X) := - [the nattrans (curry_F X \o uncurry_F X) FId of curry_fun]. + [the nattrans (curry_F X \o uncurry_F X) idfun of curry_fun]. -Definition curry_fun2 : FId ~~> uncurry_F X \o curry_F X := +Definition curry_fun2 : idfun ~~> uncurry_F X \o curry_F X := fun (A : UU0) (a : A) => pair^~ a. Lemma curry_naturality2 : naturality _ [the functor of uncurry_F X \o curry_F X] curry_fun2. @@ -461,7 +463,7 @@ Hypothesis H : F -| U. Let eta : eta_type F U := AdjointFunctor.eta H. Let eps : eps_type F U := AdjointFunctor.eps H. -Definition uni_fun : FId ~~> (U0 \o U) \o (F \o F0) := +Definition uni_fun : idfun ~~> (U0 \o U) \o (F \o F0) := fun A : UU0 => U0 # eta (F0 A) \o eta0 A. Lemma uni_naturality : @@ -577,11 +579,11 @@ Qed. End algebraic_operation_interface. -(*Lemma monad_of_ret_bind_ext (F G : functor) (RET1 : FId ~> F) (RET2 : FId ~> G) +(*Lemma monad_of_ret_bind_ext (F G : functor) (RET1 : idfun ~> F) (RET2 : idfun ~> G) (bind1 : forall A B : UU0, F A -> (A -> F B) -> F B) (bind2 : forall A B : UU0, G A -> (A -> G B) -> G B) : forall (FG : F = G), - RET1 = eq_rect _ (fun m : functor => FId ~> m) RET2 _ ((*beuh*) (esym FG)) -> + RET1 = eq_rect _ (fun m : functor => idfun ~> m) RET2 _ ((*beuh*) (esym FG)) -> bind1 = eq_rect _ (fun m : functor => forall A B : UU0, m A -> (A -> m B) -> m B) bind2 _ (esym FG) -> forall H1 K1 H2 K2 H3 K3, Monad_of_ret_bind F RET1 bind1 H1 H2 H3 = diff --git a/impredicative_set/imonad_transformer.v b/impredicative_set/imonad_transformer.v index 7d1eba19..23b189f0 100644 --- a/impredicative_set/imonad_transformer.v +++ b/impredicative_set/imonad_transformer.v @@ -91,7 +91,7 @@ Variables (S : UU0) (M : monad). Definition MS := fun A : UU0 => S -> M (A * S)%type. -Definition retS : FId ~~> MS := fun A : UU0 => curry Ret. +Definition retS : idfun ~~> MS := fun A : UU0 => curry Ret. Definition bindS (A B : UU0) (m : MS A) f : MS B := fun s => m s >>= uncurry f. @@ -211,7 +211,7 @@ Variables (Z : UU0) (* the type of exceptions *) (M : monad). Definition MX := fun X : UU0 => M (Z + X)%type. (* unit and bind operator of the transformed monad *) -Definition retX : FId ~~> MX := fun X x => Ret (inr x). +Definition retX : idfun ~~> MX := fun X x => Ret (inr x). Definition bindX X Y (t : MX X) (f : X -> MX Y) : MX Y := t >>= fun c => match c with inl z => Ret (inl z) | inr x => f x end. @@ -331,7 +331,7 @@ Variables (R : UU0) (M : monad). Definition MEnv := fun A : UU0 => R -> M A. -Definition retEnv : FId ~~> MEnv := fun (A : UU0) a r => Ret a. +Definition retEnv : idfun ~~> MEnv := fun (A : UU0) a r => Ret a. Definition bindEnv A B (m : MEnv A) f : MEnv B := fun r => m r >>= (fun a => f a r). @@ -383,7 +383,7 @@ Variables (R : UU0) (M : monad). Definition MO (X : UU0) := M (X * seq R)%type. -Definition retO : FId ~~> MO := fun (A : UU0) a => Ret (a, [::]). +Definition retO : idfun ~~> MO := fun (A : UU0) a => Ret (a, [::]). Definition bindO A B (m : MO A) (f : A -> MO B) : MO B := m >>= (fun o => let: (x, w) := o in f x >>= @@ -457,7 +457,7 @@ Variables (r : UU0) (M : monad). Definition MC : UU0 -> UU0 := fun A => (A -> M r) -> M r %type. -Definition retC : FId ~~> MC := fun (A : UU0) (a : A) k => k a. +Definition retC : idfun ~~> MC := fun (A : UU0) (a : A) k => k a. Definition bindC A B (m : MC A) f : MC B := fun k => m (f^~ k). diff --git a/meta.yml b/meta.yml index ecf22f3b..12558b10 100644 --- a/meta.yml +++ b/meta.yml @@ -35,53 +35,51 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.16-8.17 - opam: '{ (>= "8.16" & < "8.19~") | (= "dev") }' + 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.2.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.17' +- version: '2.2.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.17.0-coq-8.18' - repo: 'mathcomp/mathcomp' -- version: '1.18.0-coq-8.18' +- version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.17.0" & < "1.19~") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.16.0" & < "1.19~") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.16.0" & < "1.19~") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.16.0" & < "1.19~") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.16.0" & < "1.19~") | (= "dev") }' + version: '{ (>= "2.2.0") | (= "dev") }' description: |- [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "0.6.6") & (< "0.7~")}' + version: '{ (>= "1.1.0")}' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: name: coq-infotheo - version: '{ >= "0.6.0" & < "0.7~"}' + version: '{ >= "0.7.1"}' description: |- [Infotheo](https://github.com/affeldt-aist/infotheo) - opam: @@ -91,7 +89,7 @@ dependencies: [Paramcoq](https://github.com/coq-community/paramcoq) - opam: name: coq-hierarchy-builder - version: '{ = "1.5.0" }' + version: '{ >= "1.5.0" }' description: |- [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - opam: diff --git a/monad_model.v b/monad_model.v index 072a0eed..da594d61 100644 --- a/monad_model.v +++ b/monad_model.v @@ -342,7 +342,7 @@ Proof. by move=> A B C f g; apply boolp.funext => -[]. Qed. HB.instance Definition _ := isFunctor.Build acto func_id func_comp. End empty. End Empty. -HB.export Empty. +HB.export monae.monad_model.Empty. Module Append. Section append. @@ -1212,7 +1212,11 @@ HB.instance Definition _ := isMonadStateTraceReify.Build S T (StateMonad.acto (S End modelstatetracereify. End ModelStateTraceReify. -Notation choice_of_Type := convex.choice_of_Type. + +(* choice_of_Type is removed from infotheo.convex *) +(* Notation choice_of_Type := convex.choice_of_Type. *) +Definition choice_of_Type (T : Type) : choiceType := + Choice.Pack (Choice.Class (boolp.gen_choiceMixin T) (boolp.gen_eqMixin T)). Module ModelBacktrackableState. Local Open Scope fset_scope. @@ -1230,8 +1234,8 @@ Let ret : idfun ~~> M := fun A (a : A) s => Let bind := fun A B (m : acto A) (f : A -> S -> {fset (choice_of_Type B * choice_of_Type S)}) => - fun s => \bigcup_(i <- (fun x : [choiceType of choice_of_Type A * - choice_of_Type S] => f x.1 x.2) @` (m s)) + fun s => \bigcup_(i <- (fun x : choice_of_Type A * choice_of_Type S => f x.1 x.2) + @` (m s)) i. Let left_neutral : BindLaws.left_neutral bind ret. Proof. @@ -1243,7 +1247,7 @@ Let right_neutral : BindLaws.right_neutral bind ret. Proof. move=> A B /=; rewrite boolp.funeqE => s. apply/fsetP => /= x; apply/bigfcupP'; case: ifPn => xBs. - set x' := (x : [choiceType of choice_of_Type A * choice_of_Type S]). + set x' := (x : choice_of_Type A * choice_of_Type S). exists [fset x']; last by rewrite inE. by apply/imfsetP; exists x' => //=; case: x'. case => /= SA /imfsetP[] /= sa saBs ->{SA} /fset1P => Hx. @@ -1272,8 +1276,7 @@ HB.instance Definition _ := Lemma bindE (A B : Type) m (f : A -> [the monad of acto] B) : m >>= f = fun s => - \bigcup_(i <- (fun x : [choiceType of choice_of_Type A * - choice_of_Type S] => f x.1 x.2) + \bigcup_(i <- (fun x : choice_of_Type A * choice_of_Type S => f x.1 x.2) @` (m s)) i. Proof. @@ -1314,8 +1317,7 @@ move=> s s'; apply boolp.funext => s''. rewrite bindE; apply/fsetP => /= x; apply/bigfcupP'/fset1P. - by case => /= x0 /imfsetP[/= x1] /fset1P _ -> /fset1P. - move=> -> /=. - exists [fset ((tt, s') : [choiceType of choice_of_Type unit * - choice_of_Type S])] => /=; last first. + exists [fset ((tt, s') : choice_of_Type unit * choice_of_Type S)] => /=; last first. exact/fset1P. apply/imfsetP => /=; exists (tt, s) => //; exact/fset1P. Qed. @@ -1324,13 +1326,11 @@ Proof. move=> s; rewrite boolp.funeqE => s'. rewrite 2!bindE /=; apply/fsetP => /= x; apply/bigfcupP'/bigfcupP'. - case => /= x0 /imfsetP[/= x1] /fset1P -> -> /fset1P ->. - exists [fset ((s, s) : [choiceType of choice_of_Type S * - choice_of_Type S])]; last first. + exists [fset ((s, s) : choice_of_Type S * choice_of_Type S)]; last first. exact/fset1P. apply/imfsetP => /=; exists (tt, s) => //; exact/fset1P. - case => /= x0 /imfsetP[/= x1] /fset1P -> -> /fset1P ->. - exists [fset ((s ,s) : [choiceType of choice_of_Type S * - choice_of_Type S])]; last first. + exists [fset ((s ,s) : choice_of_Type S * choice_of_Type S)]; last first. exact/fset1P. apply/imfsetP => /=; exists (tt, s) => //; exact/fset1P. Qed. @@ -1340,8 +1340,7 @@ rewrite boolp.funeqE => s. rewrite bindE /skip /= /Ret; apply/fsetP => /= x; apply/bigfcupP'/idP. - case => /= x0 /imfsetP[/= x1] /fset1P -> -> /fset1P ->; exact/fset1P. - move/fset1P => ->. - exists [fset ((tt, s) : [choiceType of choice_of_Type unit * - choice_of_Type S])]; last first. + exists [fset ((tt, s) : choice_of_Type unit * choice_of_Type S)]; last first. exact/fset1P. by apply/imfsetP; exists (s, s) => //; rewrite inE. Qed. @@ -1358,8 +1357,7 @@ rewrite 2!bindE; apply/fsetP => x; apply/bigfcupP'/bigfcupP'. (choice_of_Type S -> {fset choice_of_Type A * choice_of_Type S}). move=> a b s'; exact: (k a b s'). exists (\bigcup_(i <- [fset k' (s, s).1 x2.1 x2.2 | - x2 in [fset (((s, s).2, (s, s).2) : [choiceType of choice_of_Type S * - choice_of_Type S])]]) i). + x2 in [fset (((s, s).2, (s, s).2) : choice_of_Type S * choice_of_Type S)]]) i). apply/imfsetP ; exists (s, s); by [rewrite inE | rewrite bindE]. apply/bigfcupP'; exists (k s s s) => //; apply/imfsetP; exists (s, s) => //=. exact/fset1P. @@ -1377,7 +1375,7 @@ Let bindfailf : BindLaws.left_zero (@bind _ ) fail. Proof. move=> A B g; rewrite boolp.funeqE => s; apply/fsetP => x; rewrite inE bindE. apply/negbTE/bigfcupP'; case => /= x0 /imfsetP[/= sa]. -by rewrite (@in_fset0 [choiceType of choice_of_Type A * choice_of_Type S]). +by rewrite (@in_fset0 (choice_of_Type A * choice_of_Type S)%type). Qed. HB.instance Definition _ := isMonadFail.Build (acto S) bindfailf. @@ -1386,8 +1384,7 @@ End fail. Section alt. Variable S : choiceType. Let M := [the monad of acto S]. -Let alt := (fun (A : Type) (a b : S -> {fset [choiceType of choice_of_Type A * - choice_of_Type S]}) (s : S) => a s `|` b s). +Let alt := (fun (A : Type) (a b : S -> {fset choice_of_Type A * choice_of_Type S}) (s : S) => a s `|` b s). Let altA : forall T : UU0, ssrfun.associative (@alt T). Proof. by move=> A a b c; rewrite boolp.funeqE => s; rewrite /alt fsetUA. Qed. Let alt_bindDl : BindLaws.left_distributive (@bind M) (@alt). @@ -1425,7 +1422,7 @@ Proof. move=> A B /= g; rewrite bindE /=; rewrite boolp.funeqE => s; apply/fsetP => /= sa. apply/idP/idP/bigfcupP'. case => /= SA /imfsetP[/= bs bsgs ->{SA}]. -by rewrite (@in_fset0 [choiceType of choice_of_Type A * choice_of_Type S]). +by rewrite (@in_fset0 (choice_of_Type A * choice_of_Type S)%type). Qed. HB.instance Definition _ := isMonadFailR0.Build (acto S) bindmfail. End failR0monad. @@ -1646,7 +1643,7 @@ End modelplusarray. End ModelPlusArray. HB.export ModelPlusArray. -Definition locT_nat := [eqType of nat]. +Definition locT_nat : eqType := nat. Module ModelTypedStore. diff --git a/monae_lib.v b/monae_lib.v index ece1557b..9562f5d9 100644 --- a/monae_lib.v +++ b/monae_lib.v @@ -217,7 +217,7 @@ Definition comparePc T (eq_dec : comparable T) : Equality.axiom eq_dec := | right b => ReflectF (x = y) b end. Definition eqPc (E : eqType) : Equality.axiom (@eq_op E) := - match E with EqType sort (EqMixin op a) => a end. + match E with Equality.Pack sort (Equality.Class (hasDecEq.Axioms_ op a)) => a end. End computable_eqtype. Section coerce. diff --git a/proba_lib.v b/proba_lib.v index 68cf282e..e7cde7d9 100644 --- a/proba_lib.v +++ b/proba_lib.v @@ -39,19 +39,23 @@ From infotheo Require Import fdist. From mathcomp Require Import reals Rstruct. Section convex. -Variable M : probMonad real_realType. +Variable M : probMonad R. Variable A : Type. Local Open Scope proba_scope. -Definition choiceA_real_realType (p q : {prob real_realType}) (a b c : M A) : - let conv := (fun p (a b : choice_of_Type (M A)) => choice p A a b) in +Definition choiceA_real_realType (p q : {prob R}) (a b c : M A) : + let conv := (fun p (a b : M A) => choice p A a b) in conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c. Proof. exact: (choiceA p q). Qed. Definition prob_convType := M A. -HB.instance Definition _ := @isConvexSpace.Build prob_convType - (Choice.class (choice_of_Type (M A))) (fun p => choice p A) +HB.instance Definition _ := boolp.gen_eqMixin prob_convType. + +HB.instance Definition _ := boolp.gen_choiceMixin prob_convType. + +HB.instance Definition _ := @infotheo.probability.convex.isConvexSpace.Build prob_convType + (fun p => choice p A) (choice1 _) choicemm choiceC @@ -62,41 +66,41 @@ Proof. by []. Qed. End convex. -Lemma choiceACA {M : probMonad real_realType} T q p : +Lemma choiceACA {M : probMonad R} T q p : @interchange (prob_convType M T) (fun a b => a <|p|> b) (fun a b => a <|q|> b). Proof. by move=> *; exact: convACA. Qed. (* NB: the parameter def is because Coq functions are total *) -Fixpoint uniform {M : probMonad real_realType} {A : Type} (def : A) (s : seq A) : M A := +Fixpoint uniform {M : probMonad R} {A : Type} (def : A) (s : seq A) : M A := match s with | [::] => Ret def | [:: x] => Ret x | x :: xs => Ret x <| (/ IZR (Z_of_nat (size (x :: xs))))%coqR%:pr |> uniform def xs end. -Lemma uniform_nil (M : probMonad real_realType) (A : Type) (def : A) : +Lemma uniform_nil (M : probMonad R) (A : Type) (def : A) : uniform def [::] = Ret def :> M A. Proof. by []. Qed. -Lemma choice_ext (q p : {prob real_realType}) (M : probMonad real_realType) A (m1 m2 : M A) : +Lemma choice_ext (q p : {prob R}) (M : probMonad R) A (m1 m2 : M A) : Prob.p p = Prob.p q :> R -> m1 <| p |> m2 = m1 <| q |> m2. Proof. by move/val_inj => ->. Qed. -Lemma uniform_cons (M : probMonad real_realType) (A : Type) (def : A) h s : +Lemma uniform_cons (M : probMonad R) (A : Type) (def : A) h s : uniform def (h :: s) = - Ret h <| (/ IZR (Z_of_nat (size (h :: s))))%coqR%:pr |> uniform def s :> M A. + Ret h <| (/ IZR (Z_of_nat (size s).+1))%coqR%:pr |> uniform def s :> M A. Proof. by case: s => //=; rewrite (@choice_ext 1%:pr) // ?choice1 //= Rinv_1. Qed. -Lemma uniform_singl (M : probMonad real_realType) (A : Type) (def : A) h : size h = 1%nat -> +Lemma uniform_singl (M : probMonad R) (A : Type) (def : A) h : size h = 1%nat -> uniform def h = Ret (head def h) :> M A. Proof. case: h => // h [|//] _. by rewrite uniform_cons uniform_nil (@choice_ext 1%:pr) ?choice1 //= invR1. Qed. -Lemma uniform_nseq (M : probMonad real_realType) (A : Type) (def : A) h n : +Lemma uniform_nseq (M : probMonad R) (A : Type) (def : A) h n : uniform def (nseq n.+1 h) = Ret h :> M A. Proof. elim: n => // n IH. @@ -104,7 +108,7 @@ by rewrite (_ : nseq _ _ = h :: nseq n.+1 h) // uniform_cons IH choicemm. Qed. From infotheo Require Import Reals_ext. -Lemma uniform_cat (M : probMonad real_realType) (A : Type) (a : A) s t : +Lemma uniform_cat (M : probMonad R) (A : Type) (a : A) s t : let m := size s in let n := size t in uniform a (s ++ t) = uniform a s <| (divRnnm m n)%:pr |> uniform a t :> M _. Proof. @@ -117,23 +121,25 @@ case/boolP : (m.-1 + n == 0)%nat => [{IH}|] m1n0. subst s2 t. rewrite cats0 (_ : Prob.mk _ = 1%:pr) ?choice1 //. by apply val_inj; rewrite /= /divRnnm div1R invR1. -rewrite cat_cons uniform_cons uniform_cons. +rewrite cat_cons. +rewrite uniform_cons. +rewrite uniform_cons. set pv := ((/ _)%coqR). -set v : {prob real_realType} := @Prob.mk _ pv _. +set v : {prob R} := @Prob.mk _ pv _. (*set u : {prob real_realType} := ((size s2)%:R / (size s2 + size t)%:R)%coqR%:pr.*) set u := @Prob.mk_ _ ((size s2)%:R / (size s2 + size t)%:R)%coqR (prob_divRnnm_subproof _ _). rewrite -[RHS](@choiceA_alternative _ _ _ v u). by rewrite IH. -rewrite -RmultE. split. - rewrite 3!probpK -INR_IZR_INZ. +rewrite -RmultE; split. + rewrite 2!probpK. + rewrite -INR_IZR_INZ. rewrite (_ : INR _ = INR m) // mulRA mulVR; last by rewrite INR_eq0'. - by rewrite mul1R /pv -INR_IZR_INZ [size _]/= size_cat -addSn. + by rewrite mul1R /= /pv -INR_IZR_INZ [size _]/= size_cat -addSn. rewrite 3!probpK. -transitivity ( (1 - 1 / INR (m + n)) * (1 - INR (m.-1) / INR (m.-1 + n)))%coqR; last first. - congr (_ .~ * _)%R. - by rewrite /v /pv probpK INR_IZR_INZ [size _]/= size_cat -addSn div1R. -transitivity (INR n / INR (m + n))%coqR. - rewrite {1}/onem -RminusE -R1E -{1}(Rinv_r (INR (m+n))); last exact/not_0_INR. +transitivity ( (1 - 1 / (m + n)%:R) * (1 - m.-1%:R / (m.-1 + n)%:R))%coqR; last first. + by congr (_ .~ * _)%R; rewrite /v /pv/= INR_IZR_INZ/= div1R size_cat. +transitivity (n%:R / (m + n)%:R)%coqR. + rewrite {1}/onem -RminusE -R1E -{1}(Rinv_r (m + n)%:R); last exact/not_0_INR. rewrite -mulRBl -minus_INR; last by apply/leP; rewrite leq_addr. by rewrite minusE addnC addnK. rewrite {1}/Rdiv mulRC. @@ -150,30 +156,32 @@ rewrite -minus_INR; last by apply/leP; rewrite leq_addr. by rewrite addnC minusE -subnBA // subnn subn0. Qed. -Lemma uniform2 (M : probMonad real_realType) (A : Type) (def : A) a b : +Lemma uniform2 (M : probMonad R) (A : Type) (def : A) a b : uniform def [:: a; b] = uniform def [:: b; a] :> M _. Proof. rewrite uniform_cons uniform_singl // uniform_cons uniform_singl //. set pa := Prob.mk _. rewrite choiceC /= (@choice_ext pa) //=. -rewrite /onem -RminusE -R1E; field. +by rewrite /onem -RminusE -R1E; field. Qed. -Lemma uniform_inde (M : probMonad real_realType) (A : Type) a (x : seq A) {B} (m : M B) : +Lemma uniform_inde (M : probMonad R) (A : Type) a (x : seq A) {B} (m : M B) : uniform a x >> m = m. Proof. elim: x m => [/= m|x xs IH m]; first by rewrite bindretf. by rewrite uniform_cons choice_bindDl IH bindretf choicemm. Qed. -Lemma uniform_naturality (M : probMonad real_realType) (A B : Type) (a : A) (b : B) (f : A -> B) : +Lemma uniform_naturality (M : probMonad R) (A B : Type) (a : A) (b : B) (f : A -> B) : forall x, (0 < size x)%nat -> ((@uniform M _ b) \o map f) x = ((M # f) \o uniform a) x. Proof. elim=> // x [_ _|x' xs]; first by rewrite [in RHS]compE fmapE bindretf. move/(_ isT) => IH _. -rewrite compE [in RHS]compE [in LHS]uniform_cons [in RHS]uniform_cons. -set p := (@Prob.mk _ (/ IZR (Z.of_nat (size _)))%coqR _ in X in _ = X). +rewrite compE [in RHS]compE. +rewrite [x' :: xs]lock [in LHS]uniform_cons -/(map _ _) [in LHS]/= -lock. +rewrite [x' :: xs]lock [in RHS]uniform_cons -/(map _ _) [in RHS]/= -lock. +set p := (X in _ <| X |> _ = _). rewrite (_ : @Prob.mk _ (/ _)%coqR _ = p); last first. by apply val_inj; rewrite /= size_map. move: IH; rewrite 2!compE => ->. @@ -181,7 +189,7 @@ by rewrite [in RHS]fmapE choice_bindDl bindretf fmapE. Qed. Arguments uniform_naturality {M A B}. -Lemma mpair_uniform_base_case (M : probMonad real_realType) (A : Type) a x (y : seq A) : +Lemma mpair_uniform_base_case (M : probMonad R) (A : Type) a x (y : seq A) : (0 < size y)%nat -> uniform (a, a) (cp [:: x] y) = mpair (uniform a [:: x], uniform a y) :> M _. Proof. @@ -193,7 +201,7 @@ transitivity (do z <- Ret x; do y' <- uniform a y; Ret (z, y') : M _)%Do. by []. Qed. -Lemma mpair_uniform (M : probMonad real_realType) (A : Type) a (x y : seq A) : +Lemma mpair_uniform (M : probMonad R) (A : Type) a (x y : seq A) : (0 < size x)%nat -> (0 < size y)%nat -> mpair (uniform a x, uniform a y) = uniform (a, a) (cp x y) :> M (A * A)%type. Proof. @@ -224,23 +232,25 @@ by apply val_inj; rewrite /= /divRnnm div1R. Qed. Section altprob_semilattconvtype. -Variable M : altProbMonad real_realType. +Variable M : altProbMonad R. Variable T : Type. -Import convex necset SemiLattice. +(*Import convex necset SemiLattice.*) Definition altProb_semiLattConvType := M T. -Let axiom (p : {prob real_realType}) (x y z : altProb_semiLattConvType) : +Let axiom (p : {prob R}) (x y z : altProb_semiLattConvType) : x <| p |> (y [~] z) = (x <| p |> y) [~] (x <| p |> z). Proof. by rewrite choiceDr. Qed. +HB.instance Definition _ := boolp.gen_eqMixin altProb_semiLattConvType. +HB.instance Definition _ := boolp.gen_choiceMixin altProb_semiLattConvType. + HB.instance Definition _ := @isSemiLattice.Build altProb_semiLattConvType - (Choice.class (choice_of_Type (M T))) (fun x y => x [~] y) (@altC M T) (@altA M T) (@altmm M T). -HB.instance Definition _ := @isConvexSpace_.isConvexSpace.Build altProb_semiLattConvType - (Choice.class (choice_of_Type (M T))) (fun p => choice p T) +HB.instance Definition _ := @probability.convex.isConvexSpace.Build altProb_semiLattConvType + (fun p : {prob R} => choice p T) (choice1 _) choicemm choiceC (@choiceA_real_realType M T). HB.instance Definition _ := @isSemiLattConv.Build altProb_semiLattConvType axiom. @@ -250,8 +260,9 @@ End altprob_semilattconvtype. (* TODO(rei): incipit of section 5 of gibbonsUTP2012 on the model of MonadAltProb *) Section convexity_property. +From mathcomp.analysis Require Import Rstruct. -Variables (M : altProbMonad real_realType) (A : Type) (p q : M A). +Variables (M : altProbMonad R) (A : Type) (p q : M A). Lemma convexity w : p [~] q = (p <| w |> p) [~] (q <| w |> p) [~] (p <| w |> q) [~] (q <| w |> q). @@ -265,13 +276,13 @@ Qed. End convexity_property. -Definition bcoin {M : probMonad real_realType} (p : {prob real_realType}) : M bool := +Definition bcoin {M : probMonad R} (p : {prob R}) : M bool := Ret true <| p |> Ret false. Arguments bcoin : simpl never. Section prob_only. -Variable M : probMonad real_realType. -Variable p q : {prob real_realType}. +Variable M : probMonad R. +Variable p q : {prob R}. Definition two_coins : M (bool * bool)%type := (do a <- bcoin p; (do b <- bcoin q; Ret (a, b) : M _))%Do. @@ -290,7 +301,7 @@ End prob_only. Section mixing_choices. -Variable M : altProbMonad real_realType. +Variable M : altProbMonad R. Definition arbcoin p : M bool := (do a <- arb ; (do c <- bcoin p; Ret (a == c) : M _))%Do. @@ -312,7 +323,7 @@ Local Open Scope R_scope. Import Order.POrderTheory Order.TotalTheory GRing.Theory Num.Theory. (* TODO? : move magnified_weight to infotheo.convex *) -Lemma magnified_weight_proof (p q r : {prob real_realType}) : +Lemma magnified_weight_proof (p q r : {prob R}) : Prob.p p < Prob.p q < Prob.p r -> (0 <= (Prob.p r - Prob.p q) / (Prob.p r - Prob.p p) <= 1)%mcR. Proof. case => /RltP pq /RltP qr. @@ -324,16 +335,16 @@ rewrite -(ler_pM2r rp). by rewrite mulrAC -mulrA mulrV // mulr1 mul1r lerD2l lerNl opprK; exact/ltW. Qed. -Definition magnified_weight (p q r : {prob real_realType}) - (H : Prob.p p < Prob.p q < Prob.p r) : {prob real_realType} := +Definition magnified_weight (p q r : {prob R}) + (H : Prob.p p < Prob.p q < Prob.p r) : {prob R} := Eval hnf in Prob.mk_ (magnified_weight_proof H). Local Notation m := magnified_weight. Local Notation "x +' y" := (addpt x y) (at level 50). Local Notation "a *' x" := (scalept a x) (at level 40). -Lemma magnify_conv (T : isConvexSpace_.ConvexSpace.Exports.convType) - (p q r : {prob real_realType}) (x y : T) (H : Prob.p p < Prob.p q < Prob.p r) : +Lemma magnify_conv (T : convType) + (p q r : {prob R}) (x y : T) (H : Prob.p p < Prob.p q < Prob.p r) : (x <|p|> y) <| magnified_weight H |> (x <|r|> y) = x <|q|> y. Proof. case: (H) => pq qr. @@ -368,7 +379,7 @@ rewrite -RminusE. ring. Qed. -Lemma arbcoin_spec_convexity (p q : {prob real_realType}) : +Lemma arbcoin_spec_convexity (p q : {prob R}) : Prob.p p < Prob.p q < (Prob.p p).~ -> arbcoin p = (bcoin p : M _) [~] bcoin (Prob.p p).~%:pr [~] bcoin q. Proof. @@ -423,20 +434,23 @@ Qed. End mixing_choices. -Definition coins23 {M : exceptProbMonad real_realType} : M bool := +Definition coins23 {M : exceptProbMonad R} : M bool := Ret true <| (/ 2)%coqR%:pr |> (Ret false <| (/ 2)%coqR%:pr |> fail). +Reserved Notation "x <= y <= z :> T" (at level 70, y, z at next level). +Notation "x <= y <= z :> T" := ((x <= y :> T)%mcR && (y <= z :> T)%mcR). + (* NB: notation for ltac:(split; fourier?)*) Local Open Scope R_scope. -Lemma choiceA_compute {N : probMonad real_realType} (T F : bool) (f : bool -> N bool) : +Lemma choiceA_compute {N : probMonad R} (T F : bool) (f : bool -> N bool) : f T <|(/ 9)%:pr|> (f F <|(/ 8)%:pr|> (f F <|(/ 7)%:pr|> (f F <|(/ 6)%:pr|> (f T <|(/ 5)%:pr|> (f F <|(/ 4)%:pr|> (f F <|(/ 3)%:pr|> (f F <|(/ 2)%:pr|> f T))))))) = f F <|(/ 3)%:pr|> (f F <|(/ 2)%:pr|> f T) :> N _. Proof. -have H27 : (0 <= (2/7 : R) <= 1)%mcR by apply/andP; split; lra. -have H721 : (0 <= (7/21 : R) <= 1)%mcR by apply/andP; split; lra. -have H2156 : (0 <= (21/56 : R) <= 1)%mcR by apply/andP; split; lra. -have H25 : (0 <= (2/5 : R) <= 1)%mcR by apply/andP; split; lra. +have H27 : 0 <= 2/7 <= 1 :> R by lra. +have H721 : 0 <= 7/21 <= 1 :> R by lra. +have H2156 : 0 <= 21/56 <= 1 :> R by lra. +have H25 : 0 <= 2/5 <= 1 :> R by lra. rewrite [in RHS](@choiceA_alternative _ _ _ _ _ (/ 2)%:pr (/ 3).~%:pr); last first. rewrite 3!probpK /= /onem. rewrite -!(RmultE,RminusE,R1E). @@ -534,10 +548,10 @@ rewrite [in LHS](@choiceA_alternative _ _ _ (/ 9)%:pr (probcplt (/ 4).~%:pr) (/ by rewrite choicemm choiceC. Qed. -Definition uFFT {M : probMonad real_realType} : M bool := +Definition uFFT {M : probMonad R} : M bool := uniform true [:: false; false; true]. -Lemma uFFTE (M : probMonad real_realType) : uFFT = bcoin (/ 3)%:pr :> M _. +Lemma uFFTE (M : probMonad R) : uFFT = bcoin (/ 3)%:pr :> M _. Proof. rewrite /uFFT /bcoin uniform_cons. rewrite (_ : _%:pr = (/ 3)%:pr)%R; last exact/val_inj. @@ -552,10 +566,10 @@ rewrite choicemm choiceC; congr (Ret true <| _ |> Ret false). by apply val_inj; rewrite /= onemK. Qed. -Definition uTTF {M : probMonad real_realType} : M bool := +Definition uTTF {M : probMonad R} : M bool := uniform true [:: true; true; false]. -Lemma uTTFE (M : probMonad real_realType) : uTTF = bcoin (/ 3).~%:pr :> M _. +Lemma uTTFE (M : probMonad R) : uTTF = bcoin (/ 3).~%:pr :> M _. Proof. rewrite /uTTF /bcoin uniform_cons. rewrite (_ : _%:pr = (/ 3)%:pr)%R; last exact/val_inj. @@ -568,7 +582,7 @@ rewrite /= /onem; split. rewrite -!RminusE -RmultE -R1E. field. Qed. -Lemma uniform_notin (M : probMonad real_realType) (A : eqType) (def : A) (s : seq A) B +Lemma uniform_notin (M : probMonad R) (A : eqType) (def : A) (s : seq A) B (ma mb : A -> M B) (p : pred A) : s != [::] -> (forall x, x \in s -> ~~ p x) -> @@ -587,7 +601,7 @@ rewrite 2!choice_bindDl; congr (_ <| _ |> _). by rewrite IH // => a ta; rewrite H // in_cons ta orbT. Qed. -Lemma choice_halfC A (M : probMonad real_realType) (a b : M A) : +Lemma choice_halfC A (M : probMonad R) (a b : M A) : a <| (/ 2)%:pr |> b = b <| (/ 2)%:pr |> a. Proof. rewrite choiceC (_ : (_.~)%:pr = (/ 2)%:pr) //. @@ -595,7 +609,7 @@ apply val_inj; rewrite /= /onem. rewrite -RminusE -R1E; field. Qed. -Lemma choice_halfACA A (M : probMonad real_realType) (a b c d : M A) : +Lemma choice_halfACA A (M : probMonad R) (a b c d : M A) : (a <| (/ 2)%:pr |> b) <| (/ 2)%:pr |> (c <| (/ 2)%:pr |> d) = (a <| (/ 2)%:pr |> c) <| (/ 2)%:pr |> (b <| (/ 2)%:pr |> d). Proof. @@ -605,7 +619,7 @@ by rewrite -choice_conv. Qed. Section keimel_plotkin_instance. -Variables (M : altProbMonad real_realType) (A : Type). +Variables (M : altProbMonad R) (A : Type). Variables (p q : M A). Lemma keimel_plotkin_instance : diff --git a/proba_monad_model.v b/proba_monad_model.v index b09b37eb..26045c02 100644 --- a/proba_monad_model.v +++ b/proba_monad_model.v @@ -16,7 +16,8 @@ Require Import monae_lib hierarchy monad_lib proba_lib. Local Open Scope monae_scope. Local Open Scope proba_scope. -Notation choice_of_Type := convex.choice_of_Type. +Require monad_model. +Notation choice_of_Type := monad_model.choice_of_Type. Module MonadProbModel. Section monadprobmodel. @@ -60,7 +61,7 @@ Proof. by move=> ? ?; exact: convC. Qed. Let choicemm : forall (T : Type) p, idempotent (@choice p T). Proof. by move=> ? ? ?; exact: convmm. Qed. -Let choiceA : forall (T : Type) (p q r s : {prob real_realType}) (a b c : acto T), +Let choiceA : forall (T : Type) (p q r s : {prob R}) (a b c : acto T), choice p _ a (choice q _ b c) = choice [s_of p, q] _ (choice [r_of p, q] _ a b) c. Proof. move=> ? p q r s a b c. @@ -69,7 +70,7 @@ rewrite [LHS](_ : _ = conv p a (conv q b c))//. (* NB: this is slow *) by rewrite convA. Qed. -HB.instance Definition _ := isMonadConvex.Build real_realType +HB.instance Definition _ := isMonadConvex.Build R acto choice1 choiceC choicemm choiceA. Let prob_bindDl p : @@ -80,7 +81,7 @@ rewrite !(@BindE (choice_of_Type A) (choice_of_Type B)). by rewrite fsdist_conv_bind_left_distr. Qed. -HB.instance Definition mixin := isMonadProb.Build real_realType +HB.instance Definition mixin := isMonadProb.Build R acto prob_bindDl. (* NB: we use Pack here for an application in gcm_model.v *) Definition t := MonadProb.Pack (MonadProb.Class mixin). diff --git a/smallstep.v b/smallstep.v index d78e9acd..f341e9a3 100644 --- a/smallstep.v +++ b/smallstep.v @@ -858,7 +858,7 @@ Compute run_ss p_nonce 0. Remark denote_p_nonce : denote _ nat p_nonce = nonce. Proof. by []. Qed. -Program Example p_nonce_twice : program bool_eqType := +Program Example p_nonce_twice : program bool := p_do nonce <- p_ret ( p_do n : nat <- p_get; p_do _ : unit <- p_put (S n); diff --git a/state_lib.v b/state_lib.v index a4d83509..ee5e1e05 100644 --- a/state_lib.v +++ b/state_lib.v @@ -411,7 +411,7 @@ Lemma nilp_intersect (A : eqType) (s t : seq A) : nilp (intersect s t) = ~~ has (mem s) t. Proof. by rewrite /intersect /nilp size_filter has_count lt0n negbK. Qed. -Definition seq_disjoint {A : eqType} : pred [eqType of Squaring (seq A)] := +Definition seq_disjoint {A : eqType} : pred (Squaring (seq A)) := (@nilp _) \o uncurry intersect. Lemma intersect0s (A : eqType) (s : seq A) : intersect [::] s = [::]. @@ -590,7 +590,7 @@ Definition swap {S : eqType} {I : eqType} {M : arrayMonad S I} (i j : I) : M uni Section monadarray_example. Local Open Scope do_notation. -Variable M : arrayMonad nat bool_eqType. +Variable M : arrayMonad nat bool. Definition does_swap (m : M unit) := (do x <- aget false ;