Port to derive.param2 of Coq-Elpi

Author: pi8027

README.md

@@ -47,8 +47,8 @@ slices in the input.
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
 - Compatible Rocq/Coq versions: 8.19 or later
 - Additional dependencies:
+  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi)
   - [MathComp](https://math-comp.github.io) ssreflect 2.3.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 `icfp25/`)
   - [Equations](https://github.com/mattam82/Coq-Equations) (required only for `icfp25/`)
 - Rocq/Coq namespace: `stablesort`

icfp25/Section3.v

@@ -12,26 +12,26 @@
 (* 3.4.3.                                                                     *)
 (******************************************************************************)
 
+From elpi Require Export derive.param2.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import zify.
-From Param Require Export Param.
 From Equations Require Import Equations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Global Ltac destruct_reflexivity :=
-  intros; repeat match goal with
-  | [ x : _ |- _ = _ ] => destruct x; reflexivity; fail
-  end.
-
-Global Parametricity Tactic := destruct_reflexivity.
-
-Parametricity bool.
-Parametricity nat.
-Parametricity list.
-Parametricity merge.
+Elpi derive.param2 bool.
+Elpi derive.param2 nat.
+Elpi derive.param2 list.
+Elpi derive.param2 pred.
+Elpi derive.param2 rel.
+Elpi derive.param2 merge.
+Elpi derive.param2 size.
+Elpi derive.param2 take.
+Elpi derive.param2 drop.
+Elpi derive.param2 foldr.
+Elpi derive.param2 map.
 
 Local Lemma bool_R_refl b1 b2 : b1 = b2 -> bool_R b1 b2.
 Proof. by case: b1 => <-; constructor. Qed.
@@ -44,6 +44,22 @@ Local Lemma rel_map_map A B (f : A -> B) (l : seq A) (fl : seq B) :
   list_R (fun x y => f x = y) l fl -> fl = map f l.
 Proof. by elim/list_R_ind: l fl / => //= ? ? <- ? ? _ ->. 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.
+
+Elpi derive.param2 half'.
+
 (******************************************************************************)
 (* Section 3.2: Characterization of stable non-tail-recursive mergesort       *)
 (* functions                                                                  *)
@@ -73,8 +89,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                                                        *)
@@ -132,7 +148,7 @@ Definition sort T R (merge : R -> R -> R) (singleton : T -> R) (empty : R) :=
   foldr (fun x => merge (singleton x)) empty.
 
 (* Its parametricity *)
-Parametricity sort.
+Elpi derive.param2 sort.
 
 End Abstract.
 
@@ -172,14 +188,16 @@ Equations sort_rec (xs : seq T) (fuel : nat) : R by struct fuel :=
   sort_rec [:: x] _   => singleton x;
   sort_rec xs fuel.+1 =>
     let k := size xs in
-    merge (sort_rec (take k./2 xs) fuel) (sort_rec (drop k./2 xs) fuel).
+    merge (sort_rec (take (half' k) xs) fuel)
+      (sort_rec (drop (half' k) xs) fuel).
 
 Definition sort (xs : seq T) : R := sort_rec xs (size xs).
 
 End Abstract.
 
 (* Its parametricity *)
-Parametricity sort.
+Elpi derive.param2 sort_rec.
+Elpi derive.param2 sort.
 
 End Abstract.
 
@@ -200,14 +218,19 @@ Definition sort (xs : seq T) : seq T := sort_rec xs (size xs).
 
 (* Equation (1) holds by definition. *)
 Lemma asort_mergeE : Abstract.sort (merge leT) (fun x => [:: x]) [::] =1 sort.
-Proof. by []. Qed.
+Proof.
+rewrite /sort /Abstract.sort => xs; move: (size xs) => n.
+elim: n xs => [|n IHn] [|x [|y xs]] //.
+by simp sort_rec; rewrite /= !half'E !IHn.
+Qed.
 
 (* The proof of Equation (2) in Lemma 3.3 *)
 Lemma asort_catE : Abstract.sort cat (fun x : T => [:: x]) [::] =1 id.
 Proof.
 rewrite /Abstract.sort => xs; move: {-1}(size xs) (leqnn (size xs)) => n.
 elim: n xs => [|n IHn] [|x [|y xs]] //= Hxs; simp sort_rec; cbn zeta.
-rewrite !IHn ?cat_take_drop //= (size_drop, size_take) /=; last case: ifP; lia.
+rewrite !half'E !IHn ?cat_take_drop //= (size_drop, size_take) /=;
+  last case: ifP; lia.
 Qed.
 
 End TopDown.
@@ -246,7 +269,9 @@ Proof. by apply_funelim (merge_pairs xs) => //= ? ? ? ->. Qed.
 End Abstract.
 
 (* Its parametricity *)
-Parametricity sort.
+Elpi derive.param2 merge_pairs.
+Elpi derive.param2 merge_all.
+Elpi derive.param2 sort.
 
 End Abstract.
 

icfp25/Section4_1.v

@@ -10,6 +10,11 @@ From mathcomp Require Import zify.
 From stablesort Require Import param stablesort.
 From Equations Require Import Equations.
 
+Elpi derive.param2 fst.
+Elpi derive.param2 size.
+Elpi derive.param2 Nat.sub.
+Elpi derive.param2 subn.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -18,6 +23,22 @@ 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.
+
+Elpi derive.param2 half'.
+
 Section Revmerge.
 
 Context (T : Type) (leT : rel T).
@@ -60,7 +81,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'').
@@ -71,7 +92,8 @@ Definition sort (xs : seq T) : R :=
 
 End Abstract.
 
-Parametricity sort.
+Elpi derive.param2 sort_rec.
+Elpi derive.param2 sort.
 
 End Abstract.
 
@@ -114,7 +136,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.
@@ -134,7 +156,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.
 

meta.yml

@@ -78,16 +78,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: '{>= "2.3.0"}'
   description: |-
     [MathComp](https://math-comp.github.io) ssreflect 2.3.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}'

rocq-stablesort.opam

@@ -41,8 +41,8 @@ run-test: [make "-j%{jobs}%" "build-icfp25"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.19"}
+  "coq-elpi" 
   "coq-mathcomp-ssreflect" {>= "2.3.0"}
-  "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-zify" {with-test}
   "coq-equations" {with-test}
 ]

theories/param.v

@@ -1,33 +1,25 @@
+From elpi 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 unit.
+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.