From 98db2badd8d4996cfafcd34f0708769a0dc4127e Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Mon, 5 May 2025 16:01:33 +0200 Subject: [PATCH 1/2] Adapt to https://github.com/math-comp/math-comp/pull/1169#52 --- examples/bubblesort.v | 15 +++++++-------- examples/quicksort.v | 17 +++++++---------- 2 files changed, 14 insertions(+), 18 deletions(-) diff --git a/examples/bubblesort.v b/examples/bubblesort.v index 8fb6810..5c68f47 100644 --- a/examples/bubblesort.v +++ b/examples/bubblesort.v @@ -11,16 +11,15 @@ See the License for the specific language governing permissions and limitations under the License. *) -From Coq Require Import ssreflect ssrbool ssrfun. +From mathcomp Require Import ssreflect ssrbool ssrfun. From mathcomp Require Import ssrnat eqtype seq path fintype tuple. -From mathcomp Require Import finfun fingroup perm interval. +From mathcomp Require Import finfun fingroup perm order interval. From pcm Require Import options axioms prelude pred ordtype slice. From pcm Require Import seqext pcm unionmap heap. -From htt Require Import options model heapauto. -From htt Require Import array. -From mathcomp Require order. -Import order.Order.NatOrder order.Order.TTheory. +From htt Require Import options model heapauto array. +Import Order.NatOrder Order.TTheory. Local Open Scope order_scope. +Local Open Scope nat_scope. (* Brief mathematics of (bubble) array sorting: *) (* Theory of permutations built out of (adjacent-element) swaps acting on *) @@ -114,13 +113,13 @@ Proof. by rewrite slice_xL // onth_codom1S. Qed. (* TODO notation fails *) Lemma codom1_ax_rcons (f : {ffun 'I_n.+1 -> A}) (a : itv_bound nat) (i : 'I_n) : - order.Order.le a (BLeft (i : nat)) -> + Order.le a (BLeft (i : nat)) -> &:(fgraph f) (Interval a (BRight (i : nat))) = rcons (&:(fgraph f) (Interval a (BLeft (i : nat)))) (f (Wo i)). Proof. by move=>H; rewrite slice_xR //= onth_codom1 /=. Qed. Lemma codom1_ax_rcons2 (f : {ffun 'I_n.+1 -> A}) (a : itv_bound nat) (i : 'I_n) : - order.Order.le a (BLeft (i : nat)) -> + Order.le a (BLeft (i : nat)) -> &:(fgraph f) (Interval a (BRight i.+1)) = rcons (rcons (&:(fgraph f) (Interval a (BLeft (i : nat)))) (f (Wo i))) (f (So i)). diff --git a/examples/quicksort.v b/examples/quicksort.v index c6530e0..1b8a894 100644 --- a/examples/quicksort.v +++ b/examples/quicksort.v @@ -13,16 +13,13 @@ limitations under the License. From mathcomp Require Import ssreflect ssrbool ssrfun. From mathcomp Require Import ssrnat eqtype seq path fintype tuple finfun. -From mathcomp Require Import finset fingroup perm. -From mathcomp Require Import interval. +From mathcomp Require Import finset fingroup perm order interval. From pcm Require Import options axioms prelude seqext pred ordtype slice. From pcm Require Import pcm unionmap heap. -From htt Require Import options model heapauto. -From htt Require Import array. -From mathcomp Require order. -Import order.Order.NatOrder order.Order.TTheory. +From htt Require Import options model heapauto array. +Import Order.NatOrder Order.TTheory. Local Open Scope order_scope. - +Local Open Scope nat_scope. (* Brief mathematics of quickorting *) (* There is some overlap with mathematics developed for bubblesort *) @@ -150,7 +147,7 @@ Lemma perm_on_fgraph (i : interval nat) (p : 'S_n) (f : {ffun 'I_n -> A}) : &:(fgraph f ) i. Proof. case: i=>i j H. -case/boolP: (order.Order.lt i j)=>[Hij|]; last first. +case/boolP: (Order.lt i j)=>[Hij|]; last first. - by rewrite -leNgt => H12; rewrite !itv_swapped_bnd. move: (perm_fgraph p f). rewrite {1}(slice_extrude (fgraph (pffun p f)) (i:=Interval i j)) //=. @@ -510,7 +507,7 @@ move: (ltn_ord v); rewrite ltnS leq_eqVlt; case/orP=>[/eqP Ev|Nv]. move: Sl Hpl; rewrite Eh Ev Epr mul1g => Sl Hpl. rewrite slice_xR; last by rewrite bnd_simp leEnat; move: Hvl; rewrite Ev. rewrite {22}(_ : n = (ord_max : 'I_n.+1)) // onth_codom /= sorted_rconsE //=. - move: Sl; rewrite slice_oPR /order.Order.lt/= lt0n -{1}Ev Nv0. + move: Sl; rewrite slice_oPR /Order.lt/= lt0n -{1}Ev Nv0. move=>->; rewrite andbT; move: Al; rewrite Ev. have ->: pffun (pl * p) f ord_max = pffun p f ord_max. - rewrite !ffunE permM (out_perm Hpl) // inE negb_and -!ltnNge /=. @@ -569,7 +566,7 @@ apply/and5P; split=>//. apply/ordW; move/allP: Ah=>/(_ y); apply. move: Hy; congr (_ = _); move: y; apply: perm_mem. by rewrite pffunEM; apply: perm_on_fgraph. -- by rewrite slice_oPR /order.Order.lt/= lt0n Nv0 in Sl. +- by rewrite slice_oPR /Order.lt/= lt0n Nv0 in Sl. have HS: subpred (ord (pffun p f v)) (oleq (pffun p f v)). - by move=>z /ordW. move/(sub_all HS): Ah; congr (_ = _); apply/esym/perm_all. From 83a0ae8e225ac66303e0e05bb9a5e736591bd448 Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Mon, 5 May 2025 16:22:04 +0200 Subject: [PATCH 2/2] updating coq and mathcomp versions --- coq-htt-core.opam | 2 +- coq-htt.opam | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/coq-htt-core.opam b/coq-htt-core.opam index 8182418..b856b31 100644 --- a/coq-htt-core.opam +++ b/coq-htt-core.opam @@ -36,7 +36,7 @@ install: [make "-C" "htt" "install"] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "9.1~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } diff --git a/coq-htt.opam b/coq-htt.opam index 4265e46..bb0c93a 100644 --- a/coq-htt.opam +++ b/coq-htt.opam @@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"] install: [make "-C" "examples" "install"] depends: [ "dune" {>= "3.6"} - "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq" { (>= "8.19" & < "9.1~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }