diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 6f17764..a192957 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -4,4 +4,4 @@ RUN opam update -y RUN opam install -y coq-lsp RUN git clone -b strat --depth 1 https://github.com/ecranceMERCE/coq-elpi RUN opam install -y ./coq-elpi -RUN opam install -y coq-hott.8.17 \ No newline at end of file +RUN opam install -y coq-mathcomp-algebra.1.19.0 \ No newline at end of file diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index b9b05a7..a8a1b78 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,6 +1,8 @@ { "name": "Trocq", - "image": "cohencyril/trocq-deps", + "build": { + "dockerfile": "Dockerfile" + }, "postAttachCommand": "make -j8 -k", "customizations": { "vscode": { diff --git a/.nix/config.nix b/.nix/config.nix index d50780c..43a9fcc 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -42,6 +42,7 @@ ## You can override Coq and other Coq coqPackages ## through the following attribute coqPackages.coq.override.version = "8.17"; + coqPackages.mathcomp.override.version = "1.19.0"; coqPackages.coq-elpi.override.version = "ecranceMERCE:strat"; ## In some cases, light overrides are not available/enough diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index c869a31..ee4c3d5 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"447fd9da2820c66dee263a327d62f3f3e9da2688" +"49d53bfc4d2ffbb834c6ee4360642a9b221704a0" diff --git a/.nix/coq-overlays/trocq/default.nix b/.nix/coq-overlays/trocq/default.nix index bba64ff..317459f 100644 --- a/.nix/coq-overlays/trocq/default.nix +++ b/.nix/coq-overlays/trocq/default.nix @@ -4,7 +4,7 @@ ## but the full doc is on nixos / nix packages website: ## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq -{ lib, mkCoqDerivation, which, coq, HoTT, coq-elpi +{ lib, mkCoqDerivation, which, coq, coq-elpi, mathcomp ## declare extra dependencies here, to be used in propagateBuildInputs e.g. # , mathcomp, coq-elpi , version ? null }: @@ -40,7 +40,7 @@ with lib; mkCoqDerivation { ## - arbitrary nix packages (you need to require them at the beginning of the file) ## - Coq packages (require them at the beginning of the file) ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) - propagatedBuildInputs = [ HoTT coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]` + propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.algebra coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]` ## Does the package contain OCaml code? mlPlugin = true; diff --git a/_CoqProject b/_CoqProject index 336efb0..9fa4f95 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,5 @@ --arg -noinit -arg -indices-matter +-arg -w -arg +elpi.typechecker -R theories/ Trocq -R elpi/ Trocq.Elpi diff --git a/coq-trocq.opam b/coq-trocq.opam index f1f95e0..03822a8 100644 --- a/coq-trocq.opam +++ b/coq-trocq.opam @@ -39,7 +39,8 @@ install: [make "install"] depends: [ "coq" {>= "8.17" & < "8.18"} "coq-elpi" {= "dev"} - "coq-hott" {>= "8.17" & < "8.18~"} + "coq-mathcomp-ssreflect" {>= "1.19.0" } + "coq-mathcomp-algebra" ] tags: [ diff --git a/elpi/annot.elpi b/elpi/annot.elpi index 619edb7..ff0fed3 100644 --- a/elpi/annot.elpi +++ b/elpi/annot.elpi @@ -22,7 +22,18 @@ coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs. % NB: the output type is term because the annotations are encoded directly in Coq % see PType in Param.v pred term->annot-term i:term, o:term. -term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.db.ptype PType, !, +term->annot-term (app [pglobal (const PPropGR) _, M, N] as P) P :- + trocq.db.pprop PPropGR, !, + cstr.univ-link _ M N. +term->annot-term (app [pglobal (const PTypeGR) _, M, N] as P) P :- + trocq.db.ptype PTypeGR, !, + cstr.univ-link _ M N. +term->annot-term (sort prop) (app [PProp , M, N]) :- + trocq.db.pprop PPropGR, !, + coq.env.global (const PPropGR) PProp, !, + cstr.univ-link _ M N. +term->annot-term (sort (typ U)) (app [pglobal (const PTypeGR) UI, M, N]) :- + trocq.db.ptype PTypeGR, !, coq.univ-instance UI [{coq.univ.variable U}], cstr.univ-link _ M N. term->annot-term (fun N T F) (fun N T' F') :- !, @@ -56,10 +67,11 @@ typecheck T ATy :- pred sub-type i:term, i:term. % SubSort sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :- - trocq.db.ptype PType, !, + (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![ cstr.univ-link C1 M1 N1, cstr.univ-link C2 M2 N2, - cstr.geq C1 C2. + cstr.geq C1 C2 + ]. % SubPi sub-type (prod N T F) (prod _ T' F') :- !, sub-type T' T, !, @@ -79,7 +91,7 @@ sub-type X Y :- coq.error "annot.sub-type:" X "vs" Y. % syntactic term equality, taking care of adding annotation equalities in the constraint graph pred eq i:term, i:term. eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2, N2]) :- - trocq.db.ptype PType, !, + (trocq.db.ptype PType; trocq.db.pprop PType), !, cstr.univ-link C1 M1 N1, cstr.univ-link C2 M2 N2, cstr.eq C1 C2. @@ -99,17 +111,17 @@ eq _ _ :- fail. % and none for output types that are not sorts, because it means values of type T are not type % constructors, so their translation will be made at class (0,0) pred classes i:term, o:list param-class, o:option param-class. -classes T Cs' Out :- +classes T Cs' Out :- std.do! [ all-classes T Cs, out-class T Out, if (not (Cs = []), Out = some C, std.last Cs LastC, LastC == C) ( std.drop-last 1 Cs Cs' ) ( Cs' = Cs - ). + )]. pred all-classes i:term, o:list param-class. -all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !, +all-classes (app [PCst, M, N]) [C] :- trocq.db.ptype-or-pprop PCst _, !, cstr.univ-link C M N. all-classes X Cs :- (X = prod _ T F ; X = fun _ T F), !, pi x\ std.append {all-classes T} {all-classes (F x)} Cs. @@ -120,7 +132,7 @@ all-classes X _ :- coq.error "all-classes:" X. % output class of a term pred out-class i:term, o:option param-class. -out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !, +out-class (app [PCst, M, N]) (some C) :- trocq.db.ptype-or-pprop PCst _, !, cstr.univ-link C M N. out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out. out-class (fun _ _ _) none :- !. diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi index a9c6c2f..dcdff10 100644 --- a/elpi/constraints/constraint-graph.elpi +++ b/elpi/constraints/constraint-graph.elpi @@ -114,18 +114,19 @@ maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained v % assign a constant class to a variable and update all the information in the graph % indeed, if the assigned variable was an output class for complex constraints, -% they can now be computed and reduced to simpler constraints on the other variables +% they can now be computed and reduced to simpler constraints on the other variables pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph. instantiate ID Class G _ :- util.when-debug dbg.steps (coq.say "instantiate" ID Class G), fail. instantiate ID Class (constraint-graph G) (constraint-graph G') :- - std.map.find ID G (pr LowerNodes HigherNodes), !, + std.map.find ID G (pr LowerNodes HigherNodes), !, std.do! [ internal.filter-var LowerNodes LowerIDs, util.unless (LowerIDs = []) (coq.error "wrong instantiation order: trying to instantiate" ID "before lower variables" LowerIDs), std.fold HigherNodes G (instantiate.aux ID Class) G1, - std.map.remove ID G1 G'. + std.map.remove ID G1 G' + ]. instantiate ID Class G G :- util.when-debug dbg.full ( coq.say "cannot instantiate" ID "at" Class "because it is not in the graph"). @@ -135,27 +136,30 @@ instantiate.aux ID Class (node.const C) G G :- util.unless (param-class.geq C Class) (coq.error "constraint not respected: instantiating" ID "at class" Class "despite upper bound" C). -instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- +instantiate.aux ID Class (node.var ct.pi [IDA, IDB]) G G' :- std.do![ util.map.update IDA (internal.remove-lower-node (node.var ct.pi [ID])) G G1, util.map.update IDB (internal.remove-lower-node (node.var ct.pi [ID])) G1 G2, % recompute the dependent product constraint and turn it into 2 order constraints param-class.dep-pi Class C1 C2, util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3, - util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'. -instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- + util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G' +]. +instantiate.aux ID Class (node.var ct.arrow [IDA, IDB]) G G' :- std.do![ util.map.update IDA (internal.remove-lower-node (node.var ct.arrow [ID])) G G1, util.map.update IDB (internal.remove-lower-node (node.var ct.arrow [ID])) G1 G2, % recompute the arrow type constraint and turn it into 2 order constraints param-class.dep-arrow Class C1 C2, util.map.update IDA (internal.add-lower-node (node.const C1)) G2 G3, - util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G'. -instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- + util.map.update IDB (internal.add-lower-node (node.const C2)) G3 G' +]. +instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- std.do![ util.map.update IDR (internal.remove-lower-node (node.var ct.type [ID])) G G1, % the constraint either vanishes or forces the relation to be (4,4) if (param-class.requires-axiom Class) (util.map.update IDR (internal.add-lower-node (node.const (pc map4 map4))) G1 G') - (G' = G1). -instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- + (G' = G1) +]. +instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- std.do! [ std.fold {std.filter IDs (id\ id > 0)} G (id\ g\ g'\ util.map.update id (internal.remove-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g') G1, @@ -164,7 +168,8 @@ instantiate.aux ID Class (node.var (ct.gref GR T Tm' GRR) IDs) G G' :- trocq.db.gref GR Class Cs GR' GRR, !, coq.env.global GR' Tm', % make sure the classes are consistent - instantiate.gref IDs TCs Cs G1 G'. + instantiate.gref IDs TCs Cs G1 G' + ]. pred instantiate.gref i:list class-id, i:list param-class, i:list param-class, i:constraint-graph-content, o:constraint-graph-content. @@ -174,12 +179,13 @@ instantiate.gref [-1|IDs] [TC|TCs] [C|Cs] G G' :- !, % we just check that it is equal to the required one TC = C, instantiate.gref IDs TCs Cs G G'. -instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- +instantiate.gref [ID|IDs] [_|TCs] [C|Cs] G G' :- std.do![ % here the identifier is not -1, which means that the class at this position is in the graph % we force it to be equal to C in the graph util.map.update ID (internal.add-lower-node (node.const C)) G G1, util.map.update ID (internal.add-higher-node (node.const C)) G1 G2, - instantiate.gref IDs TCs Cs G2 G'. + instantiate.gref IDs TCs Cs G2 G' +]. instantiate.aux ID Class (node.var ct.geq [IDH]) G G' :- % an order constraint is turned into a lower constant class util.map.update IDH (internal.remove-lower-node (node.var ct.geq [ID])) G G1, diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi index 41f3d0f..4109f79 100644 --- a/elpi/constraints/constraints.elpi +++ b/elpi/constraints/constraints.elpi @@ -56,10 +56,10 @@ dep-arrow C CA CB :- % D_□(C, C_R) pred dep-type i:param-class, i:param-class. -dep-type C CR :- var C, !, +dep-type C CR :- var C, !, std.do![ internal.link? C ID, internal.link? CR IDR, - declare_constraint (internal.c.dep-type ID IDR) [_]. + declare_constraint (internal.c.dep-type ID IDR) [_]]. dep-type C CR :- util.when (param-class.requires-axiom C) (geq CR (pc map4 map4)). @@ -118,9 +118,9 @@ pred c.vars? o:list class-id. pred c.vars! o:list class-id. pred vars? o:list class-id. -vars? IDs :- declare_constraint (c.vars? IDs) [_]. +vars? IDs :- !, declare_constraint (c.vars? IDs) [_]. pred vars! i:list class-id. -vars! IDs :- declare_constraint (c.vars! IDs) [_]. +vars! IDs :- !, declare_constraint (c.vars! IDs) [_]. constraint c.vars c.vars? c.vars! { rule (c.vars IDs) \ (c.vars? IDs') <=> (IDs' = IDs). @@ -216,21 +216,23 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra cstr-graph.add-geq IDorC1 IDorC2 G G', declare_constraint (c.graph G') [_] ). - rule \ (c.graph G) (c.reduce-graph) <=> ( + rule \ (c.graph G) (c.reduce-graph) <=> (std.do! [ + coq.say "final constraint graph START:", vars? IDs, - util.when-debug dbg.steps ( + util.when-debug dbg.full ( coq.say "final constraint graph:", cstr-graph.pp G, coq.say "***********************************************************************************" ), cstr-graph.instantiation-order IDs G SortedIDs, - util.when-debug dbg.steps ( + util.when-debug dbg.full ( coq.say "order:" SortedIDs, coq.say "***********************************************************************************" ), reduce SortedIDs G FinalValues, - util.when-debug dbg.steps (coq.say "final values:" FinalValues), + util.when-debug dbg.full (coq.say "final values:" FinalValues), std.forall FinalValues instantiate-coq + ] ). } @@ -238,23 +240,25 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra % return a list of associations of a variable and its constant class pred reduce i:list class-id, i:constraint-graph, o:list (pair class-id param-class). reduce [] _ []. -reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- +reduce [ID|IDs] ConstraintGraph [pr ID MinClass|FinalValues] :- std.do! [ cstr-graph.minimal-class ID ConstraintGraph MinClass, util.when-debug dbg.full (coq.say "min value" MinClass "for" ID), cstr-graph.maximal-class ID ConstraintGraph MaxClass, util.when-debug dbg.full (coq.say "max value" MaxClass "for" ID), util.unless (param-class.geq MaxClass MinClass) (coq.error "no solution for variable" ID), - reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues. + reduce IDs {cstr-graph.instantiate ID MinClass ConstraintGraph} FinalValues +]. % now instantiate for real pred instantiate-coq i:pair class-id param-class. -instantiate-coq (pr ID (pc M0 N0)) :- +instantiate-coq (pr ID (pc M0 N0)) :- std.do! [ util.when-debug dbg.full (coq.say "instantiating" ID "with" (pc M0 N0)), link- C ID, univ-link- C M N, map-class->term M0 M, map-class->term N0 N, - C = pc M0 N0. + C = pc M0 N0 +]. } % internal diff --git a/elpi/param.elpi b/elpi/param.elpi index 5a035e5..2771565 100644 --- a/elpi/param.elpi +++ b/elpi/param.elpi @@ -43,11 +43,13 @@ param (global GR) T' Tm' GrefR :- !, cstr.dep-gref GR T' Tm' GRR, GrefR = pglobal GRR _ ) ( - annot.typecheck (global GR) T, - annot.sub-type T T', - cstr.dep-gref GR T Tm' GRR, - weakening T T' (wfun W), - GrefR = (W (pglobal GRR _)) + std.do![ + annot.typecheck (global GR) T, + annot.sub-type T T', + cstr.dep-gref GR T Tm' GRR, + weakening T T' (wfun W), + GrefR = (W (pglobal GRR _)) + ] ). % universe-polymorphic case @@ -74,8 +76,12 @@ param X T' X' (W XR) :- name X, !, % TrocqSort param - (app [pglobal (const PType) UI, MR, NR] as Type) (app [pglobal (const PType) _, M, N]) - Type (app [pglobal (const PParamType) UI1|Args]) :- trocq.db.ptype PType, !, std.do! [ + (app [pglobal (const PType) UI, MR, NR] as Type) + (app [_, M, N]) + Type + (app [pglobal (const PParamType) UI1|Args]) :- + (trocq.db.ptype PType; trocq.db.pprop PType), !, + std.do! [ util.when-debug dbg.steps (coq.say "param/type" MR NR "@" M N), cstr.univ-link CR MR NR, util.when-debug dbg.full (coq.say "param/type:" MR NR "is linked to" CR), @@ -127,21 +133,24 @@ param (fun N T F) FunTy (fun N' T' F') FunR :- !, param (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N]) (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :- - trocq.db.ptype PType, !, std.do! [ + (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do! [ util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" M N), - cstr.univ-link C M N, !, + cstr.univ-link C M N, util.when-debug dbg.full (coq.say "param/arrow:" M N "is linked to" C), - cstr.dep-arrow C CA CB, !, + cstr.dep-arrow C CA CB, util.when-debug dbg.full (coq.say "param/arrow: added dep-arrow from" C "to" CA "and" CB), - cstr.univ-link CA MA NA, !, + cstr.univ-link CA MA NA, util.when-debug dbg.full (coq.say "param/arrow:" MA NA "is linked to" CA), - param A (app [pglobal (const PType) _, MA, NA]) A' AR, !, - cstr.univ-link CB MB NB, !, + std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", + if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA), + PTypeA = (app [pglobal (const PTypeGRA) _, MA, NA]), + param A PTypeA A' AR, + cstr.univ-link CB MB NB, util.when-debug dbg.full (coq.say "param/arrow:" MB NB "is linked to" CB), - param B (app [pglobal (const PType) _, MB, NB]) B' BR, !, + param B (app [pglobal (const PType) _, MB, NB]) B' BR, util.when-debug dbg.full (coq.say "param/arrow:" B "@" MB NB "~" B' "by" BR), util.when-debug dbg.full (coq.say "before db param-arrow" C), - trocq.db.param-arrow C ParamArrow, !, + trocq.db.param-arrow C ParamArrow, util.when-debug dbg.full (coq.say UI), prune UI [], util.when-debug dbg.full (coq.say "param/arrow: suspending proof on" C), @@ -158,7 +167,8 @@ param % TrocqPi param (prod N A B) (app [pglobal (const PType) _, M1, M2]) - (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- trocq.db.ptype PType, !, + (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- + (trocq.db.ptype PType; trocq.db.pprop PType), !, std.do![ util.when-debug dbg.steps (coq.say "param/forall" N ":" A "," B "@" M1 M2), coq.name-suffix N "'" N', coq.name-suffix N "R" NR, @@ -168,14 +178,17 @@ param util.when-debug dbg.full (coq.say "param/forall: added dep-pi from" C "to" CA "and" CB), cstr.univ-link CA M1A M2A, !, util.when-debug dbg.full (coq.say "param/forall:" M1A M2A "is linked to" CA), - param A (app [pglobal (const PType) _, M1A, M2A]) A' AR, + std.assert-ok! (coq.typecheck A TyA) "param/arrow: cannot typecheck A", + if (TyA = sort prop) (trocq.db.pprop PTypeGRA) (trocq.db.ptype PTypeGRA), + PTypeA = (app [pglobal (const PTypeGRA) _, M1A, M2A]), + param A PTypeA A' AR, cstr.univ-link CB M1B M2B, !, util.when-debug dbg.full (coq.say "param/forall:" M1B M2B "is linked to" CB), - @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => ( + @annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR => std.do![ util.when-debug dbg.full (coq.say "param/forall: introducing" a "@" A "~" a' "by" aR), param (B a) (app [pglobal (const PType) _, M1B, M2B]) (B' a') (BR a a' aR), !, util.when-debug dbg.full (coq.say "param/forall:" (B a) "@" M1B M2B "~" (B' a') "by" (BR a a' aR)) - ), + ], trocq.db.r CA RA, !, util.when-debug dbg.full (coq.say "param/forall db CA RA"), !, prune UIA [], @@ -193,7 +206,8 @@ param ) ( util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext not needed)"), Args' = Args - ). + ) + ]. % TrocqConv for F (argument B in param.args) + TrocqApp param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [ @@ -229,7 +243,7 @@ type wsuspend (term -> term) -> (term -> term) -> weakening. % cf definition of weakening in the paper pred weakening i:term, i:term, o:weakening. weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :- - trocq.db.ptype PType, !, + (trocq.db.ptype PType; trocq.db.pprop PType), !, trocq.db.weaken Weaken, prune UI [], prune Ty [], diff --git a/examples/N.v b/examples/N.v index e00db1a..721402a 100644 --- a/examples/N.v +++ b/examples/N.v @@ -11,8 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. -From HoTT Require Import HoTT. +From mathcomp Require Import all_ssreflect. From Trocq Require Import Common. Set Universe Polymorphism. @@ -109,8 +108,8 @@ Fixpoint of_nat (n : nat) : N := Lemma of_natD i j : of_nat (i + j) = (of_nat i + of_nat j)%N. Proof. -elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. -rewrite -nat_add_n_Sm/= IHi. +elim: i j => [//|i IHi] [|j]; first by rewrite addn0. +rewrite addSn addnS /= IHi. case: (of_nat i) => // p; case: (of_nat j) => //=. - by rewrite /succ/= Pos.addp1. - by move=> q; rewrite /succ/= Pos.addpS Pos.addSp. @@ -126,7 +125,7 @@ Proof. by case: n => //= ; elim=> //= p /of_nat_double/= ->. Defined. Lemma of_natK (n : nat) : to_nat (of_nat n) = n. Proof. elim: n => //= n IHn; rewrite -[in X in _ = X]IHn. -by case: (of_nat n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm. +by case: (of_nat n)=> //; elim=> //= p ->; rewrite /= addnS. Defined. Definition of_nat_iso := Iso.Build of_natK to_natK. diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 2fd852a..6b4b4bc 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -11,7 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. +From mathcomp Require Import ssreflect ssrfun ssrnat. From Trocq Require Import Trocq. From Trocq Require Import Param_nat Param_trans Param_bool Param_vector. @@ -23,7 +23,7 @@ Definition tuple (A : Type) : nat -> Type := fix F n := match n with | O => Unit - | S n' => F n' * A + | S n' => (F n' * A)%type end. Definition const : forall {A : Type} (a : A) (n : nat), tuple A n := @@ -77,7 +77,7 @@ Definition vector_to_tupleK {A : Type} : fix F n v := match v with | Vector.nil => idpath - | Vector.cons m a v' => ap (Vector.cons a) (F m v') + | Vector.cons _ a v' => ap (Vector.cons a) (F _ v') end. Definition tuple_to_vectorK {A : Type} : @@ -215,7 +215,7 @@ Trocq Use Param_append Param_const Param01_paths. Lemma append_const : forall {A : Type} (a : A) (n1 n2 : nat), append (const a n1) (const a n2) = const a (n1 + n2). Proof. - trocq. exact @Vector.append_const. + trocq; exact: @Vector.append_const. Qed. End AppendConst. @@ -279,10 +279,11 @@ Proof. by trocq. Qed. (* bounded nat and bitvector *) (* NB: we can use transitivity to make the proofs here too *) + Module BV. -Definition bounded_nat (k : nat) := {n : nat & n < pow 2 k}%nat. -Definition bitvector (k : nat) := Vector.t Bool k. +Definition bounded_nat (k : nat) := {n : nat & n < expn 2 n = true}%nat. +Definition bitvector := (Vector.t Bool). (* bounded_nat k ~ bitvector k' *) @@ -310,37 +311,12 @@ Definition bv_to_nat : forall {k : nat}, bitvector k -> nat := (match b with true => S | false => id end) (2 * F k' bv')%nat end. -Lemma S_add1 : forall (n : nat), S n = (n + 1)%nat. -Proof. - induction n. - - simpl. reflexivity. - - simpl add. apply ap. exact IHn. -Defined. - -Lemma one_lt_pow2 (k : nat) : (1 <= pow 2 k)%nat. -Proof. - induction k. - - simpl. apply leq_n. - - apply (leq_trans IHk). - simpl. - apply n_leq_add_n_k. -Defined. - -Axiom bv_bound : - forall {k : nat} (bv : bitvector k), (bv_to_nat bv <= pow 2 k - 1)%nat. - Definition bv_to_bnat {k : nat} (bv : bitvector k) : bounded_nat k. Proof. unshelve econstructor. - exact (bv_to_nat bv). - - apply (mixed_trans1 _ (pow 2 k - 1) _). - * apply bv_bound. - * apply natpmswap1. - 1: { apply one_lt_pow2. } - rewrite nat_add_comm. - rewrite <- (S_add1 (pow 2 k)). - apply n_lt_Sn. -Defined. + - by rewrite ltn_expl. +Qed. Axiom map_in_R_bv_bnat : forall {k : nat} {bv : bitvector k} {bn : bounded_nat k}, @@ -386,7 +362,7 @@ Definition Param44_bnat_bv (k k' : nat) (kR : natR k k') : Param44.Rel (bounded_nat k) (bitvector k'). Proof. unshelve eapply (@Param44_trans _ (bitvector k) _). - - exact Param44_bnat_bv_d. + - exact Param44_bnat_bv_d. - exact (Vector.Param44 Bool Bool Param44_Bool k k' kR). Defined. @@ -425,22 +401,21 @@ Axiom getBitR : (n n' : nat) (nR : natR n n'), BoolR (getBit_bnat bn n) (getBit_bv bv' n'). -(* lt ~ lt *) -Axiom Param10_lt : +Axiom Param10_le : forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'), - Param10.Rel (n1 < n2)%nat (n1' < n2')%nat. + BoolR (n1 <= n2)%nat (n1' <= n2')%nat. Axiom setBitThenGetSame : forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool), - (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b. + (i < k)%nat = true -> getBit_bv (setBit_bv bv i b) i = b. Trocq Use Param2a0_nat Param44_Bool Param2a0_bnat_bv getBitR setBitR. -Trocq Use Param01_paths Param10_lt. +Trocq Use Param01_paths Param10_paths Param10_le trueR SR. Lemma setBitThenGetSame' : forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool), - (i < k)%nat -> getBit_bnat (setBit_bnat bn i b) i = b. + (i < k)%nat = true -> getBit_bnat (setBit_bnat bn i b) i = b. Proof. trocq. exact @setBitThenGetSame. Qed. diff --git a/examples/artifact_paper_example.v b/examples/artifact_paper_example.v index d532b45..168e1a1 100644 --- a/examples/artifact_paper_example.v +++ b/examples/artifact_paper_example.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. From Trocq Require Import Trocq. From Trocq_examples Require Import N. @@ -29,7 +28,7 @@ Trocq Use RN. (* registering related types *) which we show relates the respective zero and successor constants of these types: *) Definition RN0 : RN 0%N 0%nat. Proof. done. Defined. -Definition RNS m n : RN m n -> RN (N.succ m) (S n). Proof. by case. Defined. +Definition RNS m n : RN m n -> RN (N.succ m) (S n). Proof. by case: _ /. Defined. Trocq Use RN0 RNS. (* registering related constants *) (** We can now make use of the tactic to prove an induction principle on `N` *) diff --git a/examples/flt3_step.v b/examples/flt3_step.v index b5a41df..2c58df8 100644 --- a/examples/flt3_step.v +++ b/examples/flt3_step.v @@ -71,7 +71,7 @@ Notation "x ≡ y" := (eqmodp x%int y%int) (format "x ≡ y", at level 70) : int_scope. Notation "x ≢ y" := (not (eqmodp x%int y%int)) (format "x ≢ y", at level 70) : int_scope. -Notation "x ≠ y" := (not (x = y)). +Notation "x ≠ y" := (not (x = y)) (at level 70). Notation "ℤ/9ℤ" := Zmod9. Notation ℤ := int. @@ -88,7 +88,9 @@ Variable Reqmodp01 : forall (m : int) (x : Zmod9), Rp m x -> Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01. -Trocq Use Param01_sum Param01_Empty Param10_Empty. +Trocq Use Param01_sum. +Trocq Use Param01_Empty. +Trocq Use Param10_Empty. Lemma flt3_step : forall (m n p : ℤ), m * n * p % 3 ≢ 0 -> (m³ + n³)%ℤ ≠ p³%ℤ. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 73eaff2..b51e3f2 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -11,18 +11,32 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. +From mathcomp Require Import all_ssreflect all_algebra. From Trocq Require Import Trocq. +Import GRing.Theory. +Local Open Scope bool_scope. Set Universe Polymorphism. -Declare Scope int_scope. -Delimit Scope int_scope with int. -Delimit Scope int_scope with ℤ. -Local Open Scope int_scope. -Declare Scope Zmod7_scope. -Delimit Scope Zmod7_scope with Zmod7. -Local Open Scope Zmod7_scope. +Lemma Zp_int_mod [p : nat] : 1 < p -> + forall n : int, ((n %% p)%Z%:~R)%R = (n%:~R)%R :> 'Z_p. +Proof. +move=> p_gt1 n; rewrite [in RHS](divz_eq n p) [in RHS]intrD intrM. +by rewrite [p%:~R%R]char_Zp// mulr0 add0r. +Qed. + +Lemma val_Zp_int p : 1 < p -> + forall n : int, ((n%:~R)%R : 'Z_p)%:Z%R = (n %% p)%Z. +Proof. +move=> p_gt1 n; rewrite -Zp_int_mod//. +have: ((n %% p)%Z >= 0)%R by rewrite modz_ge0//; case: p p_gt1. +rewrite -[RHS]modz_mod; case: (n %% p)%Z => //= k _ /=. +by rewrite val_Zp_nat// modz_nat. +Qed. + +Section modp. +Variable (p : nat) (p_gt1 : p > 1). +Let p_gt0 : p > 0. by case: p p_gt1. Qed. Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ (f : X -> Y -> Z) (g : X' -> Y' -> Z') := @@ -32,90 +46,81 @@ Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ We setup an axiomatic context in order not to develop arithmetic modulo in Coq/HoTT. **) -Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int) - (mul : int -> int -> int) (one : int). -Axiom (addC : forall m n, add m n = add n m). -Axiom (Zmod7 : Type) (zerop : Zmod7) (addp : Zmod7 -> Zmod7 -> Zmod7) - (mulp : Zmod7 -> Zmod7 -> Zmod7) (onep : Zmod7). -Axiom (modp : int -> Zmod7) (reprp : Zmod7 -> int) - (reprpK : forall x, modp (reprp x) = x). - -Definition eqmodp (x y : int) := modp x = modp y. +Definition eqmodp (x y : int) := (x = y %[mod p])%Z. (* for now translations need the support of a global reference: *) -Definition eq_Zmod7 (x y : Zmod7) := (x = y). -Arguments eq_Zmod7 /. - -Notation "0" := zero : int_scope. -Notation "0" := zerop : Zmod7_scope. -Notation "1" := one : int_scope. -Notation "1" := onep : Zmod7_scope. -Notation "x == y" := (eqmodp x%int y%int) - (format "x == y", at level 70) : int_scope. -Notation "x + y" := (add x%int y%int) : int_scope. -Notation "x + y" := (addp x%Zmod7 y%Zmod7) : Zmod7_scope. -Notation "x * y" := (mul x%int y%int) : int_scope. -Notation "x * y" := (mulp x%Zmod7 y%Zmod7) : Zmod7_scope. -Notation "m ²" := (m * m)%int (at level 2) : int_scope. -Notation "m ²" := (m * m)%Zmod7 (at level 2) : Zmod7_scope. -Notation "m ³" := (m * m * m)%int (at level 2) : int_scope. -Notation "m ³" := (m * m * m)%Zmod7 (at level 2) : Zmod7_scope. -Notation "x ≡ y" := (eqmodp x%int y%int) - (format "x ≡ y", at level 70) : int_scope. -Notation "x ≢ y" := (not (eqmodp x%int y%int)) - (format "x ≢ y", at level 70) : int_scope. -Notation "x ≠ y" := (not (x = y)). -Notation "ℤ/7ℤ" := Zmod7. -Notation ℤ := int. -Notation "P ∨ Q" := (P + Q)%type. - -Module IntToZmod7. - -Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK). - -Axiom Rzero : Rp zero zerop. -Axiom Rone : Rp one onep. -Variable Radd : binop_param Rp Rp Rp add addp. -Variable Rmul : binop_param Rp Rp Rp mul mulp. -Variable Reqmodp01 : forall (m : int) (x : Zmod7), Rp m x -> - forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmod7 x y). - -Trocq Use Rp Rmul Rzero Rone Param10_paths Reqmodp01. -Trocq Use Param01_sum. - -Lemma IntRedModZp : forall (m n p : ℤ), - m = n²%ℤ -> m = p³%ℤ -> m ≡ 0 ∨ m ≡ 1. +Definition eq_Zmodp (x y : 'Z_p) := (x = y). + +Lemma eq_intZp (m n : int) : (m%:~R == n%:~R :> 'Z_p)%R = (m == n %[mod p])%Z. Proof. -trocq=> /=. -Admitted. +apply/eqP/eqP. + by move=> /(congr1 val)/(congr1 Posz); rewrite !val_Zp_int. +by move=> /(congr1 (fun n => n%:~R : 'Z_p)%R); rewrite !Zp_int_mod. +Qed. -(* Print Assumptions IntRedModZp. (* No Univalence *) *) +Lemma eq_natZp (m n : nat) : (m%:R == n%:R :> 'Z_p)%R = (m == n %[mod p]). +Proof. by rewrite (eq_intZp m n) !modz_nat. Qed. +Locate "==". + +Lemma intZp_eq0 (n : int) : (n%:~R == 0 :> 'Z_p)%R = (p %| n)%Z. +Proof. by rewrite -[0%R]/(0%:~R)%R eq_intZp mod0z; apply/eqP/dvdz_mod0P. Qed. + +Lemma natZp_eq0 (n : nat) : (n%:R == 0 :> 'Z_p)%R = (p %| n). +Proof. by rewrite -[0%R]/(0%:R)%R eq_natZp mod0n. Qed. -End IntToZmod7. +Search (_ %% _)%N ('I__). +Search GRing.natmul nat_of_ord. -Module Zmod7ToInt. +Arguments eq_Zmodp /. -Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). +Definition Zp := 'Z_p. +Arguments Zp /. -Axiom Rzero : Rp zerop zero. -Variable Radd : binop_param Rp Rp Rp addp add. -Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. +Lemma reprK : cancel (val : Zp -> int) (intmul 1 : int -> Zp). +Proof. exact: natr_Zp. Qed. -Trocq Use Rp Param01_paths Param10_paths Radd Rzero. +Definition Rp := SplitSurj.toParam (SplitSurj.Build reprK). +Lemma Rzero : Rp 0%R 0%R. Proof. done. Qed. -Goal (forall x y, x + y = y + x)%Zmod7. +Arguments graph /. + + +Definition int_add (x y : int) : int := (x + y)%R. +Definition int_mul (x y : int) : int := (x * y)%R. + +Definition Zp_add (x y : Zp) : 'Z_p := (x + y)%R. +Definition Zp_mul (x y : Zp) : 'Z_p := (x * y)%R. + +Lemma Radd : binop_param Rp Rp Rp (int_add) (Zp_add). +Proof. by move=> /= m _ <- n _ <- /=; rewrite rmorphD. Qed. + +Lemma Rmul : binop_param Rp Rp Rp (int_mul) (Zp_mul). +Proof. by move=> /= m _ <- n _ <- /=; rewrite rmorphM. Qed. + +Definition Reqmodp01 : forall (m : int) (x : 'Z_p), Rp m x -> + forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y). Proof. - trocq. - exact addC. +move=> /= m _ <- n _ <-; exists (fun _ _ => True) => //=. +by split=> /eqP; rewrite eq_intZp => /eqP. Qed. -Goal (forall x y z, x + y + z = y + x + z)%Zmod7. +Lemma RTrue : Param01.Rel True True. +Admitted. +Lemma Runit : Param01.Rel unit unit. +Admitted. +Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01 RTrue Runit. + +Local Open Scope ring_scope. + +Lemma IntRedModZp : + (forall (m n : 'Z_p), m = n * n -> m = n) -> + forall (m n : int), m = int_mul n n -> eqmodp m n. Proof. - intros x y z. - suff addpC: forall x y, (x + y = y + x)%Zmod7. { - by rewrite (addpC x y). } - trocq. - exact addC. +move=> Hyp. +trocq; simpl. +exact: Hyp. Qed. -End Zmod7ToInt. +(* Print Assumptions IntRedModZp. (* No Univalence *) *) + +End modp. diff --git a/examples/misc.v b/examples/misc.v index ec979e1..01f909e 100644 --- a/examples/misc.v +++ b/examples/misc.v @@ -13,7 +13,6 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. -From HoTT Require Import HoTT. From Trocq Require Import Trocq. Set Universe Polymorphism. @@ -22,20 +21,17 @@ Set Universe Polymorphism. (* Feel free to comment commands adding the axioms to the Trocq database, in order to see which goals can be pre-processed without them, and which ones cannot *) -Axiom u : Univalence. -Axiom f : Funext. - -Trocq Register Univalence u. -Trocq Register Funext f. +Section test. +Universe i. Goal (* Type@{i}. *) (* Type@{i} -> Type@{i}. *) (* forall (A : Type@{i}), A. *) - (* forall (A : Type@{i}), A -> A. *) + forall (A : Type@{i}), A -> A. (* forall (A B : Type@{i}), A -> B. *) (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}), F A. *) - forall (F : Type@{i} -> Type@{i}) (A B : Type@{i}), F A -> F B. + (* forall (F : Type@{i} -> Type@{i}) (A B : Type@{i}), F A -> F B. *) (* forall (F : Type@{i} -> Type@{i} -> Type@{i}) (A B : Type@{i}), F A B. *) (* forall (F : Type@{i} -> Type@{i} -> Type@{i}) (A B : Type@{i}), F A B -> F B A. *) (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}), F A -> forall (B : Type@{i}), F B. *) @@ -53,3 +49,4 @@ Goal Proof. trocq. Abort. +End test. \ No newline at end of file diff --git a/examples/nat_ind.v b/examples/nat_ind.v index b972c27..ba5609e 100644 --- a/examples/nat_ind.v +++ b/examples/nat_ind.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. From Trocq Require Import Trocq. Set Universe Polymorphism. diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index a290253..dac5aeb 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -11,8 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. -From HoTT Require Import HoTT. +From mathcomp Require Import all_ssreflect. From Trocq Require Import Trocq. From Trocq_examples Require Import N. @@ -28,7 +27,7 @@ Definition RN : Param2a3.Rel N nat := would be done in the context of raw parametricity *) Definition RN0 : RN 0%N 0%nat. Proof. done. Qed. -Definition RNS m n : RN m n -> RN m.+1%N n.+1%nat. Proof. by case. Qed. +Definition RNS m n : RN m n -> RN m.+1%N n.+1%nat. Proof. by case: _ /. Qed. Trocq Use RN RN0 RNS. diff --git a/examples/summable.v b/examples/summable.v index 1891128..e1e70c5 100644 --- a/examples/summable.v +++ b/examples/summable.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. From Trocq Require Import Trocq. Set Universe Polymorphism. @@ -179,11 +178,7 @@ Definition R_add_xnnR : forall (r1 : nnR) (re1 : xnnR), R_nnR r1 re1 -> forall (r2 : nnR) (re2 : xnnR), R_nnR r2 re2 -> R_nnR (r1 + r2) (re1 + re2). -Proof. -rewrite /R_nnR /extend. -move=> r1 [_ []|]; last by discriminate. -by move=> r2 [_ []|]; last by discriminate. -Qed. +Proof. by do 2!move=> ? [_ [<-]|//]. Qed. Definition seq_nnR_add : forall (r1 : summable) (re1 : seq_xnnR), Rrseq r1 re1 -> diff --git a/examples/trocq_setoid_rewrite.v b/examples/trocq_setoid_rewrite.v index 677653e..6c66930 100644 --- a/examples/trocq_setoid_rewrite.v +++ b/examples/trocq_setoid_rewrite.v @@ -12,16 +12,16 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. +From Coq Require Import Setoid. From Trocq Require Import Trocq. -Set Universe PolymoRinthism. +Set Universe Polymorphism. Declare Scope int_scope. Delimit Scope int_scope with int. -Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int) (p : int). -Axiom (eqmodp@{i} : int@{i} -> int@{i} -> Type@{i}). +Axiom (int : Type) (zero : int) (add : int -> int -> int) (p : int). +Axiom (eqmodp : int -> int -> Prop). Notation "x + y" := (add x%int y%int) : int_scope. Notation "x == y" := (eqmodp x%int y%int) (format "x == y", at level 70) : int_scope. @@ -50,7 +50,7 @@ Lemma eqmodp01 : Param01.Rel (m == n)%int (m' == n')%int. Proof. move=> m m' Rm n n' Rn. -apply: (@Param01.BuildRel (m == n)%int (m' == n')%int (fun _ _ => Unit)). +apply: (@Param01.BuildRel (m == n)%int (m' == n')%int (fun _ _ => unit)). - constructor. - by constructor => mn; apply (eqmodp_morph _ _ Rm _ _ Rn). Qed. diff --git a/theories/Common.v b/theories/Common.v index 5b5b0d9..56f8c7c 100644 --- a/theories/Common.v +++ b/theories/Common.v @@ -13,11 +13,12 @@ Require Import ssreflect. From elpi Require Export elpi. -From HoTT Require Export HoTT. From Trocq Require Export HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param Param_paths Vernac. +Set Universe Polymorphism. + Local Open Scope param_scope. Definition graph@{i} {A B : Type@{i}} (f : A -> B) := paths o f. @@ -104,14 +105,14 @@ Let section_in_retract b a (e : section f b = a) : f a = b := Definition toParam@{} : Param42a.Rel@{i} A B := @Param42a.BuildRel A B (graph f) - (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => idmap) (fun _ _ => idmap) (fun _ _ _ => 1%path)) (@Map2a.BuildHas@{i} _ _ _ _ section_in_retract). Definition toParamSym@{} : Param2a4.Rel@{i} B A := @Param2a4.BuildRel B A (sym_rel (graph f)) (@Map2a.BuildHas@{i} _ _ _ _ (section_in_retract)) - (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => idmap) (fun _ _ => idmap) (fun _ _ _ => 1%path)). End to. @@ -120,18 +121,6 @@ End SplitSurj. End SplitSurj. Arguments SplitSurj.Build {A B retract section}. -Module Equiv. -(* This is exactly adjointify *) -Definition fromParam@{i} {A B : Type@{i}} (R : Param33.Rel@{i} A B) : - A <~> B := {| - equiv_fun := map R; - equiv_isequiv := isequiv_adjointify _ (comap R) - (fun b => R_in_map R _ _ (comap_in_R R _ _ 1%path)) - (fun a => R_in_comap R _ _ (map_in_R R _ _ 1%path)) - |}. - -End Equiv. - Module Iso. Section Iso. Universe i. @@ -157,29 +146,18 @@ Let map_in_comap b a (e : f a = b) : comap f b = a := Let map_in_comapK b a (e : f a = b) : comap_in_map b a (map_in_comap b a e) = e. -Proof. -rewrite /map_in_comap /comap_in_map /mapK' /=. -elim: e => /=; rewrite concat_1p. -rewrite ?inv_pp -?ap_V ?inv_pp ?inv_V ?ap_pp ?concat_p_pp. -rewrite -!ap_compose concat_pp_p. -have := concat_A1p (comapK f) (ap f (mapK f a)). -rewrite -!ap_compose; move=> ->. -rewrite ap_V concat_pp_p; apply: moveR_Vp; rewrite concat_p1. -rewrite !concat_p_pp; apply: moveR_pM; rewrite concat_pV. -rewrite (concat_A1p (fun x => (comapK f x))). -by rewrite concat_pV. -Qed. +Proof. exact: Prop_irrelevance. Qed. Definition toParam@{} : Param44.Rel@{i} A B := @Param44.BuildRel A B (graph f) - (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => idmap) (fun _ _ => idmap) (fun _ _ _ => 1%path)) (@Map4.BuildHas@{i} _ _ _ _ comap_in_map map_in_comap map_in_comapK). Definition toParamSym@{} : Param44.Rel@{i} B A := @Param44.BuildRel B A (sym_rel (graph f)) (@Map4.BuildHas@{i} _ _ _ _ comap_in_map map_in_comap map_in_comapK) - (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => idmap) (fun _ _ => idmap) (fun _ _ _ => 1%path)). End to. diff --git a/theories/Database.v b/theories/Database.v index ab66b95..8a24ce6 100644 --- a/theories/Database.v +++ b/theories/Database.v @@ -13,7 +13,6 @@ From Coq Require Import ssreflect. From elpi Require Export elpi. -From HoTT Require Import HoTT. Require Import HoTT_additions. Set Universe Polymorphism. @@ -37,8 +36,13 @@ Elpi Db trocq.db lp:{{ % constants PType and Weaken registered so that we do not coq.locate every time pred trocq.db.ptype o:constant. + pred trocq.db.pprop o:constant. pred trocq.db.weaken o:constant. + pred trocq.db.ptype-or-pprop i:term, o:constant. + trocq.db.ptype-or-pprop (pglobal (const PCst) _) PCst :- !, + (trocq.db.ptype PCst; trocq.db.pprop PCst). + % param-type β α {{ Param(β)_Type(α) }} % with α the level of the R field, and β the structure given to it pred trocq.db.param-type o:param-class, o:param-class, o:constant. diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v index 241e99b..684de37 100644 --- a/theories/Hierarchy.v +++ b/theories/Hierarchy.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Database. From elpi Require Import elpi. @@ -36,6 +35,9 @@ Register map4 as trocq.indc_map4. Register sym_rel as trocq.sym_rel. Register paths as trocq.paths. +Local Open Scope fibration_scope. +Local Open Scope path_scope. + (*************************) (* Parametricity Classes *) (*************************) @@ -98,11 +100,13 @@ Register sym_rel as trocq.sym_rel. * that will be mapped to variables in the constraint graph *) Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}. +Definition PProp@{} (m n : map_class) (* : Type@{i+1} *) := Prop. (* placeholder for a weakening from (m, n) to (m', n') * replaced with a real weakening function once the ground classes are known *) Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a. Register PType as trocq.ptype. +Register PProp as trocq.pprop. Register weaken as trocq.weaken. Elpi Command genhierarchy. @@ -114,6 +118,8 @@ Elpi Accumulate File util. Elpi Query lp:{{ {{:gref lib:trocq.ptype}} = const PType, coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.ptype PType)), + {{:gref lib:trocq.pprop}} = const PProp, + coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pprop PProp)), {{:gref lib:trocq.weaken}} = const Weaken, coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.weaken Weaken)). }}. @@ -148,7 +154,8 @@ Elpi Accumulate lp:{{ field [] "contravariant" (app [pglobal ContravariantSubRecord UI, b, a, app [pglobal SymRel UI, a, b, r]]) (_\ end-record)))), - @primitive! => @udecl! [L] ff [] ff => coq.env.add-indt RelDecl TrocqInd,coq.env.indt TrocqInd _ _ _ _ [TrocqBuild] _, + coq.typecheck-indt-decl RelDecl _, + @primitive! => @udecl! [L] ff [] tt => coq.env.add-indt RelDecl TrocqInd,coq.env.indt TrocqInd _ _ _ _ [TrocqBuild] _, Rel = indt TrocqInd, coq.env.projections TrocqInd [some CR, some CovariantProj, some ContravariantProj], @@ -172,7 +179,8 @@ Elpi Accumulate lp:{{ (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ fun `P` (app [pglobal Rel UI, a, b]) p\ app [pglobal (const Pr) UI, a, b, app [pglobal R UI, a, b, p], app [pglobal Covariant UI, a, b, p]]), - @udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _ + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const field-name Decl _ @transparent! _ ), % generate projections on the contravariant subrecord map-class->cofields N NCoFields, @@ -187,7 +195,8 @@ Elpi Accumulate lp:{{ app [pglobal (const Pr) UI, b, a, app [pglobal SymRel UI, a, b, app [pglobal R UI, a, b, p]], app [pglobal Contravariant UI, a, b, p]]), - @udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _ + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const field-name Decl _ @transparent! _ ), % close module coq.env.end-module _. @@ -246,7 +255,8 @@ Elpi Accumulate lp:{{ app [pglobal CovariantMN UI, a, b, p]], app [pglobal ContravariantMN UI, a, b, p]]), param-class->add-2-suffix "_" Class (pc m1 N) "forget_" ForgetName, - @udecl! [L] ff [] ff => + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const ForgetName Decl _ @transparent! ForgetCst, @global! => coq.coercion.declare (coercion (const ForgetCst) 2 RelMN (grefclass RelM1N)) @@ -268,7 +278,8 @@ Elpi Accumulate lp:{{ app [pglobal SymRel UI, a, b, app [pglobal RMN UI, a, b, p]], app [pglobal ContravariantMN UI, a, b, p]]]), param-class->add-2-suffix "_" Class (pc M n1) "forget_" ForgetName, - @udecl! [L] ff [] ff => + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const ForgetName Decl _ @transparent! ForgetCst, @global! => coq.coercion.declare (coercion (const ForgetCst) 2 RelMN (grefclass RelMN1)) @@ -307,6 +318,7 @@ Elpi Query lp:{{ Definition rel {A B} (R : Param00.Rel A B) := Param00.R A B R. Coercion rel : Param00.Rel >-> Funclass. + Definition map {A B} (R : Param10.Rel A B) : A -> B := Map1.map _ (Param10.covariant A B R). Definition map_in_R {A B} (R : Param2a0.Rel A B) : @@ -345,203 +357,194 @@ Notation MkUMap := Map4.BuildHas. Arguments Map4.BuildHas {A B R}. Arguments Param44.BuildRel {A B R}. +(* General theorems *) +Lemma ind_map@{i} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') a + (P : forall a', AR a a' -> map AR a = a' -> Type@{i}) : + (P (map AR a) (map_in_R AR a (map AR a) 1%path) 1%path) -> + forall a' aR, P a' aR (R_in_map AR a a' aR). +Proof. +by move=> P1 a' aR; rewrite -[X in P _ X](R_in_mapK AR); case: _ / R_in_map. +Defined. + +Lemma ind_mapP@{i +} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') (a : A) + (P : forall a', AR a a' -> map@{i} AR a = a' -> Type@{i}) + (P1 : P (map@{i} AR a) (map_in_R@{i} AR a (map@{i} AR a) 1%path) 1%path) + (Q : forall a' aR e, P a' aR e -> Type@{i}) : + Q (map@{i} AR a) (map_in_R@{i} AR a (map@{i} AR a) 1%path) 1%path P1 -> + forall a' aR, + Q a' aR (R_in_map@{i} AR a a' aR) (@ind_map@{i} A A' AR a P P1 a' aR). +Proof. +rewrite /ind_map => Q1 a' aR. +case: {1 6}_ / R_in_mapK. +by case: _ / R_in_map. +Qed. + +Lemma weak_ind_map@{i} {A A' : Type@{i}} (AR : Param40.Rel@{i} A A') a + (P : forall a', AR a a' -> Type@{i}) : + (P (map AR a) (map_in_R AR a (map AR a) 1%path)) -> + forall a' aR, P a' aR. +Proof. by move=> P1 a' aR; elim/(ind_map AR): aR / _. Defined. + +Lemma ind_comap@{i} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a' + (P : forall a, AR a a' -> comap AR a' = a -> Type@{i}) : + (P (comap AR a') (comap_in_R AR a' (comap AR a') 1%path) 1%path) -> + forall a aR, P a aR (R_in_comap AR a' a aR). +Proof. +by move=> P1 a aR; rewrite -[X in P _ X](R_in_comapK AR); case: _ / R_in_comap. +Defined. + +Lemma ind_comapP@{i +} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a' + (P : forall a, AR a a' -> comap AR a' = a -> Type@{i}) + (P1 : P (comap@{i} AR a') (comap_in_R@{i} AR a' (comap@{i} AR a') 1%path) 1%path) + (Q : forall a aR e, P a aR e -> Type@{i}) : + Q (comap@{i} AR a') (comap_in_R@{i} AR a' (comap@{i} AR a') 1%path) 1%path P1 -> + forall a aR, + Q a aR (R_in_comap@{i} AR a' a aR) (@ind_comap@{i} A A' AR a' P P1 a aR). +Proof. +rewrite /ind_comap => Q1 a aR. +case: {1 6}_ / R_in_comapK. +by case: _ / R_in_comap. +Qed. + +Lemma weak_ind_comap@{i} {A A' : Type@{i}} (AR : Param04.Rel@{i} A A') a' + (P : forall a, AR a a' -> Type@{i}) : + (P (comap AR a') (comap_in_R AR a' (comap AR a') 1%path)) -> + forall a aR, P a aR. +Proof. by move=> P1 a aR; elim/(ind_comap AR): aR / _. Defined. + +Definition map_ind@{i} {A A' : Type@{i}} {PA : Param40.Rel@{i} A A'} + (a : A) (a' : A') (aR : PA a a') + (P : forall (a' : A'), PA a a' -> Type@{i}) : + P a' aR -> P (map PA a) (map_in_R PA a (map PA a) idpath). +Proof. by elim/(ind_map PA): _ aR / _. Defined. +(* + +apply (transport + (fun aR0 : PA a a' => + P a' aR0 -> P (map PA a) + (map_in_R PA a (map PA a) idpath)) + (R_in_mapK PA a a' aR) + (paths_rect A' (map PA a) + (fun (a0 : A') (e : map PA a = a0) => + P a0 (map_in_R PA a a0 e) -> + P (map PA a) + (map_in_R PA a (map PA a) idpath)) idmap a' + (R_in_map PA a a' aR))). +Defined. *) + +Definition comap_ind@{i} {A A' : Type@{i}} {PA : Param04.Rel@{i} A A'} + (a : A) (a' : A') (aR : PA a a') + (P : forall (a : A), PA a a' -> Type@{i}) : + P a aR -> P (comap PA a') (comap_in_R PA a' (comap PA a') idpath). +Proof. by elim/(ind_comap PA): _ aR / _. Defined. +(* Proof. +apply (transport + (fun aR0 : PA a a' => + P a aR0 -> P (comap PA a') + (comap_in_R PA a' (comap PA a') idpath)) + (R_in_comapK PA a' a aR) + (paths_rect A (comap PA a') + (fun (a0 : A) (e : comap PA a' = a0) => + P a0 (comap_in_R PA a' a0 e) -> + P (comap PA a') + (comap_in_R PA a' (comap PA a') idpath)) idmap a + (R_in_comap PA a' a aR))). +Defined. *) + + (* symmetry lemmas for Map *) -Definition eq_Map0@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> +Definition eq_Map0w@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <--> R' a a') -> Map0.Has@{i} R' -> Map0.Has@{i} R. Proof. move=> RR' []; exists. Defined. -Definition eq_Map1@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> +Definition eq_Map1w@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <--> R' a a') -> Map1.Has@{i} R' -> Map1.Has@{i} R. Proof. move=> RR' [m]; exists. exact. Defined. -Definition eq_Map2a@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> +Definition eq_Map2aw@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <--> R' a a') -> Map2a.Has@{i} R' -> Map2a.Has@{i} R. Proof. move=> RR' [m mR]; exists m. - move=> a' b /mR /(RR' _ _)^-1%equiv; exact. + move=> a' b /mR/(snd (RR' _ _)); exact. Defined. -Definition eq_Map2b@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> +Definition eq_Map2bw@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <--> R' a a') -> Map2b.Has@{i} R' -> Map2b.Has@{i} R. Proof. move=> RR' [m Rm]; unshelve eexists m. - - move=> a' b /(RR' _ _)/Rm; exact. + - move=> a' b /(fst (RR' _ _)) /Rm; exact. Defined. -Definition eq_Map3@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> +Definition eq_Map3w@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <--> R' a a') -> Map3.Has@{i} R' -> Map3.Has@{i} R. Proof. move=> RR' [m mR Rm]; unshelve eexists m. - - move=> a' b /mR /(RR' _ _)^-1%equiv; exact. - - move=> a' b /(RR' _ _)/Rm; exact. + - move=> a' b /mR /(snd (RR' _ _)); exact. + - move=> a' b /(fst (RR' _ _))/Rm; exact. Defined. -Definition eq_Map4@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : - (forall a a', R a a' <~> R' a a') -> - Map4.Has@{i} R' -> Map4.Has@{i} R. -Proof. -move=> RR' [m mR Rm RmK]; unshelve eexists m _ _. -- move=> a' b /mR /(RR' _ _)^-1%equiv; exact. -- move=> a' b /(RR' _ _)/Rm; exact. -- by move=> a' b r /=; rewrite RmK [_^-1%function _]equiv_funK. -Defined. +Definition flipw@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + (forall a a', R a a' <--> R' a a') := +fun Rab a a' => ((Rab a a').1, (Rab a a').2.1). -(* joined elimination of comap and comap_in_R *) +Definition eq_Map0@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map0.Has@{i} R' -> Map0.Has@{i} R. +Proof. by move=> /flipw/eq_Map0w. Defined. -Definition comap_ind {A A' : Type} {PA : Param04.Rel A A'} - (a : A) (a' : A') (aR : PA a a') - (P : forall (a : A), PA a a' -> Type) : - P a aR -> P (comap PA a') (comap_in_R PA a' (comap PA a') idpath). -Proof. -apply (transport - (fun aR0 : PA a a' => - P a aR0 -> P (comap PA a') - (comap_in_R PA a' (comap PA a') idpath)) - (R_in_comapK PA a' a aR) - (paths_rect A (comap PA a') - (fun (a0 : A) (e : comap PA a' = a0) => - P a0 (comap_in_R PA a' a0 e) -> - P (comap PA a') - (comap_in_R PA a' (comap PA a') idpath)) idmap a - (R_in_comap PA a' a aR))). -Defined. -(* proofs about Param44 *) +Definition eq_Map1@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map1.Has@{i} R' -> Map1.Has@{i} R. +Proof. by move=> /flipw/eq_Map1w. Defined. + +Definition eq_Map2a@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map2a.Has@{i} R' -> Map2a.Has@{i} R. +Proof. by move=> /flipw/eq_Map2aw. Defined. -Lemma umap_equiv_sigma (A B : Type@{i}) (R : A -> B -> Type@{i}) : - IsUMap R <~> - { map : A -> B | - { mR : forall (a : A) (b : B), map a = b -> R a b | - { Rm : forall (a : A) (b : B), R a b -> map a = b | - forall (a : A) (b : B), mR a b o Rm a b == idmap } } }. -Proof. by symmetry; issig. Defined. +Definition eq_Map2b@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map2b.Has@{i} R' -> Map2b.Has@{i} R. +Proof. by move=> /flipw/eq_Map2bw. Defined. -Lemma umap_equiv_isfun `{Funext} {A B : Type@{i}} - (R : A -> B -> Type@{i}) : IsUMap R <~> IsFun R. +Definition eq_Map3@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map3.Has@{i} R' -> Map3.Has@{i} R. +Proof. by move=> /flipw/eq_Map3w. Defined. + +Definition eq_Map4@{i} {A A' : Type@{i}} {R R' : A -> A' -> Type@{i}} : + (forall a a', R a a' <->> R' a a') -> + Map4.Has@{i} R' -> Map4.Has@{i} R. Proof. -apply (equiv_composeR' (umap_equiv_sigma _ _ R)). -transitivity (forall x : A, {y : B & {r : R x y & forall yr', (y; r) = yr'}}); -last first. { - apply equiv_functor_forall_id => a. - apply (equiv_compose' (issig_contr _)). - apply equiv_sigma_assoc'. -} -apply (equiv_compose' (equiv_sig_coind _ _)). -apply equiv_functor_sigma_id => map. -apply (equiv_compose' (equiv_sig_coind _ _)). -apply (equiv_composeR' (equiv_sigma_symm _)). -transitivity {f : forall x, R x (map x) & - forall (x : A) (y : B) (r : R x y), (map x; f x) = (y; r)}; -last first. { - apply equiv_functor_sigma_id => comap. - apply equiv_functor_forall_id => a. - exact: (equiv_composeR' equiv_forall_sigma). -} -transitivity - { f : forall x, R x (map x) & - forall (x : A) (y : B) (r : R x y), {e : map x = y & e # f x = r} }; -last first. { - apply equiv_functor_sigma_id => comap. - apply equiv_functor_forall_id => a. - apply equiv_functor_forall_id => b. - apply equiv_functor_forall_id => r. - apply (equiv_compose' equiv_path_sigma_dp). - apply equiv_functor_sigma_id => e. - exact: equiv_dp_path_transport. -} -transitivity - { f : forall x, R x (map x) & - forall x y, {g : forall (r : R x y), map x = y & - forall (r : R x y), g r # f x = r } }; -last first. { - apply equiv_functor_sigma_id => comap. - apply equiv_functor_forall_id => a. - apply equiv_functor_forall_id => b. - exact: equiv_sig_coind. -} -transitivity { f : forall x, R x (map x) & - forall x, { g : forall (y : B) (r : R x y), map x = y & - forall (y : B) (r : R x y), g y r # f x = r } }; -last first. { - apply equiv_functor_sigma_id => comap. - apply equiv_functor_forall_id => a. - exact: equiv_sig_coind. -} -transitivity - { f : forall x, R x (map x) & - {g : forall (x : A) (y : B) (r : R x y), map x = y & - forall x y r, g x y r # f x = r } }; -last first. -{ apply equiv_functor_sigma_id => comap; exact: equiv_sig_coind. } -apply (equiv_compose' (equiv_sigma_symm _)). -apply equiv_functor_sigma_id => Rm. -transitivity - { g : forall (x : A) (y : B) (e : map x = y), R x y & - forall (x : A) (y : B) (r : R x y), Rm x y r # g x (map x) idpath = r }. { - apply equiv_functor_sigma_id => mR. - apply equiv_functor_forall_id => a. - apply equiv_functor_forall_id => b. - apply equiv_functor_forall_id => r. - unshelve econstructor. { apply: concat. elim (Rm a b r). reflexivity. } - unshelve econstructor. { apply: concat. elim (Rm a b r). reflexivity. } - all: move=> r'; elim r'; elim (Rm a b r); reflexivity. -} -symmetry. -unshelve eapply equiv_functor_sigma. -- move=> mR a b e; exact (e # mR a). -- move=> mR mRK x y r; apply: mRK. -- apply: isequiv_biinv. - split; (unshelve eexists; first by move=> + a; apply) => //. - move=> r; apply path_forall => a; apply path_forall => b. - by apply path_arrow; elim. -- by move=> mR; unshelve econstructor. +move=> RR' [m mR Rm RmK]; unshelve eexists m _ _. +- move=> a' b /mR /(RR' _ _).2.1; exact. +- move=> a' b /(RR' _ _).1/Rm; exact. +- move=> a' b r /=; rewrite RmK. + by case: RR' => /= f [/= g ]. Defined. -Lemma uparam_equiv `{Univalence} {A B : Type} : (A <=> B) <~> (A <~> B). -Proof. -apply (equiv_compose' equiv_sig_relequiv^-1). -unshelve eapply equiv_adjointify. -- move=> [R mR msR]; exists R; exact: umap_equiv_isfun. -- move=> [R mR msR]; exists R; exact: (umap_equiv_isfun _)^-1%equiv. -- by move=> [R mR msR]; rewrite !equiv_invK. -- by move=> [R mR msR]; rewrite !equiv_funK. -Defined. -Definition id_umap {A : Type} : IsUMap (@paths A) := +Definition id_umap@{i} {A : Type@{i}} : IsUMap (@paths A) := MkUMap idmap (fun a b r => r) (fun a b r => r) (fun a b r => 1%path). -Definition id_sym_umap {A : Type} : IsUMap (sym_rel (@paths A)) := +Definition id_sym_umap@{i} {A : Type@{i}} : IsUMap (sym_rel (@paths A)) := MkUMap idmap (fun a b r => r^) (fun a b r => r^) (fun a b r => inv_V r). -Definition id_uparam {A : Type} : A <=> A := +Definition id_uparam@{i} {A : Type@{i}} : A <=> A := MkUParam id_umap id_sym_umap. -Lemma uparam_induction `{Univalence} A (P : forall B, A <=> B -> Type) : - P A id_uparam -> forall B f, P B f. -Proof. -move=> PA1 B f; rewrite -[f]/(B; f).2 -[B]/(B; f).1. -suff : (A; id_uparam) = (B; f). { elim. done. } -apply: path_ishprop; apply: hprop_inhabited_contr => _. -apply: (contr_equiv' {x : _ & A = x}). -apply: equiv_functor_sigma_id => {f} B. -symmetry; apply: equiv_compose' uparam_equiv. -exact: equiv_path_universe. -Defined. - -Lemma uparam_equiv_id `{Univalence} A : - uparam_equiv (@id_uparam A) = equiv_idmap. -Proof. exact: path_equiv. Defined. - (* instances of MapN for A = A *) (* allows to build id_ParamMN : forall A, ParamMN.Rel A A *) @@ -633,11 +636,12 @@ Elpi Accumulate lp:{{ coq.locate {calc ("id_Map" ^ NStr ^ "_sym")} IdMapSym, Decl = (fun `A` (sort (typ U)) a\ - app [pglobal BuildRel UI, a, a, app [pglobal Paths UI, a], + app [pglobal BuildRel UI, a, a, app [global Paths, a], app [pglobal IdMap UI, a], app [pglobal IdMapSym UI, a]]), IdParam is "id_Param" ^ MStr ^ NStr, - @udecl! [L] ff [] ff => coq.env.add-const IdParam Decl _ @transparent! _. + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const IdParam Decl _ @transparent! _. }}. Elpi Typecheck. @@ -675,7 +679,8 @@ Elpi Accumulate lp:{{ app [pglobal CovariantMN UI, a, b, p] ]), ParamSym is "Param" ^ MStr ^ NStr ^ "_sym", - @udecl! [L] ff [] ff => coq.env.add-const ParamSym Decl _ @transparent! _. + coq.typecheck Decl _ _, + @udecl! [L] ff [] tt => coq.env.add-const ParamSym Decl _ @transparent! _. }}. Elpi Typecheck. @@ -690,5 +695,165 @@ Elpi Query lp:{{ ). }}. + + +Definition Prop_id_Map0 {A : Prop} : Map0.Has (@paths A). +Proof. constructor. Defined. + +Definition Prop_id_Map0_sym {A : Prop} : Map0.Has (sym_rel (@paths A)). +Proof. constructor. Defined. + +Definition Prop_id_Map1 {A : Prop} : Map1.Has (@paths A). +Proof. constructor. exact idmap. Defined. + +Definition Prop_id_Map1_sym {A : Prop} : Map1.Has (sym_rel (@paths A)). +Proof. constructor. exact idmap. Defined. + +Definition Prop_id_Map2a {A : Prop} : Map2a.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). +Defined. + +Definition Prop_id_Map2a_sym {A : Prop} : Map2a.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). +Defined. + +Definition Prop_id_Map2b {A : Prop} : Map2b.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). +Defined. + +Definition Prop_id_Map2b_sym {A : Prop} : Map2b.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). +Defined. + +Definition Prop_id_Map3 {A : Prop} : Map3.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). + - exact (fun a b e => e). +Defined. + +Definition Prop_id_Map3_sym {A : Prop} : Map3.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). + - exact (fun A B e => e^). +Defined. + +Definition Prop_id_Map4 {A : Prop} : Map4.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). + - exact (fun a b e => e). + - exact (fun a b e => 1%path). +Defined. + +Definition Prop_id_Map4_sym {A : Prop} : Map4.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). + - exact (fun A B e => e^). + - exact (fun A B e => inv_V e). +Defined. + +(* generate id_ParamMN : forall A, ParamMN.Rel A A for all M N *) + +Elpi Accumulate lp:{{ + pred generate-prop-id-param i:param-class. + generate-prop-id-param (pc M N as Class) :- + map-class->string M MStr, + map-class->string N NStr, + trocq.db.rel Class _ BuildRelGR _ _ _, + Paths = {paths}, + coq.locate {calc ("Prop_id_Map" ^ MStr)} IdMapGR, + coq.locate {calc ("Prop_id_Map" ^ NStr ^ "_sym")} IdMapSymGR, + coq.env.global BuildRelGR BuildRel, + coq.env.global IdMapGR IdMap, + coq.env.global IdMapSymGR IdMapSym, + Decl = + (fun `A` (sort prop) a\ + app [BuildRel, a, a, app [global Paths, a], + app [IdMap, a], + app [IdMapSym, a]]), + IdParam is "Prop_id_Param" ^ MStr ^ NStr, + coq.typecheck Decl _ _, + @udecl! [] tt [] tt => coq.env.add-const IdParam Decl _ @transparent! _. +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + map-classes all Classes, + std.forall Classes (m\ + std.forall Classes (n\ + generate-prop-id-param (pc m n) + ) + ). +}}. + +(* Check id_Param00. *) +(* Check id_Param32b. *) + +(* symmetry property for Param *) + +Elpi Accumulate lp:{{ + pred generate-prop-param-sym i:param-class. + generate-prop-param-sym (pc M N as Class) :- + map-class->string M MStr, + map-class->string N NStr, + trocq.db.rel Class RelMNGR _ RMNGR CovariantMNGR ContravariantMNGR, + trocq.db.rel (pc N M) _ BuildRelNMGR _ _ _, + coq.env.global BuildRelNMGR BuildRelNM, + coq.env.global {sym-rel} SymRel, + coq.env.global RelMNGR RelMN, + coq.env.global RMNGR RMN, + coq.env.global ContravariantMNGR ContravariantMN, + coq.env.global CovariantMNGR CovariantMN, + Decl = + (fun `A` (sort prop) a\ fun `B` (sort prop) b\ + fun `R` (app [RelMN, a, b]) r\ + app [BuildRelNM, b, a, + app [SymRel, a, b, app [RMN, a, b, r]], + app [ContravariantMN, a, b, r], + app [CovariantMN, a, b, r] + ]), + ParamSym is "Prop_Param" ^ MStr ^ NStr ^ "_sym", + std.assert-ok! (coq.typecheck Decl _) "generate-prop-param-sym: Decl ill-typed", + @udecl! [] tt [] tt => coq.env.add-const ParamSym Decl _ @transparent! _. +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + map-classes all Classes, + std.forall Classes (m\ + std.forall Classes (n\ + generate-prop-param-sym (pc m n) + ) + ). +}}. + (* Check Param33_sym. Check Param2a4_sym. *) + +Arguments map : simpl never. +Arguments map_in_R : simpl never. +Arguments R_in_map : simpl never. +Arguments R_in_mapK : simpl never. +Arguments comap : simpl never. +Arguments comap_in_R : simpl never. +Arguments R_in_comap : simpl never. +Arguments R_in_comapK : simpl never. \ No newline at end of file diff --git a/theories/HoTT_additions.v b/theories/HoTT_additions.v index 6dfa192..1cd7801 100644 --- a/theories/HoTT_additions.v +++ b/theories/HoTT_additions.v @@ -11,123 +11,256 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. -From HoTT Require Export HoTT. +From Coq Require Import ssreflect ssrfun ssrbool. Set Universe Polymorphism. Unset Universe Minimization ToSet. -Definition equiv_forall_sigma {A : Type} {P : A -> Type} {Q : forall a, P a -> Type} : - (forall a (b : P a), Q a b) <~> forall x : { a : A | P a }, Q x.1 x.2. -Proof. -unshelve econstructor. { move=> f [a b]; exact (f a b). } -unshelve econstructor. { move=> g a b; exact (g (a; b)). } -all: constructor. -Defined. +(* Definition equiv_forall_sigma {A : Type} {P : A -> Type} {Q : forall a, P a -> Type} : *) +(* (forall a (b : P a), Q a b) <~> forall x : { a : A | P a }, Q x.1 x.2. *) +(* Proof. *) +(* unshelve econstructor. { move=> f [a b]; exact (f a b). } *) +(* unshelve econstructor. { move=> g a b; exact (g (a; b)). } *) +(* all: constructor. *) +(* Defined. *) -Lemma equiv_invK {A B} (e : A <~> B) x : e (e^-1%equiv x) = x. -Proof. by case: e => [f []]. Defined. +(* Lemma equiv_invK {A B} (e : A <~> B) x : e (e^-1%equiv x) = x. *) +(* Proof. by case: e => [f []]. Defined. *) -Lemma equiv_funK {A B} (e : A <~> B) x : e^-1%equiv (e x) = x. -Proof. by case: e => [f []]. Defined. +(* Lemma equiv_funK {A B} (e : A <~> B) x : e^-1%equiv (e x) = x. *) +(* Proof. by case: e => [f []]. Defined. *) -Definition IsFun {A B : Type@{i}} (R : A -> B -> Type@{i}) := - (forall x, Contr {y | R x y}). +(* Definition IsFun {A B : Type@{i}} (R : A -> B -> Type@{i}) := *) +(* (forall x, Contr {y | R x y}). *) -Fact isfun_isprop `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : - IsHProp (IsFun R). -Proof. typeclasses eauto. Defined. +(* Fact isfun_isprop `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : *) +(* IsHProp (IsFun R). *) +(* Proof. typeclasses eauto. Defined. *) -Lemma fun_isfun {A B : Type@{i}} (f : A -> B) : IsFun (fun x y => f x = y). -Proof. by move=> x; eexists (f x; 1%path) => -[y]; elim. Defined. +(* Lemma fun_isfun {A B : Type@{i}} (f : A -> B) : IsFun (fun x y => f x = y). *) +(* Proof. by move=> x; eexists (f x; 1%path) => -[y]; elim. Defined. *) Definition sym_rel@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := fun b a => R a b. -Lemma isequiv_isfun `{Univalence} {A B : Type@{i}} (f : A -> B) : - IsEquiv f <~> IsFun (fun x y => f y = x). -Proof. by symmetry; apply equiv_contr_map_isequiv. Defined. +(* Lemma isequiv_isfun `{Univalence} {A B : Type@{i}} (f : A -> B) : *) +(* IsEquiv f <~> IsFun (fun x y => f y = x). *) +(* Proof. by symmetry; apply equiv_contr_map_isequiv. Defined. *) -Lemma type_equiv_contr `{Univalence} {A : Type@{i}} : - A <~> {P : A -> Type | Contr {x : A & P x}}. -Proof. -apply equiv_inverse; unshelve eapply equiv_adjointify. -- move=> [F [[a ?] ?]]; exact a. -- by move=> a; exists (paths a); apply contr_basedpaths. -- done. -- move=> [P Pc]; unshelve eapply path_sigma. { - apply: path_arrow => a; apply: equiv_path_universe. - apply: equiv_inverse; apply: equiv_path_from_contr. - by case: Pc => -[]. } - by apply: path_contr. -Defined. +(* Lemma type_equiv_contr `{Univalence} {A : Type@{i}} : *) +(* A <~> {P : A -> Type | Contr {x : A & P x}}. *) +(* Proof. *) +(* apply equiv_inverse; unshelve eapply equiv_adjointify. *) +(* - move=> [F [[a ?] ?]]; exact a. *) +(* - by move=> a; exists (paths a); apply contr_basedpaths. *) +(* - done. *) +(* - move=> [P Pc]; unshelve eapply path_sigma. { *) +(* apply: path_arrow => a; apply: equiv_path_universe. *) +(* apply: equiv_inverse; apply: equiv_path_from_contr. *) +(* by case: Pc => -[]. } *) +(* by apply: path_contr. *) +(* Defined. *) -Lemma fun_equiv_isfun `{Univalence} {A B : Type} : - (A -> B) <~> {R : A -> B -> Type | IsFun R}. -Proof. -have fe : Funext by apply: Univalence_implies_Funext. -transitivity (A -> {P : B -> Type | Contr {y : B & P y}}). - { apply: equiv_postcompose'; exact type_equiv_contr. } -by apply (equiv_composeR' (equiv_sig_coind _ _)^-1). -Defined. +(* Lemma fun_equiv_isfun `{Univalence} {A B : Type} : *) +(* (A -> B) <~> {R : A -> B -> Type | IsFun R}. *) +(* Proof. *) +(* have fe : Funext by apply: Univalence_implies_Funext. *) +(* transitivity (A -> {P : B -> Type | Contr {y : B & P y}}). *) +(* { apply: equiv_postcompose'; exact type_equiv_contr. } *) +(* by apply (equiv_composeR' (equiv_sig_coind _ _)^-1). *) +(* Defined. *) -Lemma equiv_sig_relequiv `{Univalence} {A B : Type@{i}} : - (A <~> B) <~> RelEquiv A B. -Proof. -apply (equiv_composeR' (issig_equiv _ _)^-1). -apply (equiv_compose' issig_relequiv). -apply (equiv_compose' (equiv_sigma_assoc' _ _)^-1). -unshelve eapply equiv_functor_sigma. -- exact: fun_equiv_isfun. -- by move=> f; apply: isequiv_isfun. -- exact: equiv_isequiv. -- by move=> f; apply: equiv_isequiv. -Defined. +(* Lemma equiv_sig_relequiv `{Univalence} {A B : Type@{i}} : *) +(* (A <~> B) <~> RelEquiv A B. *) +(* Proof. *) +(* apply (equiv_composeR' (issig_equiv _ _)^-1). *) +(* apply (equiv_compose' issig_relequiv). *) +(* apply (equiv_compose' (equiv_sigma_assoc' _ _)^-1). *) +(* unshelve eapply equiv_functor_sigma. *) +(* - exact: fun_equiv_isfun. *) +(* - by move=> f; apply: isequiv_isfun. *) +(* - exact: equiv_isequiv. *) +(* - by move=> f; apply: equiv_isequiv. *) +(* Defined. *) -Definition apD10_path_forall_cancel `{Funext} : - forall {A : Type} {B : A -> Type} {f g : forall x : A, B x} (p : forall x, f x = g x), - apD10 (path_forall f g p) = p. -Proof. - intros. unfold path_forall. - apply moveR_equiv_M. - reflexivity. -Defined. +(* Definition apD10_path_forall_cancel `{Funext} : *) +(* forall {A : Type} {B : A -> Type} {f g : forall x : A, B x} (p : forall x, f x = g x), *) +(* apD10 (path_forall f g p) = p. *) +(* Proof. *) +(* intros. unfold path_forall. *) +(* apply moveR_equiv_M. *) +(* reflexivity. *) +(* Defined. *) + +(* Definition transport_apD10 : *) +(* forall {A : Type} {B : A -> Type} {a : A} (P : B a -> Type) *) +(* {t1 t2 : forall x : A, B x} {e : t1 = t2} {p : P (t1 a)}, *) +(* transport (fun (t : forall x : A, B x) => P (t a)) e p = *) +(* transport (fun (t : B a) => P t) (apD10 e a) p. *) +(* Proof. *) +(* intros A B a P t1 t2 [] p; reflexivity. *) +(* Defined. *) + +(* Definition coe_inverse_cancel {A B} (e : A = B) p: coe e (coe e^ p) = p. *) +(* Proof. elim: e p; reflexivity. Defined. *) + +(* Definition coe_inverse_cancel' {A B} (e : A = B) p : coe e^ (coe e p) = p. *) +(* Proof. elim: e p; reflexivity. Defined. *) + +(* Definition path_forall_types `{Funext} A F G : *) +(* (forall (a : A), F a = G a) -> (forall a, F a) = (forall a, G a). *) +(* Proof. by move=> /(path_forall _ _)->. Defined. *) + +(* Definition equiv_flip@{i k | i <= k} : *) +(* forall (A B : Type@{i}) (P : A -> B -> Type@{k}), *) +(* Equiv@{k k} (forall (a : A) (b : B), P a b) (forall (b : B) (a : A), P a b). *) +(* Proof. *) +(* intros A B P. *) +(* unshelve eapply Build_Equiv@{k k}. *) +(* - exact (@flip@{i i k} A B P). *) +(* - by unshelve eapply *) +(* (@Build_IsEquiv@{k k} *) +(* (forall (a : A) (b : B), P a b) (forall (b : B) (a : A), P a b) *) +(* (@flip@{i i k} A B P) *) +(* (@flip@{i i k} B A (fun (b : B) (a : A) => P a b))). *) +(* Defined. *) + + +Reserved Notation "p ^" (at level 3, format "p '^'"). +Reserved Notation "p @ q" (at level 20). +Reserved Notation "p # x" (right associativity, at level 65). +Reserved Notation "p # x" (right associativity, at level 65). +Reserved Notation "p @@ q" (at level 20). +Reserved Notation "p @' q" (at level 21, left associativity, + format "'[v' p '/' '@'' q ']'"). +Reserved Notation "f == g" (at level 70, no associativity). +Reserved Notation "g 'o' f" (at level 40, left associativity). + + +Notation "f == g" := (forall x, f x = g x). +Notation "g 'o' f" := ((fun g0 f0 x => g0 (f0 x)) g f). + +Declare Scope fibration_scope. +Open Scope fibration_scope. + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. + +Reserved Notation "x .1" (at level 2, left associativity, format "x '.1'"). +Reserved Notation "x .2" (at level 2, left associativity, format "x '.2'"). + +Notation pr1 := projT1. +Notation pr2 := projT2. -Definition transport_apD10 : - forall {A : Type} {B : A -> Type} {a : A} (P : B a -> Type) - {t1 t2 : forall x : A, B x} {e : t1 = t2} {p : P (t1 a)}, - transport (fun (t : forall x : A, B x) => P (t a)) e p = - transport (fun (t : B a) => P t) (apD10 e a) p. +(** The following notation is very convenient, although it unfortunately clashes with Proof General's "electric period". We have added [format] specifiers in Notations.v so that it will display without an extra space, as [x.1] rather than as [x .1]. *) +Notation "x .1" := (pr1 x) : fibration_scope. +Notation "x .2" := (pr2 x) : fibration_scope. + +Notation paths := eq. +Notation idpath := eq_refl. + +Notation eq := paths. +Notation eq_refl := idpath. +Notation inverse := eq_sym. +Notation concat := eq_trans. +Notation "x = y" := (Logic.eq x y) : type_scope. + +Lemma transport {A : Type} (P : A -> Type) {x y : A} : x = y -> P x -> P y. +Proof. move->; exact. Defined. + +Lemma paths_rect (A : Type) (a : A) (P : forall a0 : A, a = a0 -> Type) : + P a idpath -> forall (a0 : A) (p : a = a0), P a0 p. +Proof. by move=> pa b; case: _ /. Defined. + +Reserved Notation "A <=> B" (at level 70, no associativity). +Notation "A <--> B" := ((A -> B) * (B -> A))%type (at level 70) : fibration_scope. +Notation "A <->> B" := {f : A -> B & { g : B -> A & forall x, g (f x) = x}} (at level 70) : fibration_scope. +Notation id := (fun x => x). +Notation idmap := (fun x => x). + +Declare Scope path_scope. +Delimit Scope path_scope with path. +Bind Scope path_scope with paths. +Notation "1" := idpath : path_scope. +Notation "e ^" := (eq_sym e%path) : path_scope. +Notation "p @ q" := (eq_trans p q) : path_scope. +Open Scope path_scope. + +Definition inv_V {A : Type} {x y : A} (p : x = y) : (p^)^ = p := + match p with idpath => 1 end. + +(* relation for forall *) +Monomorphic Axiom Funext : Prop. +Existing Class Funext. +Axiom path_forall@{i j} : forall `{Funext} {A : Type@{i}} {P : A -> Type@{j}} + (f g : forall x : A, P x), f == g -> f = g. +Global Arguments path_forall {_ A%type_scope P} (f g)%function_scope _. + +Lemma path_arrow `{Funext} {A B : Type} (f g : A -> B) : + f == g -> f = g. +Proof. apply path_forall. Defined. + +Definition equiv_flip@{i k} (A B : Type@{i}) (P : A -> B -> Type@{k}) : +(forall (a : A) (b : B), P a b) <->> (forall (b : B) (a : A), P a b). +Proof. by do 2!exists (fun PAB b a => PAB a b). Defined. + +Definition ap := f_equal. +Arguments ap {A B} f {x y}. + +Definition inverse2 {A : Type} {x y : A} {p q : x = y} : p = q -> p^ = q^. +Proof. exact: ap. Defined. + +Lemma concat_p1 {A : Type} {x y : A} (p : x = y) : p @ 1 = p. +Proof. reflexivity. Defined. + +Lemma concat_1p {A : Type} {x y : A} (p : x = y) : 1 @ p = p. +Proof. by case: _ / p. Defined. + +Lemma moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) : + p @ q = 1%path -> p = q^. +Proof. by case: _ / q p. Defined. + +Lemma moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : + r = q @ p^ -> r @ p = q. +Proof. by case: _ / p q r. Defined. + +Lemma transport1@{i j} {A : Type@{i}} (P : A -> Type@{j}) + {x : A} (u : P x) : transport P 1 u = u. +Proof. done. Defined. + +Lemma transport_pp@{i j} {A : Type@{i}} (P : A -> Type@{j}) + {x y z : A} (p : x = y) (q : y = z) (u : P x) : + transport P (p @ q) u = transport P q (transport P p u). Proof. - intros A B a P t1 t2 [] p; reflexivity. +case: _ / q. +done. Defined. -Definition ap2 : forall {A B C : Type} (f : A -> B -> C) {a1 a2 : A} {b1 b2 : B}, - a1 = a2 -> b1 = b2 -> f a1 b1 = f a2 b2. +Lemma concat_pV@{i} {A : Type@{i}} {x y : A} (p : x = y) : p @ p^ = 1%path. +Proof. by case: _ / p. Defined. + +Lemma concat_Vp@{i} {A : Type@{i}} {x y : A} (p : x = y) : p^ @ p = 1%path. +Proof. by case: _ / p. Defined. + +Lemma path_prod {A B : Type} (z z' : A * B) : + fst z = fst z' -> snd z = snd z' -> z = z'. Proof. - intros A B C f a1 a2 b1 b2 ea eb. - destruct ea. destruct eb. reflexivity. -Defined. +by case: z z' => [? ?] [? ?] /= -> ->. +Qed. -Definition coe_inverse_cancel {A B} (e : A = B) p: coe e (coe e^ p) = p. -Proof. elim: e p; reflexivity. Defined. -Definition coe_inverse_cancel' {A B} (e : A = B) p : coe e^ (coe e p) = p. -Proof. elim: e p; reflexivity. Defined. +Reserved Notation "n .+1" (at level 2, left associativity, format "n .+1"). +Reserved Notation "n .+2" (at level 2, left associativity, format "n .+2"). +Reserved Notation "n .+3" (at level 2, left associativity, format "n .+3"). +Reserved Notation "n .+4" (at level 2, left associativity, format "n .+4"). +Reserved Notation "n .+5" (at level 2, left associativity, format "n .+5"). +Reserved Notation "n '.-1'" (at level 2, left associativity, format "n .-1"). +Reserved Notation "n '.-2'" (at level 2, left associativity, format "n .-2"). +Reserved Notation "m +2+ n" (at level 50, left associativity). +Reserved Infix "mod" (at level 40, no associativity). +Reserved Notation "p ~ 1" (at level 7, left associativity, format "p '~' '1'"). +Reserved Notation "p ~ 0" (at level 7, left associativity, format "p '~' '0'"). -Definition path_forall_types `{Funext} A F G : - (forall (a : A), F a = G a) -> (forall a, F a) = (forall a, G a). -Proof. by move=> /(path_forall _ _)->. Defined. +Definition Prop_irrelevance_type := forall (P : Prop) (p q : P), p = q. +Definition Prop_ext_type := forall (P Q : Prop), (P <-> Q) -> P = Q. -Definition equiv_flip@{i k | i <= k} : - forall (A B : Type@{i}) (P : A -> B -> Type@{k}), - Equiv@{k k} (forall (a : A) (b : B), P a b) (forall (b : B) (a : A), P a b). -Proof. - intros A B P. - unshelve eapply Build_Equiv@{k k}. - - exact (@flip@{i i k} A B P). - - by unshelve eapply - (@Build_IsEquiv@{k k} - (forall (a : A) (b : B), P a b) (forall (b : B) (a : A), P a b) - (@flip@{i i k} A B P) - (@flip@{i i k} B A (fun (b : B) (a : A) => P a b))). -Defined. +Axiom Prop_irrelevance : Prop_irrelevance_type. +Axiom Prop_ext : Prop_ext_type. \ No newline at end of file diff --git a/theories/Param.v b/theories/Param.v index e13ee65..9084412 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -13,7 +13,6 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Export Database. Require Import HoTT_additions Hierarchy. Require Export Param_Type Param_arrow Param_forall. @@ -34,11 +33,6 @@ Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. -(* generate - PParamMN_Type P Q := ParamMN_TypePQ for all M N under 2b - PParamMN_Type P Q := ParamMN_Type44 for all M N containing 2b+ -*) - Elpi Command genpparamtype. Elpi Accumulate File util. Elpi Accumulate Db trocq.db. @@ -80,23 +74,10 @@ Elpi Accumulate lp:{{ % this typecheck is very important: it adds L < L1 to the constraint graph coq.typecheck Decl _ ok, PParamType is "PParam" ^ {param-class->string Class} ^ "_Type", - @udecl! [L, L1] ff [lt L L1] ff => - coq.env.add-const PParamType Decl _ @transparent! Const, - coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pparam-type Class Const)). - - pred generate-pparam-type44 - i:univ.variable, i:univ.variable, i:param-class. - generate-pparam-type44 L L1 Class :- - coq.univ-instance UI2 [L, L1], - coq.locate {calc ("Param" ^ {param-class->string Class} ^ "_Type44")} ParamType, - Decl = (fun `_` {{ map_class }} _\ fun `_` {{ map_class }} _\ pglobal ParamType UI2), - % this typecheck is very important: it adds L < L1 to the constraint graph - coq.typecheck Decl _ ok, - PParamType is "PParam" ^ {param-class->string Class} ^ "_Type", - @udecl! [L, L1] ff [lt L L1] ff => + @udecl! [L, L1] ff [lt L L1] tt => coq.env.add-const PParamType Decl _ @transparent! Const, coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.pparam-type Class Const)). -}}. + }}. Elpi Typecheck. Elpi Query lp:{{ @@ -105,24 +86,12 @@ Elpi Query lp:{{ coq.univ.super U U1, coq.univ.variable U1 L1, map-classes low Classes1, - map-classes high Classes2, map-classes all Classes, % first the ones where the arguments matter std.forall Classes1 (m\ std.forall Classes1 (n\ generate-pparam-type L L1 (pc m n) ) - ), - % then the ones where the (4,4) relation is always returned - std.forall Classes (m\ - std.forall Classes2 (n\ - generate-pparam-type44 L L1 (pc m n) - ) - ), - std.forall Classes2 (m\ - std.forall Classes1 (n\ - generate-pparam-type44 L L1 (pc m n) - ) ). }}. @@ -143,10 +112,11 @@ Elpi Accumulate lp:{{ }}. Elpi Accumulate lp:{{ - solve InitialGoal NewGoals :- debug dbg.none => std.do! [ + solve InitialGoal NewGoals :- debug dbg.full => std.do! [ InitialGoal = goal _Context _ G _ [], + std.assert-ok! (coq.typecheck G Ty) "goal ill-typed", util.when-debug dbg.full (coq.say "goal" G), - translate-goal G (pc map0 map1) G' GR, + translate-goal Ty G (pc map0 map1) G' GR, util.when-debug dbg.full (coq.say "trocq:" G "~" G' "by" GR), FinalProof = {{ @comap lp:G lp:G' lp:GR (_ : lp:G') }}, util.when-debug dbg.full (coq.say FinalProof), @@ -157,10 +127,12 @@ Elpi Accumulate lp:{{ refine.no_check EFinalProof InitialGoal NewGoals ]. - pred translate-goal i:term, i:param-class, o:term, o:term. - translate-goal G (pc M N) G' GR' :- std.do! [ + pred translate-goal i:term, i:term, i:param-class, o:term, o:term. + translate-goal Ty G (pc M N) G' GR' :- std.do! [ cstr.init, - T = (app [pglobal (const {trocq.db.ptype}) _, {map-class->term M}, {map-class->term N}]), + if (Ty = sort (typ _)) + (T = (app [pglobal (const {trocq.db.ptype}) _, {map-class->term M}, {map-class->term N}])) + (T = (app [pglobal (const {trocq.db.pprop}) _, {map-class->term M}, {map-class->term N}])), % first annotate the initial goal with fresh parametricity class variables term->annot-term G AG, util.when-debug dbg.steps ( diff --git a/theories/Param_Empty.v b/theories/Param_Empty.v index 1df4610..9fd8327 100644 --- a/theories/Param_Empty.v +++ b/theories/Param_Empty.v @@ -1,10 +1,11 @@ From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. +Notation Empty := False. + Inductive EmptyR : Empty -> Empty -> Type := . Definition map_Empty (e : Empty) : Empty := e. diff --git a/theories/Param_Prop.v b/theories/Param_Prop.v new file mode 100644 index 0000000..d48cc16 --- /dev/null +++ b/theories/Param_Prop.v @@ -0,0 +1,194 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * This file is distributed under the terms of *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * see LICENSE file for the text of the license *) +(*****************************************************************************) + +From elpi Require Import elpi. +From Coq Require Import ssreflect. +Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. +From Trocq.Elpi Extra Dependency "util.elpi" as util. + +Set Warnings "+elpi.typecheck". +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Local Open Scope param_scope. + +(* generate MapM_PropNP@{i} : + MapM.Has Prop@{i} Prop@{i} ParamNP.Rel@{i}, + for all N P, for M = map2a and below (above, NP is always 44) + + symmetry MapM_Prop_symNP *) + +Elpi Command genmapprop. +Elpi Accumulate Db trocq.db. +Elpi Accumulate File param_class. +Elpi Accumulate File util. +Elpi Accumulate lp:{{ + pred generate-fields + i:map-class, i:term, i:param-class, o:list term. + generate-fields map0 R _ [R]. + generate-fields map1 R _ [R, Map] :- + Map = (fun `T` (sort prop) t\ t). + generate-fields map2a R RClass [R, Map, MapInR] :- std.do! [ + Prop = sort prop, + Map = (fun `T` Prop t\ t), + (pi a\ coq.mk-app R [a] (RF a)), + coq.locate "paths" Paths, + coq.locate "transport" Transport, + coq.locate {calc ("id_Param" ^ {param-class->string RClass})} IdParam, + coq.env.global Transport TransportTm, + coq.env.global IdParam IdParamTm, + MapInR = + (fun `A` Prop a\ fun `B` Prop b\ + fun `e` (app [global Paths, Prop, a, b]) e\ + app [TransportTm, Prop, RF a, a, b, + e, app [IdParamTm, a]]) + ]. + + pred generate-map-prop i:map-class, i:param-class. + generate-map-prop M RClass :- std.do! [ + coq.locate {calc ("Param" ^ {param-class->string RClass} ^ ".Rel")} R, + Prop = sort prop, + coq.env.global R RTm, + % RTm = {{fun A B : Prop => lp:RTmNoEta A B}}, + generate-fields M RTm RClass Fields, + coq.locate "sym_rel" SymRel, + coq.env.global SymRel SymRelTm, + generate-fields + M (app [SymRelTm, Prop, Prop, RTm]) + RClass FieldsSym, + coq.locate {calc ("Map" ^ {map-class->string M} ^ ".BuildHas")} BuildHas, + coq.env.global BuildHas BuildHasTm, + coq.mk-app BuildHasTm [Prop, Prop | Fields] Decl, + coq.mk-app BuildHasTm [Prop, Prop | FieldsSym] DeclSym, + MapProp is + "Map" ^ {map-class->string M} ^ "_Prop" ^ {param-class->string RClass}, + MapPropSym is + "Map" ^ {map-class->string M} ^ "_Prop_sym" ^ + {param-class->string RClass}, + % these typechecks are very important: they add L < L1 to the constraint graph + std.assert-ok! (coq.elaborate-skeleton Decl _Ty Decl') + "generate-map-prop: Decl cannot be elaborated", + std.assert-ok! (coq.elaborate-skeleton DeclSym _Ty' DeclSym') + "generate-map-prop: Decl cannot be elaborated", + % std.assert-ok! (coq.typecheck Decl _) + % "generate-map-prop: Decl ill-typed", + % std.assert-ok! (coq.typecheck DeclSym _) + % "generate-map-prop: DeclSym ill-typed", + @udecl! [] tt [] tt => + coq.env.add-const MapProp Decl' _ @transparent! _, + @udecl! [] tt [] tt => + coq.env.add-const MapPropSym DeclSym' _ @transparent! _ + ]. +}}. +Elpi Typecheck. + +Set Printing Universes. +Set Printing All. +Print Param00.Rel. +Eval compute in (@Map0.BuildHas Prop Prop (@Param00.Rel)). + +Elpi Query lp:{{ + % cannot have only one binder in the declaration because this line creates a fresh level: + map-classes all Classes, + map-classes low LowClasses, + std.forall LowClasses (m\ + std.forall Classes (n\ + std.forall Classes (p\ + generate-map-prop m (pc n p) + ) + ) + ). +}}. + + +(* Elpi Command genparamtype. +Elpi Accumulate Db trocq.db. +Elpi Accumulate File util. +Elpi Accumulate File param_class. +Elpi Accumulate lp:{{ + pred generate-param-type + i:param-class, i:param-class, i:univ, i:univ.variable, i:univ.variable. + generate-param-type (pc M N as Class) RClass U L L1 :- + map-class->string M MStr, + map-class->string N NStr, + coq.univ-instance UI [L], + coq.univ-instance UI1 [L1], + coq.univ-instance UI2 [L, L1], + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".BuildRel")} BuildRel, + coq.locate + {calc ("Map" ^ MStr ^ "_Prop" ^ {param-class->string RClass})} MapProp, + coq.locate + {calc ("Map" ^ NStr ^ "_Prop_sym" ^ {param-class->string RClass})} + MapPropSym, + coq.locate {calc ("Param" ^ {param-class->string RClass} ^ ".Rel")} R, + if (std.mem! [map2b, map3, map4] M) ( + UnivalentDecl = true, + MapPropF = (u\ app [pglobal MapProp UI2, u]), + if (std.mem! [map2b, map3, map4] N) + (MapPropSymF = (u\ app [pglobal MapPropSym UI2, u])) + (MapPropSymF = (_\ pglobal MapPropSym UI2)) + ) ( + MapPropF = (_\ pglobal MapProp UI2), + if (std.mem! [map2b, map3, map4] N) ( + MapPropSymF = (u\ app [pglobal MapPropSym UI2, u]), + UnivalentDecl = true + ) ( + MapPropSymF = (_\ pglobal MapPropSym UI2), + UnivalentDecl = false + ) + ), + % in the univalent case, add the axiom in the binder + if (UnivalentDecl) ( + coq.locate "Univalence" Univalence, + Decl = + (fun `H` (global Univalence) u\ + app [pglobal BuildRel UI1, sort prop, sort prop, pglobal R UI, + MapPropF u, MapPropSymF u]) + ) ( + Dummy = (fun `x` (sort prop) x\ x), + Decl = + app [pglobal BuildRel UI1, sort prop, sort prop, pglobal R UI, + MapPropF Dummy, MapPropSymF Dummy] + ), + ParamProp is "Param" ^ MStr ^ NStr ^ "_Prop" ^ {param-class->string RClass}, + % this typecheck is very important: it adds L < L1 to the constraint graph + coq.typecheck Decl _ ok, + @udecl! [L, L1] ff [lt L L1] tt => + coq.env.add-const ParamProp Decl _ @transparent! Const, + coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.param-type Class RClass Const)). +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + coq.univ.super U U1, + % cannot have only one binder in the declaration because this line creates a fresh level: + coq.univ.variable U1 L1, + AllClasses = [map0, map1, map2a, map2b, map3, map4], + Classes__ = [map0, map1, map2a], + std.forall Classes__ (m\ + std.forall Classes__ (n\ + std.forall AllClasses (p\ + std.forall AllClasses (q\ + generate-param-type (pc m n) (pc p q) U L L1 + ) + ) + ) + ). +}}. +(* + Set Printing Universes. About Param00_Prop40. +Set Printing Universes. Print Param12a_Prop31. +Set Printing Universes. About Param30_Prop44. +Set Printing Universes. Print Param44_Prop44. *) *) diff --git a/theories/Param_Type.v b/theories/Param_Type.v index f7ffcc7..41b061b 100644 --- a/theories/Param_Type.v +++ b/theories/Param_Type.v @@ -13,7 +13,6 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. @@ -51,7 +50,7 @@ Elpi Accumulate lp:{{ coq.locate {calc ("id_Param" ^ {param-class->string RClass})} IdParam, MapInR = (fun `A` Type a\ fun `B` Type b\ - fun `e` (app [pglobal Paths UI1, Type, a, b]) e\ + fun `e` (app [global Paths, Type, a, b]) e\ app [pglobal Transport UI11, Type, RF a, a, b, e, app [pglobal IdParam UI, a]]). @@ -78,9 +77,9 @@ Elpi Accumulate lp:{{ % these typechecks are very important: they add L < L1 to the constraint graph coq.typecheck Decl _ ok, coq.typecheck DeclSym _ ok, - @udecl! [L, L1] ff [lt L L1] ff => + @udecl! [L, L1] ff [lt L L1] tt => coq.env.add-const MapType Decl _ @transparent! _, - @udecl! [L, L1] ff [lt L L1] ff => + @udecl! [L, L1] ff [lt L L1] tt => coq.env.add-const MapTypeSym DeclSym _ @transparent! _. }}. Elpi Typecheck. @@ -102,77 +101,6 @@ Elpi Query lp:{{ ). }}. -(* Check Map0_Type01. -Check Map1_Type_sym32b. -Check Map2a_Type44. *) - -(* now R is always Param44.Rel *) - -(* NB: here we would like to use i+1 instead of j but Coq does not allow it - * Map*.Has is a constant so it currently cannot be instantiated with an algebraic universe - *) - -Definition Map2b_Type44@{i j | i < j} `{Univalence} : - @Map2b.Has@{j} Type@{i} Type@{i} Param44.Rel@{i}. -Proof. - unshelve econstructor. - - exact idmap. - - move=> A B /uparam_equiv. apply: path_universe_uncurried. -Defined. - -Definition Map2b_Type_sym44@{i j | i < j} `{Univalence} : - @Map2b.Has@{j} Type@{i} Type@{i} (sym_rel@{j} Param44.Rel@{i}). -Proof. - unshelve econstructor. - - exact idmap. - - move=> A B /uparam_equiv /path_universe_uncurried /inverse. exact. -Defined. - -Definition Map3_Type44@{i j | i < j} `{Univalence} : - @Map3.Has@{j} Type@{i} Type@{i} Param44.Rel@{i}. -Proof. - unshelve econstructor. - - exact idmap. - - exact (fun A B e => e # id_Param44 A). - - move=> A B /uparam_equiv. apply: path_universe_uncurried. -Defined. - -Definition Map3_Type_sym44@{i j | i < j} `{Univalence} : - @Map3.Has@{j} Type@{i} Type@{i} (sym_rel@{j} Param44.Rel@{i}). -Proof. - unshelve econstructor. - - exact idmap. - - exact (fun A B e => e # id_Param44 A). - - move=> A B /uparam_equiv /path_universe_uncurried /inverse. exact. -Defined. - -Definition Map4_Type44@{i j | i < j} `{Univalence} : - @Map4.Has@{j} Type@{i} Type@{i} Param44.Rel@{i}. -Proof. - unshelve econstructor. - - exact idmap. - - exact (fun A B e => e # id_Param44 A). - - move=> A B /uparam_equiv. apply: path_universe_uncurried. - - move=> A B; elim/uparam_induction. - by rewrite uparam_equiv_id /= [path_universe_uncurried _] path_universe_1. -Defined. - -Definition Map4_Type_sym44@{i j | i < j} `{Univalence} : - @Map4.Has@{j} Type@{i} Type@{i} (sym_rel@{j} Param44.Rel@{i}). -Proof. - unshelve econstructor. - - exact idmap. - - exact (fun A B e => e # id_Param44 A). - - move=> A B /uparam_equiv /path_universe_uncurried /inverse. exact. - - move=> A B; elim/uparam_induction. - by rewrite uparam_equiv_id /= [path_universe_uncurried _] path_universe_1. -Defined. - -(* generate ParamMN_TypePQ@{i} : - ParamMN.Rel Type@{i} Type@{i}, - for all M N, having ParamPQ.Rel as the R field - (for M or N in [2b, 3, 4] PQ is always 44) *) - Elpi Command genparamtype. Elpi Accumulate File util. Elpi Accumulate Db trocq.db. @@ -225,7 +153,7 @@ Elpi Accumulate lp:{{ ParamType is "Param" ^ MStr ^ NStr ^ "_Type" ^ {param-class->string RClass}, % this typecheck is very important: it adds L < L1 to the constraint graph coq.typecheck Decl _ ok, - @udecl! [L, L1] ff [lt L L1] ff => + @udecl! [L, L1] ff [lt L L1] tt => coq.env.add-const ParamType Decl _ @transparent! Const, coq.elpi.accumulate _ "trocq.db" (clause _ _ (trocq.db.param-type Class RClass Const)). }}. @@ -239,7 +167,6 @@ Elpi Query lp:{{ coq.univ.variable U1 L1, map-classes all AllClasses, map-classes low Classes__, - map-classes high Classes44, std.forall Classes__ (m\ std.forall Classes__ (n\ std.forall AllClasses (p\ @@ -247,14 +174,6 @@ Elpi Query lp:{{ generate-param-type (pc m n) (pc p q) U L L1 ) ) - ), - std.forall Classes44 (n\ - generate-param-type (pc m n) (pc map4 map4) U L L1 - ) - ), - std.forall Classes44 (m\ - std.forall AllClasses (n\ - generate-param-type (pc m n) (pc map4 map4) U L L1 ) ). }}. diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v index 197cbdd..96d59c1 100644 --- a/theories/Param_arrow.v +++ b/theories/Param_arrow.v @@ -13,7 +13,6 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. @@ -45,7 +44,7 @@ Definition Map0_arrow@{i j k | i <= k, j <= k} Proof. exists. Defined. (* (01, 10) -> 10 *) -Definition Map1_arrow@{i j k | i <= k, j <= k} +Definition Map1_arrow@{i j k} {A A' : Type@{i}} (PA : Param01.Rel@{i} A A') {B B' : Type@{j}} (PB : Param10.Rel@{j} B B') : Map1.Has@{k} (R_arrow PA PB). @@ -54,19 +53,21 @@ Proof. Defined. (* (02b, 2a0) -> 2a0 *) -Definition Map2a_arrow@{i j k | i <= k, j <= k} +Definition Map2a_arrow@{i j k} {A A' : Type@{i}} (PA : Param02b.Rel@{i} A A') {B B' : Type@{j}} (PB : Param2a0.Rel@{j} B B') : Map2a.Has@{k} (R_arrow PA PB). Proof. - exists (Map1.map@{k} _ (Map1_arrow PA PB)). - move=> f f' /= e a a' aR; apply (map_in_R PB). - apply (transport (fun t => _ = t a') e) => /=. - by apply (transport (fun t => _ = map _ (f t)) (R_in_comap PA _ _ aR)^). + exists (Map1.map@{k} _ (Map1_arrow@{i j k} PA PB)). + move=> f f' /= e a a' aR; apply (map_in_R@{j} PB). + apply (transport@{j j} (fun t => _ = t a') e) => /=. + by apply (transport@{j j} (fun t => _ = map _ (f t)) + (R_in_comap@{i} PA _ _ aR)^). Defined. + (* (02a, 2b0) + funext -> 2b0 *) -Definition Map2b_arrow@{i j k | i <= k, j <= k} `{Funext} +Definition Map2b_arrow@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param02a.Rel@{i} A A') {B B' : Type@{j}} (PB : Param2b0.Rel@{j} B B') : Map2b.Has@{k} (R_arrow PA PB). @@ -77,7 +78,7 @@ Proof. Defined. (* (03, 30) + funext -> 30 *) -Definition Map3_arrow@{i j k | i <= k, j <= k} `{Funext} +Definition Map3_arrow@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param03.Rel@{i} A A') {B B' : Type@{j}} (PB : Param30.Rel@{j} B B') : Map3.Has@{k} (R_arrow PA PB). @@ -89,7 +90,7 @@ Proof. Defined. (* (04, 40) + funext -> 40 *) -Definition Map4_arrow@{i j k | i <= k, j <= k} `{Funext} +Definition Map4_arrow@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param04.Rel@{i} A A') {B B' : Type@{j}} (PB : Param40.Rel@{j} B B') : Map4.Has@{k} (R_arrow PA PB). @@ -99,16 +100,17 @@ Proof. (Map2a.map_in_R _ (Map2a_arrow PA PB)) (Map2b.R_in_map _ (Map2b_arrow PA PB)). move=> f f' fR /=. - apply path_forall@{i k k} => a. - apply path_forall@{i k k} => a'. - apply path_arrow@{i k k} => aR /=. - rewrite -[in X in _ = X](R_in_comapK PA a' a aR). - elim (R_in_comap PA a' a aR). - rewrite transport_apD10 /=. - rewrite apD10_path_forall_cancel/=. - rewrite <- (R_in_mapK PB). - by elim: (R_in_map _ _ _ _). -Defined. + apply path_forall@{i k} => a. + apply path_forall@{i k} => a'. + apply path_arrow@{i k} => aR /=. + elim/(ind_comap PA): _ => {a aR}. + rewrite transport1. + set X := transport _ _ _. + have -> : X = R_in_map PB (f (comap PA a')) (f' a') (fR (comap PA a') a' + (comap_in_R PA a' (comap PA a') 1)). + exact: Prop_irrelevance. + by elim/(ind_map PB): _ (fR _ _ _) / _. + Qed. (* Param_arrowMN : forall A A' AR B B' BR, ParamMN.Rel (A -> B) (A' -> B') *) @@ -250,7 +252,7 @@ Elpi Accumulate lp:{{ ParamArrow is "Param" ^ MStr ^ NStr ^ "_arrow", % this typecheck is very important: it adds L < L1 to the constraint graph coq.typecheck Decl _ ok, - @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] ff => + @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] tt => coq.env.add-const ParamArrow Decl _ @transparent! Const, coq.elpi.accumulate _ "trocq.db" (clause _ (after "default-param-arrow") (trocq.db.param-arrow Class Const)). diff --git a/theories/Param_bool.v b/theories/Param_bool.v index c031693..c8bb76d 100644 --- a/theories/Param_bool.v +++ b/theories/Param_bool.v @@ -12,12 +12,13 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. +Notation Bool := bool. + Inductive BoolR : Bool -> Bool -> Type := | falseR : BoolR false false | trueR : BoolR true true. @@ -59,14 +60,12 @@ Definition Param_Bool_sym_inv {b b' : Bool} (bR : BoolR b b') : | trueR => idpath end. -Definition BoolR_sym : forall (b b' : Bool), sym_rel BoolR b b' <~> BoolR b b'. +Definition BoolR_sym : forall (b b' : Bool), sym_rel BoolR b b' <->> BoolR b b'. Proof. - intros b b'. - unshelve eapply equiv_adjointify. + intros b b'; unshelve eexists _,_ . - apply Param_Bool_sym. - apply Param_Bool_sym. - intro bR. apply Param_Bool_sym_inv. - - intro bR. apply Param_Bool_sym_inv. Defined. Definition Map4_Bool : Map4.Has BoolR. diff --git a/theories/Param_forall.v b/theories/Param_forall.v index 4765cfb..374333b 100644 --- a/theories/Param_forall.v +++ b/theories/Param_forall.v @@ -13,7 +13,6 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. @@ -28,8 +27,7 @@ Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. -(* relation for forall *) - + Definition R_forall@{i j} {A A' : Type@{i}} (PA : Param00.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} @@ -78,7 +76,7 @@ Definition Map0_forall@{i j k | i <= k, j <= k} Proof. constructor. Defined. (* (02a, 10) -> 1 *) -Definition Map1_forall@{i j k | i <= k, j <= k} +Definition Map1_forall@{i j k} {A A' : Type@{i}} (PA : Param02a.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} (PB : forall (a : A) (a' : A'), PA a a' -> Param10.Rel@{j} (B a) (B' a')) : @@ -89,20 +87,20 @@ Proof. Defined. (* (04, 2a0) -> 2a0 *) -Definition Map2a_forall@{i j k | i <= k, j <= k} +Definition Map2a_forall@{i j k} {A A' : Type@{i}} (PA : Param04.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} (PB : forall (a : A) (a' : A'), PA a a' -> Param2a0.Rel@{j} (B a) (B' a')) : Map2a.Has@{k} (R_forall@{i j} PA PB). Proof. - exists (Map1.map@{k} _ (Map1_forall PA PB)). - move=> f f' e a a' aR; apply (map_in_R (PB _ _ _)). - apply (transport (fun t => _ = t a') e) => /=. - by elim/(comap_ind a a' aR): _. + exists (Map1.map@{k} _ (Map1_forall@{i j k} PA PB)). + move=> f f' /= e a a' aR; apply (map_in_R@{j} (PB _ _ _)). + elim/(ind_comap PA): _ aR / _. + exact: (ap (fun f => f a') e). Defined. (* (02a, 2b0) + funext -> 2b0 *) -Definition Map2b_forall@{i j k | i <= k, j <= k} `{Funext} +Definition Map2b_forall@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param02a.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} (PB : forall (a : A) (a' : A'), PA a a' -> Param2b0.Rel@{j} (B a) (B' a')) : @@ -114,7 +112,7 @@ Proof. Defined. (* (04, 30) + funext -> 30 *) -Definition Map3_forall@{i j k | i <= k, j <= k} `{Funext} +Definition Map3_forall@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param04.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} (PB : forall (a : A) (a' : A'), PA a a' -> Param30.Rel@{j} (B a) (B' a')) : @@ -126,8 +124,12 @@ Proof. apply (R_in_map (PB _ _ _)); exact: fR. Defined. +Lemma ap_path_forall `{Funext} X Y (f g : forall x : X, Y x) x (e : f == g): + ap (fun f => f x) (path_forall f g e) = e x. +Proof. exact: Prop_irrelevance. Qed. + (* (04, 40) + funext -> 40 *) -Definition Map4_forall@{i j k | i <= k, j <= k} `{Funext} +Definition Map4_forall@{i j k} `{Funext} {A A' : Type@{i}} (PA : Param04.Rel@{i} A A') {B : A -> Type@{j}} {B' : A' -> Type@{j}} (PB : forall (a : A) (a' : A'), PA a a' -> Param40.Rel@{j} (B a) (B' a')) : @@ -138,18 +140,13 @@ Proof. (Map3.map_in_R _ (Map3_forall PA PB)) (Map3.R_in_map _ (Map3_forall PA PB)). move=> f f' fR /=. - apply path_forall@{i k k} => a. - apply path_forall@{i k k} => a'. + apply path_forall@{i k} => a. + apply path_forall@{i k} => a'. apply path_forall => aR. - unfold comap_ind. - elim (R_in_comapK PA a' a aR). - elim (R_in_comap PA a' a aR). - rewrite transport_apD10. - rewrite apD10_path_forall_cancel/=. - rewrite <- (R_in_mapK (PB _ _ _)). - by elim: (R_in_map _ _ _ _). -Defined. - + elim/(ind_comapP PA): _ => {a aR}. + rewrite ap_path_forall. + by elim/(ind_map (PB (comap PA a') a' (comap_in_R PA a' (comap PA a') 1))): _ _ / _. + Qed. (* Param_forallMN : forall A A' AR B B' BR, ParamMN.Rel (forall a, B a) (forall a', B' a') *) @@ -311,7 +308,7 @@ Elpi Accumulate lp:{{ ParamForall is "Param" ^ MStr ^ NStr ^ "_forall", % this typecheck is very important: it adds L < L1 to the constraint graph coq.typecheck Decl _ ok, - @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] ff => + @udecl! [Li, Lj, Lk] ff [le Li Lk, le Lj Lk] tt => coq.env.add-const ParamForall Decl _ @transparent! Const, coq.elpi.accumulate _ "trocq.db" (clause _ (after "default-param-forall") (trocq.db.param-forall Class Const)). diff --git a/theories/Param_list.v b/theories/Param_list.v index b77608c..f08b533 100644 --- a/theories/Param_list.v +++ b/theories/Param_list.v @@ -12,11 +12,11 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. +Set Asymmetric Patterns. Inductive listR (A A' : Type) (AR : A -> A' -> Type) : list A -> list A' -> Type := | nilR : listR A A' AR (@nil A) (@nil A') @@ -118,21 +118,14 @@ Definition listR_flipK (A A' : Type) (AR : A -> A' -> Type) : 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. + 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 (sym_rel AR) l' l). + exact (listR_flipK A A' AR l l'). - + intros lR. - induction lR as [|a a' aR l l' lR IHlR]; simpl. - * reflexivity. - * rewrite IHlR. - elim (listR_flipK A A' AR l l' lR). - simpl. reflexivity. Defined. Definition Param00_list (A A' : Type) (AR : Param00.Rel A A') : Param00.Rel (list A) (list A'). diff --git a/theories/Param_nat.v b/theories/Param_nat.v index 0d54a7c..43fc731 100644 --- a/theories/Param_nat.v +++ b/theories/Param_nat.v @@ -11,8 +11,7 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) -From Coq Require Import ssreflect. -From HoTT Require Import HoTT. +From mathcomp Require Import ssreflect ssrfun ssrnat. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. @@ -22,6 +21,26 @@ Inductive natR : nat -> nat -> Type := | OR : natR O O | SR : forall (n n' : nat), natR n n' -> natR (S n) (S n'). +Lemma ind (T : Type) (X : T -> Type) t (P : X t -> Type) : + (forall t' (e : t' = t) (x : X t'), P (transport X e x)) -> + forall (x : X t), P x. +Proof. by move=> + x => /(_ t erefl); apply. Defined. + +Lemma eq_to_refl (T : Type) (x : T) (p : x = x) : unkeyed p = erefl. +Proof. exact: Prop_irrelevance. Qed. + +Lemma natR_irrelevant m n : forall (nR nR' : natR m n), nR = nR'. +Proof. +suff: forall (nR : natR m n) m' n' (nR' : natR m' n') (e : m = m') (e' : n = n') , + transport (fun m' => natR m' n') e (transport (fun n' => natR m n') e' nR) = nR'. + by move=> /(_ _ m n _ erefl erefl); apply. +elim => // [|{}m {}n nR IHnR] m' n' => - [|{}m' {}n' nR'] // e e'. + by rewrite ?eq_to_refl. +rewrite -[nR']IHnR//; do ?by [case: e|case: e']. +move=> e'' e'''. +by case: _ / e'' in e *; case: _ / e''' in e' *; rewrite ?eq_to_refl. +Qed. + Definition map_nat : nat -> nat := id. Definition map_in_R_nat : forall {n n' : nat}, map_nat n = n' -> natR n n' := @@ -44,10 +63,9 @@ Definition R_in_map_nat : forall {n n' : nat}, natR n n' -> map_nat n = n' := Definition R_in_mapK_nat : forall {n n' : nat} (nR : natR n n'), map_in_R_nat (R_in_map_nat nR) = nR. -Proof. -move=> n n'; elim=> //= {}n {}n' nR IHn. -by elim: {2}_ / IHn; elim (R_in_map_nat nR). -Defined. +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. @@ -58,20 +76,14 @@ Defined. Definition Param_nat_sym_inv {n n' : nat} : forall (nR : natR n n'), Param_nat_sym (Param_nat_sym nR) = nR. -Proof. - intro nR. induction nR; simpl. - - reflexivity. - - rewrite IHnR. reflexivity. -Defined. +Proof. by elim => //= {}n {}n' nR ->. Defined. -Definition natR_sym : forall (n n' : nat), sym_rel natR n n' <~> natR n n'. +Definition natR_sym : forall (n n' : nat), sym_rel natR n n' <->> natR n n'. Proof. - intros n n'. - unshelve eapply equiv_adjointify. + intros n n'; unshelve eexists _, _. - apply Param_nat_sym. - apply Param_nat_sym. - intro nR. apply Param_nat_sym_inv. - - intro nR. apply Param_nat_sym_inv. Defined. Definition Map4_nat : Map4.Has natR. diff --git a/theories/Param_option.v b/theories/Param_option.v index d63ed4d..d55505b 100644 --- a/theories/Param_option.v +++ b/theories/Param_option.v @@ -12,12 +12,13 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. +Notation Unit := unit. +Notation none := None. Inductive optionR (A A' : Type) (AR : A -> A' -> Type) : option A -> option A' -> Type := @@ -114,33 +115,9 @@ Definition option_R_in_map : | @noneR _ _ _ => idpath end. -Definition option_R_in_mapK : - forall (A A' : Type) (AR : Param40.Rel A A') - (oa : option A) (oa' : option A') (oaR : optionR A A' AR oa oa'), +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. - refine ( - fun A A' AR => - fun oa oa' oaR => - match oaR in optionR _ _ _ oa oa' - return - option_map_in_R A A' AR oa oa' (option_R_in_map A A' AR oa oa' oaR) - = oaR - with - | @someR _ _ _ a a' aR => _ - | @noneR _ _ _ => _ - end - ). - - simpl. - apply (ap (fun x => someR A A' AR a a' x)). - assert (H: - R_in_map AR a a' aR = - some_inj1 A' (map AR a) a' - (transport (fun t : A' => Some t = Some a') - (R_in_map AR a a' aR)^ - idpath) - ). { elim (R_in_map AR a a' aR). reflexivity. } - rewrite <- H. - exact (R_in_mapK AR a a' aR). - - reflexivity. -Defined. +by case: oaR => [a a' aR|]//=; elim/(ind_map AR): _; rewrite transport1. +Qed. \ No newline at end of file diff --git a/theories/Param_paths.v b/theories/Param_paths.v index ec8bddd..65b972f 100644 --- a/theories/Param_paths.v +++ b/theories/Param_paths.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. @@ -24,14 +23,14 @@ Inductive pathsR@{i} | idpathR : pathsR A A' AR x x' xR x x' xR idpath idpath. Definition paths_map@{i} - (A A' : Type@{i}) (AR : Param2b0.Rel A A') + (A A' : Type@{i}) (AR : Param2b0.Rel@{i} A A') (x : A) (x' : A') (xR : AR x x') (y : A) (y' : A') (yR : AR y y') : x = y -> x' = y' := fun e => (R_in_map AR x x' xR)^ @ ap (map AR) e @ (R_in_map AR y y' yR). Definition paths_map_in_R@{i} - (A A' : Type@{i}) (AR : Param40.Rel A A') + (A A' : Type@{i}) (AR : Param40.Rel@{i} A A') (x : A) (x' : A') (xR : AR x x') (y : A) (y' : A') (yR : AR y y') : forall (e : x = y) (e' : x' = y'), @@ -54,7 +53,7 @@ Proof. Defined. Definition paths_R_in_map@{i} - (A A' : Type@{i}) (AR : Param2b0.Rel A A') + (A A' : Type@{i}) (AR : Param2b0.Rel@{i} A A') (x : A) (x' : A') (xR : AR x x') (y : A) (y' : A') (yR : AR y y') : forall (e : x = y) (e' : x' = y'), @@ -71,23 +70,20 @@ Proof. - apply inverse. apply concat_1p. Defined. +Set Printing Universes. + Definition paths_R_in_mapK@{i} - (A A' : Type@{i}) (AR : Param40.Rel A A') + (A A' : Type@{i}) (AR : Param40.Rel@{i} A A') (x : A) (x' : A') (xR : AR x x') (y : A) (y' : A') (yR : AR y y') : - forall (e : x = y) (e' : x' = y'), - (paths_map_in_R A A' AR x x' xR y y' yR e e') - o (paths_R_in_map A A' AR x x' xR y y' yR e e') == idmap. + forall (e : x = y) (e' : x' = y') u, + paths_map_in_R@{i} A A' AR x x' xR y y' yR e e' + (paths_R_in_map@{i} A A' AR x x' xR y y' yR e e' u) = u. Proof. - intros e e' r. - destruct r. - simpl. - elim (R_in_mapK AR x x' xR). - simpl. - elim (R_in_map AR x x' xR). - simpl. - reflexivity. -Defined. +move=> e e' [] //=. +set X := (X in transport _ X _). +have -> // : X = 1%path by exact: Prop_irrelevance. +Qed. Definition Map0_paths A A' (AR : Param00.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : @@ -142,7 +138,7 @@ Definition pathsR_sym@{i} : forall (A A' : Type@{i}) (AR : Param01.Rel@{i} A A') (a1 : A) (a1' : A') (a1R : AR a1 a1') (a2 : A) (a2' : A') (a2R : AR a2 a2') (e' : a1' = a2') (e : a1 = a2), - sym_rel (pathsR A A' AR a1 a1' a1R a2 a2' a2R) e' e <~> + sym_rel (pathsR A A' AR a1 a1' a1R a2 a2' a2R) e' e <->> pathsR A' A (sym_rel AR) a1' a1 a1R a2' a2 a2R e' e. Proof. intros A A' AR a1 a1' a1R a2 a2' a2R e' e. @@ -151,8 +147,6 @@ Proof. - unshelve econstructor. + intros []; apply idpathR. + intros []; reflexivity. - + intros []; reflexivity. - + intros []; reflexivity. Defined. Definition Param01_paths@{i} diff --git a/theories/Param_prod.v b/theories/Param_prod.v index 3e4716c..b59ea4e 100644 --- a/theories/Param_prod.v +++ b/theories/Param_prod.v @@ -12,16 +12,16 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. -Require Import Hierarchy. +Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. 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 A A' AR B B' BR (a, b) (a', b'). + {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 @@ -37,8 +37,8 @@ Definition prod_map Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) : (a1, b1) = (a2, b2) -> a1 = a2 := fun e => - match e in @paths _ _ (a, b) return _ = a with - | @idpath _ _ => @idpath _ a1 + match e in _ = (a, b) return _ = a with + | eq_refl _ => @idpath _ a1 end. Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) : @@ -50,14 +50,14 @@ Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) : 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 A A' AR B B' BR p p' := + 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' AR B B' BR + 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 @@ -67,7 +67,7 @@ Definition prod_map_in_R 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 A A' AR B B' BR p p' -> prod_map A A' AR B B' BR p = p' := + 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 => @@ -89,42 +89,23 @@ Definition ap2 : forall {A B C : Type} {a a' : A} {b b' : B} (f : A -> B -> C), 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 A A' AR B B' BR p p'), + 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' r. - destruct r. - apply (ap2 (fun x y => pairR A A' AR B B' BR a a' x b b' y)). - - simpl. - assert (H: - R_in_map AR a a' aR = - (pair_inj1 A' B' (map AR a) a' (map BR b) b' - (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)^ 1%path))) - ). { elim (R_in_map AR a a' aR). elim (R_in_map BR b b' bR). reflexivity. } - rewrite <- H. - exact (R_in_mapK AR a a' aR). - - simpl. - assert (H: - R_in_map BR b b' bR = - (pair_inj2 A' B' (map AR a) a' (map BR b) b' - (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)^ 1%path))) - ). { elim (R_in_map AR a a' aR). elim (R_in_map BR b b' bR). reflexivity. } - rewrite <- H. - exact (R_in_mapK BR b b' bR). -Defined. +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 A A' AR B B' BR). + 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 A A' AR B B' BR). + 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 A A' AR B B' BR). + Map2a.Has (prodR AR BR). Proof. unshelve econstructor. - exact (prod_map A A' AR B B' BR). @@ -132,7 +113,7 @@ Proof. Defined. Definition Map2b_prod A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') : - Map2b.Has (prodR A A' AR B B' BR). + Map2b.Has (prodR AR BR). Proof. unshelve econstructor. - exact (prod_map A A' AR B B' BR). @@ -140,7 +121,7 @@ Proof. Defined. Definition Map3_prod A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') : - Map3.Has (prodR A A' AR B B' BR). + Map3.Has (prodR AR BR). Proof. unshelve econstructor. - exact (prod_map A A' AR B B' BR). @@ -149,7 +130,7 @@ Proof. Defined. Definition Map4_prod A A' (AR : Param40.Rel A A') B B' (BR : Param40.Rel B B') : - Map4.Has (prodR A A' AR B B' BR). + Map4.Has (prodR AR BR). Proof. unshelve econstructor. - exact (prod_map A A' AR B B' BR). diff --git a/theories/Param_sigma.v b/theories/Param_sigma.v index 1d42b6c..b7785b0 100644 --- a/theories/Param_sigma.v +++ b/theories/Param_sigma.v @@ -12,8 +12,7 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. -Require Import Hierarchy. +Require Import HoTT_additions Hierarchy. Set Universe Polymorphism. Unset Universe Minimization ToSet. @@ -37,19 +36,21 @@ Definition sig_map_in_R forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}), sig_map A A' AR P P' PR s = s' -> sigR A A' AR P P' PR s s'. Proof. -move=> x y; case: _ /; exists (map_in_R _ _ _ 1); exact: map_in_R. +move=> [x Px] [y Py]; case: _ /. +exists (@map_in_R A A' AR x _ 1); exact: map_in_R. Defined. +Arguments rel : simpl never. + Definition sig_R_in_map (A A' : Type) (AR : Param40.Rel A A') (P : A -> Type) (P' : A' -> Type) (PR : forall a a', AR a a' -> Param2b0.Rel (P a) (P' a')) : forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}), sigR A A' AR P P' PR s s' -> sig_map A A' AR P P' PR s = s'. Proof. - move=> s s'; elim=> a a' aR p p' pR. - elim (R_in_map _ _ _ pR). - elim (R_in_mapK _ _ _ aR). - by elim (R_in_map AR _ _ aR). + move=> [x Px] [u Py]; elim=> a a' aR p p' pR. + elim: (R_in_map _ _ _ pR) => {pR}. + by elim/(ind_map AR): _ aR / _. Defined. Definition sig_R_in_mapK @@ -58,10 +59,7 @@ Definition sig_R_in_mapK forall (s : {x : A & P x}) (s' : {x' : A' & P' x'}), (sig_map_in_R A A' AR P P' PR s s') o (sig_R_in_map A A' AR P P' PR s s') == idmap. Proof. - move=> s s' [a a' aR p p' pR]. - rewrite /sig_R_in_map /sig_map_in_R /=. - elim: {2}_ / (R_in_mapK (PR a a' aR) p p' pR). - elim: (R_in_map (PR a a' aR) p p' pR) => /=. - elim (R_in_mapK AR a a' aR) => /=. - by elim (R_in_map AR a a' aR). +move=> _ _ [a a' aR p p' pR] //=. +elim/(ind_map (PR a a' aR)): _. +by elim/(ind_mapP AR): _. Qed. diff --git a/theories/Param_sum.v b/theories/Param_sum.v index 4ba5fdd..bb2ffe4 100644 --- a/theories/Param_sum.v +++ b/theories/Param_sum.v @@ -11,8 +11,9 @@ (* * see LICENSE file for the text of the license *) (*****************************************************************************) + From Coq Require Import ssreflect. -From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy. Require Import Hierarchy. Set Universe Polymorphism. @@ -79,8 +80,10 @@ Definition sum_R_in_mapK 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]/=; rewrite /internal_paths_rew. -Admitted. + 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). diff --git a/theories/Param_trans.v b/theories/Param_trans.v index 0a7d8d0..0ae1fb1 100644 --- a/theories/Param_trans.v +++ b/theories/Param_trans.v @@ -12,7 +12,6 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Common. Set Universe Polymorphism. @@ -23,7 +22,7 @@ Unset Universe Minimization ToSet. *) Definition R_trans {A B C : Type} (R1 : A -> B -> Type) (R2 : B -> C -> Type) : A -> C -> Type := - fun a c => {b : B & R1 a b * R2 b c}. + fun a c => {b : B & (R1 a b * R2 b c)%type}. Definition map_trans {A B C : Type} (R1 : Param10.Rel A B) (R2 : Param10.Rel B C) : A -> C := map R2 o map R1. @@ -47,13 +46,9 @@ Definition R_in_mapK_trans {A B C : Type} (R1 : Param40.Rel A B) (R2 : Param40.R forall (a : A) (c : C) (r : R_trans R1 R2 a c), map_in_R_trans R1 R2 a c (R_in_map_trans R1 R2 a c r) = r. Proof. - intros a c [b [r1 r2]]; simpl. - unfold map_in_R_trans, R_in_map_trans. - unshelve eapply path_sigma. - - exact (R_in_map R1 a b r1). - - rewrite (R_in_mapK R2)/=. - rewrite -{3}(R_in_mapK R1 a b r1). - by elim: (R_in_map R1 a b r1) in r2 *. +move=> a c [b [ab bc]] /=; rewrite /map_in_R_trans/=. +elim/(ind_map R1): _ in bc *; rewrite transport1/=. +by elim/(ind_map R2): _. Qed. Definition Map0_trans {A B C : Type} (R1 : Param00.Rel A B) (R2 : Param00.Rel B C) : @@ -101,15 +96,14 @@ Defined. Definition R_trans_sym {A B C : Type} (R1 : Param00.Rel A B) (R2 : Param00.Rel B C) : forall (c : C) (a : A), - sym_rel (R_trans R1 R2) c a <~> R_trans (sym_rel R2) (sym_rel R1) c a. + sym_rel (R_trans R1 R2) c a <->> R_trans (sym_rel R2) (sym_rel R1) c a. Proof. intros c a. unfold sym_rel, R_trans. - unshelve eapply equiv_adjointify. + unshelve eexists _, _. - intros [b [r1 r2]]. exact (b; (r2, r1)). - intros [b [r2 r1]]. exact (b; (r1, r2)). - - reflexivity. - - reflexivity. + - intros [b [r2 r1]]; reflexivity. Defined. Definition Param44_trans {A B C : Type} : Param44.Rel A B -> Param44.Rel B C -> Param44.Rel A C. diff --git a/theories/Param_vector.v b/theories/Param_vector.v index 3eb4bf8..560b5e5 100644 --- a/theories/Param_vector.v +++ b/theories/Param_vector.v @@ -12,16 +12,17 @@ (*****************************************************************************) From Coq Require Import ssreflect. -From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Param_nat. +Set Asymmetric Patterns. Set Universe Polymorphism. Unset Universe Minimization ToSet. +Notation Unit := unit. + Module Vector. (* the standard vector type *) - Inductive t (A : Type) : nat -> Type := | nil : t A 0 | cons : forall (n : nat), A -> t A n -> t A (S n). @@ -149,24 +150,22 @@ Definition R_in_map : tR A A' AR n n' nR v v' -> map A A' AR n n' nR v = v'. Proof. intros A A' AR n n' nR v v' vR. - elim: vR => [|{}n {}n' {}nR a a' aR {}v {}v' _ []]. + elim: vR => [|{}n {}n' {}nR a a' aR {}v {}v' _]. - reflexivity. - - by elim (R_in_map AR a a' aR). + - by case: _ / (R_in_map AR a a' aR) => <-. Defined. -Definition R_in_mapK : - forall +Definition R_in_mapK : forall (A A' : Type) (AR : Param44.Rel A A') (n n' : nat) (nR : natR n n') (v : t A n) (v' : t A' n') (vR : tR A A' AR n n' nR v v'), map_in_R A A' AR n n' nR v v' (R_in_map A A' AR n n' nR v v' vR) = vR. Proof. - intros A A' AR n n' nR v v' vR. - elim: vR => {n n' nR v v'}[|n n' nR a a' aR v v' IHv r]//=. - elim: {2}aR / (R_in_mapK AR). - elim: (Hierarchy.R_in_map AR a a' aR)=> //=. - elim: {2}_ / r. - by elim: R_in_map. -Defined. + move=> A A' AR n n' nR v v'. + elim=> [//|{}n {}n' {}nR a a' aR {}v {}v' vR IHvR]. + rewrite -{}[in RHS]IHvR/=. + elim/(ind_map AR): _. + 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. @@ -178,42 +177,53 @@ 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' (Param_nat_sym (Param_nat_sym nR)) v v' -> tR A A' AR n n' nR v v'. Proof. -unshelve eapply equiv_adjointify. -- apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). +apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). symmetry; exact: Param_nat_symK. -- apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). - exact: Param_nat_symK. -- by move=> vR; rewrite -transport_pp concat_pV. -- by move=> vR; rewrite -transport_pp concat_Vp. +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'. +Proof. +apply: (transport (fun nR => tR _ _ _ _ _ nR _ _)). +exact: Param_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') : + 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. Defined. Local Notation f := (tR_sym_f _ _). Local Notation g := (tR_sym_t _ _). +Local Notation h := (tR_sym_tV _ _). Definition tR_sym_fK {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') (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}<-/=. -by elim: _ / Param_nat_symK (tR_sym_f _ _ _). -Defined. +elim: vR => // {}n {}n' {}nR a a' aR {}v {}v' vR {2}<-/=; rewrite /g /=. +by case: _ / Param_nat_symK (tR_sym_f _ _ _). +Qed. Definition tR_sym_fE {A A' : Type} (AR : A -> A' -> Type) {n n' : nat} (nR : natR n n') (v : t A n) (v' : t A' n') (vR : tR A A' AR n n' nR v v') : - f vR = g (f (g^-1 vR)). -Proof. by rewrite -{2}[vR]tR_sym_fK eissect tR_sym_fK. Qed. + f vR = g (f (h vR)). +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 (Param_nat_sym nR) v' v. Proof. - unshelve eapply equiv_adjointify. + unshelve eexists _, _. - exact: tR_sym_f. - move/tR_sym_f/tR_sym_t; exact. - - by move=> vR; rewrite [f (g _)]tR_sym_fE eissect tR_sym_fK. - - exact: tR_sym_fK. + - by move=> vR /=; rewrite tR_sym_fK. Defined. Definition Map4 (A A' : Type) (AR : Param44.Rel A A') (n n' : nat) (nR : natR n n') : diff --git a/theories/Trocq.v b/theories/Trocq.v index ef93cc1..f1bfced 100644 --- a/theories/Trocq.v +++ b/theories/Trocq.v @@ -12,7 +12,6 @@ (*****************************************************************************) From elpi Require Export elpi. -From HoTT Require Export HoTT. From Trocq Require Export HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param Param_paths Vernac Common Param_nat Param_trans Param_bool Param_sum Param_Empty. diff --git a/theories/Vernac.v b/theories/Vernac.v index f1a7544..7b65414 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -13,7 +13,6 @@ From Coq Require Import ssreflect. From elpi Require Import elpi. -From HoTT Require Import HoTT. From Trocq Require Import HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param Param_paths.