diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 2993504f..d3dcf6db 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.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 diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 9ded0a27..368041ae 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.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 diff --git a/.nix/config.nix b/.nix/config.nix index 7eeabbd9..fa46d8fb 100644 --- a/.nix/config.nix +++ b/.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 diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index d1cb4e1d..22ddfe2f 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"32b164eef0752f2e0d2b57feaba9933a1ec590fb" +"dd198b999f8526670a6f71a28bc1ea6ef7393cc5" diff --git a/.nix/coq-overlays/trocq-std-examples/default.nix b/.nix/coq-overlays/trocq-std-examples/default.nix index a6355c4c..fdd3e573 100644 --- a/.nix/coq-overlays/trocq-std-examples/default.nix +++ b/.nix/coq-overlays/trocq-std-examples/default.nix @@ -40,7 +40,6 @@ mkCoqDerivation { propagatedBuildInputs = [ trocq.std - mathcomp.ssreflect mathcomp.algebra ]; } diff --git a/coq-trocq-dev.opam b/coq-trocq-dev.opam index 7c9214c3..f4a76777 100644 --- a/coq-trocq-dev.opam +++ b/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" ] diff --git a/coq-trocq-hott.opam b/coq-trocq-hott.opam index 4e4387b1..7ed38892 100644 --- a/coq-trocq-hott.opam +++ b/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" ] diff --git a/coq-trocq.opam b/coq-trocq.opam index 0262b34f..b7f0fb48 100644 --- a/coq-trocq.opam +++ b/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: [ diff --git a/elpi/database.elpi b/elpi/database.elpi index 4a7c515d..d230c4c9 100644 --- a/elpi/database.elpi +++ b/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. diff --git a/elpi/inductives/Rm.elpi b/elpi/inductives/Rm.elpi new file mode 100644 index 00000000..4335a2ab --- /dev/null +++ b/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) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/RsymK.elpi b/elpi/inductives/RsymK.elpi new file mode 100644 index 00000000..d9ef050a --- /dev/null +++ b/elpi/inductives/RsymK.elpi @@ -0,0 +1,55 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.algo-utils.{type-of-args, whd-fuel, iota-step, invert-eqs, rewrite-with}. +shorten derive.common-algo.{mk-mR-type-rsymK, sym-tyargs}. + +namespace derive.rsymK { + +pred implement-rsymK i:int, i:term, i:term, i:term, i:list term, o:term. +implement-rsymK 0 (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ _) Sym SymK LRev (fun IN1 ITy1 i1\ fun IN2 ITy2 i2\ (R i1 i2)) :- + !, + std.rev LRev L, + sym-tyargs L LSym, + coq.mk-app Sym LSym FSym, + coq.mk-app Sym L GSym, + coq.mk-app SymK LSym SymKSym, + @pi-decl IN1 ITy1 i1\ + @pi-decl IN2 ITy2 i2\ + (F i1 i2) = {{ lp:FSym lp:i2 lp:i1 }}, + (G i1 i2) = {{ lp:GSym lp:i1 lp:i2 }}, + (FGK i1 i2) = {{ lp:SymKSym lp:i2 lp:i1 }}, + (R i1 i2) = {{ lib:trocq.exist _ lp:{{ (F i1 i2) }} (lib:trocq.exist _ lp:{{ (G i1 i2) }} lp:{{ (FGK i1 i2) }}) }}. +implement-rsymK N (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) Sym SymK L + (fun AN1 ATy1 a1\ fun AN2 ATy2 a2\ fun ARN (ARTy a1 a2) ar\ (R a1 a2 ar)) :- + 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 : Param00.Rel A1 A2 + sigma NewL\ + std.append [ar,a2,a1] L NewL, + implement-rsymK M (Bo a1 a2 ar) Sym SymK NewL (R a1 a2 ar). + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + + coq.env.indt GR _ TyParamNo _ _ _ _, + coq.env.global (indt GR) Ind, + std.assert! (param Ind Ind TR) "derive.rsymK: use derive.param2 before", + coq.typecheck TR TRTy ok, + mk-mR-type-rsymK TyParamNo TRTy TR {{ fun (A B : Type) => A <->> B }} SymKTy, + std.assert-ok! (coq.elaborate-skeleton SymKTy _ SymKTyE) "derive.rsymK generates illtyped type", + std.assert! (sym-db Ind SymInd) "derive.rsymK: use derive.sym before", + std.assert! (symK-db Ind SymKInd) "derive.rsymK: use derive.symK before", + implement-rsymK TyParamNo SymKTyE SymInd SymKInd [] R, + std.assert-ok! (coq.elaborate-skeleton R SymKTyE Re) "derive.rsymK generates illtyped term", + Name is Prefix ^ "rsymK", + coq.ensure-fresh-global-id Name FName, + coq.env.add-const FName Re SymKTyE _ C, + Clauses = [rsymK-done GR, rsymK-def (indt GR) (const C)], + std.forall Clauses (x\ + coq.elpi.accumulate _ "derive.rsymK.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/common_algo.elpi b/elpi/inductives/common_algo.elpi new file mode 100644 index 00000000..829dbcf3 --- /dev/null +++ b/elpi/inductives/common_algo.elpi @@ -0,0 +1,192 @@ + +namespace derive.common-algo { + +kind param-surgery type. +type raw param-surgery. +type refine param-surgery. +type subst param-surgery. + +pred rel-mode i:int o:term. +% 0 - 4 could be merged for the change on the type parameters, but they have a different conclusion +rel-mode 0 {{ forall (A B : Type) (AR : A -> B -> Type) (_ : lib:trocq.map1 AR) (Rest : Type), Rest }}. % my-map +rel-mode 1 {{ forall (A B : Type) (AR : A -> B -> Type) (_ : lib:trocq.map2a AR) (Rest : Type), Rest }}. % mR +rel-mode 2 {{ forall (A B : Type) (AR : A -> B -> Type) (_ : lib:trocq.map2b AR) (Rest : Type), Rest }}. % Rm +rel-mode 3 {{ forall (A B : Type) (AR : A -> B -> Type) (_ : lib:trocq.map3 AR) (Rest : Type), Rest }}. % _ +rel-mode 4 {{ forall (A B : Type) (AR : A -> B -> Type) (_ : lib:trocq.map4 AR) (Rest : Type), Rest }}. % mRRmK +% 5 - 7 don't require extra assumption, the only changes happen on the conclusion +rel-mode 5 {{ fun (A B : Type)=> A -> B -> Type }}. % sym +rel-mode 6 {{ fun (A B : Type)=> A -> B -> Type }}. % symK +rel-mode 7 {{ fun (A B : Type)=> A -> B -> Type }}. % rsymK +% substitutes the relation of type (A -> B -> Type) for (AR A B), which is provided on the client side +rel-mode 8 {{ forall (A B : Type) (AR : Type -> Type -> Type), (AR A B) }}. + +pred swap i:term, i:term, i:bool, o:term, o:term. +swap A B tt B A. +swap A B ff A B. + +% Reached a sort, return map L = R -> IR. +pred mk-impl-return i:term, i:term, i:term, i:bool, i:term, o:term. +mk-impl-return ML MR Rel SwapB ITyTy2 R :- + Map = {{ lib:@trocq.paths lp:ITyTy2 lp:ML lp:MR }}, + swap Map Rel SwapB First Second, + R = prod `_` First _\ Second. + +% 1 is mR +% 2 is Rm +% 4 is mRRmK +pred mk-return i:term, i:term, i:term, i:int, i:term, o:term. +mk-return ML MR Rel 1 ITyTy2 R :- + mk-impl-return ML MR Rel ff ITyTy2 R. +mk-return ML MR Rel 2 ITyTy2 R :- + mk-impl-return ML MR Rel tt ITyTy2 R. +% mk-return ML MR Rel + +pred sym-tyargs-priv i: list term, i: list term, o: list term. +sym-tyargs-priv [] L L. +sym-tyargs-priv [A1, A2, AR | L2] Acc R :- + coq.mk-app {{ @sym_rel }} [A1,A2,AR] RAS, + std.append Acc [A2, A1, RAS ] NewAcc, + sym-tyargs-priv L2 NewAcc R. + +pred sym-tyargs i: list term, o: list term. +sym-tyargs L R :- + sym-tyargs-priv L [] R. + +pred clean-l i: list term, o: list term. +clean-l [] []. +clean-l [A1, A2, AR, _ | L2] [A1,A2,AR | R] :- + clean-l L2 R. + +% The number of Type parameters in T +% Type of inductive T, +% Type of bin parametricity translation TR, +% ML LHS of map equality +% MR RHS of map equality +% Rel type of TR applied to arguments +% Returns the type of map in R for T +% Does it add an extra hyp on the relation? +% X is the first inductive, Y is the second inductive. +pred mk-mR-type-priv i:int, i:term, i:term, i:term, i:term, i:int, i:list term, i: term, i: term, i:param-surgery, o:term. +% Introducing X and Y. +% The RHS of the equality is Y. +mk-mR-type-priv 0 (prod IN1 ITyTy x\ prod IN2 ITyTy2 _) ML _ Rel Swap LRev _ _ _ + (prod IN1 ITyTy x\ prod IN2 ITyTy2 y\ (R x y)) :- + (Swap = 1 ; Swap = 2), + @pi-decl IN1 ITyTy x\ + @pi-decl IN2 ITyTy2 y\ + sigma NewML NewMR NewRel L\ + std.rev LRev L, + coq.mk-app ML {std.append L [x]} NewML, + NewMR = y, + clean-l L CL, + coq.mk-app Rel {std.append CL [x,y]} NewRel, + mk-return NewML NewMR NewRel Swap ITyTy2 (R x y). +mk-mR-type-priv 0 (prod IN1 ITyTy x\ prod IN2 ITyTy2 _) _ _ Rel 4 LRev MR RM _ + (prod IN1 ITyTy x\ prod IN2 ITyTy2 y\ prod `IR` (RelTy x y) iR\ (R x y iR)) :- + std.rev LRev L, + @pi-decl IN1 ITyTy x\ + @pi-decl IN2 ITyTy2 y\ + clean-l L CL, + coq.mk-app Rel {std.append CL [x,y]} (RelTy x y), + @pi-decl `IR` (RelTy x y) iR\ + % sigma NewML NewMR NewRel L\ + % whd ITyTy2 [] _ _, + coq.mk-app RM {std.append L [x,y,iR]} (Rm x y iR), + coq.mk-app MR {std.append L [x,y,(Rm x y iR)]} (MRRM x y iR), + (R x y iR) = {{ lib:@trocq.paths _ lp:{{MRRM x y iR}} lp:iR }}. +mk-mR-type-priv 0 (prod IN1 ITyTy x\ prod IN2 ITyTy2 _) _ _ Rel 5 LRev _ _ _ + (prod IN1 ITyTy x\ prod IN2 ITyTy2 y\ (R x y)) :- + std.rev LRev L, + sym-tyargs L L2, + @pi-decl IN1 ITyTy x\ + @pi-decl IN2 ITyTy2 y\ + coq.mk-app Rel {std.append L [x,y]} (RelTy1 x y), + coq.mk-app Rel {std.append L2 [y,x]} (RelTy2 x y), + R x y = {{ lp:{{RelTy1 x y}} -> lp:{{RelTy2 x y}} }}. +mk-mR-type-priv 0 (prod IN1 ITyTy x\ prod IN2 ITyTy2 _) RSym _ Rel 7 LRev _ _ _ + (prod IN1 ITyTy x\ prod IN2 ITyTy2 y\ (R x y)) :- + std.rev LRev L, + sym-tyargs L L2, + @pi-decl IN1 ITyTy x\ + @pi-decl IN2 ITyTy2 y\ + coq.mk-app Rel {std.append L [x,y]} (RelTy1 x y), + coq.mk-app Rel {std.append L2 [y,x]} (RelTy2 x y), + RSkel x y = {{ lp:RSym lp:{{RelTy2 x y}} lp:{{RelTy1 x y}} }}, + whd1 (RSkel x y) (R x y). +mk-mR-type-priv 0 (prod _ ITyTy x\ prod _ ITyTy2 _) _ RelSTy _ 8 _ _ _ _ + R :- + rel-mode 8 ARSkel, + coq.subst-prod [ITyTy, ITyTy2, RelSTy] ARSkel R. +mk-mR-type-priv 0 (prod IN1 ITyTy x\ prod IN2 ITyTy2 _) SymC _ Rel 6 LRev _ _ _ + (prod IN1 ITyTy x\ prod IN2 ITyTy2 y\ prod `IR` (RelTy x y) iR\ (R x y iR)) :- + std.rev LRev L, + sym-tyargs L L2, + @pi-decl IN1 ITyTy x\ + @pi-decl IN2 ITyTy2 y\ + coq.mk-app Rel {std.append L [x,y]} (RelTy x y), + @pi-decl `IR` (RelTy x y) iR\ + % sigma NewML NewMR NewRel L\ + coq.mk-app SymC {std.append L [x,y,iR]} (SymR x y iR), + coq.mk-app SymC {std.append L2 [y,x,(SymR x y iR)]} (SymSym x y iR), + (R x y iR) = {{ lib:@trocq.paths _ lp:{{SymSym x y iR}} lp:iR }}. +% Process two type parameters + 1 relation at a time. +% Apply these parameters to the LHS of the equation. +% This branch deals with adding the additional hypothesis in case the input boolean is set. +mk-mR-type-priv N (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) ML _ Rel Swap L MR RM refine + (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ prod NM (MTy a1 a2 ar) am\ (Rest a1 a2 ar am)) :- + M is N - 1, + rel-mode Swap ARSkel, + coq.name-suffix AN1 "M" NM, + pi a1 a2 ar am\ + sigma NewL\ + std.append [am,ar,a2,a1] L NewL, + mk-mR-type-priv M (Bo a1 a2 ar) ML {{ Type }} Rel Swap NewL MR RM refine (R a1 a2 ar am), + coq.subst-prod [a1, a2, ar] ARSkel (prod _ (MTy a1 a2 ar) _), + coq.subst-prod [a1, a2, ar, am, (R a1 a2 ar am)] ARSkel (Rest a1 a2 ar am). +% This branch deals with the branch when the boolean is unset. +mk-mR-type-priv N (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) ML _ Rel Swap L MR RM raw + (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (R a1 a2 ar)) :- + M is N - 1, + pi a1 a2 ar\ + sigma NewL\ + std.append [ar,a2,a1] L NewL, + mk-mR-type-priv M (Bo a1 a2 ar) ML {{ Type }} Rel Swap NewL MR RM raw (R a1 a2 ar). +mk-mR-type-priv N (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN _ ar\ (Bo a1 a2 ar)) ML RelSTy Rel Swap L MR RM subst + (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (NewARTy a1 a2) ar\ (R a1 a2 ar)) :- + M is N - 1, + rel-mode Swap ARSkel, + pi a1 a2 ar\ + sigma NewL\ + std.append [ar,a2,a1] L NewL, + coq.subst-prod [a1, a2, RelSTy] ARSkel (NewARTy a1 a2), + mk-mR-type-priv M (Bo a1 a2 ar) ML RelSTy Rel Swap NewL MR RM subst (R a1 a2 ar). + +pred mk-mR-type-mR i:int, i:term, i:term, i:term, i:term, o:term. +mk-mR-type-mR N T ML MR Rel RTy :- + mk-mR-type-priv N T ML MR Rel 1 [] _ _ refine RTy. + +pred mk-mR-type-Rm i:int, i:term, i:term, i:term, i:term, o:term. +mk-mR-type-Rm N T ML MR Rel R :- + mk-mR-type-priv N T ML MR Rel 2 [] _ _ refine R. + +pred mk-mR-type-mRRmK i:int, i:term, i:term, i:term, i:term, i: term, o:term. +mk-mR-type-mRRmK N T ML Rel MR RM R :- + mk-mR-type-priv N T ML _ Rel 4 [] MR RM refine R. + +pred mk-mR-type-sym i:int, i:term, i:term, o:term. +mk-mR-type-sym N T Rel R :- + mk-mR-type-priv N T _ _ Rel 5 [] _ _ raw R. + +pred mk-mR-type-symK i:int, i:term, i:term, i:term, o:term. +mk-mR-type-symK N T Rel Sym R :- + mk-mR-type-priv N T Sym _ Rel 6 [] _ _ raw R. + +pred mk-mR-type-rsymK i:int, i:term, i:term, i:term, o:term. +mk-mR-type-rsymK N T Rel RSym R :- + mk-mR-type-priv N T RSym _ Rel 7 [] _ _ raw R. + +pred mk-mR-type-relnm i:int, i:term, i:term, i:term, o:term. +mk-mR-type-relnm N T Rel RelSTy R :- + mk-mR-type-priv N T _ RelSTy Rel 8 [] _ _ subst R. + +} \ No newline at end of file diff --git a/elpi/inductives/injK.elpi b/elpi/inductives/injK.elpi new file mode 100644 index 00000000..d03fa377 --- /dev/null +++ b/elpi/inductives/injK.elpi @@ -0,0 +1,210 @@ +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.algo-utils.{duplicate-arguments,count-args, name-prefix, mk-chain, name-ijs}. + +namespace derive.injK { + +pred add-equalities i:int, i:int, i:term, o:term. +add-equalities 0 0 T T. +add-equalities 0 M (prod AN1 ATy a1\ prod AN2 ATy a2\ (Bo a1 a2)) + (prod AN1 ATy a1\ prod AN2 ATy a2\ prod EN (EqTy a1 a2) e\ (R a1 a2)) :- + O is M - 1, + name-prefix AN1 "p_" EN, + pi a1 a2\ + coq.mk-app {{lib:@trocq.paths}} [ATy, a1, a2] (EqTy a1 a2), + add-equalities 0 O (Bo a1 a2) (R a1 a2). +add-equalities N M (prod AN1 ATy a1\ (Bo a1)) + (prod AN1 ATy a1\ (R a1)) :- + O is N - 1, + pi a1\ + add-equalities O M (Bo a1) (R a1). + +pred get-injectors i:list term, i: list int, o: list (list term), o:list (list int). +get-injectors [] [] [] []. +get-injectors [K|Ks] [ArgNo|ArgNos] [R|RS] [Tmp|Tmps]:- + std.iota ArgNo Tmp, + std.map Tmp (x\r\ sigma Add1\ Add1 is x + 1, r = Add1) Add1, + std.map Add1 (x\r\ sigma R\ injections-db K x R, r = R) R, + get-injectors Ks ArgNos RS Tmps. + +% TyParam, ArgNo, type of duplicated args + eq, injector, dest path no, RHS path (dflt dummy). +% +pred add-concl i:int, i:int, i:int, i:term, i:term, i:int, i:term, i:term, i:list term, i:list term, i: list term, o:term. +add-concl 0 ArgNo ArgNo _ Injtor _ RHS K SrcArgs_R DestArgs_R Eqs_R R :- + % M > ArgNo, + !, + std.rev SrcArgs_R SrcArgs, + std.rev DestArgs_R DestArgs, + std.rev Eqs_R Eqs, + std.map DestArgs (x\r\ sigma R\ coq.typecheck x R ok, r = R) DestArgsTy, + coq.mk-app K DestArgs Ind, + coq.typecheck Ind ITyTy ok, + mk-chain SrcArgs DestArgs DestArgsTy K Eqs ITyTy Ind Chain, + coq.mk-app Injtor [Chain] LHS, + coq.mk-app {{lib:@trocq.paths}} [{{ _ }}, LHS, RHS] RSkel, + @keepunivs! => coq.elaborate-skeleton RSkel _ R ok. +add-concl 0 M ArgNo (prod AN1 ATy a1\ prod AN2 ATy a2\ prod EN (ETy a1 a2) e\ (Bo a1 a2 e)) Injtor DestPathNo RHS K SrcArgs DestArgs Eqs + (prod AN1 ATy a1\ prod AN2 ATy a2\ prod EN (ETy a1 a2) e\ (R a1 a2 e)) :- + !, + O is M + 1, + @pi-decl AN1 ATy a1\ + @pi-decl AN2 ATy a2\ + @pi-decl EN (ETy a1 a2) e\ + coq.mk-app Injtor [a1, a2] (NewInjtor a1 a2), + if (M = DestPathNo) + ((NewRHS e) = e) + ((NewRHS e) = RHS), + add-concl 0 O ArgNo (Bo a1 a2 e) (NewInjtor a1 a2) DestPathNo (NewRHS e) K [a1 | SrcArgs] [a2| DestArgs] [e | Eqs] (R a1 a2 e). + +add-concl N 0 ArgNo (prod AN1 ATy a1\ (Bo a1)) Injtor DestPathNo RHS K SrcArgs DestArgs Eqs + (prod AN1 ATy a1\ (R a1)) :- + M is N - 1, + @pi-decl AN1 ATy a1\ + coq.mk-app Injtor [a1] (NewInjtor a1), + coq.mk-app K [a1] (NewK a1), + add-concl M 0 ArgNo (Bo a1) (NewInjtor a1) DestPathNo RHS (NewK a1) SrcArgs DestArgs Eqs (R a1). + +% type of duplicated arguments + eq, list of injectors, list of dest path number. +% todo: add K applied to typaram +pred add-conclss i:list term, i:list term, i:int, i:list int, i:list (list term), i:list (list int), o: list (list term). +add-conclss [] [] _ [] [] [] []. +add-conclss [PTy|PTys] [K|Ks] TyParamNo [ArgNo|ArgNos] [Injs|Injss] [DestNos|DestNoss] [InjTys|InjTyss] :- + std.map2 Injs DestNos (x\y\r\ sigma R\ add-concl TyParamNo 0 ArgNo PTy x y {{Type}} K [] [] [] R, r = R) InjTys, + add-conclss PTys Ks TyParamNo ArgNos Injss DestNoss InjTyss. + +%TyParamNo, constructors, type of constructors, output. +% for every constructor, +% collects its injectors and build the corresponding type for every injector +pred mk-injK-types i:int, i: list constructor, i:list term, o:list (list term), o:list int, o:list (list int). +mk-injK-types TyParamNo KNs KTys InjTyss ArgNos DestNoss :- + std.map KTys (x\ r\ sigma R\ count-args TyParamNo x R, r = R) ArgNos, + std.map2 KTys ArgNos + (x\ y\ r\ sigma ArgNo R1 R2\ + duplicate-arguments TyParamNo y x R1, + add-equalities TyParamNo y R1 R2, + r = R2) PTy, + std.map KNs (x\ r\ r = {coq.env.global (indc x)}) Ks, + get-injectors Ks ArgNos Injss DestNoss, + add-conclss PTy Ks TyParamNo ArgNos Injss DestNoss InjTyss. + +% rm argno +pred mk-pred i:int, i:int, i:int, i:term, i:term, i:term, i:list term, i:list term, i:list term, i:list term, i:list term, o:term. +mk-pred _ _ _ Pred _ _ [] [] [] [] [] Pred. +mk-pred Curr I ArgNo Pred T P [A1|Args1] [_A2|Args2] [A2Ty|TyArgs2] [_Path|Paths] [_PathTy|TyPaths] R :- + Curr < I, + !, + J is Curr + 1, + coq.mk-app Pred [A1,A1,{{ lib:@trocq.idpath lp:A2Ty lp:A1}}] NewPred, + mk-pred J I ArgNo NewPred T P Args1 Args2 TyArgs2 Paths TyPaths R. + +mk-pred I I ArgNo Pred T P [A1|Args1] [_A2|Args2] [_A2Ty|TyArgs2] [_Path|Paths] [_PathTy|TyPaths] R :- + !, + J is I + 1, + coq.mk-app Pred [A1,T,P] NewPred, + mk-pred J I ArgNo NewPred T P Args1 Args2 TyArgs2 Paths TyPaths R. + +mk-pred Curr I ArgNo Pred T P [A1|Args1] [A2|Args2] [_A2Ty|TyArgs2] [Path|Paths] [_PathTy|TyPaths] R :- + coq.mk-app Pred [A1,A2,Path] NewPred, + mk-pred Curr I ArgNo NewPred T P Args1 Args2 TyArgs2 Paths TyPaths R. + +pred mk-preds i:int, i:int, i:list term, i:list term, i:list term, i:list term, i:list term, i:list term, o:list term. +mk-preds _ _ [] _ _ _ _ _ []. +mk-preds I ArgNo [P|Preds] Args1 Args2 TyArgs2 Paths TyPaths [ RP | RS ] :- + J is I + 1, + std.nth I TyPaths PTy, + whd PTy [] {{lib:@trocq.paths}} [T,A,_], + @pi-decl `t` T t\ + coq.mk-app {{lib:@trocq.paths}} [T,A,t] (PatTy t), + @pi-decl `p` (PatTy t) p\ + mk-pred 0 I ArgNo P t p Args1 Args2 TyArgs2 Paths TyPaths (R t p), + RPSkel = (fun `t` T t\ fun `p` (PatTy t) p\ (R t p)), + (@keepunivs! => coq.elaborate-skeleton RPSkel _ RP ok), + mk-preds J ArgNo Preds Args1 Args2 TyArgs2 Paths TyPaths RS. + +pred iter-convs i:list term, i:list term, i:list term, i:list term, i:list term, i:term, o:term. +iter-convs [] [] [] [] [] End End. +iter-convs [Ty|Tys] [A1|Args1] [A2|Args2] [Path|Paths] [Pred|Preds] End R :- + Conv = {{lib:@trocq.conv}}, + iter-convs Tys Args1 Args2 Paths Preds End P0, + coq.mk-app Conv [ Ty, A1, A2, Path, Pred, P0] R. + + +pred implement-injK i:int, i:int, i:int, i:int, i:term, i:term, i:list term, i:list term, i:list term, i:list term, i:list term, i:list term, o:term. +implement-injK 0 0 ArgNo DestNo _ Pred TyParamsR Args1R Args2R TyArgs2R PathsR TyPathsR R :- !, + std.rev TyParamsR TyParams, + std.rev Args1R Args1, + std.rev Args2R Args2, + std.rev TyArgs2R TyArgs2, + std.rev PathsR Paths, + std.rev TyPathsR TyPaths, + coq.mk-app Pred TyParams PredT, + std.iota ArgNo Tmp, + std.map Tmp (x\r\ r = PredT) Preds, + mk-preds 0 ArgNo Preds Args1 Args2 TyArgs2 Paths TyPaths RPreds, + + std.nth DestNo Args1 A1, + std.nth DestNo TyArgs2 Ty, + EndArg = {{ lib:@trocq.idpath lp:Ty lp:A1}}, + (@keepunivs! => coq.typecheck EndArg EndTy ok), + End = {{ lib:@trocq.idpath lp:EndTy lp:EndArg}}, + iter-convs TyArgs2 Args1 Args2 Paths RPreds End RSkel, + (@keepunivs! => coq.elaborate-skeleton RSkel _ R ok). + +% build the stuff. +% reverse args +implement-injK 0 N ArgNo DestNo (prod AN1 ATy a1\ prod AN2 ATy a2\ prod EN (EqTy a1 a2) e\ (Bo a1 a2 e)) + Pred TyParams Args1 Args2 TyArgs2 Paths TyPaths (fun AN1 ATy a1\ fun AN2 ATy a2\ fun EN (EqTy a1 a2) e\ (R a1 a2 e)) :- + M is N - 1, + @pi-decl AN1 ATy a1\ + @pi-decl AN2 ATy a2\ + @pi-decl EN (EqTy a1 a2) e\ + implement-injK 0 M ArgNo DestNo (Bo a1 a2 e) Pred TyParams [a1|Args1] [a2|Args2] [ATy|TyArgs2] [e|Paths] [(EqTy a1 a2)|TyPaths] (R a1 a2 e). + +implement-injK M N ArgNo DestNo (prod AN1 ATy a1\ (Bo a1)) Pred TyParams Args1 Args2 TyArgs2 Paths TyPaths (fun AN1 ATy a1\ (R a1)) :- + O is M - 1, + @pi-decl AN1 ATy a1\ + implement-injK O N ArgNo DestNo (Bo a1) Pred [a1|TyParams] Args1 Args2 TyArgs2 Paths TyPaths (R a1). + +% todo rm constructor as arg +pred implement-injKs i:int, i:constructor, i:int, i:list term, i:list int, o:list term. +implement-injKs _ _ _ [] [] []. +implement-injKs TyParamNo _ ArgNo [InjKTy|InjKTys] [DestNo | DestNos] [R| RS] :- + coq.prod->fun InjKTy Pred, + implement-injK TyParamNo ArgNo ArgNo DestNo InjKTy Pred [] [] [] [] [] [] RSkel, + coq.elaborate-skeleton RSkel _ R ok, + implement-injKs TyParamNo _ ArgNo InjKTys DestNos RS. + +% todo rm constructors as arg +pred implement-injK-types i:int, i: list constructor, i:list int, i:list (list term), i:list (list int), o:list (list term). +implement-injK-types _ [] [] [] [] []. +implement-injK-types TyParamNo [Kn|KNs] [ArgNo|ArgNos] [InjKTys|InjKTyss] [DestNos| DestNoss] [R|RS] :- + implement-injKs TyParamNo Kn ArgNo InjKTys DestNos R, + implement-injK-types TyParamNo KNs ArgNos InjKTyss DestNoss RS. + +register-db.aux K J C R :- + coq.env.global (indc K) Tm, + R = (injectionsK-db Tm J (global (const C))). +register-def.aux K J C R :- + coq.env.global (indc K) _, + R = (injectionsK-def (indc K) J (const C)). +register.aux K J C [R1,R2] :- + register-db.aux K J C R1, + register-def.aux K J C R2. + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + + Name is Prefix ^ "injK", + coq.ensure-fresh-global-id Name FName, + coq.env.indt GR _ TyParamNo _ _ KNs KTys, + mk-injK-types TyParamNo KNs KTys RTys ArgNos DestNos, + implement-injK-types TyParamNo KNs ArgNos RTys DestNos RS, + name-ijs FName 1 GR KNs RS register.aux Clausess, + std.flatten Clausess Clauses, + ClausesFin = [injectionsK-done GR | Clauses], + std.forall ClausesFin (x\ + coq.elpi.accumulate _ "derive.injectionsK.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/injection_lemmas.elpi b/elpi/inductives/injection_lemmas.elpi new file mode 100644 index 00000000..77f59b67 --- /dev/null +++ b/elpi/inductives/injection_lemmas.elpi @@ -0,0 +1,133 @@ +accumulate "Trocq.Elpi.inductives/utils". +accumulate "elpi.apps.derive.elpi/injection". + +shorten derive.algo-utils.{duplicate-arguments, count-args, name-ijs, for-K-get-KI}. + +namespace derive.injections { + +/* for all projectors of type forall Args T, ret +generate + +forall Args1-> Args2-> (e : Kj args->1 = Kj args->2) argj + +Take an inductive Ind, +take its constructors global references, +for each global reference GRK, +Compute the number of arguments J for each GRK, +for each ArgNumber in 1 to J+1, +get the Projector GRK ArgNumber, +Get the type ProjType, forall ArgTys Args Ind, ret +Return the processed Types */ + +% TyParam, ArgNo, F, Type of the equality, Left HS, Right HS +% F is of type forall (Typarams : Type) ((Arg1 : A1) (Arg2 : A2) ...), Ret +% Ret is discarded and replaced by Left = Right +pred craft-eq i:int, i:int, i:int, i:int, i:term, i:term, i:term, i:term, i:term, i:term, i:term, o:term. +craft-eq 0 0 _ _ _ EqTy Left Right ConclEqTy ConclL ConclR R:- !, + coq.mk-app {{lib:@trocq.paths}} [EqTy, Left, Right] AETy, + coq.mk-app {{lib:@trocq.paths}} [ConclEqTy, ConclL, ConclR] C, + R = {{ forall (e : lp:AETy), lp:C }}. + +craft-eq 0 ArgNo J Max (prod N1 T x\ prod N2 T y\ (Bo x y)) EqTy Left Right ConclEq ConclL ConclR (prod N1 T x\ prod N2 T y\ (S x y)) :- !, + M is ArgNo - 1, + J? is Max - ArgNo + 1, + @pi-decl N1 T x\ + @pi-decl N2 T y\ + sigma NewLeft NewRight NewConclEq NewConclL NewConclR\ + (if (J? = J) + (NewConclEq = T, + NewConclL = x, + NewConclR = y) + (NewConclEq = ConclEq, + NewConclL = ConclL, + NewConclR = ConclR)), + coq.mk-app Left [x] NewLeft, + coq.mk-app Right [y] NewRight, + craft-eq 0 M J Max (Bo x y) EqTy NewLeft NewRight NewConclEq NewConclL NewConclR (S x y). + +craft-eq TyParam ArgNo J Max (prod N T Bo) EqTy Left Right CE CL CR (prod N T x\ S x) :- !, + M is TyParam - 1, + @pi-decl N T x\ + sigma NewEqTy NewLeft NewRight\ + coq.mk-app EqTy [x] NewEqTy, + coq.mk-app Left [x] NewLeft, + coq.mk-app Right [x] NewRight, + craft-eq M ArgNo J Max (Bo x) NewEqTy NewLeft NewRight CE CL CR (S x). + +pred build-type-K-injector i:int, i:int, i:inductive, i:constructor, i:int, i:term, i:list term, o:list term. +build-type-K-injector _ _ _ _ _ _ [] [] :- !. +build-type-K-injector TyParamNo J GR Kn ArgNo KTy [PJ|PJs] [Eq|RS] :- std.do! [ + Jn is J + 1, + duplicate-arguments TyParamNo ArgNo PJ S, + (craft-eq TyParamNo ArgNo J ArgNo S {coq.env.global (indt GR)} {coq.env.global (indc Kn)} {coq.env.global (indc Kn)} {{tt}} {{tt}} {{tt}} Eq), + (@keepunivs! => coq.typecheck Eq _ ok), + build-type-K-injector TyParamNo Jn GR Kn ArgNo KTy PJs RS]. + +pred build-types-injectors i:int, i: inductive, i:list constructor, i: list int, i:list (term), i:list (list term), o:list (list term). +build-types-injectors _ _ [] [] [] [] [] :- !. +build-types-injectors TyParamNo GR [Kn|KNs] [ArgNo|ArgsNos] [KTy|KTys] [PJs|PJss] [R|RS] :- + build-type-K-injector TyParamNo 1 GR Kn ArgNo KTy PJs R, + build-types-injectors TyParamNo GR KNs ArgsNos KTys PJss RS. + +pred implement-K-injector-J i:int, i:int, i:int, i:int, i:term, o:term. +implement-K-injector-J 0 J 0 TyParam (prod E Ty _) R :- !, + I is J - 1, + R = {{ fun e:(lp:Ty) => lp:(PL e) }}, + @pi-decl E Ty e\ + sigma GR TyArgs GRK KArgs A B\ + ltac.injection? Ty GR TyArgs GRK KArgs A B, + ltac.injection.arg-i I J {{lib:@trocq.ap }} GR TyArgs TyParam GRK KArgs A B e [(PL e)]. + +implement-K-injector-J 0 J ArgNo TyParam (prod ArgN1 ArgTy1 a\ (prod ArgN2 ArgTy2 b\ (Bo a b))) (fun ArgN1 ArgTy1 a\ fun ArgN2 ArgTy2 b\ (R a b) ) :- !, + ArgNon is ArgNo - 1, + @pi-decl ArgN1 ArgTy1 a\ + @pi-decl ArgN2 ArgTy2 b\ + implement-K-injector-J 0 J ArgNon TyParam (Bo a b) (R a b). + +implement-K-injector-J ParamNo J ArgNo TyParam (prod TyArg T t\ (Bo t)) (fun TyArg T t\ (R t) ) :- + ParamNon is ParamNo - 1, + @pi-decl TyArg T t\ + implement-K-injector-J ParamNon J ArgNo TyParam (Bo t) (R t). + +pred implement-K-injectors i:int, i:int, i:int, i:list term, o:list term. +implement-K-injectors _ _ _ [] []. +implement-K-injectors TyParam J ArgNo [InjTy | InjTys] [R | RS] :- + Jn is J + 1, + (implement-K-injector-J TyParam J ArgNo TyParam InjTy RSkel), + (@keepunivs! => coq.elaborate-skeleton RSkel _ R ok), + implement-K-injectors TyParam Jn ArgNo InjTys RS. + +pred implement-injectors i:int, i:list int, i:list (list term), o:list (list term). +implement-injectors _ _ [] []. +implement-injectors TyParam [ArgNo | ArgNos] [InjTys | InjTyss] [R | RS ] :- + implement-K-injectors TyParam 1 ArgNo InjTys R, + implement-injectors TyParam ArgNos InjTyss RS. + +pred for-K-get-projectors i:int, i:list constructor, i:list term, o: list int, o:list (list term). +for-K-get-projectors TyParamNo KNs KTys ArgsNos PJss :- + for-K-get-KI TyParamNo KNs KTys (grk\ i\ p\ projK-db grk i p) ArgsNos PJss. + +register-def.aux K J C R :- + coq.env.global (indc K) _, + R = (injections-def (indc K) J (const C)). +register.aux K J C [R1] :- + register-def.aux K J C R1. + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + Name is Prefix ^ "injections", + coq.ensure-fresh-global-id Name FName, + coq.env.indt GR _ TyParamNo _ _ KNs KTys, + for-K-get-projectors TyParamNo KNs KTys ArgsNos PJss, + std.map PJss (x\ r\ sigma R\ (std.map x (y\ r\ sigma Ty\ (@keepunivs! => coq.typecheck y Ty ok), r = Ty) R), r = R) PJTyss, + build-types-injectors TyParamNo GR KNs ArgsNos KTys PJTyss InjTyss, + implement-injectors TyParamNo ArgsNos InjTyss Injss, + name-ijs FName 1 GR KNs Injss register.aux Clausess, + std.flatten Clausess Clauses, + ClausesFin = [injections-done GR | Clauses], %[injections-done GR, injections GR (const C)], + std.forall ClausesFin (x\ + coq.elpi.accumulate _ "derive.injections.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/mR.elpi b/elpi/inductives/mR.elpi new file mode 100644 index 00000000..ea0ac7ac --- /dev/null +++ b/elpi/inductives/mR.elpi @@ -0,0 +1,196 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". +accumulate "Trocq.Elpi.inductives/injection_lemmas". +accumulate "elpi.apps.derive.elpi/discriminate". + +shorten derive.common-algo.{mk-mR-type-mR}. +shorten derive.algo-utils.{cmp-indt}. + +namespace derive.mR { + +% Given Y and Bo: x\ y\ RT. The return type of the match on X is: substituting the binder of X in the match. +pred rty-1 i:(term -> term -> term), i:term , i:term, i: list term, i: list term, o:term. +rty-1 Bo Y _ Ts _ R :- + std.last Ts X, + R = Bo X Y. + +% Given X and Bo: x\ y\ RT. The return type of the match on Y is: substituting the binder of Y in the match. +pred rty-2 i:(term -> term -> term), i:term , i:term, i: list term, i: list term, o:term. +rty-2 Bo X _ Ts _ R :- + std.last Ts Y, + R = Bo X Y. + +pred sub-branch i:term, i:int, i: term, i:list term, i:list term, i:term, i:list term, i:list term, + i:(term -> term -> term), o:term. +sub-branch YTy TyParamNo K1 Args1 ArgTys1 K2 Args2 ArgTys2 Bo (fun `e` ETy e\ (R e)):- + coq.mk-app K1 Args1 X, + coq.mk-app K2 Args2 Y, + BoXY = Bo X Y, + coq.elaborate-skeleton BoXY _ BoXYE ok, + !, + BoXYE = prod _ ETy G, + whd K1 [] Constr1 TypeArgs1, + whd K2 [] Constr2 TypeArgs2, + @pi-decl `e` ETy e\ + matrix YTy TyParamNo Constr1 TypeArgs1 Args1 ArgTys1 Constr2 TypeArgs2 Args2 ArgTys2 e ETy (G e) (R e). + +% Each branch matches on Y as Y0, returning a term of type (Bo (K KArgs) Y0) given by matrix. +pred mkBranch i:int, i:(term -> term -> term), i:term, i:term, i:term, i:term, i:list term, i:list term, o:term. +mkBranch TyParamNo Bo Y YTy K _ Ts TYs R :- + !, + coq.mk-app K Ts X, + coq.build-match Y YTy (rty-2 Bo X) + (k2\ _\ ts\ tys\ + sub-branch YTy TyParamNo K Ts TYs k2 ts tys Bo) + R. + +pred build-mRA-ty-args i:list term, i:list term, i:term, o:term. +build-mRA-ty-args [] [] R R. +build-mRA-ty-args [ATy1| ArgsTy1] [ATy2| ArgsTy2] MR R :- + ar-db ATy1 ATy2 AR, + coq.mk-app MR [ATy1, ATy2, AR] NewMR, + build-mRA-ty-args ArgsTy1 ArgsTy2 NewMR R. + +% TODO update: this considers that type arguments come in Ts, they don't come in there. +pred build-mRA i:term, i:term, i:term, i:term, o:term. +build-mRA IndTy ATy1 ATy2 _ R :- + cmp-indt ATy1 IndTy IndS Ind, + cmp-indt ATy2 IndTy IndD Ind, + coq.safe-dest-app ATy1 _ ArgsTy1, + coq.safe-dest-app ATy2 _ ArgsTy2, + mR-db IndS IndD MR, + % TODO: change following line to implement non uniform parameters + definition of the fix. + if (IndS = Ind) + (R = MR) + (build-mRA-ty-args ArgsTy1 ArgsTy2 MR R). + +pred build-injEKJ-args i:int, i:list term, i:list term, + i:term, i:term, o:term. +% applies TyParamNo time the Type parameter of the return Inductive. +build-injEKJ-args 0 Args1 Args2 InjKJ E R :- + app-interleave InjKJ Args1 Args2 InjKJArgs, + coq.mk-app InjKJArgs [E] R. +build-injEKJ-args N [_ | ATys1] [ATy2|ATys2] InjKJ E R :- + M is N - 1, + coq.mk-app InjKJ [ATy2] InjKJA, + build-injEKJ-args M ATys1 ATys2 InjKJA E R. + +pred app-interleave i:term, i:list term, i:list term, o:term. +app-interleave R [] [] R. +app-interleave F [A|Args1] [B|Args2] R :- + coq.mk-app F [A, B] NewF, + app-interleave NewF Args1 Args2 R. + +pred build-injEKJ i:int, i:term, i:term, i:term, i:int o: term. +build-injEKJ TyParamNo E ETy K J R :- + injections-db K J InjKJ, + whd ETy [] {{lib:@trocq.paths}} [_,A,B], + whd A [] KA ArgsL, + whd B [] KB ArgsR, + coq.env.global (indc _) KA, + coq.env.global (indc _) KB, + build-injEKJ-args TyParamNo ArgsL ArgsR InjKJ E InjEKJ, + coq.elaborate-skeleton InjEKJ _ R _. + +% TODO: for processing params extend with an int of param no + db Type Type AR. +% TODO: for processing contained types, lookup mR-db apply arg1 arg2 + the ith constructor injection of the equality. +pred apply-indR i:term, i:int, i:int, i:term, i:term, i:list term, i:list term, i:list term, i:list term, i:list term, i:list term, i:term, i:term, i:term, i:term, i:int, o: term. +% N J K KR K1Args K1Tys K2Args K2Tys X Y E TyParamNo +apply-indR _ 0 _ _ KR [] [] [] [] [] [] _ _ _ _ _ KR. +% for the jth argument provide A1 A2 AR12 +% For AR12 we bring mR_ATy ATyArgs1 ATyArgs2 ARs +% For the equality we bring injectionKJ TyArgs2 (Args1 of the eq) (Args2 of the eq) +apply-indR YTy 0 J K KR [] [A1|Args1] [ATy1|ArgTys1] [] [A2|Args2] [ATy2| ArgTys2] LHS RHS E ETy TyParamNo R :- + Jn is J + 1, + build-mRA YTy ATy1 ATy2 LHS MRA, + build-injEKJ TyParamNo E ETy K J InjEKJ, + coq.mk-app MRA [A1,A2,InjEKJ] A12R, + coq.mk-app KR [A1,A2, A12R] KA12AR, + apply-indR YTy 0 Jn K KA12AR [] Args1 ArgTys1 [] Args2 ArgTys2 LHS RHS E ETy TyParamNo R. +apply-indR YTy N J K KR [Ty1|TyArgs1] Args1 ArgTys1 [Ty2|TyArgs2] Args2 ArgTys2 LHS RHS E ETy TyParamNo R :- + M is N - 1, + ar-db Ty1 Ty2 AR, + coq.mk-app KR [Ty1, Ty2, AR] NewKR, + apply-indR YTy M J K NewKR TyArgs1 Args1 ArgTys1 TyArgs2 Args2 ArgTys2 LHS RHS E ETy TyParamNo R. + +% On the diagonal return KR a1 a2 ... +% Outside the diagonal discriminate +pred matrix + i: term, + i:int, i: term, i:list term, i:list term, i:list term, i:term, i:list term, i:list term, i:list term, + i:term, i:term, i:term, o:term. +matrix YTy TyParamNo K1 TyArgs1 KArgs1 ArgTys1 K2 TyArgs2 KArgs2 ArgTys2 E ETy _ R :- + coq.env.global (indc K) K1, + coq.env.global (indc K) K2, + !, + param K1 K1 KR, + coq.mk-app K1 {std.append TyArgs1 KArgs1} LHS, + coq.mk-app K2 {std.append TyArgs2 KArgs2} RHS, + apply-indR YTy TyParamNo 1 K1 KR TyArgs1 KArgs1 ArgTys1 TyArgs2 KArgs2 ArgTys2 LHS RHS E ETy TyParamNo R. + +matrix _ _ _ _ _ _ _ _ _ _ E ETy G R :- !, + ltac.discriminate E ETy G R. + +pred implement-mR i:int, i:int, i:term, o:term. +% all TyParams processed, +% remains forall (i1: I Args1) (i2 : I Args2), map -> IR +% Bo is i1\ i2\ mapI Args1 Args2 ARs i1 = i2 -> IR Args1i Args2i ARsi i1 i2. +% todo: Carry the list of TyArgs, needed for apply-ind params. +implement-mR 0 TyParamNo (prod I1 I1Ty i1\ prod I2 I2Ty i2\ (Bo i1 i2)) (fix `f` 0 RT f\ fun I1 I1Ty i1\ fun I2 I2Ty i2\ (R f i1 i2)) :- + coq.safe-dest-app I2Ty Ind _, + coq.env.global (indt GR) Ind, + coq.env.recursive? GR, !, + RT = (prod I1 I1Ty i1\ prod I2 I2Ty i2\ (Bo i1 i2)), + @pi-decl `f` RT f\ + @pi-decl I1 I1Ty i1\ + @pi-decl I2 I2Ty i2\ + % TODO: I'm a bug fix me + mR-db Ind Ind f => + coq.build-match i1 I1Ty (rty-1 Bo i2) (mkBranch TyParamNo Bo i2 I2Ty) (R f i1 i2). +implement-mR 0 TyParamNo (prod I1 I1Ty i1\ prod I2 I2Ty i2\ (Bo i1 i2)) (fun I1 I1Ty i1\ fun I2 I2Ty i2\ (R i1 i2)) :- + @pi-decl I1 I1Ty i1\ + @pi-decl I2 I2Ty i2\ + !, coq.build-match i1 I1Ty (rty-1 Bo i2) (mkBranch TyParamNo Bo i2 I2Ty) (R i1 i2). +implement-mR N TyParamNo (prod A1 A1Ty a1\ prod A2 A2Ty a2\ prod AR (ARTy a1 a2) ar\ prod AM (AMTy a1 a2 ar) am\ (Bo a1 a2 ar am)) + (fun A1 A1Ty a1\ fun A2 A2Ty a2\ fun AR (ARTy a1 a2) ar\ fun AM (AMTy a1 a2 ar) am\ (R a1 a2 ar am)) :- + M is N - 1, + @pi-decl A1 A1Ty a1\ + @pi-decl A2 A2Ty a2\ + @pi-decl AR (ARTy a1 a2) ar\ + @pi-decl AM (AMTy a1 a2 ar) am\ + % todo: fix me: universes + Map = pglobal {{:gref lib:trocq.map1.map }} _ , + coq.mk-app Map [a1,a2,ar,am] (PMapA a1 a2 ar am), + % insert coercions + coq.elaborate-skeleton (PMapA a1 a2 ar am) _ (MapA a1 a2 ar am) ok, + MR = pglobal {{:gref lib:trocq.map2a.map_in_r }} _, + coq.mk-app MR [a1,a2,ar,am] (PMR a1 a2 ar am), + coq.elaborate-skeleton (PMR a1 a2 ar am) _ (MRA a1 a2 ar am) ok, + mymap-db A1Ty A2Ty (MapA a1 a2 ar am) ==> + mR-db a1 a2 (MRA a1 a2 ar am) ==> + % todo: check usage of ar-db in mR + ar-db a1 a2 ar ==> + implement-mR M TyParamNo (Bo a1 a2 ar am) (R a1 a2 ar am). + + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + Name is Prefix ^ "mR", + coq.env.indt GR _ UnifParamNo _ _ _ _, + coq.env.global (indt GR) Ind, + param Ind Ind TR, + coq.typecheck TR TRTy ok, + mymap-def (indt GR) IndMapGR, + mk-mR-type-mR UnifParamNo TRTy {coq.env.global IndMapGR} {{ Type }} TR MRTy, + std.assert-ok! (coq.elaborate-skeleton MRTy _ MRTyE) "derive.mR generates illtyped type", + implement-mR UnifParamNo UnifParamNo MRTyE T, + std.assert-ok! (coq.elaborate-skeleton T MRTyE TE) "derive.mR generates illtyped term", + coq.ensure-fresh-global-id Name FName, + coq.env.add-const FName TE MRTyE _ C, + Clauses = [mR-done GR, mR-def (indt GR) (const C)], + std.forall Clauses (x\ + coq.elpi.accumulate _ "derive.mR.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/mRRmK.elpi b/elpi/inductives/mRRmK.elpi new file mode 100644 index 00000000..e57022a5 --- /dev/null +++ b/elpi/inductives/mRRmK.elpi @@ -0,0 +1,300 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.common-algo.{mk-mR-type-mRRmK}. +shorten derive.algo-utils.{mk-chain, for-K-get-KI,type-of-args, whd-fuel, iota-step, invert-eqs, rewrite-with, elim-into-path-suffix, cmp-indt}. + +namespace derive.mRRmK { + +pred collect-ma1-a2 i:int, i:list term, o:list term, o:list term. +collect-ma1-a2 0 _ [] []. +collect-ma1-a2 N [A1, A2| L] [A1|A1s] [A2|A2s] :- + M is N - 1, + collect-ma1-a2 M L A1s A2s. + +pred collect-paths i:int, i:term, o:list term. +collect-paths 0 _ []. +collect-paths N T [P|Ps] :- + M is N - 1, + coq.safe-dest-app T _EqTrans [_,_,_,_,AP1,AP2], + coq.safe-dest-app AP1 _ Args1, + std.last Args1 P, + collect-paths M AP2 Ps. + +% delta beta iota iota +pred red-mR i:term, i:stack, o:term,o:stack. +red-mR X C R RS :- + whd-fuel X C 1 XX CC, + iota-step XX CC XXX CCC, + iota-step XXX CCC R RS. + +% delta beta beta eta delta beta iota (perhaps also starts with an eta red) +pred red-Rm i:term, i:stack, o:term,o:stack. +red-Rm X C R RS :- + whd-fuel X C 2 XX CC, + iota-step XX CC R RS. + +pred feed-injKs i:list term, i:list term, i:list term, i: list term, i:list term, o:list term. +feed-injKs InjKs [] [] [] [] InjKs. +feed-injKs InjKs [] [A1|Args1] [A2|Args2] [Path|Paths] ES :- + std.map InjKs (x\ r\ sigma TMP\ coq.mk-app x [A1,A2,Path] TMP, r = TMP) NewInjKs, + feed-injKs NewInjKs [] Args1 Args2 Paths ES. +feed-injKs InjKs TyArgsDest Args1 Args2 Paths Eqs :- + std.map InjKs (x\ r\ sigma TMP\ coq.mk-app x TyArgsDest TMP, r = TMP) NewInjKs, + feed-injKs NewInjKs [] Args1 Args2 Paths Eqs. + +pred collect-arguments i:int, i:int, i:term, o:list term, o:list term, o:list term, o:list term. +collect-arguments TyArgsNo InitArgs MRRM TyArgsDest Args1 Args2 Paths :- + red-mR MRRM [] _KR Args12r, % KR a1 a2 ar b1 b2 br ... + std.last Args12r LastMR, % each xr is xmR x1 x2 (inj Args12 Chain) + coq.safe-dest-app LastMR _NMR Args, + std.last Args Inj, % take the last inj + coq.safe-dest-app Inj _Injin InjArgs, + std.split-at TyArgsNo InjArgs TyArgsDest ArgsChain, % collect Type args + collect-ma1-a2 InitArgs ArgsChain Args1 Args2, % collect mapped args1 and args2 + % Args1 is (map a1), (map b1) + % Args2 is a2 b2 ... + std.last InjArgs Rm, + % last arg is IRm args which reduces to chain + coq.safe-dest-app Rm TheRm RmArgs, + red-Rm TheRm RmArgs Concat ChainArgs, + coq.mk-app Concat ChainArgs Chain, + collect-paths InitArgs Chain Paths. % Paths are Rm1 a1 a2 aR, Rm2 b1 b2 bR, ... + +pred drop-last i:list A, o:list A. +drop-last L R :- + Take is {std.length L} - 1, + std.take Take L R. + +% number of processed pats, total number of args, list of injK equations, list of patterns, list of resulting goals. +pred pierce-goal-injK i:int, i:int, i:int i:term, i:list term, o:list term, o:term. +pierce-goal-injK _ N N Goal [] [] Goal. +pierce-goal-injK TyParamNo N InitArgs CurrentGoal [Eq|Eqs] [Pat|Pats] EndGoal:- !, + M is N + 1, + coq.safe-dest-app CurrentGoal EqGoal [EqGoalTy,GoalLHS,GoalRHS], + coq.safe-dest-app GoalLHS KR Args, + Done is (TyParamNo * 3) + N * 3, + std.split-at Done Args L [A1,A2, AMRArgs | R], + coq.safe-dest-app AMRArgs AMR MArgs, + coq.typecheck {std.last MArgs} Ty ok, + (pi t\ + drop-last MArgs DArgs, + std.append DArgs [t] (NewMArgs t), + coq.mk-app AMR (NewMArgs t) (NewAMRArgs t), + coq.mk-app KR {std.append L {std.append [A1, A2, (NewAMRArgs t)] R}} (NewKR t), + coq.mk-app EqGoal [EqGoalTy,(NewKR t),GoalRHS] (NewEqGoal t)), + Pat = (fun `t` Ty t\ (NewEqGoal t)), + coq.typecheck Eq EqTy ok, + coq.safe-dest-app EqTy _ [_,LHS,_], + coq.mk-app Pat [LHS] NewGoal, + pierce-goal-injK TyParamNo M InitArgs NewGoal Eqs Pats EndGoal. + +% number of processed pats, total number of args, list of injK equations, list of patterns, list of resulting goals. +pred pierce-goal-mRRmK i:int, i:int, i:int i:term, i:list term, o:list term. +pierce-goal-mRRmK _ N N _ [] []. +pierce-goal-mRRmK TyParamNo N InitArgs CurrentGoal [Eq|Eqs] [Pat|Pats] :- !, + M is N + 1, + coq.safe-dest-app CurrentGoal EqGoal [EqGoalTy,GoalLHS,GoalRHS], + coq.safe-dest-app GoalLHS KR Args, + Done is (TyParamNo * 3) + (N * 3), + std.split-at Done Args L [A1,A2, AMRArgs | R], + coq.typecheck AMRArgs Ty ok, + (pi t\ + coq.mk-app KR {std.append L {std.append [A1, A2, t] R}} (NewKR t), + coq.mk-app EqGoal [EqGoalTy,(NewKR t),GoalRHS] (NewEqGoal t)), + Pat = (fun `t` Ty t\ (NewEqGoal t)), + coq.typecheck Eq EqTy ok, + coq.safe-dest-app EqTy _ [_,LHS,_], + coq.mk-app Pat [LHS] NewGoal, + pierce-goal-mRRmK TyParamNo M InitArgs NewGoal Eqs Pats. + +pred get-mRRmK-args i:list term, o:list (list term). +get-mRRmK-args [] []. +get-mRRmK-args [P|Paths] [Args|Argss] :- + coq.safe-dest-app P _ Args, + get-mRRmK-args Paths Argss. + +pred mix-mRRmK-args i:list term, i:list (list term), o:list term. +mix-mRRmK-args [] [] []. +mix-mRRmK-args [MRRMK| MRRMKs] [Args|Argss] [Eq| Eqs] :- + coq.mk-app MRRMK Args Eq, + mix-mRRmK-args MRRMKs Argss Eqs. + +% 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:int, i:term, i:term, i:term, i:term, +i:list term, i:list term, i:list term, o:term. +% zero more arguments to process +process-args Ksrc Kdest 0 0 _ _ Goal _ KR _ _ _ R :- + coq.mk-app Goal [Ksrc, Kdest, KR] EqTy, + whd EqTy [] _ [IRTy,_,IR], + R = {{ lib:@trocq.idpath lp:IRTy lp:IR }}. +process-args Ksrc Kdest 0 InitArgs TyArgsNo _ Goal _ KR InjKs _ MRRMKEq R:- + coq.mk-app Goal [Ksrc, Kdest, KR] EqTy, + %EqTy is the following type ImR i1 i2 (IRm i1 i2 ir) = ir for this specific branch + whd EqTy [] HD [IRTy,MRRM,IR], + collect-arguments TyArgsNo InitArgs MRRM TyArgsDest Args1 Args2 Paths, %paths are all + feed-injKs InjKs TyArgsDest Args1 Args2 Paths Eqs, + invert-eqs Eqs IEqs, + std.map MRRMKEq (x\ r\ sigma TMP\ (@keepunivs! => coq.elaborate-skeleton x _ TMP ok), r = TMP) MRRMKElab, + invert-eqs {std.rev MRRMKElab} IEqs2, + End = {{ lib:@trocq.idpath lp:IRTy lp:IR }}, + coq.mk-app HD [IRTy,{whd1 MRRM},IR] RGoal, % KR a1 a2 ar1[I_Rm] b1 b2 br[I_Rm] + pierce-goal-injK TyArgsNo 0 InitArgs RGoal IEqs PatsInj LastGoal, + pierce-goal-mRRmK TyArgsNo 0 InitArgs LastGoal IEqs2 PatsMRRMK, + rewrite-with {std.append IEqs IEqs2} {std.append PatsInj PatsMRRMK} End R. + +% still have to process an arg +process-args Ksrc Kdest N InitArgs TyArgsNo (prod AN1 A1Ty a1\ prod AN2 A2Ty a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) Goal ITyTy KR + InjKs [MRRMKSkel|MRRMKs] MRRMKEqs (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), + coq.mk-app KR [a1,a2,ar] (NewKR a1 a2 ar), + coq.mk-app MRRMKSkel [a1,a2,ar] (MRRMK a1 a2 ar), + (ar-db a2 a1 ar ==> + process-args (NewKS a1) (NewKD a2) M InitArgs TyArgsNo (Bo a1 a2 ar) Goal ITyTy (NewKR a1 a2 ar) InjKs MRRMKs [(MRRMK a1 a2 ar)|MRRMKEqs] (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 A2IndT Ind, + if (Ind = A2IndT) + (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). + +pred feed-mRRmK-type i:list term, i:term, o:term. +feed-mRRmK-type [] T T. +feed-mRRmK-type [A2|Args] T R :- + ar-db A1 A2 AR, + coq.mk-app T [A1, A2, AR] Acc, + feed-mRRmK-type Args Acc R. + +pred find-mRRmK i:list term, i:list term, i:term, o: list term. +find-mRRmK [] [] _ []. +find-mRRmK [STy| STys][DTy|DTys] IndTy [MRRMK|MRRMKs] :- + cmp-indt DTy IndTy IndD Ind, + cmp-indt STy IndTy IndS Ind, + coq.safe-dest-app DTy IndD TyArgs, + mRRmK-db IndS IndD MRRMKS, + if (Ind = IndD) + (MRRMK = MRRMKS) + (feed-mRRmK-type TyArgs MRRMKS MRRMK), + find-mRRmK STys DTys IndTy MRRMKs. + +% 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. +% Argno, InjKs +pred mkBranch i:term, i:term, i:int, i:term, i:term, i:term, i:term, i:list term, o:term. +mkBranch KS KD N KTyR ITyTy Goal KR InjKs Eq:- + type-of-args KTyR N SrcArgs DestArgs, + whd ITyTy [] Hd TyArgs, + find-mRRmK SrcArgs DestArgs Hd MRRMKS, + % for every type dest add mRRmK to a list. + process-args KS KD N N {std.length TyArgs} KTyR Goal ITyTy KR InjKs MRRMKS [] Eq. + +pred mkBranches i:list term, i:list term, i:list term, i:list term, i:term, i:term, +i:list term, i:list (list term), o:list term. +mkBranches [] [] [] [] _ _ [] [] []. +mkBranches [KS|KsS] [KD|KsD] [KTy|KTys] [KTyR|KTyRs] ITyTy Goal [KR|KRs] [InjKs|InjKss] [R|Rs] :- + mkBranch KS KD {coq.count-prods KTy} KTyR ITyTy Goal KR InjKs R, + mkBranches KsS KsD KTys KTyRs ITyTy Goal KRs InjKss Rs. + +pred for-K-get-injKs i:int, i:list constructor, i:list term, o: list int, o:list (list term). +for-K-get-injKs TyParamNo KNs KTys ArgsNos InjKss :- + F = (grk\ i\ p\ injectionsK-db {coq.env.global (indc grk)} i p), + for-K-get-KI TyParamNo KNs KTys F ArgsNos InjKss. + +pred implement-mRRmK i:int, i:term, i:list term, i:list term, i:list term, i:list term, i:term, i:term, i:list term, i:list (list term), o:term. +% Pred comes with Type parameters applied +% RInd comes with Type parameters applied +% mRRmK +implement-mRRmK 0 (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) ar\ (Bo i1 i2 ar)) KsS KsD KTys KTyRs Pred RInd KRs InjKss + (fix `f` 2 RT f\ fun IN1 ITy1 i1\ fun IN2 ITy2 i2\ fun ARN (ARTy i1 i2) ar\ (Re f i1 i2 ar)) :- + coq.safe-dest-app ITy1 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\ + % to implement non uniformity change f's RT + db entry for Ind *) + (mRRmK-db Ind Ind f => + mkBranches KsS KsD KTys KTyRs ITy2 Pred KRs InjKss (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), + coq.elaborate-skeleton (R f i1 i2 ar) _ (Re f i1 i2 ar) ok. +implement-mRRmK 0 (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) _) KsS KsD KTys KTyRs Pred RInd KRs InjKss + (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 KRs InjKss Brs, + std.append Brs [i1,i2,ar] (IndArgs i1 i2 ar), + coq.mk-app RIndP (IndArgs i1 i2 ar) (R i1 i2 ar). +implement-mRRmK N (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 KRs InjKss + (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 : A1 -> A2 -> Type + @pi-decl AMN (AMTy a1 a2 ar) am\ % Map4.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), + 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), + std.map KRs (x\ r\ sigma TMP\ coq.mk-app x [a1,a2,ar] TMP, r = TMP) (NewKRs a1 a2 ar), + + MRRMK = pglobal {{:gref lib:trocq.map4.r_in_mapk }} _, + coq.mk-app MRRMK [a1, a2, ar, am] (MRRMKS a1 a2 ar am), + coq.typecheck (MRRMKS a1 a2 ar am) _ ok, + ar-db a1 a2 ar ==> + mRRmK-db a1 a2 (MRRMKS a1 a2 ar am) ==> + implement-mRRmK M (Bo a1 a2 ar am) (NewKsS a1) (NewKsD a2) (NewKTys a2) (NewKTyRs a1 a2 ar) (NewPred a1 a2 ar am) (NewRInd a1 a2 ar) (NewKRs a1 a2 ar) InjKss (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, + param Ind Ind TR, + coq.typecheck TR TRTy ok, + mymap-def (indt GR) IndMapGR, + coq.env.global IndMapGR IndMap, + coq.env.global {mR-def (indt GR)} MR, + coq.env.global {rm-def (indt GR)} RM, + mk-mR-type-mRRmK TyParamNo TRTy IndMap TR MR RM MRTy, + (@keepunivs! => coq.elaborate-skeleton MRTy _ MRTyE ok), + 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 _ _ _ _ KNRs KTyRs, + std.map KNs (x\ r\ r = {coq.env.global (indc x)}) Ks, + std.map KNRs (x\ r\ r = {coq.env.global (indc x)}) KRs, + for-K-get-injKs TyParamNo KNs KTys _ InjKss, + implement-mRRmK TyParamNo MRTyE Ks Ks KTys KTyRs Pred {coq.env.global RInd} KRs InjKss R, + (@keepunivs! => coq.elaborate-skeleton R MRTyE Re ok), + Name is Prefix ^ "mRRmK", + coq.ensure-fresh-global-id Name FName, + @dropunivs! => coq.env.add-const FName Re MRTyE _ C, + Clauses = [mRRmK-done GR, (mRRmK-def (indt GR) (const C)) ], + std.forall Clauses (x\ + coq.elpi.accumulate _ "derive.mRRmK.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/mapn.elpi b/elpi/inductives/mapn.elpi new file mode 100644 index 00000000..c6129f8e --- /dev/null +++ b/elpi/inductives/mapn.elpi @@ -0,0 +1,106 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.algo-utils.{gen-names-map}. +namespace derive.mapn { + +% TyParamNo +% Arity +% Ind +% IndR +% TyArgs1 +% TyArgs2 +% ARArgs +pred mk-mapn-type-priv i:int, i:term, i:term, i:term, i:term, i:term, o:term. +mk-mapn-type-priv 0 _ IndL IndR Rel MTy {{ lp:MTy lp:IndL lp:IndR lp:Rel}}. +mk-mapn-type-priv N (prod TN Ty t\ (Bo t)) IndL IndR Rel MTy + (prod TN1 Ty t1\ prod TN2 Ty t2\ prod TRN (ARTy t1 t2) ar\ prod URN (UMTy t1 t2 ar) ur\ (R t1 t2 ar ur)) :- + M is N - 1, + gen-names-map TN TN1 TN2 TRN URN, + @pi-decl TN1 Ty t1\ + @pi-decl TN2 Ty t2\ + (ARTy t1 t2) = {{ lp:t1 -> lp:t2 -> Type }}, + @pi-decl TRN (ARTy t1 t2) ar\ + (UMTy t1 t2 ar) = {{ lp:MTy lp:t1 lp:t2 lp:ar }}, + @pi-decl URN (UMTy t1 t2 ar) ur\ + coq.mk-app IndL [t1] (NIndL t1), + coq.mk-app IndR [t2] (NIndR t2), + coq.mk-app Rel [t1,t2,ar] (NRel t1 t2 ar), + mk-mapn-type-priv M (Bo t1) (NIndL t1) (NIndR t2) (NRel t1 t2 ar) MTy (R t1 t2 ar ur). + +% TyParamNo Arity Ind MapTy Rel +pred mk-mapn-type i:int, i:term, i:term, i:term, i:term, o:term. +mk-mapn-type TyParamNo Arity Ind Rel MTy R :- + mk-mapn-type-priv TyParamNo Arity Ind Ind Rel MTy R. + +% TyParamNo MapnTy IndL IndR Rel listReqs IndMap MR RM MRRMK +pred implement-mapn i:int, i:term, i:term, i:term, i:term, i: list term, i:term, o:term. +implement-mapn 0 _ IndL IndR Rel Reqs BH R :- + coq.mk-app BH [IndL,IndR,Rel | Reqs] R. +implement-mapn N (prod TN1 Ty1 t1\ prod TN2 Ty2 t2\ prod TRN (ARTy t1 t2) ar\ prod URN (UMTy t1 t2 ar) ur\ (Bo t1 t2 ar ur)) IndL IndR Rel Reqs BH (fun TN1 Ty1 t1\ fun TN2 Ty2 t2\ fun TRN (ARTy t1 t2) ar\ fun URN (UMTy t1 t2 ar) ur\ (R t1 t2 ar ur)) :- + M is N - 1, + @pi-decl TN1 Ty1 t1\ + @pi-decl TN2 Ty2 t2\ + @pi-decl TRN (ARTy t1 t2) ar\ + @pi-decl URN (UMTy t1 t2 ar) ur\ + coq.mk-app IndL [t1] (NIndL t1), + coq.mk-app IndR [t2] (NIndR t2), + coq.mk-app Rel [t1,t2,ar] (NRel t1 t2 ar), + std.map Reqs (x\ r\ sigma TMP\ coq.mk-app x [t1,t2,ar,ur] TMP, r = TMP) (NewReqs t1 t2 ar ur), + implement-mapn M (Bo t1 t2 ar ur) (NIndL t1) (NIndR t2) (NRel t1 t2 ar) + (NewReqs t1 t2 ar ur) BH (R t1 t2 ar ur). + +pred build-has-of i:map-class, o:gref. +build-has-of M R :- + coq.locate {calc ("Map" ^ {map-class.to_string M} ^ ".BuildHas")} R. + +pred map-reqs i:map-class, i:gref, o: list gref. +map-reqs map0 _ []. +map-reqs map1 Ind [IndMap] :- + std.assert! (mymap-def Ind IndMap) "derive.mapn: use derive.mymap before". +map-reqs map2a Ind [MR | M1] :- + map-reqs map1 Ind M1, + std.assert! (mR-def Ind MR) "derive.mapn: use derive.mR before". +map-reqs map2b Ind [RM | M1] :- + map-reqs map1 Ind M1, + std.assert! (rm-def Ind RM) "derive.mapn: use derive.Rm before". +map-reqs map3 Ind [RM | M2a] :- + map-reqs map2a Ind M2a, + std.assert! (rm-def Ind RM) "derive.mapn: use derive.Rm before". +map-reqs map4 Ind [MRRMK | M3] :- + map-reqs map3 Ind M3, + std.assert! (mRRmK-def Ind MRRMK) "derive.mapn: use derive.MRRMK before". + +pred implement-mapM i:map-class, i:inductive, o: term. +implement-mapM M GR RMapn :- + coq.env.indt GR _ TyParamNo _ Arity _ _, + coq.env.global (indt GR) Ind, + std.assert! (param Ind Ind IndR) "derive.mapn: use derive.param2 before", + std.rev {map-reqs M (indt GR)} ReqsGR, + std.map ReqsGR (x\ r\ r = {coq.env.global x}) Reqs, + + trocq.db.map->class M UM, + build-has-of M BH4, + % todo: address universe polymorphism + mk-mapn-type TyParamNo Arity Ind IndR (pglobal UM _) MapnTySkel, + std.assert-ok! (coq.elaborate-skeleton MapnTySkel _ MapnTy) "derive.mapn generates illtyped type", + implement-mapn TyParamNo MapnTy Ind Ind IndR Reqs (pglobal BH4 _) RMapnSkel, + std.assert-ok! (coq.elaborate-skeleton RMapnSkel _ RMapn) "derive.mapn generates illtyped term". + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + std.fold {map-class.all-of-kind all} [] (M\ C\ C'\ sigma RMapn NameMapn FNameMapn CMapn Entry\ + implement-mapM M GR RMapn, + NameMapn is Prefix ^ "map" ^ {map-class.to_string M}, + coq.ensure-fresh-global-id NameMapn FNameMapn, + coq.env.add-const FNameMapn RMapn _ _ CMapn, + Entry = trocq.db.map-def (indt GR) M (const CMapn), + coq.elpi.accumulate _ "trocq.db" (clause _ _ Entry), + C' = [Entry | C] + ) MClauses, + DEntry = (trocq.db.map-ind-done GR), + coq.elpi.accumulate _ "trocq.db" (clause _ _ DEntry), + Clauses = [DEntry | MClauses], +]. + +} \ No newline at end of file diff --git a/elpi/inductives/mymap.elpi b/elpi/inductives/mymap.elpi new file mode 100644 index 00000000..292c6daa --- /dev/null +++ b/elpi/inductives/mymap.elpi @@ -0,0 +1,220 @@ +/* map over a container */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ + +shorten std.{split-at, length, rev, append, do!, drop-last, assert!}. + +mymap-db (app[ A1HD|A1]) (app[ A2HD |A2]) R :- + coq.env.global (indt GR1) A1HD, + coq.env.global (indt GR2) A2HD, + coq.env.indt GR1 _ Lno1 _ _ _ _, + coq.env.indt GR2 _ Lno2 _ _ _ _, + {length A1} > Lno1, {length A2} > Lno2, + split-at Lno1 A1 Args1 Points1, + split-at Lno2 A2 Args2 Points2, + Points1 = Points2, !, + mymap-db {coq.mk-app A1HD Args1} {coq.mk-app A2HD Args2} F, + coq.mk-app F Points1 R. + +namespace derive.mymap { + +% Building the body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred bo-idx + i:term, % inductive arity (input) + i:term, % inductive type (input) applied to params & idx handled so far + i:term, % inductive type (output) applied to params & idx handled so far + i:int, % current index no + o:int, % Recno + i:list term, % rev list of (output) parameters + o:term, % body + o:term. % type + +bo-idx (prod _ S1 T1) Ity1 Ity2 N M Ps (fun `x` S1 Bo) (prod `x` S1 Ty) :- !, + pi x\ sigma Ity1x Ity2x\ + coq.mk-app Ity1 [x] Ity1x, + coq.mk-app Ity2 [x] Ity2x, + N1 is N + 1, + decl x `x` S1 => bo-idx (T1 x) Ity1x Ity2x N1 M Ps (Bo x) (Ty x). + +bo-idx (sort _) Ity1 Ity2 N N Ps (fun `x` Ity1 Bo) (prod `_` Ity1 _\ Ity2) :- !, + @pi-decl `x` Ity1 x\ + coq.safe-dest-app Ity1 IndT _, + coq.env.global GR IndT, + coq.build-match x Ity1 (bo-idx-rty Ps Ity2) (bo-k-args Ps GR) (Bo x). + +bo-idx X Ity1 Ity2 N M Ps R1 R2 :- whd1 X X1, !, + bo-idx X1 Ity1 Ity2 N M Ps R1 R2. + +pred bo-idx-rty i:list term, i:term, i:term, i:list term, i:list term, o:term. +bo-idx-rty Ps ItyArgs _ Vs _ R :- + rev Vs [_|IdxsRev], + rev IdxsRev Idxs, + coq.safe-dest-app ItyArgs HD _, + coq.mk-app HD {append {rev Ps} Idxs} R. + +pred bo-k-args i:list term, i:gref, i:term, i:term, i:list term, i:list term, o:term. +bo-k-args ParamsRev IndGR K _ Args Tys R :- + rev ParamsRev Params, + coq.safe-dest-app K KB _, + coq.env.global (indc GR) KB, + coq.env.typeof (indc GR) T, coq.subst-prod Params T KT, + (bo-k-args.aux {coq.mk-app {coq.env.global (indc GR)} Params} IndGR Args Tys KT R), + !. % the first combination that typechecks + +pred bo-k-args.aux i:term, i:gref, i:list term, i:list term, i:term, o:term. +bo-k-args.aux R _ [] [] _ R :- coq.typecheck R _ ok. +bo-k-args.aux K IndGR [A|As] [T|Ts] (prod _ S Ty) R :- + mymap-db T S F, + coq.mk-app F [A] FA, + bo-k-args.aux {coq.mk-app K [FA]} IndGR As Ts (Ty FA) R. +bo-k-args.aux K IndGR [A|As] [T|Ts] (prod _ _ Ty) R :- + coq.safe-dest-app T IndT _, + coq.env.global IndGR IndT, !, + mymap-db IndT IndT F, + coq.mk-app F [A] FA, + bo-k-args.aux {coq.mk-app K [FA]} IndGR As Ts (Ty FA) R. +bo-k-args.aux K IndGR [A|As] [_|Ts] (prod _ _ Ty) R :- !, + bo-k-args.aux {coq.mk-app K [A]} IndGR As Ts (Ty A) R. +bo-k-args.aux K IndGR As Ts X R :- whd1 X X1, !, + bo-k-args.aux K IndGR As Ts X1 R. + + +% Take in input a mapping function for each parameter +% and then do the fixpoint + +pred bo-params + i:int, % current parameter + i:int, % number of parameters + i:term, % inductive type (input) applied to parameters handled so far + i:term, % inductive type (output) applied to parameters handled so far + i:term, % inductive arity (input) + i:term, % inductive arity (output) + i:list term, % output parameters so far + o:term. % map function + +bo-params Lno Lno Ity1 Ity2 A1 _ Ps (fix `f` Recno Fty Bo) :- + coq.safe-dest-app Ity1 Ind _, + coq.env.global (indt I) Ind, + coq.env.recursive? I, !, + @pi-decl `rec` Fty f\ + mymap-db Ind Ind f => + bo-idx A1 Ity1 Ity2 0 Recno Ps (Bo f) Fty. +bo-params Lno Lno Ity1 Ity2 A1 _ Ps Bo :- !, + bo-idx A1 Ity1 Ity2 0 _ Ps Bo _. + +bo-params N Lno Ity1 Ity2 (prod A Sty1 Rty1) (prod _ Sty2 Rty2) Ps R :- + coq.name-suffix A 1 A1, + coq.name-suffix A 2 A2, + coq.name-suffix A "r" Ar, + coq.name-suffix A "f" Af, + N1 is N + 1, + (pi a b r f \ mk-map-ty a Sty1 b Sty2 (RAB a b) r (FAB a b r) f _ (Clause a b r f)), + R = (fun A1 Sty1 a\ fun A2 Sty2 b\ fun Ar (RAB a b) r\ fun Af (FAB a b r) f\ Bo a b r f), + @pi-decl A1 Sty1 a\ + @pi-decl A2 Sty2 b\ + coq.elaborate-skeleton (RAB a b) _ (RABTy a b) ok, + coq.mk-app Ity1 [a] (Ity1A a), + coq.mk-app Ity2 [b] (Ity2A b), + @pi-decl Ar (RABTy a b) r\ + coq.elaborate-skeleton (FAB a b r) _ (FABTy a b r) ok, + pi f\ + decl f Af (FABTy a b r) =!=> + Clause a b r f =!=> + (mymap-db a b (FAB a b r)==> + bo-params N1 Lno (Ity1A a) (Ity2A b) (Rty1 a) (Rty2 b) [b|Ps] (Bo a b r f)). + +bo-params N Lno Ity1 Ity2 T OT Ps R :- + whd1 T T1, whd1 OT OT1, !, + bo-params N Lno Ity1 Ity2 T1 OT1 Ps R. + +bo-params _ _ _ _ _ _ _ _ :- + stop "derive.mymap: Indexed data types not supported". + +pred map-pi i:any, o:list prop. +map-pi (x\ []) []. +map-pi (x\ [X x| XS x]) [pi x\ X x | YS] :- map-pi XS YS. + +pred mk-map-ty + i:term, % input variable + i:term, % and its type + i:term, % output variable + i:term, % an its type + o:term, % type of relation input -> ouput -> type + i:term, % a term of type above + o:term, % type of a mapping function from input to output + i:term, % map function (having the type above) + o:int, % arity of the predicate + o:list prop. % mymap-db clause for map function +mk-map-ty A (prod _ SA T1) B (prod _ SB T2) RelTy RTerm (prod `x` SA x\ R x) F N C1 :- + mymap-db SA SB Fa, !, + (pi x\ sigma Ax Fx BFx \ + coq.mk-app A [x] Ax, coq.mk-app Fa [x] Fx, coq.mk-app B [Fx] BFx, + mk-map-ty Ax (T1 x) BFx (T2 BFx) RelTy RTerm (R x) {coq.mk-app F [x]} M (C x), + N is M + 1), + map-pi C C1. +mk-map-ty A (prod _ S1 T1) B (prod _ _ T2) RelTy RTerm (prod `x` S1 x\ R x) F N C1 :- + (pi x\ sigma Ax Bx \ coq.mk-app A [x] Ax, coq.mk-app B [x] Bx, + mk-map-ty Ax (T1 x) Bx (T2 x) RelTy RTerm (R x) {coq.mk-app F [x]} M (C x), + N is M + 1), + map-pi C C1. +mk-map-ty (app[X|XS] as A) _ (app[Y|YS] as B) _ (prod `x` A _\ B) _ _ (app [G|GS] as F) 0 [mymap-db PLA PLB PLF,mymap-db A B F] :- + drop-last 1 XS LA, + drop-last 1 YS LB, + drop-last 1 GS LF, + coq.mk-app X LA PLA, + coq.mk-app Y LB PLB, + coq.mk-app G LF PLF. +mk-map-ty A _ B _ RelTy RTerm Map F 0 [mymap-db A B {{ lp:M1mTerm lp:A lp:B _ lp:F }} ] :- + coq.env.global {{:gref lib:trocq.map1.map }} M1mTerm, + RelTy = {{ lp:A -> lp:B -> Type }} , + Map = {{ lib:trocq.map1 lp:RTerm }}. + + +% mk-map-ty A _ B _ (prod `x` A _\ B) F 0 [mymap-db A B F]. + +% Build a clause %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred mk-clause + i:int, % current parameter + i:int, % number of parameters + i:term, % inductive type (input) + i:term, % inductive type (output) + i:term, % arity of the inductive + i:list prop, % premises of the clause + i:term, % map function + o:prop. % clause for mymap-db +mk-clause N N Ity1 Ity2 _ Todo Map (mymap-db Ity1 Ity2 Map :- Todo). +mk-clause N Lno Ity1 Ity2 (prod _ _ T) Todo Map (pi x y f\ C x y f) :- !, + N1 is N + 1, + pi x y f\ sigma Ity1x Ity2y Mapf\ + coq.mk-app Ity1 [x] Ity1x, + coq.mk-app Ity2 [y] Ity2y, + coq.mk-app Map [x,y,f] Mapf, + mk-clause N1 Lno Ity1x Ity2y (T x) [mymap-db x y f|Todo] Mapf (C x y f). +mk-clause N Lno Ity1 Ity2 X Todo Map C :- whd1 X X1, !, + mk-clause N Lno Ity1 Ity2 X1 Todo Map C. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +func main inductive, string -> list prop. +main GR Prefix C :- do! [ + coq.env.global (indt GR) T, + coq.env.indt GR _Ind Lno Luno Arity _ _, + assert! (Lno = Luno) "derive.mymap: Non-uniform parameters not supported", + + % generate map and add to the env + (bo-params 0 Lno T T Arity Arity [] RSkel), + std.assert-ok! (coq.elaborate-skeleton RSkel Rty R) "derive.mymap generates illtyped term", + Name is Prefix ^ "mymap", + coq.ensure-fresh-global-id Name FName, + coq.env.add-const FName R Rty @transparent! Funct, + + % generate clause and add to the db + mk-clause 0 Lno T T Arity [] (global (const Funct)) Clause, + coq.elpi.accumulate _ "derive.mymap.db" (clause _ _ (mymap-def (indt GR) (const Funct))), + coq.elpi.accumulate _ "derive.mymap.db" (clause _ _ Clause), + coq.elpi.accumulate _ "derive.mymap.db" (clause _ _ (mymap-done GR)), + C = [mymap-done GR,Clause, (mymap-def (indt GR) (const Funct))] +]. + +} \ No newline at end of file diff --git a/elpi/inductives/relnm.elpi b/elpi/inductives/relnm.elpi new file mode 100644 index 00000000..d19ed64f --- /dev/null +++ b/elpi/inductives/relnm.elpi @@ -0,0 +1,91 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.algo-utils.{type-of-args, whd-fuel, iota-step, invert-eqs, rewrite-with}. +shorten derive.common-algo.{mk-mR-type-relnm,sym-tyargs}. + +namespace derive.relnm { + +pred refine-covariant-tyargs i: list term, i:term, i:list term, o: list term. +refine-covariant-tyargs [] _ L L. +refine-covariant-tyargs [A1, A2, AR | L2] Refiner Acc R :- + coq.mk-app Refiner [A1,A2,AR] Refined, + std.append Acc [A1, A2, AR, Refined] NewAcc, + refine-covariant-tyargs L2 Refiner NewAcc R. + +pred refine-Lsym i: list term, i:list term, i:term, i:list term, o: list term. +refine-Lsym [] [] _ L L. +refine-Lsym [A1, A2, AR | L2] [_,_,_,Refined | L2Ref] Refiner Acc R :- + coq.safe-dest-app Refined _ Lref, + coq.mk-app Refiner Lref RefinedContra, + std.append Acc [A1, A2, AR, RefinedContra] NewAcc, + refine-Lsym L2 L2Ref Refiner NewAcc R. + +% TyargNo, relnm Type, mapnCov, mapmContra, eq_map, rsymK, list of args +pred implement-relnm i:int, i:term, i:term, i:term, i:term, i:term, i:term, i:term, i:term, i:list term, o:term. +implement-relnm 0 _ + MapNCov MapMContra Eq_map RsymK CovariantNN ContravariantNN BuildNN LRev R :- + !, + std.rev LRev L, + refine-covariant-tyargs L CovariantNN [] LCo, + sym-tyargs L LSym, + refine-Lsym LSym LCo ContravariantNN [] LContra, + coq.mk-app MapNCov LCo MapCovariant, + coq.mk-app MapMContra LContra MapContravariant, + coq.mk-app RsymK LSym RsymKSym, + R = {{ lp:BuildNN _ _ _ lp:MapCovariant (lp:Eq_map lp:RsymKSym lp:MapContravariant )}}. +implement-relnm N (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) + MapNCov MapMContra Eq_map RsymK CovariantNN ContravariantNN BuildNN L + (fun AN1 ATy1 a1\ fun AN2 ATy2 a2\ fun ARN (ARTy a1 a2) ar\ (R a1 a2 ar)) :- + 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 : ParamNM.Rel A1 A2 + sigma NewL\ + std.append [ar,a2,a1] L NewL, + implement-relnm M (Bo a1 a2 ar) MapNCov MapMContra Eq_map RsymK CovariantNN ContravariantNN BuildNN NewL (R a1 a2 ar). + +pred get-eq-map i:map-class, o:term. +get-eq-map map0 {{ lib:trocq.eq_map0 }}. +get-eq-map map1 {{ lib:trocq.eq_map1 }}. +get-eq-map map2a {{ lib:trocq.eq_map2a }}. +get-eq-map map2b {{ lib:trocq.eq_map2b }}. +get-eq-map map3 {{ lib:trocq.eq_map3 }}. +get-eq-map map4 {{ lib:trocq.eq_map4 }}. + +pred generate-relNM i:inductive, i:param-class, o: term, o: term. +generate-relNM GR (pc N M as PC) ReTy Re :- + coq.env.indt GR _ TyParamNo _ _ _ _, + coq.env.global (indt GR) Ind, + std.assert! (param Ind Ind TR) "derive.relNM: use derive.param2 before", + coq.typecheck TR TRTy ok, + trocq.db.rel PC PRelNM BuildNM _ CovNM ContraNM, + mk-mR-type-relnm TyParamNo TRTy TR (pglobal PRelNM _) RTy, + std.assert-ok! (coq.elaborate-skeleton RTy _ ReTy) "derive.relNM generates illtyped type", + std.assert! (trocq.db.map-ind Ind N UmapNCov) "derive.relNM: use derive.umap before", + std.assert! (trocq.db.map-ind Ind M UmapMContra) "derive.relNM: use derive.umap before", + std.assert! (rsymK-db Ind RSymKInd) "derive.relNM: use derive.rsymK before", + get-eq-map M Eq_map, + implement-relnm TyParamNo ReTy UmapNCov UmapMContra Eq_map RSymKInd (pglobal CovNM _) (pglobal ContraNM _) (pglobal BuildNM _) [] R, + std.assert-ok! (coq.elaborate-skeleton R ReTy Re) "derive.relNM generates illtyped term". + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + coq.env.global (indt GR) I, + std.fold {param-class.all-of-kind all} [] + (PC\ Cls\ Cls'\ + sigma N M C ReTy Re Name FName\ + (pc N M) = PC, + generate-relNM GR PC ReTy Re, + Name is Prefix ^ "rel" ^ {map-class.to_string N} ^ {map-class.to_string M}, + coq.ensure-fresh-global-id Name FName, + coq.env.add-const FName Re ReTy _ C, + Cls' = [trocq.db.param-ind I PC (global (const C))| Cls]) + RCls, + Clauses = [trocq.db.param-ind-done GR | RCls], + std.forall Clauses (x\ + coq.elpi.accumulate _ "trocq.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/sym.elpi b/elpi/inductives/sym.elpi new file mode 100644 index 00000000..83f77021 --- /dev/null +++ b/elpi/inductives/sym.elpi @@ -0,0 +1,125 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.common-algo.{mk-mR-type-sym}. +shorten derive.algo-utils.{cmp-indt}. + +namespace derive.sym { + +% [|K|], remaining args, number of type args, KRTy, Type of args Ksource, Type of args KDest, Goal, +pred process-args i:term, i:int, i:int, i:term, i:term, i:term, o:term. +process-args KR 0 _ _ _ _ KR. +process-args KR N _TyArgsNo (prod AN1 A1Ty a1\ prod AN2 A2Ty a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) Goal 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\ + cmp-indt A1Ty ITyTy A1IndT Ind, + sym-db A1IndT SymC, + coq.mk-app SymC [a1,a2,ar] (RA a1 a2 ar), + coq.mk-app KR [a2,a1,(RA a1 a2 ar)] (NewKR a1 a2 ar), + (param a2 a1 ar =!=> + process-args (NewKR a1 a2 ar) M _ (Bo a1 a2 ar) Goal ITyTy (R a1 a2 ar)), + % if the type of the argument is an instance of the inductive type add an induction hypothesis + if (Ind = A1IndT) + (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 R, 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:int, i:term, i:term, i:term, o:term. +mkBranch KR N KTyR ITyTy Goal Eq:- + whd ITyTy [] _ TyArgs, + process-args KR N {std.length TyArgs} KTyR Goal ITyTy Eq. + +pred mkBranches i:list term, i:list term, i:list term, i:term, i:term o:list term. +mkBranches [] [] [] _ _ []. +mkBranches [KR|KRs][KTy|KTys] [KTyR|KTyRs] ITyTy Goal [R|Rs] :- + mkBranch KR {coq.count-prods KTy} KTyR ITyTy Goal R, + mkBranches KRs KTys KTyRs ITyTy Goal Rs. + +pred implement-sym i:int, i:int, i: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-sym 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) ar\ (Bo i1 i2 ar)) KRs 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\ + (sym-db Ind f => + mkBranches KRs 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-sym 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) _) KRs 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 KRs 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-sym N TyParamNo (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) KRs KTys KTyRs Pred RInd + (fun AN1 ATy1 a1\ fun AN2 ATy2 a2\ fun ARN (ARTy a1 a2) ar\ (R a1 a2 ar)) :- + 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 : Param00.Rel A1 A2 + coq.mk-app Pred [a1,a2,ar] (NewPred a1 a2 ar), + + (ARType a1 a2) = {{ lp:a1 -> lp:a2 -> Type }}, + coq.elaborate-skeleton ar (ARType a1 a2) (RelAR a1 a2 ar) ok, + coq.elaborate-skeleton {{ sym_rel lp:{{ RelAR a1 a2 ar }} }} (ARType a2 a1) (RelRA a1 a2 ar) ok, + + coq.mk-app RInd [a1,a2,ar] (NewRIndSkel a1 a2 ar), + coq.elaborate-skeleton (NewRIndSkel a1 a2 ar) _ (NewRInd a1 a2 ar) ok, + + std.map KRs (x\ r\ sigma TMP\ coq.mk-app x [a2,a1, (RelRA a1 a2 ar)] TMP, r = TMP) (NewKRs a1 a2 ar), + + 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,(RelAR a1 a2 ar)] x TMP1, r = TMP1) (NewKTyRs a1 a2 ar), + Sym = {{ @sym_rel }}, + coq.mk-app Sym [a1, a2, ar] (SymApp a1 a2 ar), + (SymFun a1 a2 ar) = {{ fun (a1 : lp:{{a1}}) (a2 : lp:{{a2}}) (ar : lp:{{SymApp a1 a2 ar}})=> ar }}, + sym-db a1 (SymFun a1 a2 ar) ==> + implement-sym M TyParamNo (Bo a1 a2 ar) (NewKRs a1 a2 ar) (NewKTys a2) (NewKTyRs a1 a2 ar) (NewPred a1 a2 ar) (NewRInd a1 a2 ar) (R a1 a2 ar). + +func main inductive, string -> list prop. +main GR Prefix Clauses :- std.do! [ + + coq.env.indt GR _ TyParamNo _ _ _ KTys, + coq.env.global (indt GR) Ind, + std.assert! (param Ind Ind TR) "derive.sym: use derive.param2 before", + coq.env.global (indt GRR) TR, + coq.gref->id (indt GRR) Rname, + coq.env.indt GRR _ _ _ TRTy KRNs KTyRs, + + mk-mR-type-sym TyParamNo TRTy TR MRTy, + std.assert-ok! (coq.elaborate-skeleton MRTy _ MRTyE) "derive.sym generates illtyped type", + RInductionName is Rname ^ "_rect", + coq.locate RInductionName RInd, + coq.env.global RInd RIndT, + coq.prod->fun MRTyE Pred, + std.map KRNs (x\ r\ sigma TMP\ coq.env.global (indc x) TMP, r = TMP) KRs, + implement-sym TyParamNo TyParamNo MRTyE KRs KTys KTyRs Pred RIndT R, + std.assert-ok! (coq.elaborate-skeleton R MRTyE Re) "derive.sym generates illtyped term", + Name is Prefix ^ "sym", + coq.ensure-fresh-global-id Name FName, + coq.env.add-const FName Re MRTyE _ C, + Clauses = [sym-done GR, sym-def (indt GR) (const C)], + std.forall Clauses (x\ + coq.elpi.accumulate _ "derive.sym.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/symK.elpi b/elpi/inductives/symK.elpi new file mode 100644 index 00000000..9cdcb684 --- /dev/null +++ b/elpi/inductives/symK.elpi @@ -0,0 +1,170 @@ +accumulate "Trocq.Elpi.inductives/common_algo". +accumulate "Trocq.Elpi.inductives/utils". + +shorten derive.algo-utils.{type-of-args, whd-fuel, iota-step, invert-eqs, rewrite-with}. +shorten derive.common-algo.{mk-mR-type-symK}. +shorten derive.algo-utils.{cmp-indt}. + +namespace derive.symK { + +% delta delta iota +pred red-symK i:term, i:stack, o:term,o:stack. +red-symK X C R RS :- + whd-fuel X C 2 XX CC, + iota-step XX CC R RS. + +pred pierce-goal-symK i:int, i:int, i:int, i:term, i: list term, o: list term, o: term. +pierce-goal-symK _ N N Goal [] [] Goal. +pierce-goal-symK TyParamNo N InitArgs CurrentGoal [Eq|Eqs] [Pat|Pats] EndGoal :- + M is N + 1, + coq.safe-dest-app CurrentGoal EqGoal [EqGoalTy,GoalLHS,GoalRHS], + coq.safe-dest-app GoalLHS KR Args, + Done is (TyParamNo * 3) + N * 3, + std.split-at Done Args L [A1,A2, SymSym | R], + coq.typecheck SymSym Ty ok, + (pi t\ + coq.mk-app KR {std.append L {std.append [A1, A2, t] R}} (NewKR t), + coq.mk-app EqGoal [EqGoalTy,(NewKR t),GoalRHS] (NewEqGoal t)), + Pat = (fun `t` Ty t\ (NewEqGoal t)), + coq.typecheck Eq EqTy ok, + coq.safe-dest-app EqTy _ [_,LHS,_], + coq.mk-app Pat [LHS] NewGoal, + pierce-goal-symK TyParamNo M InitArgs NewGoal Eqs Pats EndGoal. + +% [|K|], remaining args, number of type args, KRTy, Type of args Ksource, Type of args KDest, Goal, +pred process-args i:term, i:term, i:term, i:int,i:int, i:int, i:term, i:list term, i:term, i:term, o:term. +process-args KsS KsD KR 0 ArgNo TyArgsNo _ RevEqs Goal _ R:- + !, + std.rev RevEqs Eqs, + invert-eqs Eqs IEqs, + coq.mk-app Goal [KsS,KsD,KR] SubstGoal, + whd SubstGoal [] HD [IRTy,SymSymIR,IR], + red-symK SymSymIR [] KRHD KRArgs, + coq.mk-app KRHD KRArgs RedLHS, + coq.mk-app HD [IRTy,RedLHS,IR] StartingGoal, + pierce-goal-symK TyArgsNo 0 ArgNo StartingGoal IEqs PatsSym _, + End = {{ lib:@trocq.idpath lp:IRTy lp:IR }}, + rewrite-with IEqs PatsSym End R. + +process-args KsS KsD KR N O TyArgsNo (prod AN1 A1Ty a1\ prod AN2 A2Ty a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) Eqs Goal 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 KsS [a1] (NewKsS a1), + coq.mk-app KsD [a2] (NewKsD a2), + coq.mk-app KR [a1,a2,ar] (NewKR a1 a2 ar), + + cmp-indt A2Ty ITyTy IndD Ind, + symK-db IndD SymKA2, + coq.mk-app SymKA2 [a1, a2, ar] (SymKEq a1 a2 ar), + std.append [(SymKEq a1 a2 ar)] Eqs (NewEqs a1 a2 ar), + (param a2 a1 ar =!=> + process-args (NewKsS a1) (NewKsD a2) (NewKR a1 a2 ar) M O TyArgsNo (Bo a1 a2 ar) (NewEqs a1 a2 ar) Goal ITyTy (R a1 a2 ar)), + % if the type of the argument is an instance of the inductive type add an induction hypothesis + 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 R, 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:term, i:int, i:int, i:term, i:term, i:term, o:term. +mkBranch KsS KsD KR N M KTyR ITyTy Goal Eq:- + whd ITyTy [] _ TyArgs, + process-args KsS KsD KR N M {std.length TyArgs} KTyR [] Goal ITyTy Eq. + +pred mkBranches i:list term, i:list term, i:list term, i:list term, i:list term, i:term, i:term o:list term. +mkBranches [] [] [] [] [] _ _ []. +mkBranches [KsS|KsSs] [KsD| KsDs] [KR|KRs][KTy|KTys] [KTyR|KTyRs] ITyTy Goal [R|Rs] :- + coq.count-prods KTy ArgNo, + mkBranch KsS KsD KR ArgNo ArgNo KTyR ITyTy Goal RSkel, + (@keepunivs! => coq.elaborate-skeleton RSkel _ R ok), + mkBranches KsSs KsDs KRs KTys KTyRs ITyTy Goal Rs. + +pred implement-symK i:int, i:int, i:term, i:list 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-symK 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) ar\ (Bo i1 i2 ar)) KsS KsD KRs 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\ + (symK-db Ind f => + mkBranches KsS KsD KRs 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-symK 0 _TyParamNo (prod IN1 ITy1 i1\ prod IN2 ITy2 i2\ prod ARN (ARTy i1 i2) _) KsS KsD KRs 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 KRs 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-symK N TyParamNo (prod AN1 ATy1 a1\ prod AN2 ATy2 a2\ prod ARN (ARTy a1 a2) ar\ (Bo a1 a2 ar)) KsS KsD KRs KTys KTyRs Pred RInd + (fun AN1 ATy1 a1\ fun AN2 ATy2 a2\ fun ARN (ARTy a1 a2) ar\ (R a1 a2 ar)) :- + 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 : Param00.Rel A1 A2 + coq.mk-app Pred [a1,a2,ar] (NewPred a1 a2 ar), + + (ARType a1 a2) = {{ lp:a1 -> lp:a2 -> Type }}, + coq.elaborate-skeleton ar (ARType a1 a2) (RelAR a1 a2 ar) ok, + + coq.mk-app RInd [a1,a2,ar] (NewRIndSkel a1 a2 ar), + 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 KRs (x\ r\ sigma TMP\ coq.mk-app x [a1,a2, (RelAR a1 a2 ar)] TMP, r = TMP) (NewKRs a1 a2 ar), + + 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,(RelAR a1 a2 ar)] x TMP1, r = TMP1) (NewKTyRs a1 a2 ar), + + (SymFun a1 a2 ar) = {{ fun (a1 : lp:{{a1}}) (a2 : lp:{{a2}}) (ar : (lp:{{ar}} a1 a2))=> lib:@trocq.idpath (lp:{{ar}} a1 a2) ar }}, + symK-db a2 (SymFun a1 a2 ar) ==> + implement-symK M TyParamNo (Bo a1 a2 ar) (NewKsS a1) (NewKsD a2) (NewKRs a1 a2 ar) (NewKTys a2) (NewKTyRs a1 a2 ar) (NewPred a1 a2 ar) (NewRInd a1 a2 ar) (R a1 a2 ar). + +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! (param Ind Ind TR) "derive.sym: use derive.param2 before", + coq.typecheck TR TRTy ok, + std.assert! (sym-db Ind SymInd) "derive.sym: use derive.sym before", + mk-mR-type-symK TyParamNo TRTy TR SymInd SymKTy, + (@keepunivs! => std.assert-ok! (coq.elaborate-skeleton SymKTy _ SymKTyE) "derive.symK generates illtyped type"), + (@keepunivs! => coq.env.global (indt GRR) TR), + coq.gref->id (indt GRR) Rname, + RInductionName is Rname ^ "_rect", + coq.locate RInductionName RInd, + coq.prod->fun SymKTyE Pred, + coq.env.indt GRR _ _ _ _ KRNs KTyRs, + std.map KNs (x\ r\ r = {coq.env.global (indc x)}) Ks, + std.map KRNs (x\ r\ r = {coq.env.global (indc x)}) KRs, + implement-symK TyParamNo TyParamNo SymKTyE Ks Ks KRs KTys KTyRs Pred {coq.env.global RInd} R, + (@keepunivs! => std.assert-ok! (coq.elaborate-skeleton R SymKTyE Re) "derive.symK generates illtyped term"), + Name is Prefix ^ "symK", + coq.ensure-fresh-global-id Name FName, + (@dropunivs! => coq.env.add-const FName Re SymKTyE _ C), + Clauses = [symK-done GR, symK-def (indt GR) (const C)], + std.forall Clauses (x\ + coq.elpi.accumulate _ "derive.symK.db" (clause _ _ x) + ), +]. + +} \ No newline at end of file diff --git a/elpi/inductives/utils.elpi b/elpi/inductives/utils.elpi new file mode 100644 index 00000000..e23e552d --- /dev/null +++ b/elpi/inductives/utils.elpi @@ -0,0 +1,222 @@ +namespace derive.algo-utils { + +func names12 name -> name, name. +names12 N N1 N2 :- !, + coq.name-suffix N 1 N1, coq.name-suffix N 2 N2. + +pred gen-names-map i:name, o:name, o:name, o:name, o:name. +gen-names-map N N1 N2 NR NU :- + coq.name-suffix N 1 N1, + coq.name-suffix N 2 N2, + coq.name-suffix N "R" NR, + coq.name-suffix N "M" NU. + +pred name-prefix i: name, i:string, o:name. +name-prefix N P R :- + coq.name->id N NS, + S is P ^ NS, + coq.string->name S R. + +pred elim-into-path-suffix i:string, o:string. +elim-into-path-suffix Id Suff :- + (indt Eq) = {{:gref @lib:trocq.paths}}, + if ( Id = "paths") (Suff = "_nondep") + (coq.env.indt Eq _ _ _ (prod _ _ _\ (prod _ _ _\ (prod _ _ _\ sort S))) _ _, + if (S = prop) + (Suff = "_ind") + (Suff = "_rect")). + +% given TyParam ArgNo and T, +% duplicate-argument skips TyParam products, +% then for the first ArgNo products adds another product expecting an argument of the same Type, +% after all lambdas are processed returns the body unchanged +pred duplicate-arguments i:int, i:int, i:term, o:term. +duplicate-arguments 0 0 T T :- !. +duplicate-arguments 0 O (prod N TyA T) (prod Arg1 TyA a1\ (prod Arg2 TyA a2\ (S a1 a2))) :- + O > 0, + P is O - 1, + names12 N Arg1 Arg2, + (pi a1 a2\ duplicate-arguments 0 P (T a1) (S a1 a2)). +duplicate-arguments N O (prod TyName TyArg T) (prod TyName TyArg S) :- !, + N > 0, + M is N - 1, + pi a1\ duplicate-arguments M O (T a1) (S a1). + +pred count-args i:int, i:term, o:int. +count-args N T R :- + coq.count-prods T M, + R is M - N. + +% given list eta-src type, eta-RT, list of etas, list of src, list of dest, list of src = dest, +% builds the corresponding ap. +pred mk-aps-etas i:list term, i:term, i:list term, i:list term, i:list term, i:list term, o:list term. +mk-aps-etas [] _ [] [] [] [] []. +mk-aps-etas [DTy|DestTys] ITyTy [Eta|Etas] [SA|SrcArgs] [DA|DestArgs] [Eq|Eqs] [RE | RS] :- + Ap = {{ lib:@trocq.ap }}, + coq.mk-app Ap [DTy,ITyTy,Eta,SA,DA,Eq] R, + (@keepunivs! => coq.elaborate-skeleton R _ RE ok), + mk-aps-etas DestTys ITyTy Etas SrcArgs DestArgs Eqs RS. + +% K comes with type arguments already applied. +pred mk-ith-eta i:int, i:list term, i:list term, i:list term, i:term, o:term. +mk-ith-eta I MArgs DestArgs DestTys K FR :- + J is I - 1, + std.take J DestArgs Done, % list of args already processed. + std.drop I MArgs MTODO, % list of args to yet process + std.nth J DestTys CurrTy, + (pi curr\ + coq.mk-app K {std.append Done [curr|MTODO]} (KArgs curr)), + FR = fun `R` CurrTy (r\ (KArgs r)). + + +% KDest comes with the type arguments already applied. +pred mk-etas-priv i:list term, i:list term, i:list term, i:int, i:int, i: term, o:list term. +mk-etas-priv _ _ _ M N _ [] :- M > N. +mk-etas-priv SrcArgs DestArgs DestTys I N KDest [R| RS] :- + J is I + 1, + mk-ith-eta I SrcArgs DestArgs DestTys KDest R, + mk-etas-priv SrcArgs DestArgs DestTys J N KDest RS. + +pred mk-etas i:list term, i:list term, i:list term, i: term, o:list term. +mk-etas SrcArgs DestArgs TyDest KAppTyArgs REtas :- + mk-etas-priv SrcArgs DestArgs TyDest 1 {std.length DestArgs} KAppTyArgs REtas. + +pred compose-path i:list term, i:term, i:term o: term. +compose-path [] End _ End. +compose-path [Argk|Args] End ITy {{ lib:@trocq.concat lp:ITy _ _ _ lp:Argk lp:R }} :- + compose-path Args End ITy R. + +% List of src args, list of dest args and their types, K applied to type parameters, equalities src = dest, type of K TyParam Dest. +% returns (ap eta1 s1 d1 e1) @ ... @ ap etan sn dn en. +pred mk-chain i:list term, i:list term, i:list term, i:term, i:list term, i:term, i:term, o:term. +mk-chain SrcArgs DestArgs DestArgsTy K Eqs ITyTy RHS R :- + mk-etas SrcArgs DestArgs DestArgsTy K REtas, + mk-aps-etas DestArgsTy ITyTy REtas SrcArgs DestArgs Eqs Raps, + compose-path Raps {{ lib:@trocq.idpath lp:ITyTy lp:RHS }} ITyTy RSkel, + @keepunivs! => coq.elaborate-skeleton RSkel _ R ok. + +% pred name-ij i:string, i:int, i:int, i:inductive, i:constructor, i:list term, i: constructor -> int -> constant -> prop, o:list prop. +pred name-ij i:string, i:int, i:int, i:inductive, i:constructor, i:list term, i: (pred i:constructor, i:int, i:constant, o:list prop), o:list prop. +name-ij _ _ _ _ _ [] _ []. +name-ij FName I J GR Kn [InjTyS|InjTyss] F ClausesR :- + Jn is J + 1, + NameIJ is {std.any->string FName} ^ {std.any->string I} ^ {std.any->string J}, + (@dropunivs! => coq.elaborate-skeleton InjTyS _ InjTy ok), + (@dropunivs! => coq.env.add-const NameIJ InjTy _ _ C), + (F Kn J C Clauses), + name-ij FName I Jn GR Kn InjTyss F ClausesRec, + std.append Clauses ClausesRec ClausesR. + +% Prefix, current constructor, an inductive, its constructors, list of list of terms to name +pred name-ijs i:string, i:int, i:inductive, i:list constructor, i:list (list term), i: (pred i:constructor, i:int, i:constant, o:list prop), o:list (list prop). +% pred name-ijs i:string, i:int, i:inductive, i:list constructor, i:list (list term), i: constructor -> int -> constant -> prop, o:list (list prop). +name-ijs _ _ _ [] [] _ []. +name-ijs FName I GR [Kn | KNs] [InjTys | InjTyss] F [Clauses | Clausess] :- + In is I + 1, + name-ij FName I 1 GR Kn InjTys F Clauses, + name-ijs FName In GR KNs InjTyss F Clausess. + +% Returns the list of P of F K I P of a constructor. +pred get-KI i:constructor, i:int, i:int, i:(pred i:constructor, i:int, o:term), o:list term. +get-KI _ Max Max _ [] :- !. +get-KI GRK J Max F [P|PJs] :- + I is J + 1, + F GRK I P, + get-KI GRK I Max F PJs. + +% for a list of P of F K I for a list of constructors +pred for-K-get-KI i:int, i:list constructor, i:list term, +i:(pred i:constructor, i:int, o:term), +o: list int, o:list (list term). +for-K-get-KI _ [] [] _ [] []:- !. +for-K-get-KI TyParamNo [Kn|KNs] [KTy|KTys] F [ArgsNo|ArgsNos] [R|RS]:- + count-args TyParamNo KTy ArgsNo, + get-KI Kn 0 ArgsNo F R, + for-K-get-KI TyParamNo KNs KTys F ArgsNos RS. + +% from a type of shape 3*(forall (a1 : T1) (a2 : T2), AR a1 a2, ...) extracts list of T1 and T2 +pred type-of-args i:term, i:int, o:list term, o:list term. +type-of-args _ 0 [] []. +type-of-args (prod _ ATy1 a1\ prod _ ATy2 a2\ prod _ _ ar\ (Bo a1 a2 ar)) N [ATy1| SR] [ATy2 | DR] :- + M is N - 1, + pi a1 a2 ar\ + type-of-args (Bo a1 a2 ar) M SR DR. + + % whd beta-iota-delta-zeta, main code +pred whd-fuel i:term, i:stack, i:int, o:term, o:stack. +whd-fuel T S 0 T S. +whd-fuel (app [Hd|Args]) C N X XC :- !, whd-fuel Hd {std.append Args C} N X XC. +whd-fuel (fun _ _ _ as X) [] _ X [] :- !. +whd-fuel (fun N T F) [B|C] M X XC :- !, + (pi x\ def x N T B => cache x BN_ => whd-fuel (F x) C M (F1 x) (C1 x)), X = F1 B, XC = C1 B. +whd-fuel (let N T B F) C M X XC :- !, + (pi x\ def x N T B => cache x BN_ => whd-fuel (F x) C M (F1 x) (C1 x)), X = F1 B, XC = C1 B. +whd-fuel (global (const GR)) C M X XC :- + O is M - 1, unfold GR none C D DC, !, whd-fuel D DC O X XC. +whd-fuel (pglobal (const GR) I) C M X XC :- + O is M - 1, + unfold GR (some I) C D DC, !, whd-fuel D DC O X XC. +whd-fuel (primitive (proj _ N)) [A|C] M X XC :- whd-indc A _ KA, !, + O is M - 1, + whd-fuel {proj-red KA N C} O X XC. +whd-fuel (global (const GR) as HD) C M X XC :- coq.env.primitive? GR, !, + O is M - 1, + unwind HD C Orig, + coq.reduction.lazy.whd_all Orig R, + if (same_term Orig R) (X = HD, XC = C) (whd-fuel R [] O X XC). +whd-fuel (match A _ L) C M X XC :- whd-indc A GR KA, !, + whd-fuel {match-red GR KA L C} M X XC. +whd-fuel (fix _ N _ F as Fix) C M X XC :- nth-stack N C LA A RA, whd-indc A GR KA, !, + whd-fuel {fix-red F Fix LA GR KA RA} M X XC. +whd-fuel N C M X XC :- name N, def N _ _ V, !, cache-whd N VN V, whd-fuel VN C M X XC. +whd-fuel X C _ X C. + +pred unfold-prim-proj i:term, i:stack, o:term, o:stack. +unfold-prim-proj (let _ _ ((app [ (primitive (proj _ _)) | _ ]) as B) F) C XX CC :- + whd B [] B' [], + Hd = F B', Args = C, + unfold-prim-proj Hd Args XX CC. +unfold-prim-proj X C XX CC :- + hd-beta X C XX CC. + +pred iota-step i:term, i:stack, o:term, o:stack. +iota-step (match A _ L) C X XC :- whd-indc A GR KA, !, + match-red GR KA L C X XC. +% deals with primitive projections +iota-step (let _ _ B F) C X XC :- !, + Hd = F B, Args = C, + unfold-prim-proj Hd Args X XC. + +pred invert-eqs i:list term, o:list term. +invert-eqs Eqs IEqs :- + std.map Eqs (x\r\ sigma Skel TMP Err\ Skel = {{ lib:@trocq.inverse _ _ _ lp:x}}, + (@keepunivs! => coq.elaborate-skeleton Skel _ TMP ok), + r = TMP + ) IEqs. + +% expects list of equations +pred rewrite-with i:list term, i:list term, i:term, o:term. +rewrite-with [] [] End End. +rewrite-with [Eq|Eqs] [Pat|Pats] End R :- + (pi rest\ + + coq.gref->id {{:gref @lib:trocq.paths }} PathsID, + elim-into-path-suffix PathsID Suff, + PathIndName is PathsID ^ Suff, + coq.locate PathIndName PathIndGR, + coq.env.global PathIndGR PathInd, + (T rest) = {{ lp:PathInd _ _ lp:Pat lp:rest _ lp:Eq }}), + rewrite-with Eqs Pats End RestSkel, + (@keepunivs! => coq.elaborate-skeleton RestSkel _ Rest ok), + RSkel = (T Rest), + (@keepunivs! => coq.elaborate-skeleton RSkel _ R ok). + +% checks if two types refer to the same indt, and returns a canonical one. +pred cmp-indt i:term, i:term, o:term, o:term. +cmp-indt T1 T2 R T2Hd:- + coq.safe-dest-app T1 T1Hd _, + coq.safe-dest-app T2 T2Hd _, + coq.env.global (indt GR) T2Hd, + if ( T1Hd = pglobal (indt GR) _) (R = T2Hd) ( R = T1Hd ). + +} \ No newline at end of file diff --git a/examples/list_option.v b/examples/list_option.v index bef50844..85ae30db 100644 --- a/examples/list_option.v +++ b/examples/list_option.v @@ -67,11 +67,10 @@ Definition mapR (l : list A) (l' : list A') (lR : listR A A' AR l l') : listR B B' BR (map f l) (map f' l'). Proof. - induction lR; simpl. + elim: lR=> /= [| a1 a2 a_R l1 l2 lr]. - apply nilR. - apply consR. - + apply (fR a a' aR). - + apply IHlR. + + apply (fR a1 a2 a_R). Defined. Lemma option_to_list_map_morph (A B : Type) (f : A -> B) (xo : option A) : diff --git a/examples/std/Vector_tuple.v b/examples/std/Vector_tuple.v index 42746c83..aa4fde3a 100644 --- a/examples/std/Vector_tuple.v +++ b/examples/std/Vector_tuple.v @@ -15,6 +15,7 @@ From mathcomp Require Import ssreflect ssrfun. From Trocq Require Import Trocq. Set Universe Polymorphism. +Unset Universe Minimization ToSet. (* iterated tuple type *) @@ -357,7 +358,6 @@ Proof. - exact (@Map4_bnat_bv k). - exact (@Map4_bv_bnat k). Defined. - Definition Param44_bnat_bv (k k' : nat) (kR : natR k k') : Param44.Rel (bounded_nat k) (bitvector k'). Proof. diff --git a/examples/std/flt3_step.v b/examples/std/flt3_step.v index 70982d08..a740b9bc 100644 --- a/examples/std/flt3_step.v +++ b/examples/std/flt3_step.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_boot all_algebra. From Trocq Require Import Stdlib Trocq. Import GRing.Theory. diff --git a/examples/std/int_to_Zp.v b/examples/std/int_to_Zp.v index 3ee876ec..0f982eda 100644 --- a/examples/std/int_to_Zp.v +++ b/examples/std/int_to_Zp.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_boot all_algebra. From Trocq Require Import Stdlib Trocq. Import GRing.Theory. Local Open Scope bool_scope. diff --git a/examples/std/square_and_cube_mod7.v b/examples/std/square_and_cube_mod7.v index 7a21635f..c1eb7964 100644 --- a/examples/std/square_and_cube_mod7.v +++ b/examples/std/square_and_cube_mod7.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_boot all_algebra. From Trocq Require Import Stdlib Trocq. Import GRing.Theory. diff --git a/generic/Param_Empty.v b/generic/Param_Empty.v index 3349a559..8c384ede 100644 --- a/generic/Param_Empty.v +++ b/generic/Param_Empty.v @@ -11,76 +11,20 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy. +From Trocq Require Import HoTTNotations Relnm. + +(* translations of inductives in Prop is not yet supported, +but we can still generate everything for False by manually defining its parametricity translation and making it land in Type. *) +Unset Universe Polymorphism. +Inductive EmptyR : Empty -> Empty -> Type :=. +(* param2 does not handle universe polymorphic inductives. + Hence we have define EmptyR before seting Universe Polymorphism. *) +Elpi derive.param2.register "False" "EmptyR". Set Universe Polymorphism. Unset Universe Minimization ToSet. -Import HoTTNotations. - -Inductive EmptyR : Empty -> Empty -> Type := . - -Definition map_Empty (e : Empty) : Empty := e. - -Definition map_in_R_Empty : forall (e e' : Empty), map_Empty e = e' -> EmptyR e e' := - fun e => match e with end. - -Definition R_in_map_Empty : forall (e e' : Empty), EmptyR e e' -> map_Empty e = e' := - fun e => match e with end. - -Definition R_in_mapK_Empty : forall (e e' : Empty) (eR : EmptyR e e'), - map_in_R_Empty e e' (R_in_map_Empty e e' eR) = eR := - fun e => match e with end. - -Definition Map0_Empty : Map0.Has EmptyR. -Proof. constructor. Defined. - -Definition Map1_Empty : Map1.Has EmptyR. -Proof. constructor. exact map_Empty. Defined. - -Definition Map2a_Empty : Map2a.Has EmptyR. -Proof. - unshelve econstructor. - - exact map_Empty. - - exact map_in_R_Empty. -Defined. - -Definition Map2b_Empty : Map2b.Has EmptyR. -Proof. - unshelve econstructor. - - exact map_Empty. - - exact R_in_map_Empty. -Defined. - -Definition Map3_Empty : Map3.Has EmptyR. -Proof. - unshelve econstructor. - - exact map_Empty. - - exact map_in_R_Empty. - - exact R_in_map_Empty. -Defined. - -Definition Map4_Empty : Map4.Has EmptyR. -Proof. - unshelve econstructor. - - exact map_Empty. - - exact map_in_R_Empty. - - exact R_in_map_Empty. - - exact R_in_mapK_Empty. -Defined. - -Definition Param01_Empty : Param01.Rel Empty Empty. -Proof. -unshelve econstructor; first exact: EmptyR. -- done. -- constructor; exact map_Empty. -Defined. - -Definition Param10_Empty : Param10.Rel Empty Empty. -Proof. -unshelve econstructor; first exact: EmptyR. -- constructor; exact map_Empty. -- done. -Defined. +#[prefix="Empty_"] Elpi derive Empty. +Definition Param01_Empty := Empty_rel01. +Definition Param10_Empty := Empty_rel10. diff --git a/generic/Param_bool.v b/generic/Param_bool.v index ff44c3a2..fc7f4ed1 100644 --- a/generic/Param_bool.v +++ b/generic/Param_bool.v @@ -11,77 +11,24 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. +From Trocq Require Import HoTTNotations. Set Universe Polymorphism. Unset Universe Minimization ToSet. -Import HoTTNotations. - -Inductive BoolR : Bool -> Bool -> Type := - | falseR : BoolR false false - | trueR : BoolR true true. - -Definition map_Bool : Bool -> Bool := idmap. - -Definition map_in_R_Bool {b b' : Bool} (e : map_Bool b = b') : BoolR b b' := - match e with - | idpath => - match b with - | false => falseR - | true => trueR - end - end. - -Definition R_in_map_Bool {b b' : Bool} (bR : BoolR b b') : map_Bool b = b' := - match bR with - | falseR => idpath - | trueR => idpath - end. - -Definition R_in_mapK_Bool {b b' : Bool} (bR : BoolR b b') : - map_in_R_Bool (R_in_map_Bool bR) = bR := - match bR with - | falseR => idpath - | trueR => idpath - end. - -Definition Param_Bool_sym {b b' : Bool} (bR : BoolR b b') : BoolR b' b := - match bR with - | falseR => falseR - | trueR => trueR - end. - -Definition Param_Bool_sym_inv {b b' : Bool} (bR : BoolR b b') : - Param_Bool_sym (Param_Bool_sym bR) = bR := - match bR with - | falseR => idpath - | trueR => idpath - end. - -Definition BoolR_sym : forall (b b' : Bool), sym_rel BoolR b b' <->> BoolR b b'. -Proof. - intros b b'; unshelve eexists _,_ . - - apply Param_Bool_sym. - - apply Param_Bool_sym. - - intro bR. apply Param_Bool_sym_inv. -Defined. - -Definition Map4_Bool : Map4.Has BoolR. -Proof. - unshelve econstructor. - - exact map_Bool. - - exact @map_in_R_Bool. - - exact @R_in_map_Bool. - - exact @R_in_mapK_Bool. -Defined. - -Definition Param44_Bool : Param44.Rel Bool Bool. -Proof. - unshelve econstructor. - - exact BoolR. - - exact Map4_Bool. - - apply (fun e => @eq_Map4 _ _ (sym_rel BoolR) BoolR e Map4_Bool). - apply BoolR_sym. -Defined. +#[prefix="Bool_"] Elpi derive Bool. + +(* Enables to generically deal with Bool +despite one is a notation to bool and the other an inductive Bool*) +(* The inductive generates Bool_R = [| Bool |], +and the notation generates bool_R = [| Bool |]*) +(* Since param declares monomorphic definitions [| Bool |] has to be wrapped with a universe polymorphic definition *) +Module FakeBool. + Definition Bool := Bool. +End FakeBool. +Elpi derive.param2 FakeBool.Bool. + +Definition BoolR := Bool_R. +Definition trueR := true_R. +Definition Param44_Bool := Bool_rel44. diff --git a/generic/Param_list.v b/generic/Param_list.v index e5c82067..8f77ba13 100644 --- a/generic/Param_list.v +++ b/generic/Param_list.v @@ -11,182 +11,26 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. Set Universe Polymorphism. Unset Universe Minimization ToSet. Set Asymmetric Patterns. -Import HoTTNotations. +Elpi derive list. -Inductive listR (A A' : Type) (AR : A -> A' -> Type) : list A -> list A' -> Type := - | nilR : listR A A' AR (@nil A) (@nil A') - | consR : - forall (a : A) (a' : A') (aR : AR a a') - (l : list A) (l' : list A') (lR : listR A A' AR l l'), - listR A A' AR (cons a l) (cons a' l'). +Notation listR := list_R. +Notation nilR := nil_R. +Notation consR := cons_R. -Definition map_list (A A' : Type) (AR : Param10.Rel A A') : list A -> list A' := - fix F (l : list A) : list A' := - match l with - | nil => nil - | cons a l => cons (map AR a) (F l) - end. - -Definition map_in_R_list (A A' : Type) (AR : Param2a0.Rel A A') : - forall (l : list A) (l' : list A'), map_list A A' AR l = l' -> listR A A' AR l l' := - fun l l' e => - match e with - | idpath => - (fix F l : listR A A' AR l (map_list A A' AR l) := - match l with - | nil => nilR A A' AR - | cons a l => - consR A A' AR - a (map AR a) (map_in_R AR a (map AR a) idpath) - l (map_list A A' AR l) (F l) - end) l - end. - -Definition R_in_map_list (A A' : Type) (AR : Param2b0.Rel A A') : - forall (l : list A) (l' : list A'), listR A A' AR l l' -> map_list A A' AR l = l' := - fix F l l' lR := - match lR with - | nilR => idpath - | consR a a' aR l l' lR => - match R_in_map AR a a' aR with - | idpath => - match F l l' lR with - | idpath => idpath - end - end - end. - -Definition Map2a_list (A A' : Type) (AR : Param2a0.Rel A A') : Map2a.Has (listR A A' AR). -Proof. - unshelve econstructor. - - exact (map_list A A' AR). - - exact (map_in_R_list A A' AR). -Defined. - -Definition Map2b_list (A A' : Type) (AR : Param2b0.Rel A A') : Map2b.Has (listR A A' AR). -Proof. - unshelve econstructor. - - exact (map_list A A' AR). - - exact (R_in_map_list A A' AR). -Defined. - -Definition Map3_list (A A' : Type) (AR : Param30.Rel A A') : Map3.Has (listR A A' AR). -Proof. - unshelve econstructor. - - exact (map_list A A' AR). - - exact (map_in_R_list A A' AR). - - exact (R_in_map_list A A' AR). -Defined. - -Definition Map4_list (A A' : Type) (AR : Param40.Rel A A') : Map4.Has (listR A A' AR). -Proof. - unshelve econstructor. - - exact (map_list A A' AR). - - exact (map_in_R_list A A' AR). - - exact (R_in_map_list A A' AR). - - move=> a b; elim => //= {}a {}a' aR l l' lR /=. - elim: {2}_ / => //=. - case: _ / (R_in_map_list A A' AR l l' lR) => {l' lR}. - rewrite -{2}[aR](R_in_mapK AR). - by case: _ / (R_in_map AR a a' aR). -Qed. - -Definition listR_flip (A A' : Type) (AR : A -> A' -> Type) : - forall (l : list A) (l' : list A'), listR A A' AR l l' -> listR A' A (sym_rel AR) l' l := - fix F l l' lR := - match lR with - | nilR => nilR A' A (sym_rel AR) - | consR a a' aR l l' lR => - consR A' A (sym_rel AR) a' a aR l' l (F l l' lR) - end. - -Definition listR_flipK (A A' : Type) (AR : A -> A' -> Type) : - forall (l : list A) (l' : list A') (lR : listR A A' AR l l'), - listR_flip A' A (sym_rel AR) l' l (listR_flip A A' AR l l' lR) = lR := - fix F l l' lR := - match lR with - | nilR => idpath - | consR a a' aR l l' lR => - ap (fun lR => consR A A' AR a a' aR l l' lR) (F l l' lR) - end. - -Definition listR_sym (A A' : Type) (AR : A -> A' -> Type) : - forall (l' : list A') (l : list A), - listR A A' AR l l' <->> listR A' A (sym_rel AR) l' l. -Proof. - intros l' l. - unshelve econstructor. - - exact (listR_flip A A' AR l l'). - - unshelve econstructor. - + exact (listR_flip A' A (sym_rel AR) l' l). - + exact (listR_flipK A A' AR l l'). -Defined. - -Definition Param00_list (A A' : Type) (AR : Param00.Rel A A') : Param00.Rel (list A) (list A'). -Proof. - unshelve econstructor. - - exact (listR A A' AR). - - constructor. - - constructor. -Defined. - -Definition Param42a_list (A A' : Type) (AR : Param42a.Rel A A') : Param42a.Rel (list A) (list A'). -Proof. - unshelve econstructor. - - exact (listR A A' AR). - - exact (Map4_list A A' AR). - - refine (eq_Map2a _ _). - + apply listR_sym. - + exact (Map2a_list A' A (Param2a2a_sym _ _ AR)). -Defined. - -Definition Param42b_list (A A' : Type) (AR : Param42b.Rel A A') : Param42b.Rel (list A) (list A'). -Proof. - unshelve econstructor. - - exact (listR A A' AR). - - exact (Map4_list A A' AR). - - refine (eq_Map2b _ _). - + apply listR_sym. - + exact (Map2b_list A' A (Param2b2b_sym _ _ AR)). -Defined. - -Definition Param2a4_list (A A' : Type) (AR : Param2a4.Rel A A') : - Param2a4.Rel (list A) (list A') := Param42a_sym _ _ (Param42a_list _ _ (Param2a4_sym _ _ AR)). - -Definition Param2b4_list (A A' : Type) (AR : Param2b4.Rel A A') : - Param2b4.Rel (list A) (list A') := Param42b_sym _ _ (Param42b_list _ _ (Param2b4_sym _ _ AR)). - -Definition Param33_list (A A' : Type) (AR : Param33.Rel A A') : Param33.Rel (list A) (list A'). -Proof. - unshelve econstructor. - - exact (listR A A' AR). - - exact (Map3_list A A' AR). - - refine (eq_Map3 _ _). - + apply listR_sym. - + exact (Map3_list A' A (Param33_sym _ _ AR)). -Defined. - -Definition Param44_list (A A' : Type) (AR : Param44.Rel A A') : Param44.Rel (list A) (list A'). -Proof. - unshelve econstructor. - - exact (listR A A' AR). - - exact (Map4_list A A' AR). - - refine (eq_Map4 _ _). - + apply listR_sym. - + exact (Map4_list A' A (Param44_sym _ _ AR)). -Defined. +Definition Param42b_list := list_rel42b. +Definition Param2a4_list := list_rel2a4. +Definition Param44_list := list_rel44. Definition Param_nil : forall (A A' : Type) (AR : Param00.Rel A A'), - listR A A' AR (@nil A) (@nil A') := @nilR. + list_R A A' AR (@nil A) (@nil A') := @nil_R. Definition Param_cons : forall (A A' : Type) (AR : Param00.Rel A A') (a : A) (a' : A') (aR : AR a a') - (l : list A) (l' : list A') (lR : listR A A' AR l l'), - listR A A' AR (cons a l) (cons a' l') := @consR. + (l : list A) (l' : list A') (lR : list_R A A' AR l l'), + list_R A A' AR (cons a l) (cons a' l') := @cons_R. diff --git a/generic/Param_nat.v b/generic/Param_nat.v index 5c31a198..4d111de1 100644 --- a/generic/Param_nat.v +++ b/generic/Param_nat.v @@ -11,120 +11,17 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect ssrbool. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. Set Universe Polymorphism. Unset Universe Minimization ToSet. -Import HoTTNotations. +Elpi derive nat. +Notation natR := nat_R. +Definition OR := O_R. +Definition SR := S_R. -Inductive natR : nat -> nat -> Type := - | OR : natR O O - | SR : forall (n n' : nat), natR n n' -> natR (S n) (S n'). - -(* From Rocq's stdlib *) -Fixpoint eqb n m : Bool := - match n, m with - | O, O => true - | O, S _ => false - | S _, O => false - | S n', S m' => eqb n' m' - end. - -Lemma uip_lifted_bool (b: Bool) (x1 x2 : is_true b): - x1 = x2. -Proof. - revert x1 x2. - case b=> /= ; case. - by case. -Qed. - -Lemma natR_irrelevant m n (nR nR' : natR m n) : nR = nR'. -Proof. -have @phi k l (r : natR k l) : is_true (eqb k l). -1: { - elim: r => {k l}; first by reflexivity. - move=> k l r e; exact: e. -} -have @psi k l (e : is_true (eqb k l)) : natR k l. - - elim: k l e => [| k ihk] l e. - + case: l e => [| l] // _; exact OR. - + case: l e => [| l] // e. - exact: SR (ihk _ e). - - have phiK k l r : psi k l (phi k l r) = r. - + elim: r => {k l} // k l r e /=. - by rewrite [X in SR _ _ X]e. - + rewrite -(phiK m n nR) -(phiK m n nR'). - suff -> : phi _ _ nR = phi _ _ nR' by []. - apply uip_lifted_bool. -Defined. - -Definition map_nat : nat -> nat := idmap. - -Definition map_in_R_nat : forall {n n' : nat}, map_nat n = n' -> natR n n' := - fun n n' e => - match e with - | idpath => - (fix F n := - match n with - | O => OR - | S m => SR m m (F m) - end) n - end. - -Definition R_in_map_nat : forall {n n' : nat}, natR n n' -> map_nat n = n' := - fix F n n' (nR : natR n n') : map_nat n = n' := - match nR with - | OR => idpath - | SR m m' mR => ap S (F m m' mR) - end. - -Definition R_in_mapK_nat : forall {n n' : nat} (nR : natR n n'), - map_in_R_nat (R_in_map_nat nR) = nR. -Proof. -by move=> n n'; case: _ / => //= {}n {}n' nR; apply: natR_irrelevant. -Qed. - -Definition Param_nat_sym {n n' : nat} : natR n n' -> natR n' n. -Proof. - intro nR. induction nR as [|m m' _ IH]. - - exact OR. - - exact (SR m' m IH). -Defined. - -Definition Param_nat_sym_inv {n n' : nat} : - forall (nR : natR n n'), Param_nat_sym (Param_nat_sym nR) = nR. -Proof. by elim => //= {}n {}n' nR ->. Defined. - -Definition natR_sym : forall (n n' : nat), sym_rel natR n n' <->> natR n n'. -Proof. - intros n n'; unshelve eexists _, _. - - apply Param_nat_sym. - - apply Param_nat_sym. - - intro nR. apply Param_nat_sym_inv. -Defined. - -Definition Map4_nat : Map4.Has natR. -Proof. - unshelve econstructor. - - exact map_nat. - - exact @map_in_R_nat. - - exact @R_in_map_nat. - - exact @R_in_mapK_nat. -Defined. - -Definition Param44_nat : Param44.Rel nat nat. -Proof. - unshelve econstructor. - - exact natR. - - exact Map4_nat. - - apply (fun e => @eq_Map4 _ _ (sym_rel natR) natR e Map4_nat). - apply natR_sym. -Defined. - -Definition Param00_nat : Param00.Rel nat nat := Param44_nat. -Definition Param2a0_nat : Param2a0.Rel nat nat := Param44_nat. +Definition Param2a0_nat := nat_rel2a0. Definition Param_add : forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'), @@ -134,4 +31,4 @@ Proof. induction n1R as [|n1 n1' n1R IHn1R]. - simpl. exact n2R. - simpl. apply SR. exact IHn1R. -Defined. +Defined. diff --git a/generic/Param_option.v b/generic/Param_option.v index 52a927d6..69ce3cca 100644 --- a/generic/Param_option.v +++ b/generic/Param_option.v @@ -11,111 +11,9 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. Set Universe Polymorphism. Unset Universe Minimization ToSet. -Import HoTTNotations. - -Inductive optionR (A A' : Type) (AR : A -> A' -> Type) : - option A -> option A' -> Type := - | someR : - forall (a : A) (a' : A'), AR a a' -> - optionR A A' AR (Some a) (Some a') - | noneR : optionR A A' AR None None. - -Definition option_map : -forall (A A' : Type) (AR : Param10.Rel A A'), option A -> option A' := - fun A A' AR => - fun oa => - match oa in option _ return option A' with - | Some a => Some (map AR a) - | None => None - end. - -Definition some_inj1 : -forall (A : Type) (a1 a2 : A), Some a1 = Some a2 -> a1 = a2 := - fun A a1 a2 e => - let proj1 (oa : option A) := - match oa with - | Some a => a - | None => a1 - end - in ap proj1 e. - -Definition exfalso_option_some_none : - forall (T : Type) (A : Type) (a : A), Some a = None -> T := - fun T A a e => - match e in @paths _ _ t - return - match t with - | Some _ => Unit - | _ => T - end - with - | idpath => tt - end. - -Definition exfalso_option_none_some : - forall (T : Type) (A : Type) (a : A), None = Some a -> T := - fun T A a e => - match e in @paths _ _ t - return - match t with - | None => Unit - | Some _ => T - end - with - | idpath => tt - end. - -Definition option_map_in_R : - forall (A A' : Type) (AR : Param2a0.Rel A A') - (oa : option A) (oa' : option A'), - option_map A A' AR oa = oa' -> optionR A A' AR oa oa' := - fun A A' AR => - fun oa oa' => - match oa with - | Some a => - match oa' with - | Some a' => - fun e => - someR A A' AR a a' (map_in_R AR a a' (some_inj1 A' (map AR a) a' e)) - | None => - fun e => - exfalso_option_some_none (optionR A A' AR (Some a) (None)) - A' (map AR a) e - end - | None => - match oa' with - | Some a' => - fun e => - exfalso_option_none_some (optionR A A' AR (None) (Some a')) - A' a' e - | None => fun e => noneR A A' AR - end - end. - -Definition option_R_in_map : - forall (A A' : Type) (AR : Param2b0.Rel A A') - (oa : option A) (oa' : option A'), - optionR A A' AR oa oa' -> option_map A A' AR oa = oa' - := - fun A A' AR => - fun oa oa' oaR => - match oaR in optionR _ _ _ oa oa' return option_map A A' AR oa = oa' with - | @someR _ _ _ a a' aR => - @transport A' (fun t => Some t = Some a') - a' (map AR a) (R_in_map AR a a' aR)^ - idpath - | @noneR _ _ _ => idpath - end. - -Definition option_R_in_mapK (A A' : Type) (AR : Param40.Rel A A') - (oa : option A) (oa' : option A') (oaR : optionR A A' AR oa oa') : - option_map_in_R A A' AR oa oa' (option_R_in_map A A' AR oa oa' oaR) = oaR. -Proof. -by case: oaR => [a a' aR|]//=; elim/(ind_map AR): _; rewrite transport_1. -Qed. +Elpi derive option. \ No newline at end of file diff --git a/generic/Param_prod.v b/generic/Param_prod.v index 6788fb2e..a2d9d862 100644 --- a/generic/Param_prod.v +++ b/generic/Param_prod.v @@ -11,125 +11,19 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. Set Universe Polymorphism. Unset Universe Minimization ToSet. -Import HoTTNotations. - -Inductive prodR - {A A'} (AR : A -> A' -> Type) {B B'} (BR : B -> B' -> Type) : A * B -> A' * B' -> Type := - | pairR a a' (aR : AR a a') b b' (bR : BR b b') : prodR AR BR (a, b) (a', b'). - -Arguments pairR {A A' AR B B' BR} a a' aR b b' bR. - -(* *) - -Definition prod_map - (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') : - A * B -> A' * B' := - fun p => - match p with - | (a, b) => (map AR a, map BR b) - end. - -(* *) - -Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) : - (a1, b1) = (a2, b2) -> a1 = a2 := - fun e => - match e in _ = (a, b) return _ = a with - | @idpath _ _ => @idpath _ a1 - end. - -Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) : - (a1, b1) = (a2, b2) -> b1 = b2 := - fun e => - match e in @paths _ _ (a, b) return _ = b with - | @idpath _ _ => @idpath _ b1 - end. - -Definition prod_map_in_R - (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') : - forall p p', prod_map A A' AR B B' BR p = p' -> prodR AR BR p p' := - fun p p' => - match p with - | (a, b) => - match p' with - | (a', b') => - fun e => - pairR - a a' (map_in_R AR a a' (pair_inj1 A' B' (map AR a) a' (map BR b) b' e)) - b b' (map_in_R BR b b' (pair_inj2 A' B' (map AR a) a' (map BR b) b' e)) - end - end. - -(* *) - -Definition prod_R_in_map - (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') : - forall p p', prodR AR BR p p' -> prod_map A A' AR B B' BR p = p' := - fun p p' r => - match r with - | pairR a a' aR b b' bR => - @transport _ (fun t => (t, map BR b) = (a', b')) _ _ (R_in_map AR a a' aR)^ - (@transport _ (fun t => (a', t) = (a', b')) _ _ (R_in_map BR b b' bR)^ idpath) - end. - -(* *) - -Definition prod_R_in_mapK - (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') : - forall p p' (r : prodR AR BR p p'), - prod_map_in_R A A' AR B B' BR p p' (prod_R_in_map A A' AR B B' BR p p' r) = r. -Proof. -intros p p' []; rewrite /prod_R_in_map/=. -by elim/(ind_map AR): _; elim/(ind_map BR): _. -Qed. - -(* *) - -Definition Map0_prod A A' (AR : Param00.Rel A A') B B' (BR : Param00.Rel B B') : - Map0.Has (prodR AR BR). -Proof. constructor. Defined. - -Definition Map1_prod A A' (AR : Param10.Rel A A') B B' (BR : Param10.Rel B B') : - Map1.Has (prodR AR BR). -Proof. constructor. exact (prod_map A A' AR B B' BR). Defined. - -Definition Map2a_prod A A' (AR : Param2a0.Rel A A') B B' (BR : Param2a0.Rel B B') : - Map2a.Has (prodR AR BR). -Proof. - unshelve econstructor. - - exact (prod_map A A' AR B B' BR). - - exact (prod_map_in_R A A' AR B B' BR). -Defined. - -Definition Map2b_prod A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') : - Map2b.Has (prodR AR BR). -Proof. - unshelve econstructor. - - exact (prod_map A A' AR B B' BR). - - exact (prod_R_in_map A A' AR B B' BR). -Defined. - -Definition Map3_prod A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') : - Map3.Has (prodR AR BR). -Proof. - unshelve econstructor. - - exact (prod_map A A' AR B B' BR). - - exact (prod_map_in_R A A' AR B B' BR). - - exact (prod_R_in_map A A' AR B B' BR). -Defined. +Unset Universe Polymorphism. +Inductive prod_R (A1 A2 : Type) (A_R : A1 -> A2 -> Type) (B1 B2 : Type) (B_R : B1 -> B2 -> Type) +: prod A1 B1 -> prod A2 B2 -> Type := + pair_R : forall (a1 : A1) (a2 : A2), +A_R a1 a2 -> forall (b3 : B1) (b4 : B2), +B_R b3 b4 -> prod_R A1 A2 A_R B1 B2 B_R (@pair A1 B1 a1 b3) (@pair A2 B2 a2 b4). +Set Universe Polymorphism. -Definition Map4_prod A A' (AR : Param40.Rel A A') B B' (BR : Param40.Rel B B') : - Map4.Has (prodR AR BR). -Proof. - unshelve econstructor. - - exact (prod_map A A' AR B B' BR). - - exact (prod_map_in_R A A' AR B B' BR). - - exact (prod_R_in_map A A' AR B B' BR). - - exact (prod_R_in_mapK A A' AR B B' BR). -Defined. +Elpi derive.param2.register "prod" "prod_R". +Elpi derive.param2.register "pair" "pair_R". +Elpi derive prod. \ No newline at end of file diff --git a/generic/Param_sum.v b/generic/Param_sum.v index 9d329da6..89727f75 100644 --- a/generic/Param_sum.v +++ b/generic/Param_sum.v @@ -11,153 +11,11 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -Require Import ssreflect. -Require Import Stdlib Hierarchy Param_lemmas. +From Trocq Require Import Relnm. Set Universe Polymorphism. Unset Universe Minimization ToSet. Set Asymmetric Patterns. -Import HoTTNotations. - -Inductive sumR - A A' (AR : A -> A' -> Type) B B' (BR : B -> B' -> Type) : A + B -> A' + B' -> Type := - | inlR a a' (aR : AR a a') : sumR A A' AR B B' BR (inl a) (inl a') - | inrR b b' (bR : BR b b') : sumR A A' AR B B' BR (inr b) (inr b'). - -(* *) - -Definition sum_map - (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') : - A + B -> A' + B' := - fun p => - match p with - | inl a => inl (map AR a) - | inr b => inr (map BR b) - end. - -Definition inl_inj {A B} {a1 a2 : A} : - @inl A B a1 = inl a2 -> a1 = a2 := - fun e => - match e in @paths _ _ (inl a1) return _ = a1 with - | @idpath _ _ => @idpath _ a1 - end. - -Definition inr_inj {A B} {b1 b2 : B} : - @inr A B b1 = inr b2 -> b1 = b2 := - fun e => - match e in @paths _ _ (inr b1) return _ = b1 with - | @idpath _ _ => @idpath _ b1 - end. - -Definition inl_inr {A B a b} : @inl A B a = inr b -> False. -Proof. discriminate. Defined. - -Definition inr_inl {A B b a} : @inr A B b = inl a -> False. -Proof. discriminate. Defined. - -Definition sum_map_in_R - (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') : - forall p p', sum_map A A' AR B B' BR p = p' -> sumR A A' AR B B' BR p p'. -Proof. -case=> [a|b] [a'|b']; do ?discriminate. -- by move=> /inl_inj<-; constructor; apply: map_in_R. -- by move=> /inr_inj<-; constructor; apply: map_in_R. -Defined. - -(* *) - -Definition sum_R_in_map - (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') : - forall p p', sumR A A' AR B B' BR p p' -> sum_map A A' AR B B' BR p = p'. -Proof. -by move=> _ _ [a a' aR|b b' bR]/=; apply: ap; apply: R_in_map. -Defined. - -Definition sum_R_in_mapK - (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') : - forall p p' (r : sumR A A' AR B B' BR p p'), - sum_map_in_R A A' AR B B' BR p p' (sum_R_in_map A A' AR B B' BR p p' r) = r. -Proof. - move=> _ _ [a a' aR|b b' bR]/=. - - by elim/(ind_map AR): _ => /=. - - by elim/(ind_map BR): _ => /=. -Qed. - -Definition Map0_sum A A' (AR : Param00.Rel A A') B B' (BR : Param00.Rel B B') : - Map0.Has (sumR A A' AR B B' BR). -Proof. constructor. Defined. - -Definition Map1_sum A A' (AR : Param10.Rel A A') B B' (BR : Param10.Rel B B') : - Map1.Has (sumR A A' AR B B' BR). -Proof. constructor. exact (sum_map A A' AR B B' BR). Defined. - -Definition Map2a_sum A A' (AR : Param2a0.Rel A A') B B' (BR : Param2a0.Rel B B') : - Map2a.Has (sumR A A' AR B B' BR). -Proof. - unshelve econstructor. - - exact (sum_map A A' AR B B' BR). - - exact (sum_map_in_R A A' AR B B' BR). -Defined. - -Definition Map2b_sum A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') : - Map2b.Has (sumR A A' AR B B' BR). -Proof. - unshelve econstructor. - - exact (sum_map A A' AR B B' BR). - - exact (sum_R_in_map A A' AR B B' BR). -Defined. - -Definition Map3_sum A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') : - Map3.Has (sumR A A' AR B B' BR). -Proof. - unshelve econstructor. - - exact (sum_map A A' AR B B' BR). - - exact (sum_map_in_R A A' AR B B' BR). - - exact (sum_R_in_map A A' AR B B' BR). -Defined. - -Definition Map4_sum A A' (AR : Param40.Rel A A') B B' (BR : Param40.Rel B B') : - Map4.Has (sumR A A' AR B B' BR). -Proof. - unshelve econstructor. - - exact (sum_map A A' AR B B' BR). - - exact (sum_map_in_R A A' AR B B' BR). - - exact (sum_R_in_map A A' AR B B' BR). - - exact (sum_R_in_mapK A A' AR B B' BR). -Defined. - -Definition sumR_flip {A A' : Type} (AR : A -> A' -> Type) - {B B' : Type} (BR : B -> B' -> Type) (s : A + B) (s' : A' + B') - (sR : sumR A A' AR B B' BR s s') : - sumR A' A (sym_rel AR) B' B (sym_rel BR) s' s := - match sR with - | inlR a a' aR => inlR A' A (sym_rel AR) B' B (sym_rel BR) a' a aR - | inrR b b' bR => inrR A' A (sym_rel AR) B' B (sym_rel BR) b' b bR - end. - -Definition sumR_flipK {A A' : Type} (AR : A -> A' -> Type) - {B B' : Type} (BR : B -> B' -> Type) (s : A + B) (s' : A' + B') - (sR : sumR A A' AR B B' BR s s') : - sumR_flip (sym_rel AR) (sym_rel BR) s' s (sumR_flip AR BR s s' sR) = sR. -Proof. case sR; constructor. Defined. - -Definition sumR_sym {A A' : Type} (AR : A -> A' -> Type) - {B B' : Type} (BR : B -> B' -> Type) (s : A + B) (s' : A' + B') : - sumR A A' AR B B' BR s s' <->> sumR A' A (sym_rel AR) B' B (sym_rel BR) s' s. -Proof. - unshelve econstructor. - - exact (sumR_flip AR BR s s'). - - unshelve econstructor. - + exact (sumR_flip (sym_rel AR) (sym_rel BR) s' s). - + exact (sumR_flipK AR BR s s'). -Defined. - -Definition Param01_sum A A' (AR : Param01.Rel A A') B B' (BR : Param01.Rel B B') : - Param01.Rel (A + B) (A' + B'). -exists (sumR A A' AR B B' BR). -- exact: Map0_sum. -- constructor. - exact (Map1.map _ (Map1_sum _ _ - (Param01_sym _ _ AR) _ _ (Param01_sym _ _ BR))). -Defined. +Elpi derive sum. +Definition Param01_sum := sum_rel01. diff --git a/generic/Param_vector.v b/generic/Param_vector.v index 83a6404b..313df934 100644 --- a/generic/Param_vector.v +++ b/generic/Param_vector.v @@ -96,8 +96,8 @@ Definition map : fun A A' AR => fix F n n' nR := match nR with - | OR => fun _ => nil - | SR m m' mR => fun v => cons (map AR (hd v)) (F m m' mR (tail v)) + | O_R => fun _ => nil + | S_R m m' mR => fun v => cons (map AR (hd v)) (F m m' mR (tail v)) end. Definition t0 {A} (v : t A O) : v = nil := match v in t _ m return @@ -169,36 +169,32 @@ Proof. by case: _ / R_in_map. Qed. -Definition Param_nat_symK m n (nR : natR m n) : nR = Param_nat_sym (Param_nat_sym nR). -Proof. by elim: nR => //= {}m {}n mn emn; apply: ap. Defined. - Definition tR_sym_f {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') {v : t A n} {v' : t A' n'} : - sym_rel (tR A A' AR n n' nR) v' v -> tR A' A (sym_rel AR) n' n (Param_nat_sym nR) v' v. + sym_rel (tR A A' AR n n' nR) v' v -> tR A' A (sym_rel AR) n' n (nat_sym _ _ nR) v' v. Proof. by elim=> //=; constructor. Defined. Definition tR_sym_t {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') {v' : t A' n'} {v : t A n} : - tR A A' AR n n' (Param_nat_sym (Param_nat_sym nR)) v v' -> tR A A' AR n n' nR v v'. + tR A A' AR n n' (nat_sym _ _ (nat_sym _ _ nR)) v v' -> tR A A' AR n n' nR v v'. Proof. apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). - symmetry; exact: Param_nat_symK. + exact: nat_symK. Defined. Definition tR_sym_tV {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') {v' : t A' n'} {v : t A n} : - tR A A' AR n n' nR v v' -> tR A A' AR n n' (Param_nat_sym (Param_nat_sym nR)) v v'. + tR A A' AR n n' nR v v' -> tR A A' AR n n' (nat_sym _ _ (nat_sym _ _ nR)) v v'. Proof. apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). -exact: Param_nat_symK. +symmetry; exact: nat_symK. Defined. -(* Definition tR_symK *) Lemma tR_sym_tK A A' AR n n' nR v v' (vR : tR A A' AR n n' - (Param_nat_sym (Param_nat_sym nR)) v v') : + (nat_sym _ _ (nat_sym _ _ nR)) v v') : tR_sym_tV AR nR (tR_sym_t AR nR vR) = vR. Proof. -by rewrite /tR_sym_t /tR_sym_tV -transport_pp concat_Vp. +by rewrite /tR_sym_t /tR_sym_tV -transport_pp concat_pV. Defined. Local Notation f := (tR_sym_f _ _). @@ -209,8 +205,18 @@ Definition tR_sym_fK {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : nat (v : t A n) (v' : t A' n') (vR : tR A A' AR n n' nR v v') : g (f (f vR)) = vR. Proof. -elim: vR => // {}n {}n' {}nR a a' aR {}v {}v' vR {2}<-/=; rewrite /g /=. -by case: _ / Param_nat_symK (tR_sym_f _ _ _). +elim: vR => // {}n {}n' {}nR a a' aR {}v {}v' vR {2}<-/=; rewrite /g/=. +move: (tR_sym_f _ _ _)=> vR'; move: vR'. +move: ((nat_symK _ _ _))=> p. +set f := (X in (X nR _ )). +by refine (match p as p0 in (_ = nRR) +return +forall vR' : tR A A' (sym_rel (sym_rel AR)) n n' (nat_sym n' n (nat_sym n n' nR)) v v', +transport _ (f nRR (fun t1 : nat_R n n' => S_R n n' t1 = S_R n n' nRR) 1 _ p0^) + (consR A A' (sym_rel (sym_rel AR)) n n' (nat_sym n' n (nat_sym n n' nR)) a a' aR v v' vR') += consR A A' AR n n' nRR a a' aR v v' (transport _ p0 vR') +with idpath => _ end +). Qed. Definition tR_sym_fE {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') @@ -220,7 +226,7 @@ Proof. by rewrite -{2}[vR]tR_sym_fK tR_sym_tK tR_sym_fK. Qed. Definition tR_sym (A A' : Type) (AR : A -> A' -> Type) (n n' : nat) (nR : natR n n') (v' : t A' n') (v : t A n) : - sym_rel (tR A A' AR n n' nR) v' v <->> tR A' A (sym_rel AR) n' n (Param_nat_sym nR) v' v. + sym_rel (tR A A' AR n n' nR) v' v <->> tR A' A (sym_rel AR) n' n (nat_sym _ _ nR) v' v. Proof. unshelve eexists _, _. - exact: tR_sym_f. @@ -249,9 +255,9 @@ Proof. - unshelve eapply (@eq_Map4 _ _ (sym_rel (tR A A' AR n n' nR)) - (tR A' A (sym_rel AR) n' n (Param_nat_sym nR))). + (tR A' A (sym_rel AR) n' n (nat_sym _ _ nR))). + exact (tR_sym A A' AR n n' nR). - + exact (Map4 A' A (Param44_sym A A' AR) n' n (Param_nat_sym nR)). + + exact (Map4 A' A (Param44_sym A A' AR) n' n (nat_sym _ _ nR)). Defined. (* append ~ append *) diff --git a/generic/inductives/DeriveLib.v b/generic/inductives/DeriveLib.v new file mode 100644 index 00000000..b8fd44e0 --- /dev/null +++ b/generic/inductives/DeriveLib.v @@ -0,0 +1,15 @@ +(* Compatibility layer with elpi's derive *) +From elpi Require Export elpi. +From Trocq Require Export Stdlib. +From Trocq Require Import HoTTNotations. + +Definition eq_f := @ap. +Register eq_f as elpi.derive.eq_f. +Register paths as elpi.eq. + +Definition bool_discr : Datatypes.true = Datatypes.false -> forall T : Type, T := +fun e T => + match e in _ = t + return match t with Datatypes.false => T | Datatypes.true => Unit end + with idpath => tt end. +Register bool_discr as elpi.bool_discr. \ No newline at end of file diff --git a/generic/inductives/Relnm.v b/generic/inductives/Relnm.v new file mode 100644 index 00000000..5dc5fb00 --- /dev/null +++ b/generic/inductives/Relnm.v @@ -0,0 +1,45 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "relnm.elpi" as relnm. +From Trocq Require Import sym symK RsymK Param_lemmas mapn map4. +Import HoTTNotations. + +From elpi.apps Require Import derive derive.param2. + +From Trocq Require Export Stdlib Hierarchy Param_lemmas. +Unset Uniform Inductive Parameters. + +Elpi Command derive.relnm. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.rsymK.db. +Elpi Accumulate Db Header trocq.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File relnm. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.rsymK.db. +Elpi Accumulate Db trocq.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, + coq.locate I (indt GR), + % Ind is (indt GR) + coq.gref->id (indt GR) Tname, + Suffix is Tname ^ "_", + derive.relnm.main GR Suffix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.relnm ". +}}. + +(* hook into derive *) +Elpi Accumulate Db Header derive.rsymK.db. +Elpi Accumulate derive File relnm. +Elpi Accumulate Db derive.rsymK.db. +Elpi Accumulate Db trocq.db. +Elpi Accumulate derive lp:{{ + +dep1 "relnm" "rsymK". +dep1 "relnm" "mapn". +derivation (indt T) Prefix ff (derive "relnm" (derive.relnm.main T Prefix) (trocq.db.param-ind-done T)). + +}}. diff --git a/generic/inductives/Rm.v b/generic/inductives/Rm.v new file mode 100644 index 00000000..6ea2bb95 --- /dev/null +++ b/generic/inductives/Rm.v @@ -0,0 +1,60 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "Rm.elpi" as Rm. + +From elpi Require Import elpi. +From Trocq Require Export Hierarchy Param_lemmas mymap. + +From elpi.apps Require Export derive derive.param2. + +Unset Uniform Inductive Parameters. +Elpi Db derive.Rm.db lp:{{ + % [ar-db A1 A2 AR] returns the relation between a type A1 and A2. + pred ar-db i:term, i:term, o:term. + + % [Rm-db T D] links an inductive type T to its corresponding R in map. + pred rm-def i:gref, o:gref. + pred rm-db i:term, o:term, o:term. + + % [Rm-done T] mean T was already derived + pred rm-done o:inductive. + + % refactor db dispatchers + rm-db I _ R :- + coq.env.global (indt GRI) I, + rm-def (indt GRI) GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.Rm. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.mymap.db. +Elpi Accumulate Db Header derive.Rm.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File Rm. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.mymap.db. +Elpi Accumulate Db derive.Rm.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + derive.Rm.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.Rm ". +}}. + +(* hook into derive *) +Elpi Accumulate derive Db Header derive.Rm.db. +Elpi Accumulate derive File Rm. +Elpi Accumulate derive Db derive.Rm.db. + +Elpi Accumulate derive lp:{{ +dep1 "Rm" "mymap". +dep1 "Rm" "param2". +derivation (indt T) Prefix ff (derive "Rm" (derive.Rm.main T Prefix) (rm-done T)). + +}}. diff --git a/generic/inductives/RsymK.v b/generic/inductives/RsymK.v new file mode 100644 index 00000000..09307fc6 --- /dev/null +++ b/generic/inductives/RsymK.v @@ -0,0 +1,71 @@ + +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "RsymK.elpi" as rsymK. +From Trocq Require Import sym symK. +Import HoTTNotations. + +From elpi.apps Require Import derive derive.param2. + +From Trocq Require Export Hierarchy. +Unset Uniform Inductive Parameters. + +Elpi Db derive.rsymK.db lp:{{ + + % [rsymK I S] links I inductive type, + % with the function showing i1 i2, [| I |]^ i2 i1 <->> [| I |] i1 i2 + pred rsymK-db i:term, o:term. + pred rsymK-def i:gref, o:gref. + + % [rsymK-done T K] means T K was already derived + pred rsymK-done o:inductive. + + % refactor db dispatchers + rsymK-db I R :- + coq.env.global (indt GRI) I, + rsymK-def (indt GRI) GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.rsymK. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.sym.db. +Elpi Accumulate Db Header derive.symK.db. +Elpi Accumulate Db Header derive.rsymK.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File rsymK. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.sym.db. +Elpi Accumulate Db derive.symK.db. +Elpi Accumulate Db derive.rsymK.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, + coq.locate I (indt GR), + % Ind is (indt GR) + coq.gref->id (indt GR) Tname, + Suffix is Tname ^ "_", + derive.rsymK.main GR Suffix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.rsymK ". +}}. + +(* hook into derive *) +Elpi Accumulate derive Db Header derive.rsymK.db. +Elpi Accumulate derive Db Header derive.sym.db. +Elpi Accumulate derive Db Header derive.symK.db. +Elpi Accumulate derive File rsymK. +Elpi Accumulate derive Db derive.rsymK.db. +Elpi Accumulate derive Db derive.sym.db. +Elpi Accumulate derive Db derive.symK.db. + +Elpi Accumulate derive lp:{{ + +dep1 "rsymK" "param2". +dep1 "rsymK" "sym". +dep1 "rsymK" "symK". +derivation (indt T) Prefix ff (derive "rsymK" (derive.rsymK.main T Prefix) (rsymK-done T)). + +}}. \ No newline at end of file diff --git a/generic/inductives/injK.v b/generic/inductives/injK.v new file mode 100644 index 00000000..3f161980 --- /dev/null +++ b/generic/inductives/injK.v @@ -0,0 +1,66 @@ + +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "injK.elpi" as injK. +From Trocq Require Export injection_lemmas. + +From Trocq Require Import DeriveLib HoTTNotations Stdlib Hierarchy. + +Unset Uniform Inductive Parameters. +Unset Universe Minimization ToSet. + +Unset Universe Polymorphism. +Definition conv (A : Type) (x y : A) (p: x = y) + (P : forall x0 : A, x = x0 -> Type) (P0 : P x idpath) := + match p as p0 in _ = t return (P t p0) + with idpath => P0 end. +Register conv as trocq.conv. +Set Universe Polymorphism. + +Elpi Db derive.injectionsK.db lp:{{ + + % [injectionsK-db I K ILs] links I, + % constructor inductive type, + % and K, + % a natural number > 0 (representing the constructor number) + % with the list of injectionK lemmas for that constructor + pred injectionsK-db i:term, i:int, o:term. + pred injectionsK-def i:gref, i:int, o:gref. + + % [injectionsK-done T K] means T K was already derived + pred injectionsK-done o:inductive. + + injectionsK-db K N R :- + coq.env.global (indc GRK) K, + injectionsK-def (indc GRK) N GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.injK. +Elpi Accumulate Db Header derive.injections.db. +Elpi Accumulate Db Header derive.injectionsK.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File injK. +Elpi Accumulate Db derive.injections.db. +Elpi Accumulate Db derive.injectionsK.db. +Elpi Accumulate lp:{{ + main [str I] :- !, coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + derive.injK.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.Rm ". +}}. + +(* hook into derive *) +Elpi Accumulate derive File injK. +Elpi Accumulate derive Db derive.injectionsK.db. + +Elpi Accumulate derive lp:{{ + +dep1 "injK" "injections". +derivation (indt T) Prefix ff (derive "injK" (derive.injK.main T Prefix) (injectionsK-done T)). + +}}. diff --git a/generic/inductives/injection_lemmas.v b/generic/inductives/injection_lemmas.v new file mode 100644 index 00000000..f9008b63 --- /dev/null +++ b/generic/inductives/injection_lemmas.v @@ -0,0 +1,61 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "injection_lemmas.elpi" as injections. + +From elpi.apps Require Export derive. +From elpi.apps Require Export derive.projK. +From Trocq Require Export DeriveLib. + +Unset Uniform Inductive Parameters. +Unset Universe Minimization ToSet. +Elpi Db derive.injections.db lp:{{ + + % [injections I K ILs] links I, + % constructor inductive type, + % and K, + % a natural number > 0 (representing the constructor number) + % with the list of injection lemmas for that constructor + pred injections-db i:term, i:int, o:term. + pred injections-def i:gref, i:int, o:gref. + + % [injections-done T K] means T K was already derived + pred injections-done o:inductive. + + injections-db K N R :- + coq.env.global (indc GRK) K, + injections-def (indc GRK) N GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.injections. +Elpi Accumulate Db Header derive.projK.db. +Elpi Accumulate Db Header derive.injections.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File injections. +Elpi Accumulate Db derive.projK.db. +Elpi Accumulate Db derive.injections.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, + coq.locate I (indt GR), + % Ind is (indt GR) + coq.gref->id (indt GR) Tname, + Suffix is Tname ^ "_", + derive.injections.main GR Suffix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.injections ". + +}}. + +(* hook into derive *) +Elpi Accumulate derive File injections. +Elpi Accumulate derive Db derive.injections.db. + +Elpi Accumulate derive lp:{{ + +dep1 "injections" "projK". +derivation (indt T) Prefix ff (derive "injections" (derive.injections.main T Prefix) (injections-done T)). + +}}. diff --git a/generic/inductives/mR.v b/generic/inductives/mR.v new file mode 100644 index 00000000..d9b9e373 --- /dev/null +++ b/generic/inductives/mR.v @@ -0,0 +1,69 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "mR.elpi" as mR. + +From elpi Require Import elpi. +From elpi.apps Require Export derive.param2 derive.isK. (* for isK db required by discriminate *) +From Trocq Require Export DeriveLib mymap injection_lemmas. + +From Trocq Require Export Hierarchy Param_lemmas Stdlib. +Unset Uniform Inductive Parameters. + +Elpi Db derive.mR.db lp:{{ + % [ar-db A1 A2 AR] returns the relation between a type A1 and A2. + pred ar-db i:term, i:term, o:term. + % [mR-db T D] links an inductive T to its corresponding map in R. + pred mR-def i:gref, o:gref. + + pred mR-db i:term, i:term, o:term. + + % [mR-done T] mean T was already derived + pred mR-done o:inductive. + + % refactor db dispatchers + mR-db I _ R :- + coq.env.global (indt GRI) I, + mR-def (indt GRI) GRR, + coq.env.global GRR R. +}}. + +Elpi Command derive.mR. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.isK.db. +Elpi Accumulate Db Header derive.mymap.db. +Elpi Accumulate Db Header derive.injections.db. +Elpi Accumulate Db Header derive.mR.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File mR. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.mymap.db. +Elpi Accumulate Db derive.isK.db. +Elpi Accumulate Db derive.injections.db. +Elpi Accumulate Db derive.mR.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + derive.mR.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.mR ". +}}. + +(* hook into derive *) +Elpi Accumulate derive File mR. +Elpi Accumulate derive Db derive.mR.db. + +#[phases="both"] Elpi Accumulate derive lp:{{ + dep1 "mR" "param2". + dep1 "mR" "mymap". + dep1 "mR" "injections". + dep1 "mR" "isK". +}}. + +Elpi Accumulate derive lp:{{ + +derivation (indt T) Prefix ff (derive "mR" (derive.mR.main T Prefix) (mR-done T)). + +}}. diff --git a/generic/inductives/mRRmK.v b/generic/inductives/mRRmK.v new file mode 100644 index 00000000..b52ea0b8 --- /dev/null +++ b/generic/inductives/mRRmK.v @@ -0,0 +1,72 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "mRRmK.elpi" as mRRmK. +From Trocq Require Export mymap injK mR Rm. + +From elpi Require Import elpi. +From elpi.apps Require Export derive.param2. +From Trocq Require Import Hierarchy. +Unset Uniform Inductive Parameters. + +Elpi Db derive.mRRmK.db lp:{{ + % [ar-db A1 A2 AR] returns the relation between a type A1 and A2. + pred ar-db i:term, i:term, o:term. + + % [mRRmK-def T D] links an inductive type T to its corresponding R in mapK. + pred mRRmK-def i:gref, o:gref. + + pred mRRmK-db i:term, o:term, o:term. + + % [mRRmK-done T] mean T was already derived + pred mRRmK-done o:inductive. + + % refactor db dispatchers + mRRmK-db I _ R :- + coq.env.global (indt GRI) I, + mRRmK-def (indt GRI) GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.mRRmK. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.injectionsK.db. +Elpi Accumulate Db Header derive.mymap.db. +Elpi Accumulate Db Header derive.mR.db. +Elpi Accumulate Db Header derive.Rm.db. +Elpi Accumulate Db Header derive.mRRmK.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File mRRmK. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.mymap.db. +Elpi Accumulate Db derive.injectionsK.db. +Elpi Accumulate Db derive.mR.db. +Elpi Accumulate Db derive.Rm.db. + +Elpi Accumulate Db derive.mRRmK.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + derive.mRRmK.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.mRRmK ". +}}. + + +(* hook into derive *) +Elpi Accumulate derive File mRRmK. +Elpi Accumulate derive Db derive.mRRmK.db. + +Elpi Accumulate derive lp:{{ + +dep1 "mRRmK" "param2". +dep1 "mRRmK" "mymap". +dep1 "mRRmK" "injK". +dep1 "mRRmK" "mR". +dep1 "mRRmK" "Rm". +derivation (indt T) Prefix ff (derive "mRRmK" (derive.mRRmK.main T Prefix) (mRRmK-done T)). + +}}. diff --git a/generic/inductives/map4.v b/generic/inductives/map4.v new file mode 100644 index 00000000..d391e572 --- /dev/null +++ b/generic/inductives/map4.v @@ -0,0 +1,7 @@ +From Trocq Require Export mymap. +From Trocq Require Export injection_lemmas. +From Trocq Require Export mR. +From Trocq Require Export Rm. +From Trocq Require Export injK. +From Trocq Require Export mRRmK. +From Trocq Require Export Stdlib Hierarchy. \ No newline at end of file diff --git a/generic/inductives/mapn.v b/generic/inductives/mapn.v new file mode 100644 index 00000000..e21cc3d5 --- /dev/null +++ b/generic/inductives/mapn.v @@ -0,0 +1,48 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi Extra Dependency "inductives/mapn.elpi" as mapn. +From Trocq Require Import Database map4. +Unset Uniform Inductive Parameters. + +Elpi Command derive.mapn. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.mymap.db. +Elpi Accumulate Db Header derive.mR.db. +Elpi Accumulate Db Header derive.Rm.db. +Elpi Accumulate Db Header derive.mRRmK.db. +Elpi Accumulate Db Header trocq.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File mapn. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.mymap.db. +Elpi Accumulate Db derive.mR.db. +Elpi Accumulate Db derive.Rm.db. +Elpi Accumulate Db derive.mRRmK.db. +Elpi Accumulate Db trocq.db. +Elpi Accumulate lp:{{ + main [str I] :- !, coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + derive.mapn.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.rel40 ". +}}. + +#[superglobal] Elpi Accumulate trocq.db lp:{{ + + trocq.db.map-ind I M R :- + coq.env.global (indt GRI) I, + trocq.db.map-def (indt GRI) M GRR, + coq.env.global GRR R. + +}}. +Elpi Accumulate derive File mapn. +Elpi Accumulate derive Db trocq.db. + +Elpi Accumulate derive lp:{{ + +dep1 "mapn" "mRRmK". +derivation (indt T) Prefix ff (derive "mapn" (derive.mapn.main T Prefix) (trocq.db.map-ind-done T)). + +}}. diff --git a/generic/inductives/mymap.v b/generic/inductives/mymap.v new file mode 100644 index 00000000..242bef47 --- /dev/null +++ b/generic/inductives/mymap.v @@ -0,0 +1,47 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "mymap.elpi" as mymap. + +From elpi Require Import elpi. +From elpi.apps Require Import derive. +From Trocq Require Export Stdlib Hierarchy. +Unset Uniform Inductive Parameters. + +Elpi Db derive.mymap.db lp:{{ + % [mymap-def I C] brings the constant defined for mapping inductive I. + pred mymap-def i:gref, o:gref. + + % [mymap T1 T2 D] for T1 and T2 brings a map D from T1 to T2. + pred mymap-db i:term, i:term, o:term. + + % [mymap-done T] mean T was already derived + pred mymap-done o:inductive. +}}. + +Elpi Command derive.mymap. +Elpi Accumulate Db Header derive.mymap.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File mymap. +Elpi Accumulate Db derive.mymap.db. +Elpi Accumulate lp:{{ + main [str I] :- !, + coq.locate I (indt GR), + coq.gref->id (indt GR) Tname, + Prefix is Tname ^ "_", + + derive.mymap.main GR Prefix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.mymap ". +}}. + +(* hook into derive *) +Elpi Accumulate derive Db Header derive.mymap.db. +Elpi Accumulate derive File mymap. +Elpi Accumulate derive Db derive.mymap.db. + +Elpi Accumulate derive lp:{{ + +derivation (indt T) Prefix ff (derive "mymap" (derive.mymap.main T Prefix) (mymap-done T)). + +}}. diff --git a/generic/inductives/sym.v b/generic/inductives/sym.v new file mode 100644 index 00000000..6cab0cc5 --- /dev/null +++ b/generic/inductives/sym.v @@ -0,0 +1,60 @@ +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "sym.elpi" as sym. + +From elpi.apps Require Export derive derive.param2. +From Trocq Require Export Hierarchy Stdlib. +Unset Uniform Inductive Parameters. + +Elpi Db derive.sym.db lp:{{ + + % [sym I S] links I inductive type, + % with the function showing symmetry + pred sym-db i:term, o:term. + pred sym-def i:gref, o:gref. + + % [sym-done T K] means T K was already derived + pred sym-done o:inductive. + + % refactor db dispatchers + sym-db I R :- + coq.env.global (indt GRI) I, + sym-def (indt GRI) GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.sym. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.sym.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File sym. +Elpi Accumulate Db derive.sym.db. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, + coq.locate I (indt GR), + % Ind is (indt GR) + coq.gref->id (indt GR) Tname, + Suffix is Tname ^ "_", + derive.sym.main GR Suffix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.sym ". +}}. + +(* hook into derive *) + + +Elpi Accumulate derive Db Header derive.sym.db. +Elpi Accumulate derive File sym. +Elpi Accumulate derive Db derive.sym.db. + +Elpi Accumulate derive lp:{{ + +dep1 "sym" "param2". +derivation (indt T) Prefix ff (derive "sym" (derive.sym.main T Prefix) (sym-done T)). + +}}. + diff --git a/generic/inductives/symK.v b/generic/inductives/symK.v new file mode 100644 index 00000000..97860bdd --- /dev/null +++ b/generic/inductives/symK.v @@ -0,0 +1,65 @@ + +From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. +From Trocq.Elpi.inductives Extra Dependency "symK.elpi" as symK. +From Trocq Require Import sym. + +From elpi.apps Require Import derive derive.param2. + +From Trocq Require Export Hierarchy Stdlib. +Unset Uniform Inductive Parameters. + +Elpi Db derive.symK.db lp:{{ + + % [symK I S] links I inductive type, + % with the function showing symmetry is "involutive" + pred symK-db i:term, o:term. + pred symK-def i:gref, o:gref. + + % [symK-done T K] means T K was already derived + pred symK-done o:inductive. + + % refactor db dispatchers + symK-db I R :- + coq.env.global (indt GRI) I, + symK-def (indt GRI) GRR, + coq.env.global GRR R. + +}}. + +Elpi Command derive.symK. +Elpi Accumulate Db Header derive.param2.db. +Elpi Accumulate Db Header derive.sym.db. +Elpi Accumulate Db Header derive.symK.db. +Elpi Accumulate File derive_hook. +Elpi Accumulate File symK. +Elpi Accumulate Db derive.param2.db. +Elpi Accumulate Db derive.sym.db. +Elpi Accumulate Db derive.symK.db. +Elpi Accumulate lp:{{ + + main [str I] :- !, + coq.locate I (indt GR), + % Ind is (indt GR) + coq.gref->id (indt GR) Tname, + Suffix is Tname ^ "_", + derive.symK.main GR Suffix _. + main _ :- usage. + + pred usage. + usage :- coq.error "Usage: derive.symK ". +}}. + +(* hook into derive *) +Elpi Accumulate derive Db Header derive.symK.db. +Elpi Accumulate derive Db Header derive.sym.db. +Elpi Accumulate derive File symK. +Elpi Accumulate derive Db derive.symK.db. +Elpi Accumulate derive Db derive.sym.db. + +Elpi Accumulate derive lp:{{ + +dep1 "symK" "param2". +dep1 "symK" "sym". +derivation (indt T) Prefix ff (derive "symK" (derive.symK.main T Prefix) (symK-done T)). + +}}. diff --git a/hott/Hierarchy.v b/hott/Hierarchy.v index 84fc549c..6515d682 100644 --- a/hott/Hierarchy.v +++ b/hott/Hierarchy.v @@ -89,16 +89,21 @@ End Map4. Register Map0.Has as trocq.map0. Register Map1.Has as trocq.map1. +Register Map1.map as trocq.map1.map. Register Map2a.Has as trocq.map2a. +(* I would rather define trocq.map2a.map-in-r in elpi *) +Register Map2a.map_in_R as trocq.map2a.map_in_r. Register Map2b.Has as trocq.map2b. +(* I would rather define trocq.map2b.r-in-map in elpi *) +Register Map2b.R_in_map as trocq.map2b.r_in_map. Register Map3.Has as trocq.map3. Register Map4.Has as trocq.map4. +Register Map4.R_in_mapK as trocq.map4.r_in_mapk. Elpi Query lp:{{register-map-classes}}. Definition sym_rel@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := fun b a => R a b. Register sym_rel as trocq.sym_rel. -Register paths as trocq.paths. Elpi Query lp:{{ coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.sym-rel {{:gref lib:trocq.sym_rel}})), diff --git a/hott/HoTTNotations.v b/hott/HoTTNotations.v new file mode 100644 index 00000000..ab782c60 --- /dev/null +++ b/hott/HoTTNotations.v @@ -0,0 +1 @@ +(* File for compatibility with /std *) \ No newline at end of file diff --git a/hott/Param_lemmas.v b/hott/Param_lemmas.v index d8f9a134..11a7a7a6 100644 --- a/hott/Param_lemmas.v +++ b/hott/Param_lemmas.v @@ -168,6 +168,220 @@ move=> RR' [m mR Rm RmK]; unshelve eexists m _ _. by case: RR' => /= f [/= g ]. Defined. +Register eq_Map0 as trocq.eq_map0. +Register eq_Map1 as trocq.eq_map1. +Register eq_Map2a as trocq.eq_map2a. +Register eq_Map2b as trocq.eq_map2b. +Register eq_Map3 as trocq.eq_map3. +Register eq_Map4 as trocq.eq_map4. + +Section rel_uniq_refl. + + Variable A : Type. + + Variable AR : A -> A -> Type. + Hypothesis AR_refl : forall a : A, AR a a. + Hypothesis AR_eqb : forall a1 a2 : A, AR a1 a2 -> a1 = a2. + Hypothesis rel_refl_uniq : forall (a : A) (r1 : AR a a), r1 = (AR_refl a). + + Lemma eqb_AR (a1 a2 : A) : a1 = a2 -> AR a1 a2. + Proof. by move=> ->; apply AR_refl. Qed. + + Lemma AR_irrel : forall (a1 a2 : A) (r1 r2 : AR a1 a2), r1 = r2. + Proof. + move=> a1 a2 r. + have e : a1 = a2 by apply AR_eqb. + move: r; rewrite {}e=> r1 r2. + by rewrite (rel_refl_uniq _ r1) (rel_refl_uniq _ r2). + Qed. + + Definition mapR : A -> A := idmap. + + Lemma mR : forall a1 a2 : A, mapR a1 = a2 -> AR a1 a2. + Proof. by move=> a1 a2; by rewrite /mapR=> ->; apply AR_refl. Qed. + + Lemma Rm : forall a1 a2 : A, AR a1 a2 -> idmap a1 = a2. + Proof. by move=> /= a1 a2 /AR_eqb ->. Qed. + + Lemma mRRmK : forall (a1 a2 : A) (r : AR a1 a2), mR a1 a2 (Rm a1 a2 r) = r. + Proof. by move=> a1 a2 r; apply AR_irrel. Qed. + + Lemma Map4_AR : Map4.Has AR. + Proof. + unshelve econstructor. + - by apply mapR. + - by apply mR. + - by apply Rm. + - by apply mRRmK. + Qed. + + Lemma AR_sym : forall a1 a2, AR a1 a2 -> AR a2 a1. + Proof. by move=> a1 a2 /AR_eqb ->; apply AR_refl. Qed. + + Lemma AR_sym_R : forall (a1 a2 : A), sym_rel AR a1 a2 <->> AR a1 a2. + Proof. + move=> a1 a2; unshelve eexists _,_ . + - by apply AR_sym. + - by apply AR_sym. + - by move=> r; apply AR_irrel. + Qed. + + Lemma Param44_AR : Param44.Rel A A. + Proof. + unshelve econstructor. + - exact AR. + - exact Map4_AR. + - apply (fun e => @eq_Map4 _ _ (sym_rel AR) AR e Map4_AR). + apply AR_sym_R. + Qed. + +End rel_uniq_refl. + +Section RmmRK. + + Variable A B : Type. + Variable R : A -> B -> Type. + Variable map : A -> B. + Variable map_in_R : forall x y, map x = y -> R x y. + Variable R_in_map : forall x y, R x y -> map x = y. + Variable mRRmK : forall x y (r : R x y), map_in_R _ _ (R_in_map _ _ r) = r. + + Definition F {x : A} {y : B} (p : map x = y) := apD (R_in_map x) p. + + Definition inverses_concat_tr : forall x y, + forall p : map x = y, + R_in_map x (map x) (map_in_R x (map x) 1) @ p + = R_in_map x y (transport _ p (map_in_R x (map x) 1)). + Proof. + move=> x y p. + rewrite -transport_paths_r. + apply Wdpath_arrow. + exact: F. + Defined. + + Definition path_shape {x y} : + forall p : map x = y, + p = (R_in_map x (map x) (map_in_R x (map x) 1))^ + @ R_in_map x y (transport _ p (map_in_R x (map x) 1)). + Proof. + move=> p. + rewrite -[X in X = _](concat_1p p). + rewrite -[X in X @ p](concat_Vp (R_in_map x (map x) (map_in_R x (map x) 1))). + rewrite concat_pp_p; apply ap. + apply inverses_concat_tr. + Defined. + + Lemma tr_1 : forall (x : A) y (p : map x = y), + transport (fun y=> R x y) p (map_in_R _ _ 1) = (map_in_R x y p). + Proof. + move=> x y p. + by case: _ / p . + Defined. + + Lemma Rm_concat : forall a b b' + (e : map a = b) + (e1 : b = b'), + R_in_map a b' (map_in_R a b' (e @ e1)) = + R_in_map a b (map_in_R a b e) @ e1. + Proof. + move=> a b1 b2 e e1. + by case: _ / e1; rewrite !concat_p1. + Defined. + + Definition RmmRK : forall a b (e : map a = b), + R_in_map _ _ (map_in_R _ _ e) = e. + Proof. + move=> a b e. + rewrite [X in _ = X](path_shape e). + rewrite tr_1. + set q := R_in_map a b _. + set p := R_in_map _ _ _. + apply (moveL_Vp q q p). + rewrite -Rm_concat concat_1p. + by rewrite /q mRRmK. + Defined. + +End RmmRK. +Section Genthm722. + + Variable A B : Type. + Variable R : A -> B -> Type. + Variable m : A -> B. + Variable Rrefl : forall x y, m x = y -> R x y. (* 2a *) + Variable imp : forall x y, R x y -> m x = y. (* 2b *) + Variable MereR : forall x y (r1 r2 : R x y), r1 = r2. + + Definition inverses_concat_tr' : forall x, + forall p : m x = m x, + imp x (m x) (Rrefl x _ 1) @ p = imp x (m x) (transport _ p (Rrefl x _ 1)). + Proof. + move=> x p. + rewrite -transport_paths_r. + apply Wdpath_arrow. + exact: F. + Defined. + + Definition path_shape' : forall x, + forall p : m x = m x, + p = (imp x (m x) (Rrefl x _ 1))^ @ imp x (m x) (@transport _ _ _ _ p (Rrefl x _ 1)). + Proof. + move=> x p. + rewrite -[X in X = _](concat_1p p). + rewrite -[X in X @ p](concat_Vp (imp x (m x) (Rrefl x _ 1))). + rewrite concat_pp_p. + apply ap. + apply inverses_concat_tr. + Defined. + + Lemma tr_id : forall (x : A) (p : m x = m x), + transport (fun y=> R x y) p (Rrefl x _ 1) = (Rrefl x _ 1). + Proof. move=> x p; apply MereR. Qed. + + Definition UIP_MA {x y : A} (p q : m x = m y): p = q. + Proof. + move: q. + case: _ /p. + move=> q. + rewrite (path_shape' x 1) /=. + rewrite (path_shape' x q). + by rewrite !tr_id. + Defined. + + Section surj. + + Hypothesis comap : B -> A. + Hypothesis corefl : forall b, R (comap b) b. + + Lemma UIP_B : forall (x y : B) (p q : x = y), p = q. + Proof. + move=> x y. + rewrite -(imp _ _ (corefl x)). + rewrite -(imp _ _ (corefl y)). + apply UIP_MA. + Qed. + + End surj. + +End Genthm722. + +Section thm722. + + Variable A : Type. + Variable R : A -> A -> Type. + Variable rrefl : forall x, R x x. (* 2a *) + Definition rrefl' : forall x y, x = y -> R x y. + by move=> x y p; case: _ /p; apply rrefl. + Defined. + Variable imp : forall x y, R x y -> x = y. (* 2b *) + Variable mereR : forall x y (r1 r2 : R x y), r1 = r2. + + Lemma uip_a (x y : A) (p q : x = y) : p = q. + Proof. + apply (UIP_MA A A R (idmap) (rrefl') imp). + by move=> e ?; apply mereR. + Qed. + +End thm722. (************************) (* Proofs about Param44 *) diff --git a/hott/Stdlib.v b/hott/Stdlib.v index 7e7d052e..1f6c1b05 100644 --- a/hott/Stdlib.v +++ b/hott/Stdlib.v @@ -17,3 +17,25 @@ From Trocq Require Export HoTT_additions. Module HoTTNotations. (* Stub for compatibility with stdlib version *) End HoTTNotations. + +Register paths as trocq.paths. +Register concat as trocq.concat. +Register idpath as trocq.idpath. +Register inverse as trocq.inverse. +Register paths_ind as trocq.paths_ind. +Register exist as trocq.exist. +Register ap as trocq.ap. + +Definition paths_nondep (A : Type) (x : A) (P : A -> Type) : P x -> forall y : A, x = y -> P y := + fun w y e=> paths_rect A x (fun a0 e => P a0) w y e. + +(* Weak HoTT.Types.Arrow.dpath_arrow. *) +Lemma Wdpath_arrow : forall {T : Type}{P Q : T -> Type} {x y : T} (p : x = y) + (f : P x -> Q x) (g : P y -> Q y), + transport (fun x => P x -> Q x) p f = g -> + forall x, transport _ p (f x) = g (transport _ p x). +Proof. +intros T P Q x y p. +destruct p; simpl; intros f g ->. +reflexivity. +Defined. diff --git a/hott/_CoqProject b/hott/_CoqProject index f3b6d9a6..aa6dc5b5 100644 --- a/hott/_CoqProject +++ b/hott/_CoqProject @@ -3,8 +3,10 @@ -arg -w -arg +elpi.typechecker -R . Trocq +-R ./generic/inductives Trocq -R ../elpi/ Trocq.Elpi +HoTTNotations.v Common.v Hierarchy.v HoTT_additions.v @@ -15,16 +17,31 @@ Param_arrow.v Param_forall.v Param_lemmas.v Stdlib.v + +generic/inductives/DeriveLib.v +generic/inductives/sym.v +generic/inductives/symK.v +generic/inductives/RsymK.v +generic/inductives/mymap.v +generic/inductives/injection_lemmas.v +generic/inductives/mR.v +generic/inductives/Rm.v +generic/inductives/injK.v +generic/inductives/mRRmK.v +generic/inductives/map4.v +generic/inductives/mapn.v +generic/inductives/Relnm.v + generic/Database.v generic/Param_Empty.v generic/Param_bool.v -generic/Param_list.v generic/Param_nat.v generic/Param_option.v -generic/Param_paths.v generic/Param_prod.v -generic/Param_sigma.v generic/Param_sum.v +generic/Param_list.v +generic/Param_paths.v +generic/Param_sigma.v generic/Param_trans.v generic/Param_vector.v generic/Trocq.v diff --git a/hott/generic/inductives b/hott/generic/inductives new file mode 120000 index 00000000..b05dbf4f --- /dev/null +++ b/hott/generic/inductives @@ -0,0 +1 @@ +../../generic/inductives \ No newline at end of file diff --git a/std/Hierarchy.v b/std/Hierarchy.v index 7696791f..629942c6 100644 --- a/std/Hierarchy.v +++ b/std/Hierarchy.v @@ -89,10 +89,14 @@ End Map4. Register Map0.Has as trocq.map0. Register Map1.Has as trocq.map1. +Register Map1.map as trocq.map1.map. Register Map2a.Has as trocq.map2a. +Register Map2a.map_in_R as trocq.map2a.map_in_r. Register Map2b.Has as trocq.map2b. +Register Map2b.R_in_map as trocq.map2b.r_in_map. Register Map3.Has as trocq.map3. Register Map4.Has as trocq.map4. +Register Map4.R_in_mapK as trocq.map4.r_in_mapk. Elpi Query lp:{{register-map-classes}}. Definition sym_rel@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := fun b a => R a b. @@ -100,7 +104,6 @@ Definition sym_rel@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := fun b a => R Import HoTTNotations. Register sym_rel as trocq.sym_rel. -Register paths as trocq.paths. Elpi Query lp:{{ coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.sym-rel {{:gref lib:trocq.sym_rel}})), diff --git a/std/Param_lemmas.v b/std/Param_lemmas.v index 428d68db..861264a2 100644 --- a/std/Param_lemmas.v +++ b/std/Param_lemmas.v @@ -168,3 +168,217 @@ move=> RR' [m mR Rm RmK]; unshelve eexists m _ _. - move=> a' b r /=; rewrite RmK. by case: RR' => /= f [/= g ]. Defined. + +Register eq_Map0 as trocq.eq_map0. +Register eq_Map1 as trocq.eq_map1. +Register eq_Map2a as trocq.eq_map2a. +Register eq_Map2b as trocq.eq_map2b. +Register eq_Map3 as trocq.eq_map3. +Register eq_Map4 as trocq.eq_map4. + +Section propRel. + + Variable A : Type. + + Variable AR : A -> A -> Type. + Hypothesis AR_refl : forall a : A, AR a a. + Hypothesis AR_eqb : forall a1 a2 : A, AR a1 a2 -> a1 = a2. + Hypothesis rel_refl_uniq : forall (a : A) (r1 : AR a a), r1 = (AR_refl a). + + Lemma eqb_AR (a1 a2 : A) : a1 = a2 -> AR a1 a2. + Proof. by move=> ->; apply AR_refl. Qed. + + Lemma AR_irrel : forall (a1 a2 : A) (r1 r2 : AR a1 a2), r1 = r2. + Proof. + move=> a1 a2 r. + have e : a1 = a2 by apply AR_eqb. + move: r; rewrite {}e=> r1 r2. + by rewrite (rel_refl_uniq _ r1) (rel_refl_uniq _ r2). + Qed. + + Definition mapR : A -> A := idmap. + + Lemma mR : forall a1 a2 : A, mapR a1 = a2 -> AR a1 a2. + Proof. by move=> a1 a2; by rewrite /mapR=> ->; apply AR_refl. Qed. + + Lemma Rm : forall a1 a2 : A, AR a1 a2 -> idmap a1 = a2. + Proof. by move=> /= a1 a2 /AR_eqb ->. Qed. + + Lemma mRRmK : forall (a1 a2 : A) (r : AR a1 a2), mR a1 a2 (Rm a1 a2 r) = r. + Proof. by move=> a1 a2 r; apply AR_irrel. Qed. + + Lemma Map4_AR : Map4.Has AR. + Proof. + unshelve econstructor. + - by apply mapR. + - by apply mR. + - by apply Rm. + - by apply mRRmK. + Qed. + + Lemma AR_sym : forall a1 a2, AR a1 a2 -> AR a2 a1. + Proof. by move=> a1 a2 /AR_eqb ->; apply AR_refl. Qed. + + Lemma AR_sym_R : forall (a1 a2 : A), sym_rel AR a1 a2 <->> AR a1 a2. + Proof. + move=> a1 a2; unshelve eexists _,_ . + - by apply AR_sym. + - by apply AR_sym. + - by move=> r; apply AR_irrel. + Qed. + + Lemma Param44_AR : Param44.Rel A A. + Proof. + unshelve econstructor. + - exact AR. + - exact Map4_AR. + - apply (fun e => @eq_Map4 _ _ (sym_rel AR) AR e Map4_AR). + apply AR_sym_R. + Qed. + +End propRel. + +Section RmmRK. + + Variable A B : Type. + Variable R : A -> B -> Type. + Variable map : A -> B. + Variable map_in_R : forall x y, map x = y -> R x y. + Variable R_in_map : forall x y, R x y -> map x = y. + Variable mRRmK : forall x y (r : R x y), map_in_R _ _ (R_in_map _ _ r) = r. + + Definition F {x : A} {y : B} (p : map x = y) := apd (R_in_map x) p. + + Definition inverses_concat_tr : forall x y, + forall p : map x = y, + R_in_map x (map x) (map_in_R x (map x) 1) @ p + = R_in_map x y (transport _ p (map_in_R x (map x) 1)). + Proof. + move=> x y p. + rewrite -tr_concat. + apply Wdpath_arrow. + exact: F. + Defined. + + Definition path_shape {x y} : + forall p : map x = y, + p = (R_in_map x (map x) (map_in_R x (map x) 1))^ + @ R_in_map x y (transport _ p (map_in_R x (map x) 1)). + Proof. + move=> p. + rewrite -[LHS](concat_1p p). + rewrite -[X in X @ p](concat_Vp (R_in_map x (map x) (map_in_R x (map x) 1))). + rewrite concat_pp_p; apply ap. + by apply inverses_concat_tr. + Defined. + + Lemma tr_1 : forall (x : A) y (p : map x = y), + transport (fun y=> R x y) p (map_in_R _ _ 1) = (map_in_R x y p). + Proof. + move=> x y p. + by case: _ / p . + Defined. + + Lemma Rm_concat : forall a b b' + (e : map a = b) + (e1 : b = b'), + R_in_map a b' (map_in_R a b' (e @ e1)) = + R_in_map a b (map_in_R a b e) @ e1. + Proof. + move=> a b1 b2 e e1. + by case: _ / e1. + Defined. + + Definition RmmRK : forall a b (e : map a = b), + R_in_map _ _ (map_in_R _ _ e) = e. + Proof. + move=> a b e. + rewrite [RHS](path_shape e) tr_1. + set q := R_in_map a b _. + set p := R_in_map _ _ _. + apply (moveL_Vp p q q). + rewrite -Rm_concat concat_1p. + by rewrite /q mRRmK. + Defined. + +End RmmRK. +Section Genthm722. + + Variable A B : Type. + Variable R : A -> B -> Type. + Variable m : A -> B. + Variable Rrefl : forall x y, m x = y -> R x y. (* 2a *) + Variable imp : forall x y, R x y -> m x = y. (* 2b *) + Variable MereR : forall x y (r1 r2 : R x y), r1 = r2. + + Definition inverses_concat_tr' : forall x, + forall p : m x = m x, + imp x (m x) (Rrefl x _ 1) @ p = imp x (m x) (transport _ p (Rrefl x _ 1)). + Proof. + move=> x p. + rewrite -tr_concat. + apply Wdpath_arrow. + exact: F. + Defined. + + Definition path_shape' : forall x, + forall p : m x = m x, + p = (imp x (m x) (Rrefl x _ 1))^ @ imp x (m x) (@transport _ _ _ _ p (Rrefl x _ 1)). + Proof. + move=> x p. + rewrite -[LHS](concat_1p p). + rewrite -[X in X @ p = _](concat_Vp (imp x (m x) (Rrefl x _ 1))). + rewrite concat_pp_p. + apply ap. + apply inverses_concat_tr. + Defined. + + Lemma tr_id : forall (x : A) (p : m x = m x), + transport (fun y=> R x y) p (Rrefl x _ 1) = (Rrefl x _ 1). + Proof. move=> x p; apply MereR. Qed. + + Definition UIP_MA {x y : A} (p q : m x = m y): p = q. + Proof. + move: q. + case: _ / p. + move=> q. + rewrite (path_shape' x 1) /=. + rewrite (path_shape' x q). + by rewrite !tr_id. + Defined. + + Section surj. + + Hypothesis comap : B -> A. + Hypothesis corefl : forall b, R (comap b) b. + + Lemma UIP_B : forall (x y : B) (p q : x = y), p = q. + Proof. + move=> x y. + rewrite -(imp _ _ (corefl x)). + rewrite -(imp _ _ (corefl y)). + apply UIP_MA. + Qed. + + End surj. + +End Genthm722. + +Section thm722. + + Variable A : Type. + Variable R : A -> A -> Type. + Variable rrefl : forall x, R x x. (* 2a *) + Definition rrefl' : forall x y, x = y -> R x y. + by move=> x y p; case: _ /p; apply rrefl. + Defined. + Variable imp : forall x y, R x y -> x = y. (* 2b *) + Variable mereR : forall x y (r1 r2 : R x y), r1 = r2. + + Lemma uip_a (x y : A) (p q : x = y) : p = q. + Proof. + apply (UIP_MA A A R (@id A) (rrefl') imp). + by move=> e ?; apply mereR. + Qed. + +End thm722. \ No newline at end of file diff --git a/std/Stdlib.v b/std/Stdlib.v index a1b680f1..e850d07f 100644 --- a/std/Stdlib.v +++ b/std/Stdlib.v @@ -12,6 +12,14 @@ (*****************************************************************************) Require Import ssreflect. From Trocq Require Import HoTTNotations. +From elpi Require Export elpi. + +Register paths as trocq.paths. +Register idpath as trocq.idpath. +Register concat as trocq.concat. +Register inverse as trocq.inverse. +Register eq_ind as trocq.paths_ind. +Register existT as trocq.exist. Set Universe Polymorphism. Unset Universe Minimization ToSet. @@ -29,6 +37,7 @@ Definition inv_V {A : Type} {x y : A} (p : x = y) : (p^)^ = p := Definition ap := f_equal. Arguments ap {A B} f {x y}. +Register ap as trocq.ap. (* relation for forall *) Monomorphic Axiom Funext : Prop. @@ -159,3 +168,28 @@ Definition is_true: Bool -> Type := | false => Empty end. +Definition apd {T : Type}{P : T -> Type} (f : forall x, P x) {x y : T} (p : x = y) : + transport _ p (f x) = f y. +Proof. by case: _ / p. Defined. + +Lemma tr_concat {T : Type} {x y z : T} (p : x = y) (q : y = z) : transport _ q p = p @ q. +Proof. by case: _ /q; case: _ /p. Defined. + +Lemma moveL_Vp : forall {T : Type} + {x y : T} (p : x = y) {z : T} (q : y = z) (r : x = z), + p @ q = r -> q = p^ @ r. +Proof. +move=> T x y p. +case : _ / p => /= z q r. +by rewrite !concat_1p. +Defined. + +Lemma Wdpath_arrow : forall {T : Type}{P Q : T -> Type} {x y : T} (p : x = y) + (f : P x -> Q x) (g : P y -> Q y), + transport (fun x => P x -> Q x) p f = g -> + forall x, transport _ p (f x) = g (transport _ p x). +Proof. +move=> T P Q x y p. +case: _ / p. +by rewrite /transport/eq_rect_r/= => f g -> //. +Defined. \ No newline at end of file diff --git a/std/_CoqProject b/std/_CoqProject index b88b3df3..57daa0a4 100644 --- a/std/_CoqProject +++ b/std/_CoqProject @@ -2,6 +2,7 @@ -arg -w -arg +elpi.typechecker -R . Trocq +-R ./generic/inductives Trocq -R ../elpi/ Trocq.Elpi HoTTNotations.v @@ -14,16 +15,31 @@ Param_arrow.v Param_forall.v Param_lemmas.v Stdlib.v + +generic/inductives/DeriveLib.v +generic/inductives/sym.v +generic/inductives/symK.v +generic/inductives/RsymK.v +generic/inductives/mymap.v +generic/inductives/injection_lemmas.v +generic/inductives/mR.v +generic/inductives/Rm.v +generic/inductives/injK.v +generic/inductives/mRRmK.v +generic/inductives/map4.v +generic/inductives/mapn.v +generic/inductives/Relnm.v + generic/Database.v generic/Param_Empty.v generic/Param_bool.v -generic/Param_list.v generic/Param_nat.v generic/Param_option.v -generic/Param_paths.v generic/Param_prod.v -generic/Param_sigma.v generic/Param_sum.v +generic/Param_list.v +generic/Param_paths.v +generic/Param_sigma.v generic/Param_trans.v generic/Param_vector.v generic/Trocq.v diff --git a/std/generic/inductives b/std/generic/inductives new file mode 120000 index 00000000..b05dbf4f --- /dev/null +++ b/std/generic/inductives @@ -0,0 +1 @@ +../../generic/inductives \ No newline at end of file diff --git a/tests/_CoqProject.hott b/tests/_CoqProject.hott index 0dce3862..e002a367 100644 --- a/tests/_CoqProject.hott +++ b/tests/_CoqProject.hott @@ -3,6 +3,7 @@ -arg -w -arg +elpi.typechecker -R ../hott/ Trocq +-R ../generic/inductives Trocq -R ../elpi/ Trocq.Elpi unit_arrow_contravariant.v @@ -28,3 +29,17 @@ unit_transfer5.v unit_twoTranslations.v unit_typeArrow.v unit_type.v + +inductives/coverage.v +inductives/test_sym.v +inductives/test_symK.v +inductives/test_RsymK.v +inductives/test_mymap.v +inductives/test_injection_lemmas.v +inductives/test_mR.v +inductives/test_Rm.v +inductives/test_injK.v +inductives/test_mRRmK.v +inductives/test_map4.v +inductives/test_mapn.v +inductives/test_Relnm.v diff --git a/tests/_CoqProject.std b/tests/_CoqProject.std index 2e7b131f..dce87c4b 100644 --- a/tests/_CoqProject.std +++ b/tests/_CoqProject.std @@ -2,6 +2,7 @@ -arg -w -arg +elpi.typechecker -R ../std/ Trocq +-R ../generic/inductives Trocq -R ../elpi/ Trocq.Elpi unit_arrow_contravariant.v @@ -27,3 +28,17 @@ unit_transfer5.v unit_twoTranslations.v unit_typeArrow.v unit_type.v + +inductives/coverage.v +inductives/test_sym.v +inductives/test_symK.v +inductives/test_RsymK.v +inductives/test_mymap.v +inductives/test_injection_lemmas.v +inductives/test_mR.v +inductives/test_Rm.v +inductives/test_injK.v +inductives/test_mRRmK.v +inductives/test_map4.v +inductives/test_mapn.v +inductives/test_Relnm.v diff --git a/tests/inductives/coverage.v b/tests/inductives/coverage.v new file mode 100644 index 00000000..6944b858 --- /dev/null +++ b/tests/inductives/coverage.v @@ -0,0 +1,42 @@ +Unset Universe Polymorphism. +Unset Uniform Inductive Parameters. + +Inductive testFalse : Set :=. + +Inductive testUnit : Set := +| TT : testUnit. + +Inductive testBool : Set := +| Falseb +| Trueb. + +Inductive Wrap : Set := +| KWrap1 : forall _ : testUnit, Wrap. + +Inductive WrapMore : Set := +| KWrap : forall (_: testUnit) (_ : testBool), WrapMore +| KWrapWrap : forall (_ : Wrap), WrapMore +| F : forall (_ : testUnit) (_ : testUnit) (_ : testUnit), WrapMore. + +Inductive Nat : Set := +| O' +| S' : forall (_ : Nat), Nat. + +Inductive Box (A : Type) : Type := +| B : forall (_: A), Box A. + +Inductive Option (A : Type) : Type := +| None' : Option A +| Some' : forall (_ : A), Option A. + +Inductive Prod (A B : Type) : Type := +| PR : forall (_ : A) (_ : B), Prod A B. + +Inductive ThreeTypes (A B C : Type) := +| C1 : forall (_ : A), ThreeTypes A B C +| C2 : forall (_ : B), ThreeTypes A B C +| C3 : forall (_ : C), ThreeTypes A B C. + +Inductive List (A : Type) : Type := +| Nil : List A +| Cons : forall (_ : A) (_ : List A), List A. diff --git a/tests/inductives/test_Relnm.v b/tests/inductives/test_Relnm.v new file mode 100644 index 00000000..b0b43384 --- /dev/null +++ b/tests/inductives/test_Relnm.v @@ -0,0 +1,36 @@ +From Trocq Require Import Relnm. +Require Import coverage. + +Elpi derive testFalse. +Check testFalse_rel44. + +Elpi derive testUnit. +Check testUnit_rel44. + +Elpi derive testBool. +Check testBool_rel44. + +Elpi derive Wrap. +Check Wrap_rel44. + +Elpi derive WrapMore. +Check WrapMore_rel44. + +Elpi derive Nat. +Check Nat_rel44. + +Elpi derive Box. +Check Box_rel44. + +Elpi derive Option. +Check Option_rel44. + +Elpi derive Prod. +Check Prod_rel44. + +Elpi derive ThreeTypes. +Check ThreeTypes_rel44. + +Elpi derive List. +Check List_rel44. +Check List_rel2a2a. \ No newline at end of file diff --git a/tests/inductives/test_Rm.v b/tests/inductives/test_Rm.v new file mode 100644 index 00000000..b32db4a3 --- /dev/null +++ b/tests/inductives/test_Rm.v @@ -0,0 +1,47 @@ +From Trocq Require Import Rm. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.param2 testFalse. +Elpi derive.mymap testFalse. +Elpi derive.Rm testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.mymap testUnit. +Elpi derive.Rm testUnit. + +Elpi derive.param2 testBool. +Elpi derive.mymap testBool. +Elpi derive.Rm testBool. + +Elpi derive.param2 Wrap. +Elpi derive.mymap Wrap. +Elpi derive.Rm Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.mymap WrapMore. +Elpi derive.Rm WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.mymap Nat. +Elpi derive.Rm Nat. + +Elpi derive.param2 Box. +Elpi derive.mymap Box. +Elpi derive.Rm Box. + +Elpi derive.param2 Option. +Elpi derive.mymap Option. +Elpi derive.Rm Option. + +Elpi derive.param2 Prod. +Elpi derive.mymap Prod. +Elpi derive.Rm Prod. + +Elpi derive.param2 ThreeTypes. +Elpi derive.mymap ThreeTypes. +Elpi derive.Rm ThreeTypes. + +Elpi derive.param2 List. +Elpi derive.mymap List. +Elpi derive.Rm List. \ No newline at end of file diff --git a/tests/inductives/test_RsymK.v b/tests/inductives/test_RsymK.v new file mode 100644 index 00000000..cbb1f709 --- /dev/null +++ b/tests/inductives/test_RsymK.v @@ -0,0 +1,60 @@ + +From elpi.apps Require Import derive.param2. +From Trocq Require Import sym symK RsymK. +Require Import coverage. + +Elpi derive.param2 testFalse. +Elpi derive.sym testFalse. +Elpi derive.symK testFalse. +Elpi derive.rsymK testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.sym testUnit. +Elpi derive.symK testUnit. +Elpi derive.rsymK testUnit. + +Elpi derive.param2 testBool. +Elpi derive.sym testBool. +Elpi derive.symK testBool. +Elpi derive.rsymK testBool. + +Elpi derive.param2 Wrap. +Elpi derive.sym Wrap. +Elpi derive.symK Wrap. +Elpi derive.rsymK Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.sym WrapMore. +Elpi derive.symK WrapMore. +Elpi derive.rsymK WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.sym Nat. +Elpi derive.symK Nat. +Elpi derive.rsymK Nat. + +Elpi derive.param2 Box. +Elpi derive.sym Box. +Elpi derive.symK Box. +Elpi derive.rsymK Box. + +Elpi derive.param2 Option. +Elpi derive.sym Option. +Elpi derive.symK Option. +Elpi derive.rsymK Option. + +Elpi derive.param2 Prod. +Elpi derive.sym Prod. +Elpi derive.symK Prod. +Elpi derive.rsymK Prod. + + +Elpi derive.param2 ThreeTypes. +Elpi derive.sym ThreeTypes. +Elpi derive.symK ThreeTypes. +Elpi derive.rsymK ThreeTypes. + +Elpi derive.param2 List. +Elpi derive.sym List. +Elpi derive.symK List. +Elpi derive.rsymK List. \ No newline at end of file diff --git a/tests/inductives/test_injK.v b/tests/inductives/test_injK.v new file mode 100644 index 00000000..35a43d9a --- /dev/null +++ b/tests/inductives/test_injK.v @@ -0,0 +1,47 @@ +From Trocq Require Import injK. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.projK testFalse. +Elpi derive.injections testFalse. +Elpi derive.injK testFalse. + +Elpi derive.projK testUnit. +Elpi derive.injections testUnit. +Elpi derive.injK testUnit. + +Elpi derive.projK testBool. +Elpi derive.injections testBool. +Elpi derive.injK testBool. + +Elpi derive.projK Wrap. +Elpi derive.injections Wrap. +Elpi derive.injK Wrap. + +Elpi derive.projK WrapMore. +Elpi derive.injections WrapMore. +Elpi derive.injK WrapMore. + +Elpi derive.projK Nat. +Elpi derive.injections Nat. +Elpi derive.injK Nat. + +Elpi derive.projK Box. +Elpi derive.injections Box. +Elpi derive.injK Box. + +Elpi derive.projK Option. +Elpi derive.injections Option. +Elpi derive.injK Option. + +Elpi derive.projK Prod. +Elpi derive.injections Prod. +Elpi derive.injK Prod. + +Elpi derive.projK ThreeTypes. +Elpi derive.injections ThreeTypes. +Elpi derive.injK ThreeTypes. + +Elpi derive.projK List. +Elpi derive.injections List. +Elpi derive.injK List. \ No newline at end of file diff --git a/tests/inductives/test_injection_lemmas.v b/tests/inductives/test_injection_lemmas.v new file mode 100644 index 00000000..44230065 --- /dev/null +++ b/tests/inductives/test_injection_lemmas.v @@ -0,0 +1,36 @@ +From Trocq Require Import injection_lemmas. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.projK testFalse. +Elpi derive.injections testFalse. + +Elpi derive.projK testUnit. +Elpi derive.injections testUnit. + +Elpi derive.projK testBool. +Elpi derive.injections testBool. + +Elpi derive.projK Wrap. +Elpi derive.injections Wrap. + +Elpi derive.projK WrapMore. +Elpi derive.injections WrapMore. + +Elpi derive.projK Nat. +Elpi derive.injections Nat. + +Elpi derive.projK Box. +Elpi derive.injections Box. + +Elpi derive.projK Option. +Elpi derive.injections Option. + +Elpi derive.projK Prod. +Elpi derive.injections Prod. + +Elpi derive.projK ThreeTypes. +Elpi derive.injections ThreeTypes. + +Elpi derive.projK List. +Elpi derive.injections List. \ No newline at end of file diff --git a/tests/inductives/test_mR.v b/tests/inductives/test_mR.v new file mode 100644 index 00000000..5c9155bb --- /dev/null +++ b/tests/inductives/test_mR.v @@ -0,0 +1,77 @@ +From Trocq Require Import mR. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.param2 testFalse. +Elpi derive.mymap testFalse. +Elpi derive.projK testFalse. +Elpi derive.injections testFalse. +Elpi derive.isK testFalse. +Elpi derive.mR testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.mymap testUnit. +Elpi derive.projK testUnit. +Elpi derive.injections testUnit. +Elpi derive.isK testUnit. +Elpi derive.mR testUnit. + +Elpi derive.param2 testBool. +Elpi derive.mymap testBool. +Elpi derive.isK testBool. +Elpi derive.mR testBool. + +Elpi derive.param2 Wrap. +Elpi derive.mymap Wrap. +Elpi derive.projK Wrap. +Elpi derive.injections Wrap. +Elpi derive.mR Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.mymap WrapMore. +Elpi derive.projK WrapMore. +Elpi derive.injections WrapMore. +Elpi derive.isK WrapMore. +Elpi derive.mR WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.mymap Nat. +Elpi derive.projK Nat. +Elpi derive.injections Nat. +Elpi derive.isK Nat. +Elpi derive.mR Nat. + +Elpi derive.param2 Box. +Elpi derive.mymap Box. +Elpi derive.projK Box. +Elpi derive.injections Box. +Elpi derive.isK Box. +Elpi derive.mR Box. + +Elpi derive.param2 Option. +Elpi derive.mymap Option. +Elpi derive.projK Option. +Elpi derive.injections Option. +Elpi derive.isK Option. +Elpi derive.mR Option. + +Elpi derive.param2 Prod. +Elpi derive.mymap Prod. +Elpi derive.projK Prod. +Elpi derive.injections Prod. +Elpi derive.isK Prod. +Elpi derive.mR Prod. + +Elpi derive.param2 ThreeTypes. +Elpi derive.mymap ThreeTypes. +Elpi derive.projK ThreeTypes. +Elpi derive.injections ThreeTypes. +Elpi derive.isK ThreeTypes. +Elpi derive.mR ThreeTypes. + +Elpi derive.param2 List. +Elpi derive.mymap List. +Elpi derive.projK List. +Elpi derive.injections List. +Elpi derive.isK List. +Elpi derive.mR List. \ No newline at end of file diff --git a/tests/inductives/test_mRRmK.v b/tests/inductives/test_mRRmK.v new file mode 100644 index 00000000..25333f12 --- /dev/null +++ b/tests/inductives/test_mRRmK.v @@ -0,0 +1,113 @@ +From Trocq Require Import mR Rm injK mRRmK. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.param2 testFalse. +Elpi derive.mymap testFalse. +Elpi derive.projK testFalse. +Elpi derive.injections testFalse. +Elpi derive.isK testFalse. +Elpi derive.mR testFalse. +Elpi derive.Rm testFalse. +Elpi derive.injK testFalse. +Elpi derive.mRRmK testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.mymap testUnit. +Elpi derive.projK testUnit. +Elpi derive.injections testUnit. +Elpi derive.isK testUnit. +Elpi derive.mR testUnit. +Elpi derive.Rm testUnit. +Elpi derive.injK testUnit. +Elpi derive.mRRmK testUnit. + +Elpi derive.param2 testBool. +Elpi derive.mymap testBool. +Elpi derive.projK testBool. +Elpi derive.injections testBool. +Elpi derive.isK testBool. +Elpi derive.mR testBool. +Elpi derive.Rm testBool. +Elpi derive.injK testBool. +Elpi derive.mRRmK testBool. + +Elpi derive.param2 Wrap. +Elpi derive.mymap Wrap. +Elpi derive.projK Wrap. +Elpi derive.injections Wrap. +Elpi derive.isK Wrap. +Elpi derive.mR Wrap. +Elpi derive.Rm Wrap. +Elpi derive.injK Wrap. +Elpi derive.mRRmK Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.mymap WrapMore. +Elpi derive.projK WrapMore. +Elpi derive.injections WrapMore. +Elpi derive.isK WrapMore. +Elpi derive.mR WrapMore. +Elpi derive.Rm WrapMore. +Elpi derive.injK WrapMore. +Elpi derive.mRRmK WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.mymap Nat. +Elpi derive.projK Nat. +Elpi derive.injections Nat. +Elpi derive.isK Nat. +Elpi derive.mR Nat. +Elpi derive.Rm Nat. +Elpi derive.injK Nat. +Elpi derive.mRRmK Nat. + +Elpi derive.param2 Box. +Elpi derive.mymap Box. +Elpi derive.projK Box. +Elpi derive.injections Box. +Elpi derive.isK Box. +Elpi derive.mR Box. +Elpi derive.Rm Box. +Elpi derive.injK Box. +Elpi derive.mRRmK Box. + +Elpi derive.param2 Option. +Elpi derive.mymap Option. +Elpi derive.projK Option. +Elpi derive.injections Option. +Elpi derive.isK Option. +Elpi derive.mR Option. +Elpi derive.Rm Option. +Elpi derive.injK Option. +Elpi derive.mRRmK Option. + +Elpi derive.param2 Prod. +Elpi derive.mymap Prod. +Elpi derive.projK Prod. +Elpi derive.injections Prod. +Elpi derive.isK Prod. +Elpi derive.mR Prod. +Elpi derive.Rm Prod. +Elpi derive.injK Prod. +Elpi derive.mRRmK Prod. + +Elpi derive.param2 ThreeTypes. +Elpi derive.mymap ThreeTypes. +Elpi derive.projK ThreeTypes. +Elpi derive.injections ThreeTypes. +Elpi derive.isK ThreeTypes. +Elpi derive.mR ThreeTypes. +Elpi derive.Rm ThreeTypes. +Elpi derive.injK ThreeTypes. +Elpi derive.mRRmK ThreeTypes. + +Elpi derive.param2 List. +Elpi derive.mymap List. +Elpi derive.projK List. +Elpi derive.injections List. +Elpi derive.isK List. +Elpi derive.mR List. +Elpi derive.Rm List. +Elpi derive.injK List. +Elpi derive.mRRmK List. \ No newline at end of file diff --git a/tests/inductives/test_map4.v b/tests/inductives/test_map4.v new file mode 100644 index 00000000..d195a20d --- /dev/null +++ b/tests/inductives/test_map4.v @@ -0,0 +1,45 @@ +From Trocq Require Import map4. +Import HoTTNotations. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive testFalse. +Check testFalse_mRRmK : forall f1 f2 fR, testFalse_mR f1 f2 (testFalse_Rm f1 f2 fR) = fR. + +Elpi derive testUnit. +Check testUnit_mRRmK : forall u1 u2 uR, testUnit_mR u1 u2 (testUnit_Rm u1 u2 uR) = uR. + +Elpi derive testBool. +Check testBool_mRRmK : forall b1 b2 bR, testBool_mR b1 b2 (testBool_Rm b1 b2 bR) = bR. + +Elpi derive Wrap. +Check Wrap_mRRmK : forall w1 w2 wR, Wrap_mR w1 w2 (Wrap_Rm w1 w2 wR) = wR. + +Elpi derive WrapMore. +Check WrapMore_mRRmK : forall w1 w2 wR, WrapMore_mR w1 w2 (WrapMore_Rm w1 w2 wR) = wR. + +Elpi derive Nat. +Check Nat_mRRmK : forall n1 n2 nR, Nat_mR n1 n2 (Nat_Rm n1 n2 nR) = nR. + +Elpi derive Box. +About Box_mRRmK. +(* Check Box_mRRmK. Bug? Why does it break? *) + +Elpi derive Option. +About Option_mRRmK. +(* Check Option_mRRmK : forall A1 A2 (AR : forall (_: A1) (_ : A2), Type) (AM : Map4.Has AR), + forall o1 o2 oR, Option_mR A1 A2 AR AM o1 o2 (Option_Rm A1 A2 AR AM o1 o2 oR) = oR. *) + +Elpi derive Prod. +Check Prod_mRRmK : forall A1 A2 (AR : forall (_ : A1) (_ : A2), Type) (AM : Map4.Has AR) B1 B2 (BR : forall (_ : B1) (_ : B2), Type) (BM : Map4.Has BR), + forall p1 p2 pR, Prod_mR A1 A2 AR AM B1 B2 BR BM p1 p2 (Prod_Rm A1 A2 AR AM B1 B2 BR BM p1 p2 pR) = pR. + +Elpi derive ThreeTypes. +Check ThreeTypes_mRRmK : +forall A1 A2 (AR : forall (_:A1) (_:A2), Type) (AM : Map4.Has AR), +forall B1 B2 (BR : forall (_:B1) (_:B2), Type) (BM : Map4.Has BR), +forall C1 C2 (CR : forall (_:C1) (_:C2), Type) (CM : Map4.Has CR), + forall t1 t2 tR, ThreeTypes_mR A1 A2 AR AM B1 B2 BR BM C1 C2 CR CM t1 t2 (ThreeTypes_Rm A1 A2 AR AM B1 B2 BR BM C1 C2 CR CM t1 t2 tR) = tR. + +Elpi derive List. +Check List_mRRmK : forall A1 A2 (AR : forall (_ :A1) (_ : A2), Type) (AM : Map4.Has AR), forall l1 t2 lR, List_mR A1 A2 AR AM l1 t2 (List_Rm A1 A2 AR AM l1 t2 lR) = lR. \ No newline at end of file diff --git a/tests/inductives/test_mapn.v b/tests/inductives/test_mapn.v new file mode 100644 index 00000000..a993aade --- /dev/null +++ b/tests/inductives/test_mapn.v @@ -0,0 +1,46 @@ +From Trocq Require Import map4 mapn. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive testFalse. +Check testFalse_map0 : Map0.Has testFalse_R. +Check testFalse_map1 : Map1.Has testFalse_R. +Check testFalse_map2a : Map2a.Has testFalse_R. +Check testFalse_map2b : Map2b.Has testFalse_R. +Check testFalse_map3 : Map3.Has testFalse_R. +Check testFalse_map4 : IsUMap testFalse_R. + +Elpi derive testUnit. +Check testUnit_map4 : IsUMap testUnit_R. + +Elpi derive testBool. +Check testBool_map4 : IsUMap testBool_R. + +Elpi derive Wrap. +Check Wrap_map4 : IsUMap Wrap_R. + +Elpi derive WrapMore. +Check WrapMore_map4 : IsUMap WrapMore_R. + +Elpi derive Nat. +Check Nat_map4 : IsUMap Nat_R. + +Elpi derive Box. +Check Box_map4 : forall A1 A2 AR UR, IsUMap (Box_R A1 A2 AR). + +Elpi derive Option. +Check Option_map4 : forall A1 A2 AR UR, IsUMap (Option_R A1 A2 AR). + +Elpi derive Prod. +Check Prod_map4 : forall A1 A2 AR UR B1 B2 BR BUR, IsUMap (Prod_R A1 A2 AR B1 B2 BR). + +Elpi derive ThreeTypes. +Check ThreeTypes_map4 : forall A1 A2 AR UR B1 B2 BR BUR C1 C2 CR CUR, IsUMap (ThreeTypes_R A1 A2 AR B1 B2 BR C1 C2 CR). + +Elpi derive List. +Check List_map0 : forall A1 A2 AR UR, Map0.Has (List_R A1 A2 AR). +Check List_map1 : forall A1 A2 AR UR, Map1.Has (List_R A1 A2 AR). +Check List_map2a: forall A1 A2 AR UR, Map2a.Has (List_R A1 A2 AR). +Check List_map2b: forall A1 A2 AR UR, Map2b.Has (List_R A1 A2 AR). +Check List_map3: forall A1 A2 AR UR, Map3.Has (List_R A1 A2 AR). +Check List_map4: forall A1 A2 AR UR, IsUMap (List_R A1 A2 AR). \ No newline at end of file diff --git a/tests/inductives/test_mymap.v b/tests/inductives/test_mymap.v new file mode 100644 index 00000000..dd8add1d --- /dev/null +++ b/tests/inductives/test_mymap.v @@ -0,0 +1,14 @@ +From Trocq Require Import mymap. +Require Import coverage. +Unset Uniform Inductive Parameters. + +Elpi derive.mymap testFalse. +Elpi derive.mymap testUnit. +Elpi derive.mymap testBool. +Elpi derive.mymap Wrap. +Elpi derive.mymap WrapMore. +Elpi derive.mymap Box. +Elpi derive.mymap Option. +Elpi derive.mymap Prod. +Elpi derive.mymap ThreeTypes. +Elpi derive.mymap List. diff --git a/tests/inductives/test_sym.v b/tests/inductives/test_sym.v new file mode 100644 index 00000000..572e9750 --- /dev/null +++ b/tests/inductives/test_sym.v @@ -0,0 +1,32 @@ +From elpi Require Import elpi. +From elpi.apps Require Import derive derive.param2. + +Require Import coverage. +From Trocq Require Import sym. + +Elpi derive.param2 testFalse. +Elpi derive.sym testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.sym testUnit. + +Elpi derive.param2 testBool. +Elpi derive.sym testBool. + +Elpi derive.param2 Wrap. +Elpi derive.sym Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.sym WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.sym Nat. + +Elpi derive.param2 Option. +Elpi derive.sym Option. + +Elpi derive.param2 Prod. +Elpi derive.sym Prod. + +Elpi derive.param2 List. +Elpi derive.sym List. \ No newline at end of file diff --git a/tests/inductives/test_symK.v b/tests/inductives/test_symK.v new file mode 100644 index 00000000..5f71bd98 --- /dev/null +++ b/tests/inductives/test_symK.v @@ -0,0 +1,40 @@ +From elpi Require Import elpi. +From elpi.apps Require Import derive.param2. +From Trocq Require Import sym symK. +Require Import coverage. + +Elpi derive.param2 testFalse. +Elpi derive.sym testFalse. +Elpi derive.symK testFalse. + +Elpi derive.param2 testUnit. +Elpi derive.sym testUnit. +Elpi derive.symK testUnit. + +Elpi derive.param2 testBool. +Elpi derive.sym testBool. +Elpi derive.symK testBool. + +Elpi derive.param2 Wrap. +Elpi derive.sym Wrap. +Elpi derive.symK Wrap. + +Elpi derive.param2 WrapMore. +Elpi derive.sym WrapMore. +Elpi derive.symK WrapMore. + +Elpi derive.param2 Nat. +Elpi derive.sym Nat. +Elpi derive.symK Nat. + +Elpi derive.param2 Option. +Elpi derive.sym Option. +Elpi derive.symK Option. + +Elpi derive.param2 Prod. +Elpi derive.sym Prod. +Elpi derive.symK Prod. + +Elpi derive.param2 List. +Elpi derive.sym List. +Elpi derive.symK List.