From ed161f29c5e31f3567e53f319ce0aca595e1b1cb Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 20 Dec 2024 17:23:05 +0900 Subject: [PATCH] upd to MathComp 2.3.0 (#150) * upd to MathComp 2.3.0 --- .github/workflows/docker-action.yml | 4 ++-- coq-monae.opam | 16 ++++++++-------- impredicative_set/ifail_lib.v | 6 +++--- meta.yml | 20 ++++++++++---------- theories/applications/example_iquicksort.v | 20 ++++++++++---------- theories/applications/example_quicksort.v | 16 +++++++++------- theories/applications/example_typed_store.v | 20 ++++++++++---------- theories/lib/array_lib.v | 2 +- theories/lib/fail_lib.v | 11 +++++------ theories/models/altprob_model.v | 4 ++-- theories/models/monad_model.v | 6 +++--- 11 files changed, 63 insertions(+), 62 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index d56c3026..89d4af4b 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,8 +17,8 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.2.0-coq-8.19' - - 'mathcomp/mathcomp:2.2.0-coq-8.20' + - 'mathcomp/mathcomp:2.3.0-coq-8.19' + - 'mathcomp/mathcomp:2.3.0-coq-8.20' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/coq-monae.opam b/coq-monae.opam index e756575b..47667d46 100644 --- a/coq-monae.opam +++ b/coq-monae.opam @@ -19,15 +19,15 @@ build: [make "-j%{jobs}%" ] install: [make "install_full"] depends: [ "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-analysis" { (>= "1.5.0")} - "coq-infotheo" { >= "0.7.3"} + "coq-mathcomp-ssreflect" { (>= "2.3.0") | (= "dev") } + "coq-mathcomp-fingroup" { (>= "2.3.0") | (= "dev") } + "coq-mathcomp-algebra" { (>= "2.3.0") | (= "dev") } + "coq-mathcomp-solvable" { (>= "2.3.0") | (= "dev") } + "coq-mathcomp-field" { (>= "2.3.0") | (= "dev") } + "coq-mathcomp-analysis" { (>= "1.7.0")} + "coq-infotheo" { >= "0.7.6"} "coq-paramcoq" { >= "1.1.3" & < "1.2~" } - "coq-hierarchy-builder" { >= "1.5.0" } + "coq-hierarchy-builder" { >= "1.7.0" } "coq-equations" { >= "1.3" & < "1.4~" } ] diff --git a/impredicative_set/ifail_lib.v b/impredicative_set/ifail_lib.v index aca01694..253c08d4 100644 --- a/impredicative_set/ifail_lib.v +++ b/impredicative_set/ifail_lib.v @@ -386,7 +386,7 @@ rewrite -fmap_oE (_ : map f \o cons y = cons (f y) \o map f) //. by rewrite fmap_oE -(fcompE (map f)) -IH [RHS]/= insertE. Qed. -Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A). +Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A). Variables (A : UU0) (p : pred A). @@ -547,7 +547,7 @@ apply funext; elim => [/=|x xs IH]. by rewrite fcompE [in iperm _]/= fmap_bind -insert_map -bind_fmap -fcompE -IH. Qed. -Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A). +Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A). Variables (A : UU0) (p : pred A). @@ -815,7 +815,7 @@ move=> mn1 mn2; rewrite /liftM2. by apply: (refin_bind mn1 _) => a; exact: refin_bindr. Qed. -Lemma refin_guard_le (M : plusMonad) (d : unit) (T : orderType d) (x y : T) : +Lemma refin_guard_le (M : plusMonad) d (T : orderType d) (x y : T) : (guard (~~ (y <= x)%O) : M _) `<=` guard (x <= y)%O. Proof. rewrite -ltNge le_eqVlt. diff --git a/meta.yml b/meta.yml index 8b05dcdc..2fd6d9ef 100644 --- a/meta.yml +++ b/meta.yml @@ -39,45 +39,45 @@ supported_coq_versions: opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }' tested_coq_opam_versions: -- version: '2.2.0-coq-8.19' +- version: '2.3.0-coq-8.19' repo: 'mathcomp/mathcomp' -- version: '2.2.0-coq-8.20' +- version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "2.2.0") | (= "dev") }' + version: '{ (>= "2.3.0") | (= "dev") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "2.2.0") | (= "dev") }' + version: '{ (>= "2.3.0") | (= "dev") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "2.2.0") | (= "dev") }' + version: '{ (>= "2.3.0") | (= "dev") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "2.2.0") | (= "dev") }' + version: '{ (>= "2.3.0") | (= "dev") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "2.2.0") | (= "dev") }' + version: '{ (>= "2.3.0") | (= "dev") }' description: |- [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "1.5.0")}' + version: '{ (>= "1.7.0")}' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: name: coq-infotheo - version: '{ >= "0.7.3"}' + version: '{ >= "0.7.6"}' description: |- [Infotheo](https://github.com/affeldt-aist/infotheo) - opam: @@ -87,7 +87,7 @@ dependencies: [Paramcoq](https://github.com/coq-community/paramcoq) - opam: name: coq-hierarchy-builder - version: '{ >= "1.5.0" }' + version: '{ >= "1.7.0" }' description: |- [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - opam: diff --git a/theories/applications/example_iquicksort.v b/theories/applications/example_iquicksort.v index 4c7e9449..85050c87 100644 --- a/theories/applications/example_iquicksort.v +++ b/theories/applications/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). +Context d (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). +Context d (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). +Context d (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 := @@ -129,7 +129,7 @@ Arguments qperm_partl {d E M}. solve[exact: qperm_partl_isNondet] : core. Section ipartl. -Variables (d : unit) (T : orderType d). +Context d (T : orderType d). Section arrayMonad. Variable M : arrayMonad T nat. @@ -168,7 +168,7 @@ End ipartl. Arguments ipartl {d T M}. Section dipartl. -Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat). +Context d (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)}. @@ -219,7 +219,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). +Context d (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* page 11 step 4 *) @@ -283,7 +283,7 @@ Qed. End derivation_qperm_partl_ipartl. Section refin_qperm_partl. -Variables (d : unit) (E : orderType d) (M : plusArrayMonad E nat). +Context d (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) `<=` @@ -318,7 +318,7 @@ End refin_qperm_partl. (* specification of ipartl *) Section refin_ipartl. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). +Context d (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* page 12, used in the proof of lemma 10 *) @@ -383,7 +383,7 @@ Qed. End refin_ipartl. Section iqsort_def. -Variables (d : unit) (T : orderType d) (M : plusArrayMonad T nat). +Context d (T : orderType d) (M : plusArrayMonad T nat). Local Obligation Tactic := idtac. @@ -501,7 +501,7 @@ End iqsort_def. Arguments iqsort {d T M}. Section iqsort_spec. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). +Context d (E : orderType d) (M : plusArrayMonad E nat). Implicit Types i : nat. (* eqn 12 page 13 *) diff --git a/theories/applications/example_quicksort.v b/theories/applications/example_quicksort.v index bb8fa073..71ce6e95 100644 --- a/theories/applications/example_quicksort.v +++ b/theories/applications/example_quicksort.v @@ -37,7 +37,7 @@ Local Open Scope order_scope. From mathcomp Require Import ssrnat. Section sorted. -Variables (d : unit) (T : orderType d). +Context d (T : orderType d). Local Notation sorted := (sorted <=%O). @@ -62,7 +62,7 @@ Local Open Scope tuple_ext_scope. Local Open Scope mprog. Section partition. -Variables (M : plusMonad) (d : unit) (T : orderType d). +Context (M : plusMonad) d (T : orderType d). Definition is_partition p (yz : seq T * seq T) := all (<= p) yz.1 && all (>= p) yz.2. @@ -123,7 +123,7 @@ Qed. End partition. Section slowsort. -Variables (M : plusMonad) (d : unit) (T : orderType d). +Context (M : plusMonad) d (T : orderType d). Local Notation sorted := (sorted <=%O). @@ -204,7 +204,7 @@ Ltac sub := repeat rewrite !alt_bindDl !bindretf; repeat rewrite !qpermE !bindA !bindretf /=. Ltac bindSF := rewrite !bindskipf !bindfailf. -Variables (d : unit) (T : orderType d). +Context d (T : orderType d). Example slowsort2 : @slowsort M _ _ [:: 2; 1]%N = Ret [:: 1; 2]%N. Proof. @@ -219,7 +219,7 @@ Qed. End slowsort_example. Section slowsort_preserves. -Context (M : plusMonad) {d : unit} {E : orderType d}. +Context (M : plusMonad) d {E : orderType d}. Let slowsort_preserves_size : preserves (@slowsort M _ E) size. Proof. @@ -252,7 +252,7 @@ End slowsort_preserves. Section qsort. Variables (M : plusMonad). -Variables (d : unit) (T : orderType d). +Context d (T : orderType d). (* let *) Equations? qsort (s : seq T) : seq T by wf (size s) lt := @@ -307,7 +307,8 @@ End qsort. Module qsort_function. Section qsort_function. -Variables (M : plusMonad) (d : unit) (T : orderType d). +Context (M : plusMonad) d (T : orderType d). + Function qsort (s : seq T) {measure size s} : seq T := (* if s is h :: t then let '(ys, zs) := partition h t in @@ -326,5 +327,6 @@ by rewrite pht_yz /= => <-; apply/ltP; rewrite ltnS leq_addl. move=> s h t _ ys zs pht_yz; have := size_partition h t. by rewrite pht_yz /= => <-; apply/ltP; rewrite ltnS leq_addr. Defined. + End qsort_function. End qsort_function. diff --git a/theories/applications/example_typed_store.v b/theories/applications/example_typed_store.v index 759b86bf..e3d5da77 100644 --- a/theories/applications/example_typed_store.v +++ b/theories/applications/example_typed_store.v @@ -459,12 +459,12 @@ Variable (N : monad) (M : typedStoreRunMonad N). Local Notation fact_ref := (fact_ref N M). Theorem fact_ref_ok n : - crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some (fact_rec n). + crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some n`!. Proof. -set fn := fact_rec n. +set fn := n`!. set m := n. set s := 1. -have smn : s * fact_rec m = fn by rewrite mul1n. +have smn : s * m`! = fn by rewrite mul1n. elim: m s smn => [|m IH] s /= smn. rewrite /fact_ref -smn muln1. under eq_bind do rewrite bindskipf. @@ -500,14 +500,14 @@ Local Open Scope do_notation. Local Notation fact_for := (fact_for N M). -Theorem fact_for_ok n : crun (fact_for n) = Some (fact_rec n). +Theorem fact_for_ok n : crun (fact_for n) = Some n`!. Proof. rewrite /fact_for. under eq_bind do rewrite !bindA !bindretf. -transitivity (crun (cnew ml_int (fact_rec n) >> Ret (fact_rec n) : M _)); +transitivity (crun (cnew ml_int n`! >> Ret n`! : M _)); last by rewrite crunret // crunnew0. congr crun. -rewrite -{1}/(fact_rec 0). +rewrite -{1}/(factorial 0). pose m := n. have -> : 0 = n - m by rewrite subnn. have : m <= n by []. @@ -860,16 +860,16 @@ Local Notation fact_for63 := (fact_for63 N M). Variable n : nat. Hypothesis Hn : (Z.of_nat n < Sint63.to_Z Sint63.max_int)%Z. -Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int (fact_rec n)). +Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int n`!). Proof. rewrite /fact_for63. under eq_bind do rewrite !bindA !bindretf. -set fn := N2int (fact_rec n). +set fn := N2int n`!. transitivity (crun (cnew ml_int fn >> Ret fn : M _)); last by rewrite crunret // crunnew0. congr crun. have {1}-> : (1 = N2int 1)%int63 by []. -rewrite -/(fact_rec 0). +rewrite -/(0`!). have -> : (1 = Uint63.succ (N2int 0))%int63 by []. pose m := n. have -> : 0 = n - m by rewrite subnn. @@ -884,7 +884,7 @@ case: m IH mn => [|m] IH mn. rewrite cnewget. under eq_bind do rewrite bindretf -cgetret. rewrite cnewput -N2int_mul mulnC -{1}(prednK mn) cnewget subn1. - by rewrite -/(fact_rec n.-1.+1) prednK. + by rewrite -/(n.-1.+1`!) prednK. under eq_bind do rewrite forloop63S !(ltsb_subr,bindA) //. rewrite cnewget. under eq_bind do rewrite bindretf. diff --git a/theories/lib/array_lib.v b/theories/lib/array_lib.v index eb3c32fd..d519c403 100644 --- a/theories/lib/array_lib.v +++ b/theories/lib/array_lib.v @@ -179,7 +179,7 @@ Fixpoint readList i (n : nat) : M (seq S) := End write_read. Section refin_writeList_aswap. -Variable (d : unit) (E : orderType d) (M : plusArrayMonad E nat). +Context d (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/theories/lib/fail_lib.v b/theories/lib/fail_lib.v index ece6ab07..88d97d8c 100644 --- a/theories/lib/fail_lib.v +++ b/theories/lib/fail_lib.v @@ -485,7 +485,7 @@ rewrite -fmap_oE (_ : map f \o cons y = cons (f y) \o map f) //. by rewrite fmap_oE -(fcompE (map f)) -IH [RHS]/= insertE. Qed. -Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A). +Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A). Variables (A : UU0) (p : pred A). @@ -646,7 +646,7 @@ apply boolp.funext; elim => [/=|x xs IH]. by rewrite fcompE [in iperm _]/= fmap_bind -insert_map -bind_fmap -fcompE -IH. Qed. -Hypothesis Mmm : forall A, idempotent (@alt _ A : M A -> M A -> M A). +Hypothesis Mmm : forall A, idempotent_op (@alt _ A : M A -> M A -> M A). Variables (A : UU0) (p : pred A). @@ -1017,8 +1017,7 @@ Local Close Scope mprog. End splits_prePlusMonad. Section qperm. - -Variables (M : altMonad) (A : UU0) (d : unit) (T : orderType d). +Context (M : altMonad) (A : UU0) d (T : orderType d). Local Obligation Tactic := idtac. Program Definition qperm' (s : seq A) @@ -1085,7 +1084,7 @@ Arguments qperm {M} {A}. Module qperm_function. Section qperm_function. -Variables (M : plusMonad) (A : UU0) (d : unit) (T : orderType d). +Context (M : plusMonad) (A : UU0) d (T : orderType d). Local Obligation Tactic := idtac. Program Definition qperm' (s : seq A) @@ -1586,7 +1585,7 @@ move=> mn1 mn2; rewrite /liftM2. by apply: (refin_bind mn1 _) => a; exact: refin_bindr. Qed. -Lemma refin_guard_le (M : plusMonad) (d : unit) (T : orderType d) (x y : T) : +Lemma refin_guard_le (M : plusMonad) d (T : orderType d) (x y : T) : (guard (~~ (y <= x)%O) : M _) `<=` guard (x <= y)%O. Proof. rewrite -ltNge le_eqVlt. diff --git a/theories/models/altprob_model.v b/theories/models/altprob_model.v index fdbe0290..c6fac0fc 100644 --- a/theories/models/altprob_model.v +++ b/theories/models/altprob_model.v @@ -113,7 +113,7 @@ End bindaltDl. HB.instance Definition _ := @isMonadAlt.Build (Monad_of_category_monad.acto Mgcm) alt altA bindaltDl. -Lemma altxx A : idempotent (@alt A). +Lemma altxx A : idempotent_op (@alt A). Proof. by move=> x; rewrite /= /alt lubxx. Qed. Lemma altC A : commutative (@alt A). Proof. by move=> a b; rewrite /= /alt /= lubC. Qed. @@ -127,7 +127,7 @@ Lemma choice1 A (x y : gcm A) : x <| 1%:pr |> y = x. Proof. by rewrite conv1. Qed. Lemma choiceC A p (x y : gcm A) : x <|p|> y = y <|(Prob.p p).~%:pr|> x. Proof. by rewrite convC. Qed. -Lemma choicemm A p : idempotent (@choice p A). +Lemma choicemm A p : idempotent_op (@choice p A). Proof. by move=> m; rewrite /choice convmm. Qed. Let choiceA A (p q r s : {prob R}) (x y z : gcm A) : diff --git a/theories/models/monad_model.v b/theories/models/monad_model.v index 5e4196e2..dfe10a30 100644 --- a/theories/models/monad_model.v +++ b/theories/models/monad_model.v @@ -940,7 +940,7 @@ Module AltCI. Section set. Let M := [the altMonad of set]. -Let altmm (A : UU0) : idempotent (@alt M A). +Let altmm (A : UU0) : idempotent_op (@alt M A). Proof. by move=> ?; exact: setUid. Qed. Let altC (A : UU0) : commutative (@alt M A). Proof. by move=> ?; exact: setUC. Qed. @@ -1659,7 +1659,7 @@ move=> A m; apply boolp.funext => a/=; apply boolp.funext => -[x a1]/=. by rewrite /alt/= /aalt altmfail. Qed. HB.instance Definition _ := isMonadNondet.Build M altfailm altmfail. -Let altmm (A : UU0) : idempotent (@alt [the altMonad of M] A). +Let altmm (A : UU0) : idempotent_op (@alt [the altMonad of M] A). Proof. move=> m; apply boolp.funext => a/=; apply boolp.funext => -[x a1]/=. by rewrite /alt/= /aalt altmm. @@ -1769,7 +1769,7 @@ HB.instance Definition _ := isMonadAlt.Build M altA alt_bindDl. Let altfailm : @BindLaws.left_id M fail aalt. Proof. by []. Qed. Let altmfail : @BindLaws.right_id M fail aalt. Proof. by []. Qed. HB.instance Definition _ := isMonadNondet.Build M altfailm altmfail. -Let altmm (A : UU0) : idempotent (@aalt (M A)). Proof. by case. Qed. +Let altmm (A : UU0) : idempotent_op (@aalt (M A)). Proof. by case. Qed. Let altC (A : UU0) : commutative (@aalt (M A)). Proof. by []. Qed. HB.instance Definition _ := @isMonadAltCI.Build M altmm altC. Let bindmfail : BindLaws.right_zero bind fail. Proof. by []. Qed.