Skip to content

updating coq and mathcomp versions #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
aleksnanevski wants to merge 2 commits into from
Closed

updating coq and mathcomp versions #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
98db2ba
Adapt to https://github.com/math-comp/math-comp/pull/1169#52
aleksnanevski May 5, 2025
83a0ae8
updating coq and mathcomp versions
aleksnanevski May 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion coq-htt-core.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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") }
Expand Down
4 changes: 2 additions & 2 deletions coq-htt.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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") }
Expand Down
15 changes: 7 additions & 8 deletions examples/bubblesort.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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)).
Expand Down
17 changes: 7 additions & 10 deletions examples/quicksort.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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)) //=.
Expand Down Expand Up @@ -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 /=.
Expand Down Expand Up @@ -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.
Expand Down