Skip to content

Commit b5189b9

Browse files
pi8027pi8027
authored
Merge pull request #18 from pi8027/fix-simpl-mutual-rec
Remove workaround for rocq-prover/rocq#3488
2 parents f01766c + 5552dd3 commit b5189b9

File tree

5 files changed

+9
-131
lines changed

5 files changed

+9
-131
lines changed

‎.github/workflows/docker-action.yml‎

Lines changed: 0 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -17,45 +17,9 @@ jobs:
1717
strategy:
1818
matrix:
1919
image:
20-
- 'mathcomp/mathcomp:1.13.0-coq-8.13'
21-
- 'mathcomp/mathcomp:1.13.0-coq-8.14'
22-
- 'mathcomp/mathcomp:1.13.0-coq-8.15'
23-
- 'mathcomp/mathcomp:1.14.0-coq-8.13'
24-
- 'mathcomp/mathcomp:1.14.0-coq-8.14'
25-
- 'mathcomp/mathcomp:1.14.0-coq-8.15'
26-
- 'mathcomp/mathcomp:1.15.0-coq-8.13'
27-
- 'mathcomp/mathcomp:1.15.0-coq-8.14'
28-
- 'mathcomp/mathcomp:1.15.0-coq-8.15'
29-
- 'mathcomp/mathcomp:1.15.0-coq-8.16'
30-
- 'mathcomp/mathcomp:1.16.0-coq-8.13'
31-
- 'mathcomp/mathcomp:1.16.0-coq-8.14'
32-
- 'mathcomp/mathcomp:1.16.0-coq-8.15'
33-
- 'mathcomp/mathcomp:1.16.0-coq-8.16'
34-
- 'mathcomp/mathcomp:1.16.0-coq-8.17'
35-
- 'mathcomp/mathcomp:1.16.0-coq-8.18'
36-
- 'mathcomp/mathcomp:1.17.0-coq-8.15'
37-
- 'mathcomp/mathcomp:1.17.0-coq-8.16'
38-
- 'mathcomp/mathcomp:1.17.0-coq-8.17'
39-
- 'mathcomp/mathcomp:1.17.0-coq-8.18'
40-
- 'mathcomp/mathcomp:1.18.0-coq-8.16'
41-
- 'mathcomp/mathcomp:1.18.0-coq-8.17'
42-
- 'mathcomp/mathcomp:1.18.0-coq-8.18'
43-
- 'mathcomp/mathcomp:1.19.0-coq-8.16'
44-
- 'mathcomp/mathcomp:1.19.0-coq-8.17'
45-
- 'mathcomp/mathcomp:1.19.0-coq-8.18'
4620
- 'mathcomp/mathcomp:1.19.0-coq-8.19'
47-
- 'mathcomp/mathcomp:2.0.0-coq-8.16'
48-
- 'mathcomp/mathcomp:2.0.0-coq-8.17'
49-
- 'mathcomp/mathcomp:2.0.0-coq-8.18'
50-
- 'mathcomp/mathcomp:2.1.0-coq-8.16'
51-
- 'mathcomp/mathcomp:2.1.0-coq-8.17'
52-
- 'mathcomp/mathcomp:2.1.0-coq-8.18'
53-
- 'mathcomp/mathcomp:2.2.0-coq-8.16'
54-
- 'mathcomp/mathcomp:2.2.0-coq-8.17'
55-
- 'mathcomp/mathcomp:2.2.0-coq-8.18'
5621
- 'mathcomp/mathcomp:2.2.0-coq-8.19'
5722
- 'mathcomp/mathcomp:2.2.0-coq-8.20'
58-
- 'mathcomp/mathcomp:2.3.0-coq-8.18'
5923
- 'mathcomp/mathcomp:2.3.0-coq-8.19'
6024
- 'mathcomp/mathcomp:2.3.0-coq-8.20'
6125
- 'mathcomp/mathcomp:2.4.0-coq-8.20'

‎README.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,9 @@ slices in the input.
4242
- Kazuhiko Sakaguchi (initial)
4343
- Cyril Cohen
4444
- License: [CeCILL-B Free Software License Agreement](CeCILL-B)
45-
- Compatible Coq versions: 8.13 or later
45+
- Compatible Coq versions: 8.19 or later
4646
- Additional dependencies:
47-
- [MathComp](https://math-comp.github.io) 1.13.0 or later
47+
- [MathComp](https://math-comp.github.io) 1.19.0, 2.2.0, or later
4848
- [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
4949
- [Mczify](https://github.com/math-comp/mczify) (required only for `icfp25/`)
5050
- [Equations](https://github.com/mattam82/Coq-Equations) (required only for `icfp25/`)

‎coq-stablesort.opam‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -37,13 +37,11 @@ In addition, each of the above two kinds of mergesort functions has a smooth
3737
slices in the input."""
3838

3939
build: [make "-j%{jobs}%"]
40-
# The filter below has been added by hand to avoid running the test suite with
41-
# Coq 8.17 or MathComp < 1.15.
42-
run-test: [ [make "-j%{jobs}%" "build-icfp25" ] { "1.16~" <= coq-mathcomp-ssreflect:version & (coq:version < "8.17~" | "8.18~" <= coq:version) } ]
40+
run-test: [make "-j%{jobs}%" "build-icfp25"]
4341
install: [make "install"]
4442
depends: [
45-
"coq" {>= "8.13"}
46-
"coq-mathcomp-ssreflect" {>= "1.13.0"}
43+
"coq" {>= "8.19"}
44+
"coq-mathcomp-ssreflect" {(>= "1.19.0" & < "2.0~") | (>= "2.2.0")}
4745
"coq-paramcoq" {>= "1.1.3"}
4846
"coq-mathcomp-zify" {with-test}
4947
"coq-equations" {with-test}

‎meta.yml‎

Lines changed: 4 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -52,90 +52,18 @@ license:
5252
file: CeCILL-B
5353

5454
supported_coq_versions:
55-
text: 8.13 or later
56-
opam: '{>= "8.13"}'
55+
text: 8.19 or later
56+
opam: '{>= "8.19"}'
5757

5858
tested_coq_nix_versions:
5959

6060
tested_coq_opam_versions:
61-
- version: '1.13.0-coq-8.13'
62-
repo: 'mathcomp/mathcomp'
63-
- version: '1.13.0-coq-8.14'
64-
repo: 'mathcomp/mathcomp'
65-
- version: '1.13.0-coq-8.15'
66-
repo: 'mathcomp/mathcomp'
67-
- version: '1.14.0-coq-8.13'
68-
repo: 'mathcomp/mathcomp'
69-
- version: '1.14.0-coq-8.14'
70-
repo: 'mathcomp/mathcomp'
71-
- version: '1.14.0-coq-8.15'
72-
repo: 'mathcomp/mathcomp'
73-
- version: '1.15.0-coq-8.13'
74-
repo: 'mathcomp/mathcomp'
75-
- version: '1.15.0-coq-8.14'
76-
repo: 'mathcomp/mathcomp'
77-
- version: '1.15.0-coq-8.15'
78-
repo: 'mathcomp/mathcomp'
79-
- version: '1.15.0-coq-8.16'
80-
repo: 'mathcomp/mathcomp'
81-
- version: '1.16.0-coq-8.13'
82-
repo: 'mathcomp/mathcomp'
83-
- version: '1.16.0-coq-8.14'
84-
repo: 'mathcomp/mathcomp'
85-
- version: '1.16.0-coq-8.15'
86-
repo: 'mathcomp/mathcomp'
87-
- version: '1.16.0-coq-8.16'
88-
repo: 'mathcomp/mathcomp'
89-
- version: '1.16.0-coq-8.17'
90-
repo: 'mathcomp/mathcomp'
91-
- version: '1.16.0-coq-8.18'
92-
repo: 'mathcomp/mathcomp'
93-
- version: '1.17.0-coq-8.15'
94-
repo: 'mathcomp/mathcomp'
95-
- version: '1.17.0-coq-8.16'
96-
repo: 'mathcomp/mathcomp'
97-
- version: '1.17.0-coq-8.17'
98-
repo: 'mathcomp/mathcomp'
99-
- version: '1.17.0-coq-8.18'
100-
repo: 'mathcomp/mathcomp'
101-
- version: '1.18.0-coq-8.16'
102-
repo: 'mathcomp/mathcomp'
103-
- version: '1.18.0-coq-8.17'
104-
repo: 'mathcomp/mathcomp'
105-
- version: '1.18.0-coq-8.18'
106-
repo: 'mathcomp/mathcomp'
107-
- version: '1.19.0-coq-8.16'
108-
repo: 'mathcomp/mathcomp'
109-
- version: '1.19.0-coq-8.17'
110-
repo: 'mathcomp/mathcomp'
111-
- version: '1.19.0-coq-8.18'
112-
repo: 'mathcomp/mathcomp'
11361
- version: '1.19.0-coq-8.19'
11462
repo: 'mathcomp/mathcomp'
115-
- version: '2.0.0-coq-8.16'
116-
repo: 'mathcomp/mathcomp'
117-
- version: '2.0.0-coq-8.17'
118-
repo: 'mathcomp/mathcomp'
119-
- version: '2.0.0-coq-8.18'
120-
repo: 'mathcomp/mathcomp'
121-
- version: '2.1.0-coq-8.16'
122-
repo: 'mathcomp/mathcomp'
123-
- version: '2.1.0-coq-8.17'
124-
repo: 'mathcomp/mathcomp'
125-
- version: '2.1.0-coq-8.18'
126-
repo: 'mathcomp/mathcomp'
127-
- version: '2.2.0-coq-8.16'
128-
repo: 'mathcomp/mathcomp'
129-
- version: '2.2.0-coq-8.17'
130-
repo: 'mathcomp/mathcomp'
131-
- version: '2.2.0-coq-8.18'
132-
repo: 'mathcomp/mathcomp'
13363
- version: '2.2.0-coq-8.19'
13464
repo: 'mathcomp/mathcomp'
13565
- version: '2.2.0-coq-8.20'
13666
repo: 'mathcomp/mathcomp'
137-
- version: '2.3.0-coq-8.18'
138-
repo: 'mathcomp/mathcomp'
13967
- version: '2.3.0-coq-8.19'
14068
repo: 'mathcomp/mathcomp'
14169
- version: '2.3.0-coq-8.20'
@@ -156,9 +84,9 @@ tested_coq_opam_versions:
15684
dependencies:
15785
- opam:
15886
name: coq-mathcomp-ssreflect
159-
version: '{>= "1.13.0"}'
87+
version: '{(>= "1.19.0" & < "2.0~") | (>= "2.2.0")}'
16088
description: |-
161-
[MathComp](https://math-comp.github.io) 1.13.0 or later
89+
[MathComp](https://math-comp.github.io) 1.19.0, 2.2.0, or later
16290
- opam:
16391
name: coq-paramcoq
16492
version: '{>= "1.1.3"}'

‎theories/stablesort.v‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -517,13 +517,10 @@ case=> // x xs; have [n] := ubnP (size xs).
517517
rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack [::]).
518518
elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs].
519519
by rewrite [LHS]apop_mergeE.
520-
rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
521520
have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same.
522521
move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)).
523522
elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE.
524523
by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP.
525-
rewrite /Abstract.sortNrec'.
526-
rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
527524
rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //.
528525
by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP.
529526
Qed.
@@ -569,12 +566,9 @@ case=> // x xs; have [n] := ubnP (size xs).
569566
rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]).
570567
elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs];
571568
first by rewrite [LHS]apop_catE.
572-
rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
573569
pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _).
574570
elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs.
575571
by rewrite [LHS]apop_catE if_same -catA.
576-
rewrite /Abstract.sortNrec'.
577-
rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
578572
move: (IHxs Hxs y z (rcons rs x)).
579573
by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->.
580574
Qed.
@@ -869,13 +863,10 @@ case=> // x xs; have [n] := ubnP (size xs).
869863
rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack false [::]).
870864
elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs].
871865
by rewrite [LHS]apop_mergeE.
872-
rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
873866
have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same.
874867
move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)).
875868
elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE.
876869
by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP.
877-
rewrite /Abstract.sortNrec'.
878-
rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
879870
rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //.
880871
by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP.
881872
Qed.
@@ -928,12 +919,9 @@ case=> // x xs; have [n] := ubnP (size xs).
928919
rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]).
929920
elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs];
930921
first by rewrite [LHS]apop_catE.
931-
rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
932922
pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _).
933923
elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs.
934924
by rewrite [LHS]apop_catE if_same -catA.
935-
rewrite /Abstract.sortNrec'.
936-
rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
937925
move: (IHxs Hxs y z (rcons rs x)).
938926
by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->.
939927
Qed.

0 commit comments

Comments
 (0)