Algorithm for populating Trocq database for inductives

.github/workflows/nix-action-rocq-9.0.yml

@@ -171,6 +171,60 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-9.0" --argstr job "rocq-core"
+  rocq-elpi:
+    needs: []
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v6
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{ github.event.repository.html_url
+        }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n  mergeable=$(git
+        merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
+        2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n  if [ -z \"$merge_commit\"\
+        \ -o \"x$mergeable\" != \"x0\" ]; then\n    echo \"tested_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\n  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
+        \  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v6
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v31
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v16
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, math-comp
+        name: coq-community
+    - id: stepGetDerivation
+      name: Getting derivation for current job (rocq-elpi)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"rocq-9.0\" --argstr job \"rocq-elpi\" \\\n   --dry-run 2> err > out || (touch
+        fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
+        failed\"; exit 1; fi\n"
+    - id: stepCheck
+      name: Checking presence of CI target for current job
+      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
+        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
+        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
+        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
+        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-9.0" --argstr job "rocq-elpi"
   trocq:
     needs:
     - trocq-std
@@ -499,10 +553,6 @@ jobs:
       name: 'Building/fetching previous CI target: trocq-std'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-9.0" --argstr job "trocq-std"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-9.0" --argstr job "mathcomp-ssreflect"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-algebra'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 

.github/workflows/nix-action-rocq-9.1.yml

@@ -230,6 +230,60 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-9.1" --argstr job "rocq-core"
+  rocq-elpi:
+    needs: []
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v6
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{
+        github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{ github.event.repository.html_url
+        }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n  mergeable=$(git
+        merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
+        2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n  if [ -z \"$merge_commit\"\
+        \ -o \"x$mergeable\" != \"x0\" ]; then\n    echo \"tested_commit=${{ github.event.pull_request.head.sha
+        }}\" >> $GITHUB_ENV\n  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
+        \  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v6
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v31
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v16
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, math-comp
+        name: coq-community
+    - id: stepGetDerivation
+      name: Getting derivation for current job (rocq-elpi)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"rocq-9.1\" --argstr job \"rocq-elpi\" \\\n   --dry-run 2> err > out || (touch
+        fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
+        failed\"; exit 1; fi\n"
+    - id: stepCheck
+      name: Checking presence of CI target for current job
+      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
+        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
+        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
+        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
+        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-9.1" --argstr job "rocq-elpi"
   trocq:
     needs:
     - trocq-std
@@ -559,10 +613,6 @@ jobs:
       name: 'Building/fetching previous CI target: trocq-std'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-9.1" --argstr job "trocq-std"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-9.1" --argstr job "mathcomp-ssreflect"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-algebra'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 

.nix/config.nix

@@ -15,14 +15,23 @@
     };
   in {
     "rocq-9.0" = {
-      rocqPackages = { rocq-core.override.version = "9.0"; };
-      coqPackages = common-bundles // { coq.override.version = "9.0"; };
+      rocqPackages = { rocq-core.override.version = "9.0"; 
+        rocq-elpi.override.version = "ba3cc750eda486c85d94e3eb35fb0eba77609338"; # 3.4.0. is enough for trocq-std, trocq-hott needs https://github.com/LPCIC/coq-elpi/pull/1030
+	};
+      coqPackages = common-bundles // { 
+        coq.override.version = "9.0"; 
+        coq-elpi.override.version = "ba3cc750eda486c85d94e3eb35fb0eba77609338"; # 3.4.0. is enough for trocq-std, trocq-hott needs https://github.com/LPCIC/coq-elpi/pull/1030
+      };
     };
     "rocq-9.1" = {
-      rocqPackages = { rocq-core.override.version = "9.1"; };
+      rocqPackages = { rocq-core.override.version = "9.1"; 
+        rocq-elpi.override.version = "ba3cc750eda486c85d94e3eb35fb0eba77609338"; # 3.4.0. is enough for trocq-std, trocq-hott needs https://github.com/LPCIC/coq-elpi/pull/1030
+	};
       coqPackages = common-bundles // {
         coq.override.version = "9.1";
         HoTT.override.version = "9dbe413246b53352d4891efb85cd2ea1a8d01c12"; # HoTT isn't available yet for 9.1
+        coq-elpi.override.version = "ba3cc750eda486c85d94e3eb35fb0eba77609338"; # 3.4.0. is enough for trocq-std, trocq-hott needs https://github.com/LPCIC/coq-elpi/pull/1030
+
       };
     };
     ## Trocq is broken on Rocq-master

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"32b164eef0752f2e0d2b57feaba9933a1ec590fb"
+"dd198b999f8526670a6f71a28bc1ea6ef7393cc5"

.nix/coq-overlays/trocq-std-examples/default.nix

@@ -40,7 +40,6 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [
     trocq.std
-    mathcomp.ssreflect
     mathcomp.algebra
   ];
 }

coq-trocq-dev.opam

@@ -38,7 +38,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.20" & < "9.2"}
-  "coq-elpi" {>= "2.5.2"}
+  "coq-elpi" {>= "3.4.0"}
   "coq-hott"
   "coq-mathcomp-algebra"
 ]

coq-trocq-hott.opam

@@ -41,7 +41,7 @@ build: [make "-j%{jobs}%" "hott"]
 install: [make "install" "-C" "hott"]
 depends: [
   "coq" {>= "8.20" & < "9.1"}
-  "coq-elpi" {= "2.5.2"}
+  "coq-elpi" {>= "3.4.0"}
   "coq-hott"
 ]
 

coq-trocq.opam

@@ -41,7 +41,7 @@ build: [make "-j%{jobs}%" "std"]
 install: [make "install" "-C" "std"]
 depends: [
   "coq" {>= "9.0" & < "9.2"}
-  "coq-elpi" {>= "2.5.2"}
+  "coq-elpi" {>= "3.4.0"}
 ]
 
 tags: [

elpi/database.elpi

@@ -23,6 +23,21 @@ pred map->class o:map-class, o:gref.
 % Given the class M, obtain {{indc_mapM}}
 pred map-class->indc-class o:map-class, o:gref.
 
+% Given an inductive I and class M, obtain a proof that M has [|I|]
+pred map-ind i:term, i:map-class, o:term.
+% Dispatcher of the above for universe polymorphic definitions.
+pred map-def i:gref, i:map-class, o:gref.
+
+% Given an inductive I and class M, checks if M has [|I|] has been derived
+pred map-ind-done o:inductive.
+
+% Given an inductive I and ParamNM, obtain a proof that
+% given Tys1 NM related Tys2 then I Tys2 is NM related to I Tys2
+pred param-ind i:term, i:param-class, o:term.
+
+% Given an inductive and class M, checks if M has [|I|] has been derived
+pred param-ind-done o:inductive.
+
 % Given the class M, obtain {{Id_MapM}}
 pred id-map o:map-class, o:constant.
 

elpi/inductives/Rm.elpi

@@ -0,0 +1,167 @@
+accumulate "Trocq.Elpi.inductives/common_algo".
+accumulate "Trocq.Elpi.inductives/utils".
+
+shorten derive.common-algo.{mk-mR-type-Rm}.
+shorten derive.algo-utils.{mk-chain, type-of-args, elim-into-path-suffix}.
+shorten derive.algo-utils.{cmp-indt}.
+
+namespace derive.Rm {
+
+pred whds i:term, o:term.
+whds T R :-
+  whd T [] HD ARGS,
+  unwind HD ARGS R.
+
+pred build-Rm-args i:list term, i:list term, i:term, o:term.
+build-Rm-args [] _ T T.
+build-Rm-args [A1|Args1] [A2|Args2] T R :-
+  ar-db A1 A2 AR,
+  coq.mk-app T [A1, A2, AR] TAR,
+  build-Rm-args Args1 Args2 TAR R.
+
+pred build-Rm i:term, i:term, o:term.
+build-Rm STy ITyTy R :-
+  cmp-indt STy ITyTy SInd Ind,
+  coq.safe-dest-app STy _ Args1,
+  coq.safe-dest-app ITyTy _ Args2,
+  rm-db SInd _ RM,
+  if (Ind = SInd)
+    (R = RM)
+    (build-Rm-args Args1 Args2 RM RSkel,
+     (@keepunivs! => coq.elaborate-skeleton RSkel _ R ok)).
+
+pred mk-equalities i:list term, i:term, i: list term, i: list term, o:list term.
+mk-equalities [] _ [] [] [].
+mk-equalities [STy| SrcTys] ITyTy [_|Sargs] [DA|Dargs] [R|RS] :-
+  paramR A DA AR,
+  build-Rm STy ITyTy RM,
+  coq.mk-app RM [A, DA, AR] R,
+  mk-equalities SrcTys ITyTy Sargs Dargs RS.
+
+% Ksource, Kdest, remaining args, number of type args, KRTy, Type of args Ksource, Type of args KDest, Goal,
+pred process-args i:term, i:term, i:int, i:int, i:term, i:term, i:list term, i:list term, i:term, o:term.
+process-args Ksrc Kdest 0 TyArgsNo _ Goal TySrc TyDest ITyTy R:-
+  coq.mk-app Goal [Ksrc, Kdest, {{ Type }}] EqTy, %discards the relation between Ksrc and Kdest, we want the equality.
+  % todo: change elpi.eq for trocq.idpath
+  whd EqTy [] {{lib:@trocq.paths }} [ITyTy,MapA,B],
+  whd MapA [] K TySrcMappedArgs,
+  coq.env.global (indc _) K, !,
+  whd B [] KDest TyDestArgs,
+  std.drop TyArgsNo TySrcMappedArgs SrcArgs,
+  std.drop TyArgsNo TyDestArgs DestArgs,
+  coq.mk-app KDest {std.take TyArgsNo TyDestArgs} KAppTyArgs,
+  mk-equalities TySrc ITyTy SrcArgs DestArgs Eqs,
+  mk-chain SrcArgs DestArgs TyDest KAppTyArgs Eqs ITyTy B R.
+process-args Ksrc Kdest N TyArgsNo (prod AN1 A1Ty a1\ prod AN2 A2Ty a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) Goal TySrc TyDest ITyTy
+                                   (fun AN1 A1Ty a1\ fun AN2 A2Ty a2\ fun ARN (ARTy a1 a2) ar\ (RF a1 a2 ar)):-
+  M is N - 1,
+  @pi-decl AN1 A1Ty a1\
+  @pi-decl AN2 A2Ty a2\
+  @pi-decl ARN (ARTy a1 a2) ar\
+    coq.mk-app Ksrc [a1] (NewKS a1),
+    coq.mk-app Kdest [a2] (NewKD a2),
+    (paramR a1 a2 ar =!=>
+    process-args (NewKS a1) (NewKD a2) M TyArgsNo (Bo a1 a2 ar) Goal TySrc TyDest ITyTy (R a1 a2 ar)),
+    % if the type of the argument is an instance of the inductive type add an induction hypothesis
+    cmp-indt A2Ty ITyTy IndD Ind,
+    if (Ind = IndD)
+       (coq.mk-app Goal [a1, a2, ar] (EqTy a1 a2 ar),
+        (RF a1 a2 ar) = fun `e` (EqTy a1 a2 ar) e\ (R a1 a2 ar))
+        (RF = R).
+
+% invariant: all type arguments were already processed.
+% Constructor src, Constructor dest, Constructor dest Type, No of Arguments to process,
+% constructorR Type, type of i2, something of type : i1 i2 iR => goal.
+pred mkBranch i:term, i:term, i:int, i:term, i:term, i:term, o:term.
+mkBranch KS KD N KTyR ITyTy Goal Eq:-
+  type-of-args KTyR N SrcArgs DestArgs,
+  whd ITyTy [] _ TyArgs,
+  process-args KS KD N {std.length TyArgs} KTyR Goal SrcArgs DestArgs ITyTy Eq.
+
+pred mkBranches i:list term, i:list term, i:list term, i:list term, i:term, i:term o:list term.
+mkBranches [] [] [] [] _ _ [].
+mkBranches [KS|KsS] [KD|KsD] [KTy|KTys] [KTyR|KTyRs] ITyTy Goal [R|Rs] :-
+  mkBranch KS KD {coq.count-prods KTy} KTyR ITyTy Goal R,
+  mkBranches KsS KsD KTys KTyRs ITyTy Goal Rs.
+
+pred implement-Rm i:int, i:int, i:term, i:list term, i:list term, i:list term, i:list term, i:term, i:term, o:term.
+% Pred comes with Type parameters applied
+% RInd comes with Type parameters applied
+implement-Rm 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) ar\ (Bo i1 i2 ar)) KsS KsD KTys KTyRs Pred RInd
+            (fix `f` 2 RT f\ fun IN1 ITy1 i1\ fun IN2 ITy2 i2\ fun ARN (ARTy i1 i2) ar\ (R f i1 i2 ar)) :-
+  coq.safe-dest-app ITy2 Ind _,
+  coq.env.global (indt GR) Ind,
+  coq.env.recursive? GR, !,
+  RT = (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) ar\ (Bo i1 i2 ar)),
+  coq.mk-app RInd [Pred] RIndP,
+  @pi-decl `f` RT f\
+  @pi-decl IN1 ITy1 i1\
+  @pi-decl IN2 ITy2 i2\
+  @pi-decl ARN (ARTy i1 i2) ar\
+    (rm-db Ind Ind f =>
+      mkBranches KsS KsD KTys KTyRs ITy2 Pred (Brs f)),
+    std.append (Brs f) [i1,i2,ar] (IndArgs f i1 i2 ar),
+    coq.mk-app RIndP (IndArgs f i1 i2 ar) (R f i1 i2 ar).
+implement-Rm 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) _) KsS KsD KTys KTyRs Pred RInd
+            (fun IN1 ITy1 i1\ fun IN2 ITy2 i2\ fun ARN (ARTy i1 i2) ar\ (R i1 i2 ar)) :-
+  coq.mk-app RInd [Pred] RIndP, !,
+  @pi-decl IN1 ITy1 i1\
+  @pi-decl IN2 ITy2 i2\
+  @pi-decl ARN (ARTy i1 i2) ar\
+    mkBranches KsS KsD KTys KTyRs ITy2 Pred Brs,
+    std.append Brs [i1,i2,ar] (IndArgs i1 i2 ar),
+    coq.mk-app RIndP (IndArgs i1 i2 ar) (R i1 i2 ar).
+implement-Rm N TyParamNo (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ prod AMN (AMTy a1 a2 ar) am\ (Bo a1 a2 ar am)) KsS KsD KTys KTyRs Pred RInd
+            (fun AN1 ATy1 a1\ fun AN2 ATy2 a2\ fun ARN (ARTy a1 a2) ar\ fun AMN (AMTy a1 a2 ar) am\ (R a1 a2 ar am)) :-
+  M is N - 1,
+  @pi-decl AN1 ATy1 a1\ %A1 : Type
+  @pi-decl AN2 ATy2 a2\ %A2 : Type
+  @pi-decl ARN (ARTy a1 a2) ar\ % AR : Param2b0.Rel A1 A2 Changing into A1 -> A2 -> Type
+  @pi-decl AMN (AMTy a1 a2 ar) am\ % Map2b.Has AR
+
+    coq.mk-app Pred [a1,a2,ar,am] (NewPred a1 a2 ar am),
+    coq.mk-app RInd [a1,a2,ar] (NewRIndSkel a1 a2 ar),
+    (@keepunivs! => coq.elaborate-skeleton (NewRIndSkel a1 a2 ar) _ (NewRInd a1 a2 ar) ok),
+
+    std.map KsS (x\ r\ sigma TMP\ coq.mk-app x [a1] TMP, r = TMP) (NewKsS a1),
+    std.map KsD (x\ r\ sigma TMP\ coq.mk-app x [a2] TMP, r = TMP) (NewKsD a2),
+    std.map KTys (x\ r\ sigma TMP\ coq.subst-prod [a2] x TMP, r = TMP) (NewKTys a2),
+    std.map KTyRs (x\ r\ sigma TMP1\ coq.subst-prod [a1,a2,ar] x TMP1, r = TMP1) (NewKTyRs a1 a2 ar),
+    %todo: fixme use of universes
+    coq.env.global {{:gref lib:trocq.map2b.r_in_map }} Rm,
+    coq.mk-app Rm [a1, a2, ar, am] (RMS a1 a2 ar am),
+    ar-db a1 a2 ar ==>
+    rm-db a1 a2 (RMS a1 a2 ar am) ==>
+    implement-Rm M TyParamNo (Bo a1 a2 ar am) (NewKsS a1) (NewKsD a2) (NewKTys a2) (NewKTyRs a1 a2 ar) (NewPred a1 a2 ar am) (NewRInd a1 a2 ar) (R a1 a2 ar am).
+
+
+func main inductive, string -> list prop.
+main GR Prefix Clauses :- std.do! [
+
+  coq.env.indt GR _ TyParamNo _ _ KNs KTys,
+  coq.env.global (indt GR) Ind,
+  std.assert! (paramR Ind Ind TR) "derive.Rm: use derive.param2 before",
+  coq.typecheck TR TRTy ok,
+  std.assert! (mymap-def (indt GR) IndMapGR) "derive.Rm: use derive.mymap before",
+  mk-mR-type-Rm TyParamNo TRTy {coq.env.global IndMapGR} {{ Type }} TR MRTy,
+  (@keepunivs! => std.assert-ok! (coq.elaborate-skeleton MRTy _ MRTyE) "derive.Rm generates illtyped type"),
+  coq.env.global (indt GRR) TR,
+  coq.gref->id (indt GRR) Rname,
+  elim-into-path-suffix Rname Suff,
+  RInductionName is Rname ^ Suff,
+  coq.locate RInductionName RInd,
+  coq.prod->fun MRTyE Pred,
+  coq.env.indt GRR _ _ _ _ _ KTyRs,
+  std.map KNs (x\ r\ r = {coq.env.global (indc x)}) Ks,
+  implement-Rm TyParamNo TyParamNo MRTyE Ks Ks KTys KTyRs Pred {coq.env.global RInd} R,
+  std.assert-ok! (coq.elaborate-skeleton R TyE Re) "derive.Rm generates illtyped term",
+  Name is Prefix ^ "Rm",
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName Re TyE _ C,
+  Clauses = [rm-done GR, rm-def (indt GR) (const C)],
+  std.forall Clauses (x\
+    coq.elpi.accumulate _ "derive.Rm.db" (clause _ _ x)
+  ),
+].
+
+}