Port to derive.param2 of Coq-Elpi

Author: pi8027

README.md

@@ -59,8 +59,8 @@ slices in the input.
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
 - Compatible Coq versions: 8.13 or later
 - Additional dependencies:
+  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi)
   - [MathComp](https://math-comp.github.io) 1.13.0 or later
-  - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
   - [Mczify](https://github.com/math-comp/mczify) (required only for the test suite)
   - [Equations](https://github.com/mattam82/Coq-Equations) (required only for the test suite)
 - Coq namespace: `stablesort`

coq-stablesort.opam

@@ -58,8 +58,8 @@ run-test: [ [make "-j%{jobs}%" "build-misc" ] { coq:version < "8.17~" | "8.18~"
 install: [make "install"]
 depends: [
   "coq" {>= "8.13"}
+  "coq-elpi" 
   "coq-mathcomp-ssreflect" {>= "1.13.0"}
-  "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-zify" {with-test}
   "coq-equations" {with-test}
 ]

meta.yml

@@ -169,16 +169,15 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
+- opam:
+    name: coq-elpi
+  description: |-
+    [Coq-Elpi](https://github.com/LPCIC/coq-elpi)
 - opam:
     name: coq-mathcomp-ssreflect
     version: '{>= "1.13.0"}'
   description: |-
     [MathComp](https://math-comp.github.io) 1.13.0 or later
-- opam:
-    name: coq-paramcoq
-    version: '{>= "1.1.3"}'
-  description: |-
-    [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
     name: coq-mathcomp-zify
     version: '{with-test}'

misc/topdown_tailrec.v

@@ -13,6 +13,20 @@ Lemma if_nilp (T S : Type) (s : seq T) (x y : S) :
   (if nilp s then x else y) = if s is [::] then x else y.
 Proof. by case: s. Qed.
 
+(* We define a non-mutual-fixpoint alternative of ssrnat.half, so that        *)
+(* derive.param2 accepts it.                                                  *)
+Fixpoint half' (n : nat) : nat :=
+  match n with
+  | n.+2 => (half' n).+1
+  | _ => 0
+  end.
+
+Lemma half'E : half' =1 half.
+Proof.
+move=> n; have [m ltnm] := ubnP n.
+by elim: m n ltnm => // m IHm [|[|n]] //= /ltnW /IHm ->.
+Qed.
+
 Section Revmerge.
 
 Context (T : Type) (leT : rel T).
@@ -55,7 +69,7 @@ Equations sort_rec (xs : seq T) (b : bool) (n fuel : nat) :
   (* end absurd cases *)
   sort_rec (x :: xs) _ 1 _ => (singleton x, xs);
   sort_rec xs b n fuel.+1 =>
-    let n1 := n./2 in
+    let n1 := half' n in
     let (s1, xs') := sort_rec xs (~~ b) n1 fuel in
     let (s2, xs'') := sort_rec xs' (~~ b) (n - n1) fuel in
     ((if b then merge' s1 s2 else merge s1 s2), xs'').
@@ -66,7 +80,13 @@ Definition sort (xs : seq T) : R :=
 
 End Abstract.
 
-Parametricity sort.
+Elpi derive.param2 size.
+Elpi derive.param2 fst.
+Elpi derive.param2 half'.
+Elpi derive.param2 Nat.sub.
+Elpi derive.param2 subn.
+Elpi derive.param2 sort_rec.
+Elpi derive.param2 sort.
 
 End Abstract.
 
@@ -109,7 +129,7 @@ rewrite {}/rhs; move: {2 4}(size xs) => fuel.
 apply_funelim (sort_rec xs true (size xs) fuel);
   try by move=> *; case: (b in condrev b).
 move=> x {}xs b n {}fuel IHl IHr.
-rewrite Abstract.sort_rec_equation_5 /= {}IHl /= {IHr}(IHr [::]) /=.
+rewrite Abstract.sort_rec_equation_5 /= !half'E {}IHl /= {IHr}(IHr [::]) /=.
 case: (sort_rec (x :: xs)) => s1 xs' /=; case: sort_rec => s2 xs'' /=.
 by rewrite !revmergeE /condrev; case: b; rewrite /= !revK.
 Qed.
@@ -129,7 +149,7 @@ apply_funelim
 - by [].
 - by move=> x {}xs; rewrite /= take0 drop0.
 move=> x {}xs b n {}fuel IHl IHr; rewrite ltnS => n_lt_fuel.
-rewrite [LHS]/= {}IHl 1?{}(IHr [::]) 1?if_same; try lia.
+rewrite [LHS]/= {}IHl 1?{}(IHr [::]) 1?if_same half'E; try lia.
 rewrite -takeD drop_drop; congr (take _ _, drop _ _); lia.
 Qed.
 

theories/param.v

@@ -1,33 +1,24 @@
+From elpi.apps Require Export derive.param2.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
-From Param Require Export Param.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Ltac destruct_reflexivity := 
-  intros ; repeat match goal with 
-    | [ x : _ |- _ = _ ] => destruct x; reflexivity; fail
-  end.
- 
-Global Parametricity Tactic := ((destruct_reflexivity; fail) || auto).
-
-Parametricity False.
-Parametricity eq.
-Parametricity or.
-Parametricity Acc.
-Parametricity unit.
-Parametricity bool.
-Parametricity option.
-Parametricity prod.
-Parametricity nat.
-Parametricity list.
-Parametricity pred.
-Parametricity rel.
-Parametricity BinNums.positive.
-Parametricity BinNums.N.
-Parametricity merge.
-Parametricity rev.
+Elpi derive.param2 bool.
+Elpi derive.param2 nat.
+Elpi derive.param2 option.
+Elpi derive.param2 prod.
+Elpi derive.param2 list.
+Elpi derive.param2 pred.
+Elpi derive.param2 rel.
+Elpi derive.param2 negb.
+Elpi derive.param2 addb.
+Elpi derive.param2 eqb.
+Elpi derive.param2 merge.
+Elpi derive.param2 catrev.
+Elpi derive.param2 rev.
+Elpi derive.param2 foldr.
 
 Lemma bool_R_refl b1 b2 : b1 = b2 -> bool_R b1 b2.
 Proof. by case: b1 => <-; constructor. Qed.

theories/stablesort.v

@@ -54,8 +54,8 @@ Definition asort_ty :=
     seq T ->                            (* input                              *)
     R.                                  (* output                             *)
 
-Parametricity sort_ty.
-Parametricity asort_ty.
+Elpi derive.param2 sort_ty.
+Elpi derive.param2 asort_ty.
 
 Structure function := Pack {
   (* the sort function                                                        *)
@@ -255,7 +255,7 @@ Definition sort (T R : Type) (leT : rel T)
   (merge merge' : R -> R -> R) (singleton : T -> R) (empty : R) :=
   foldr (fun x => merge (singleton x)) empty.
 
-Parametricity sort.
+Elpi derive.param2 sort.
 
 End Abstract.
 
@@ -350,27 +350,34 @@ Fixpoint sort3rec (stack : seq (option R)) (xs : seq T) : R :=
 Definition sort3 : seq T -> R := sort3rec [::].
 
 Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R :=
-  if xs is y :: xs then
-    sortNrec' (leT x y) stack y xs (singleton x) else pop (singleton x) stack
-with sortNrec' (incr : bool) (stack : seq (option R))
-       (x : T) (xs : seq T) (accu : R) : R :=
+  let fix sortNrec' (incr : bool) (stack : seq (option R))
+        (x : T) (xs : seq T) (accu : R) : R :=
   let accu' := (if incr then merge' else merge) accu (singleton x) in
   if xs is y :: xs then
     if eqb incr (leT x y) then
       sortNrec' incr stack y xs accu' else sortNrec (push accu' stack) y xs
   else
-    pop accu' stack.
+    pop accu' stack
+  in
+  if xs is y :: xs then
+    sortNrec' (leT x y) stack y xs (singleton x) else pop (singleton x) stack.
 
 #[using="All"]
 Definition sortN (xs : seq T) : R :=
   if xs is x :: xs then sortNrec [::] x xs else empty.
 
 End Abstract.
 
-Parametricity sort1.
-Parametricity sort2.
-Parametricity sort3.
-Parametricity sortN.
+Elpi derive.param2 pop.
+Elpi derive.param2 push.
+Elpi derive.param2 sort1rec.
+Elpi derive.param2 sort1.
+Elpi derive.param2 sort2rec.
+Elpi derive.param2 sort2.
+Elpi derive.param2 sort3rec.
+Elpi derive.param2 sort3.
+Elpi derive.param2 sortNrec.
+Elpi derive.param2 sortN.
 
 End Abstract.
 
@@ -512,13 +519,10 @@ case=> // x xs; have [n] := ubnP (size xs).
 rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack [::]).
 elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs].
   by rewrite [LHS]apop_mergeE.
-rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
 have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same.
 move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)).
 elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE.
-  by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP.
-rewrite /Abstract.sortNrec'.
-rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
+  by rewrite apop_mergeE /= incrE mergeEcons; case: ifP.
 rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //.
 by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP.
 Qed.
@@ -564,12 +568,9 @@ case=> // x xs; have [n] := ubnP (size xs).
 rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]).
 elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs];
   first by rewrite [LHS]apop_catE.
-rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
 pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _).
 elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs.
   by rewrite [LHS]apop_catE if_same -catA.
-rewrite /Abstract.sortNrec'.
-rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
 move: (IHxs Hxs y z (rcons rs x)).
 by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->.
 Qed.
@@ -678,29 +679,36 @@ Fixpoint sort3rec (stack : seq (option R)) (xs : seq T) : R :=
 Definition sort3 : seq T -> R := sort3rec [::].
 
 Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R :=
-  if xs is y :: xs then
-    sortNrec' (leT x y) stack y xs (singleton x)
-  else
-    pop false (singleton x) stack
-with sortNrec' (incr : bool) (stack : seq (option R))
-       (x : T) (xs : seq T) (accu : R) : R :=
+  let fix sortNrec' (incr : bool) (stack : seq (option R))
+        (x : T) (xs : seq T) (accu : R) : R :=
   let accu' := (if incr then merge' else merge) accu (singleton x) in
   if xs is y :: xs then
     if eqb incr (leT x y) then
       sortNrec' incr stack y xs accu' else sortNrec (push accu' stack) y xs
   else
-    pop false accu' stack.
+    pop false accu' stack
+  in
+  if xs is y :: xs then
+    sortNrec' (leT x y) stack y xs (singleton x)
+  else
+    pop false (singleton x) stack.
 
 #[using="All"]
 Definition sortN (xs : seq T) : R :=
   if xs is x :: xs then sortNrec [::] x xs else empty.
 
 End Abstract.
 
-Parametricity sort1.
-Parametricity sort2.
-Parametricity sort3.
-Parametricity sortN.
+Elpi derive.param2 pop.
+Elpi derive.param2 push.
+Elpi derive.param2 sort1rec.
+Elpi derive.param2 sort1.
+Elpi derive.param2 sort2rec.
+Elpi derive.param2 sort2.
+Elpi derive.param2 sort3rec.
+Elpi derive.param2 sort3.
+Elpi derive.param2 sortNrec.
+Elpi derive.param2 sortN.
 
 End Abstract.
 
@@ -864,13 +872,10 @@ case=> // x xs; have [n] := ubnP (size xs).
 rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack false [::]).
 elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs].
   by rewrite [LHS]apop_mergeE.
-rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
 have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same.
 move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)).
 elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE.
-  by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP.
-rewrite /Abstract.sortNrec'.
-rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
+  by rewrite apop_mergeE /= incrE mergeEcons; case: ifP.
 rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //.
 by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP.
 Qed.
@@ -923,12 +928,9 @@ case=> // x xs; have [n] := ubnP (size xs).
 rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]).
 elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs];
   first by rewrite [LHS]apop_catE.
-rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _).
 pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _).
 elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs.
   by rewrite [LHS]apop_catE if_same -catA.
-rewrite /Abstract.sortNrec'.
-rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _).
 move: (IHxs Hxs y z (rcons rs x)).
 by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->.
 Qed.