ipartlE (#132)

* ipartlE

.github/workflows/docker-action.yml

@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - '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

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.17-8.19
+- Compatible Coq versions: Coq 8.18-8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

coq-monae.opam

@@ -15,17 +15,17 @@ description: """
 This Coq library contains a hierarchy of monads with their laws used
 in several examples of monadic equational reasoning."""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install_full"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.18" & < "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-mathcomp-analysis" { (>= "1.2.0")}
+  "coq-infotheo" { >= "0.7.2"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }

example_iquicksort.v

@@ -181,8 +181,7 @@ Definition dipartl p i y z x : M (dipartlT y z x) :=
     dassert [pred n | (n.1 <= x + y + z) && (n.2 <= x + y + z)].
 
 Local Open Scope mprog.
-Lemma ipartlE p i n : ipartl p i 0 0 n =
-  fmap (fun x => (dipartlT1 x, dipartlT2 x)) (dipartl p i 0 0 n).
+Lemma ipartlE p i y z x : ipartl p i y z x = (M # sval) (dipartl p i y z x).
 Proof.
 rewrite fmapE /dipartl bindA ipartl_guard bindA; bind_ext => -[a b].
 rewrite bindA; apply: bind_ext_guard => /andP[na nb].
@@ -482,8 +481,7 @@ Proof. by rewrite /iqsort Fix_eq //; exact: iqsort'_Fix. Qed.
 
 Lemma iqsort_cons i (n : nat) : iqsort (i, n.+1) = aget i >>= (fun p =>
   dipartl p i.+1 0 0 n >>= (fun nynz =>
-    let ny := dipartlT1 nynz in
-    let nz := dipartlT2 nynz in
+    let '(ny, nz) := (dipartlT1 nynz, dipartlT2 nynz) in
     aswap i (i + ny) >>
     iqsort (i, ny) >> iqsort (i + ny.+1, nz))).
 Proof. by rewrite [in LHS]/iqsort Fix_eq //=; exact: iqsort'_Fix. Qed.
@@ -553,9 +551,10 @@ apply: (@refin_trans _ _ p1).
     apply: refin_bindl => -[].
     rewrite /= iqsort_cons.
     rewrite bindA; apply: refin_bindl => x.
-    rewrite ipartlE /= fmapE [in X in _ `<=` X]bindA.
+    rewrite [in X in _ `<=` X]ipartlE fmapE [in X in _ `<=` X]bindA.
+    rewrite -/(dipartlT 0 0 (size xs)).
     under [in X in _ `<=` X]eq_bind do rewrite bindretf.
-    exact: refin_refl.
+    by apply: refin_bindl => /= -[[n1 n2]/= n1n2]; exact: refin_refl.
   + apply: refin_bindl => -[ys sz].
     rewrite 4!bindA.
     apply: refin_bindl => -[].

meta.yml

@@ -35,12 +35,10 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.17-8.19
-  opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
+  text: Coq 8.18-8.19
+  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'