diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..89ab55e --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.elpi linguist-language=prolog \ No newline at end of file diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..95119e3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,9 @@ +.*.aux +.lia.cache +*.glob +*.vo +*.vok +*.vos +*~ +.*.d +Makefile.coq* \ No newline at end of file diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..825c32f --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1 @@ +# Changelog diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..0a04128 --- /dev/null +++ b/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..e814639 --- /dev/null +++ b/Makefile @@ -0,0 +1,10 @@ +.PHONY: all + +all: Makefile.coq + $(MAKE) -f Makefile.coq all + +Makefile.coq: + coq_makefile -f _CoqProject -o Makefile.coq + +%:: Makefile.coq + $(MAKE) -f Makefile.coq $@ diff --git a/README.md b/README.md new file mode 100644 index 0000000..0b7e0b9 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# Trocq + +This repository contains Trocq, a modular parametricity plugin for proof transfer in Coq. + +NB: it relies on a [custom version of Coq-Elpi](https://github.com/ecranceMERCE/coq-elpi/tree/strat), mainly changing its behaviour regarding the translation of universe variables between Elpi and Coq. \ No newline at end of file diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..4925924 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,22 @@ +-arg -noinit +-arg -indices-matter + +-R theories/ Trocq +-R elpi/ Trocq.Elpi + +theories/HoTT_additions.v +theories/Hierarchy.v +theories/Param_Type.v +theories/Param_forall.v +theories/Param_arrow.v +theories/Database.v +theories/Param.v +theories/Trocq.v +theories/Param_paths.v + +examples/Example.v +examples/int_to_Zp.v +examples/peano_bin_nat.v +examples/setoid_rewrite.v +examples/summable.v +examples/trocq_setoid_rewrite.v diff --git a/coq-trocq.opam b/coq-trocq.opam new file mode 100644 index 0000000..c1a5c48 --- /dev/null +++ b/coq-trocq.opam @@ -0,0 +1,39 @@ +opam-version: "2.0" +name: "coq-trocq" +version: "dev" +maintainer: "Enzo Crance " +authors: [ "Cyril Cohen", "Enzo Crance", "Assia Mahboubi" ] +homepage: "https://github.com/ecranceMERCE/trocq" +bug-reports: "https://github.com/ecranceMERCE/trocq/issues" +dev-repo: "https://github.com/ecranceMERCE/trocq.git" +# doc: "https://ecranceMERCE.github.io/trocq" +build: [ make "-j%{jobs}%" ] +install: [ make "install" ] +depends: [ + "coq" {>= "8.17.0" & < "8.18~" } + "coq-elpi" {= "dev"} + "coq-hott" {>= "8.17" & < "8.18~"} +] +tags: [ + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Miscellaneous/Coq Extensions" + "keyword:automation" + "keyword:elpi" + "date:2023-11-10" + "logpath:Trocq" +] +synopsis: "A modular parametricity plugin for proof transfer in Coq" +description: """ +Trocq is a prototype of modular parametricity plugin for Coq, aiming to perform proof transfer by translating the goal into an associated goal featuring the target data structures as well as a rich parametricity witness from which a function justifying the goal substitution can be extracted. + +The plugin features a hierarchy of parametricity witness types, ranging from structure-less relations to a new formulation of type equivalence, gathering several pre-existing parametricity translations, among which univalent parametricity (*), under the same framework. + +This modular translation performs a fine-grained analysis and generates witnesses that are rich enough to preprocess the goal yet are not always a full-blown type equivalence, allowing to perform proof transfer with the power of univalent parametricity, but trying not to pull in the univalence axiom in cases where it is not required. + +The translation is implemented in Coq-Elpi and features transparent and readable code with respect to a sequent-style theoretical presentation. + +(*) The marriage of univalence and parametricity, Tabareau et al. (2021) +""" +url { + src: "git+https://github.com/ecranceMERCE/trocq.git" +} diff --git a/elpi/annot.elpi b/elpi/annot.elpi new file mode 100644 index 0000000..ae44c45 --- /dev/null +++ b/elpi/annot.elpi @@ -0,0 +1,133 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% annotated type theory +% -------------------------------------------------------------------------------------------------- + +% this allows to easily make sure an application is beta-reduced +:before "subst-fun:fail" +coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs. + +% annotate a term +% 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]) :- param.db.ptype PType, !, + coq.univ-instance UI [{coq.univ.variable U}], + cstr.univ-link _ M N. +term->annot-term (fun N T F) (fun N T' F') :- !, + term->annot-term T T', + pi x\ term->annot-term (F x) (F' x). +term->annot-term (prod N T F) (prod N T' F') :- !, + term->annot-term T T', + pi x\ term->annot-term (F x) (F' x). +term->annot-term (app L) (app L') :- !, + std.map L term->annot-term L'. +term->annot-term X X :- (name X ; X = global _ ; X = pglobal _ _), !. +term->annot-term T _ :- coq.error "term->annot-term:" T. + +macro @annot-pi-decl N T F :- pi x\ annot.adecl x N T => F x. + +namespace annot { + +% typechecking a term calls Coq's typechecker, which gives back a non annotated term +% calling term->annot-term on it will add fresh annotations +% if we want to typecheck a variable several times and get the same type everytime, we need to +% add some memory, which is the purpose of adecl +pred adecl i:term, o:name, o:term. + +pred typecheck i:term, o:term. +typecheck T ATy :- adecl T _ ATy, !. +typecheck T ATy :- + coq.typecheck T Ty ok, !, + term->annot-term Ty ATy. + +% sub-typing predicate following the sub-typing rules in the article +pred sub-type i:term, i:term. +% SubUniv +sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :- + param.db.ptype PType, !, + cstr.univ-link C1 M1 N1, + cstr.univ-link C2 M2 N2, + cstr.geq C1 C2. +% SubPi +sub-type (prod N T F) (prod _ T' F') :- !, + sub-type T' T, + @annot-pi-decl N T' x\ sub-type (F x) (F' x). +% SubLam +sub-type (fun N T F) (fun _ T F') :- !, + @annot-pi-decl N T x\ sub-type (F x) (F' x). +% SubApp +sub-type (app [F|Xs]) (app [F'|Xs']) :- !, + sub-type F F', + std.forall2 Xs Xs' eq. +% SubConv +sub-type X X :- (name X ; X = global _ ; X = pglobal _ _), !. +sub-type X _ :- coq.error "annot.sub-type:" X. + +% 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]) :- + param.db.ptype PType, !, + cstr.univ-link C1 M1 N1, + cstr.univ-link C2 M2 N2, + cstr.eq C1 C2. +eq (prod _ T F) (prod _ T' F') :- !, + eq T T', + pi x\ eq (F x) (F' x). +eq (fun _ T F) (fun _ T' F') :- !, + eq T T', + pi x\ eq (F x) (F' x). +eq (app L) (app L') :- !, + std.forall2 L L' eq. +eq X X :- (name X ; X = global _ ; X = pglobal _ _), !. +eq X _ :- coq.error "annot.eq:" X. + +% get all the annotations in a type T, as well as the "output class", i.e., the parametricity class +% of the output type of T, as an option basically returning some (A,B) for an output type PType A B, +% 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 :- + 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] :- param.db.ptype PType, !, + 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. +all-classes (app L) Cs :- !, + std.flatten {std.map L all-classes} Cs. +all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !. +all-classes X _ :- coq.error "all-classes:" X. + +pred out-class i:term, o:option param-class. +out-class (app [pglobal (const PType) _, M, N]) (some C) :- param.db.ptype PType, !, + cstr.univ-link C M N. +out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out. +out-class (fun _ _ _) none :- !. +out-class (app [F|Xs]) Out :- !, + coq.subst-fun Xs F App, + if (App = app [F|Xs]) (Out = none) (out-class App Out). +out-class X none :- (name X ; X = global _ ; X = pglobal _ _), !. +out-class X _ :- coq.error "out-class:" X. +% constant applications convertible to terms having a sort as output are not supported + +} % annot diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi new file mode 100644 index 0000000..ef8c386 --- /dev/null +++ b/elpi/constraints/constraint-graph.elpi @@ -0,0 +1,262 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% definition of the constraint graph +% -------------------------------------------------------------------------------------------------- + +% in the constraint graph, parametricity classes are represented with integers (it is easier to +% index on this type than on variables of type param-class) +typeabbrev class-id int. + +% the graph is a map from a class to two lists: the nodes that are higher than it, and the ones +% that are lower; it means that the graph stores each piece of information twice (in both ways +kind constraint-graph type. +type constraint-graph + std.map class-id (pair (list cstr-graph.node) (list cstr-graph.node)) + -> constraint-graph. + +namespace cstr-graph { + +% a node represents one or several edges starting from a class, with additional information to be +% used when reducing the graph; see the predicates below +kind node type. +type node.var constraint-type -> list class-id -> node. +type node.const param-class -> node. + +% this basically represents annotations on the edges +kind constraint-type type. +type ct.pi constraint-type. +type ct.arrow constraint-type. +type ct.type constraint-type. +type ct.gref gref -> term -> gref -> gref -> constraint-type. +type ct.geq constraint-type. + +typeabbrev + constraint-graph-content + (std.map class-id (pair (list node) (list node))). + +pred empty o:constraint-graph. +empty (constraint-graph G) :- + std.map.make util.cmp-int G. + +% D_π(C, C_A, C_B) is represented as two edges C -> C_A and C -> C_B +% here one node from C to [C_A, C_B], and two nodes from C_A and C_B to C +pred add-dep-pi i:class-id, i:class-id, i:class-id, i:constraint-graph, o:constraint-graph. +add-dep-pi ID IDA IDB (constraint-graph G) (constraint-graph G') :- + util.map.update ID (internal.add-higher-node (node.var ct.pi [IDA, IDB])) G G1, + util.map.update IDA (internal.add-lower-node (node.var ct.pi [ID])) G1 G2, + util.map.update IDB (internal.add-lower-node (node.var ct.pi [ID])) G2 G'. + +% D_->(C, C_A, C_B) is similar +pred add-dep-arrow i:class-id, i:class-id, i:class-id, i:constraint-graph, o:constraint-graph. +add-dep-arrow ID IDA IDB (constraint-graph G) (constraint-graph G') :- + util.map.update ID (internal.add-higher-node (node.var ct.arrow [IDA, IDB])) G G1, + util.map.update IDA (internal.add-lower-node (node.var ct.arrow [ID])) G1 G2, + util.map.update IDB (internal.add-lower-node (node.var ct.arrow [ID])) G2 G'. + +% D_□(C, C_R) is an edge C -> C_R, which is one node in each direction +pred add-dep-type i:class-id, i:class-id, i:constraint-graph, o:constraint-graph. +add-dep-type ID IDR (constraint-graph G) (constraint-graph G') :- + util.map.update ID (internal.add-higher-node (node.var ct.type [IDR])) G G1, + util.map.update IDR (internal.add-lower-node (node.var ct.type [ID])) G1 G'. + +% D_K(C, C_1, ... C_n) is an edge from the output class C of constant K to each class C_i present +% in its type, see the article for explanation +% the constraint is represented here by one node from C to all the C_i +% we store information in the node about K, its type, and the output variables +pred add-dep-gref + i:class-id, i:gref, i:term, i:gref, i:gref, i:list class-id, i:constraint-graph, + o:constraint-graph. +add-dep-gref ID GR T GR' GRR IDs (constraint-graph G) (constraint-graph G') :- + % the classes C_i (IDs) are not really "higher" than the output class C (ID) + % here, higher is a way to say that they must be instantiated later than the output class + util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T GR' GRR) IDs)) G G1, + std.fold IDs G1 (id\ g\ g'\ + util.map.update id (internal.add-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g') + G'. + +% simple order constraint C >= C', handled differently if C and C' are constant classes or variables +pred add-geq + i:or class-id param-class, i:or class-id param-class, i:constraint-graph, o:constraint-graph. +add-geq (inl IDA) (inl IDB) (constraint-graph G) (constraint-graph G') :- + util.map.update IDB (internal.add-higher-node (node.var ct.geq [IDA])) G G1, + util.map.update IDA (internal.add-lower-node (node.var ct.geq [IDB])) G1 G'. +add-geq (inl ID) (inr C) (constraint-graph G) (constraint-graph G') :- + util.map.update ID (internal.add-lower-node (node.const C)) G G'. +add-geq (inr C) (inl ID) (constraint-graph G) (constraint-graph G') :- + util.map.update ID (internal.add-higher-node (node.const C)) G G'. + +% compute the minimal possible constant class for a variable class in the constraint graph +% = least upper bound of all the lower constant classes +pred minimal-class i:class-id, i:constraint-graph, o:param-class. +minimal-class ID (constraint-graph G) MinClass :- + std.map.find ID G (pr LowerNodes _), !, + std.fold {internal.filter-const LowerNodes} (pc map0 map0) param-class.union MinClass. +minimal-class _ _ (pc map0 map0). % default minimal class for an unconstrained variable + +% compute the maximal possible constant class for a variable class in the constraint graph +% = greatest lower bound of all the higher constant classes +pred maximal-class i:class-id, i:constraint-graph, o:param-class. +maximal-class ID (constraint-graph G) MaxClass :- + std.map.find ID G (pr _ HigherNodes), !, + std.fold {internal.filter-const HigherNodes} (pc map4 map4) param-class.inter MaxClass. +maximal-class _ _ (pc map4 map4). % default maximal class for an unconstrained variable + +% 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 +pred instantiate i:class-id, i:param-class, i:constraint-graph, o:constraint-graph. +instantiate ID Class G _ :- coq.say "instantiate" ID Class G, fail. +instantiate ID Class (constraint-graph G) (constraint-graph G') :- + std.map.find ID G (pr LowerNodes HigherNodes), !, + 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'. +instantiate ID Class G G :- + coq.say "cannot instantiate" ID "at" Class "because it is not in the graph". +pred instantiate.aux + i:class-id, i:param-class, i:node, i:constraint-graph-content, o:constraint-graph-content. +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' :- + 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 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 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 GR' GRR) IDs) G G' :- + 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, + annot.classes T TCs _, + % find the output constant and proof, as well as the required classes Cs + param.db.gref GR Class Cs GR' GRR, + % make sure the classes are consistent + 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. +instantiate.gref [] [] [] G G. +instantiate.gref [-1|IDs] [TC|TCs] [C|Cs] G G' :- !, + % here the class in the type of the constant is a constant class, it is not in the graph + % 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' :- + % 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.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, + util.map.update IDH (internal.add-lower-node (node.const Class)) G1 G'. + +% compute the precedence graph from the constraint graph to find the instantiation order +pred instantiation-order i:list class-id, i:constraint-graph, o:list class-id. +instantiation-order IDs ConstraintGraph SortedIDs :- + internal.to-precedence-graph IDs ConstraintGraph PrecedenceGraph, + simple-graph.toposort PrecedenceGraph OSIDs, + std.assert! (OSIDs = some SortedIDs) "the precedence graph is not acyclic". + +% pretty printing +pred pp i:constraint-graph. +pp (constraint-graph G) :- + std.forall {std.map.bindings G} pp.aux. +pp.aux (pr ID (pr LowerNodes HigherNodes)) :- + coq.say "id" ID, + coq.say "higher than:" LowerNodes, + coq.say "lower than:" HigherNodes. + +namespace internal { + +pred filter-const i:list node, o:list param-class. +filter-const [] []. +filter-const [node.const C|Nodes] [C|Classes] :- + filter-const Nodes Classes. +filter-const [node.var _ _|Nodes] Classes :- + filter-const Nodes Classes. + +pred filter-var i:list node, o:list class-id. +filter-var [] []. +filter-var [node.var _ IDs1|Nodes] IDs :- + filter-var Nodes IDs2, + std.append IDs1 IDs2 IDs. +filter-var [node.const _|Nodes] IDs :- + filter-var Nodes IDs. + +pred add-higher-node + i:node, i:option (pair (list node) (list node)), o:option (pair (list node) (list node)). +add-higher-node Node none (some (pr [] [Node])). +add-higher-node Node (some (pr LowerNodes HigherNodes)) (some (pr LowerNodes [Node|HigherNodes])). + +pred remove-higher-node + i:node, i:option (pair (list node) (list node)), o:option (pair (list node) (list node)). +remove-higher-node _ none none. +remove-higher-node Node (some (pr LowerNodes HigherNodes)) Nodes :- + util.delete Node HigherNodes HigherNodes', + if (LowerNodes = [], HigherNodes' = []) + (Nodes = none) + (Nodes = some (pr LowerNodes HigherNodes')). + +pred add-lower-node + i:node, i:option (pair (list node) (list node)), o:option (pair (list node) (list node)). +add-lower-node Node none (some (pr [Node] [])). +add-lower-node Node (some (pr LowerNodes HigherNodes)) (some (pr [Node|LowerNodes] HigherNodes)). + +pred remove-lower-node + i:node, i:option (pair (list node) (list node)), o:option (pair (list node) (list node)). +remove-lower-node _ none none. +remove-lower-node Node (some (pr LowerNodes HigherNodes)) Nodes :- + util.delete Node LowerNodes LowerNodes', + if (LowerNodes' = [], HigherNodes = []) + (Nodes = none) + (Nodes = some (pr LowerNodes' HigherNodes)). + +pred to-precedence-graph i:list class-id, i:constraint-graph, o:simple-graph class-id. +to-precedence-graph IDs (constraint-graph G) PrecedenceGraph :- + std.fold IDs {simple-graph.empty util.cmp-int} simple-graph.add-node SG, + std.map.bindings G Bindings, + std.fold Bindings SG to-precedence-graph.aux PrecedenceGraph. +to-precedence-graph.aux (pr ID (pr _ HigherNodes)) G G' :- + std.fold HigherNodes G (to-precedence-graph.aux2 ID) G'. +to-precedence-graph.aux2 _ (node.const _) G G. +to-precedence-graph.aux2 ID (node.var _ IDHs) G G' :- + % for each variable Y higher than X in the constraint graph, + % the precedence graph has an edge X -> Y + std.fold IDHs G (simple-graph.add-edge ID) G'. + +} % internal + +} % cstr-graph diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi new file mode 100644 index 0000000..d0d488c --- /dev/null +++ b/elpi/constraints/constraints.elpi @@ -0,0 +1,261 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% API accessible to the rest of the plugin to handle the constraint graph +% -------------------------------------------------------------------------------------------------- + +typeabbrev class-id int. + +namespace cstr { + +pred init. +init :- + cstr-graph.empty G, + declare_constraint (internal.c.vars []) [_], + declare_constraint (internal.c.graph G) [_]. + +% link a variable parametricity class C to its Coq representation (arguments of PType) +pred univ-link o:param-class, o:term, o:term. +univ-link C M N :- var C, var M, var N, !, + declare_constraint (internal.c.univ-link? C M N) [_]. +univ-link C M N :- var C, !, + C = pc {term->map-class M} {term->map-class N}. +univ-link (pc M' N') M N :- + map-class->term M' M, + map-class->term N' N. + +% D_π(C) = (C_A, C_B) +pred dep-pi i:param-class, o:param-class, o:param-class. +dep-pi C CA CB :- var C, !, + internal.link? C ID, + internal.link? CA IDA, + internal.link? CB IDB, + declare_constraint (internal.c.dep-pi ID IDA IDB) [_]. +dep-pi C CA CB :- + param-class.dep-pi C CA CB. + +% D_->(C) = (C_A, C_B) +pred dep-arrow i:param-class, o:param-class, o:param-class. +dep-arrow C CA CB :- var C, !, + internal.link? C ID, + internal.link? CA IDA, + internal.link? CB IDB, + declare_constraint (internal.c.dep-arrow ID IDA IDB) [_]. +dep-arrow C CA CB :- + param-class.dep-arrow C CA CB. + +% D_□(C, C_R) +pred dep-type i:param-class, i:param-class. +dep-type C CR :- var C, !, + internal.link? C ID, + internal.link? CR 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)). + +% D_K(T) +pred dep-gref i:gref, i:term, o:gref, o:gref. +dep-gref GR T GR' GRR :- + annot.classes T TCs OutOpt, + util.option.value OutOpt (pc map0 map0) Out, + if (var Out) ( + internal.link? Out ID, + std.map TCs internal.link? IDs, + declare_constraint (internal.c.dep-gref ID GR T GR' GRR IDs) [_] + ) ( + param.db.gref GR Out Cs GR' GRR, + std.forall2 TCs Cs eq + ). + +% C >= C' +pred geq i:param-class, i:param-class. +geq C1 C2 :- var C1, var C2, !, + internal.link? C1 ID1, + internal.link? C2 ID2, + util.unless (ID1 = ID2) (declare_constraint (internal.c.geq (inl ID1) (inl ID2)) [_]). +geq C1 C :- var C1, !, + internal.link? C1 ID, + declare_constraint (internal.c.geq (inl ID) (inr C)) [_]. +geq C C1 :- var C1, !, + internal.link? C1 ID, + declare_constraint (internal.c.geq (inr C) (inl ID)) [_]. +geq C1 C2 :- + param-class.geq C1 C2. + +% C = C' +pred eq i:param-class, i:param-class. +eq C1 C2 :- geq C1 C2, geq C2 C1. + +% trigger reduction of the graph and instantiation of variables +pred reduce-graph. +reduce-graph :- + declare_constraint internal.c.reduce-graph [_]. + +% ================================================================================================== + +namespace internal { + +% NB: +% - constraints with a '?' suffix are getters; +% - constraints with a '!' suffix are setters; +% - constraints with a '-' suffix both get and delete information. + +% store all the variable classes encountered so far +pred c.vars o:list class-id. +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) [_]. +pred vars! i:list class-id. +vars! IDs :- declare_constraint (c.vars! IDs) [_]. + +constraint c.vars c.vars? c.vars! { + rule (c.vars IDs) \ (c.vars? IDs') <=> (IDs' = IDs). + rule \ (c.vars _) (c.vars! IDs) <=> (declare_constraint (c.vars IDs) [_]). +} + +% link a class to an integer in the constraint store +pred c.link o:param-class, o:class-id. +pred c.link? o:param-class, o:class-id. +pred c.link- o:param-class, o:class-id. + +pred link? o:param-class, o:class-id. +link? C ID :- var C, !, declare_constraint (c.link? C ID) [_]. +link? _ (-1). % when the class is constant, it does not exist in the graph, default value is -1 +pred link- o:param-class, o:class-id. +link- C ID :- declare_constraint (c.link- C ID) [_]. + +constraint c.link c.link? c.link- { + % we know the class, we need the integer + rule (c.link C ID) \ (c.link? C ID') <=> (ID' = ID). + rule \ (c.link C ID) (c.link- C ID') <=> (ID' = ID). + % we know the integer, we need the class + rule (c.link C ID) \ (c.link? C' ID) <=> (C' = C). + rule \ (c.link C ID) (c.link- C' ID) <=> (C' = C). + % both are unknown, create the fresh node + rule \ (c.link? C ID') <=> ( + vars? IDs, + new_int ID, + prune C [], + declare_constraint (c.link C ID) [_], + vars! [ID|IDs], + ID' = ID + ). + rule \ (c.link- _ _). +} + +% link a class C to a pair of Coq map classes +pred c.univ-link o:param-class, o:term, o:term. +pred c.univ-link? o:param-class, o:term, o:term. +pred c.univ-link- o:param-class, o:term, o:term. + +pred univ-link- o:param-class, o:term, o:term. +univ-link- C M N :- declare_constraint (c.univ-link- C M N) [_]. + +constraint c.univ-link c.univ-link? c.univ-link- { + % we know the class, we need the Coq values + rule (c.univ-link C M N) \ (c.univ-link? C M' N') <=> (M' = M, N' = N). + rule \ (c.univ-link C M N) (c.univ-link- C M' N') <=> (M' = M, N' = N). + % we know the Coq values, we need the class + rule (c.univ-link C M N) \ (c.univ-link? C' M N) <=> (C' = C). + rule \ (c.univ-link C M N) (c.univ-link- C' M N) <=> (C' = C). + % both are unknown, create the fresh link and loop + rule (c.univ-link? C M N) <=> ( + link? C _, + prune M [], + prune N [], + declare_constraint (c.univ-link C M N) [_] + ). + rule \ (c.univ-link- _ _ _). +} + +% store the constraint graph in the Elpi constraint store +pred c.graph o:constraint-graph. + +% constraints to trigger addition of information to the constraint graph +pred c.dep-pi o:class-id, o:class-id, o:class-id. +pred c.dep-arrow o:class-id, o:class-id, o:class-id. +pred c.dep-type o:class-id, o:class-id. +pred c.dep-gref o:class-id, o:gref, o:term, o:gref, o:gref, o:list class-id. +pred c.geq o:or class-id param-class, o:or class-id param-class. + +% trigger reduction of the graph +pred c.reduce-graph. + +constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-graph { + rule \ (c.graph G) (c.dep-pi ID IDA IDB) <=> ( + cstr-graph.add-dep-pi ID IDA IDB G G', + declare_constraint (c.graph G') [_] + ). + rule \ (c.graph G) (c.dep-arrow ID IDA IDB) <=> ( + cstr-graph.add-dep-arrow ID IDA IDB G G', + declare_constraint (c.graph G') [_] + ). + rule \ (c.graph G) (c.dep-type ID IDR) <=> ( + cstr-graph.add-dep-type ID IDR G G', + declare_constraint (c.graph G') [_] + ). + rule \ (c.graph G) (c.dep-gref ID GR T GR' GRR IDs) <=> ( + cstr-graph.add-dep-gref ID GR T GR' GRR IDs G G', + declare_constraint (c.graph G') [_] + ). + rule \ (c.graph G) (c.geq IDorC1 IDorC2) <=> ( + cstr-graph.add-geq IDorC1 IDorC2 G G', + declare_constraint (c.graph G') [_] + ). + rule \ (c.graph G) (c.reduce-graph) <=> ( + vars? IDs, + util.when-debug dbg.steps ( + coq.say "final constraint graph:", + cstr-graph.pp G, + coq.say "***********************************************************************************" + ), + cstr-graph.instantiation-order IDs G SortedIDs, + util.when-debug dbg.steps ( + coq.say "order:" SortedIDs, + coq.say "***********************************************************************************" + ), + reduce SortedIDs G FinalValues, + util.when-debug dbg.steps (coq.say "final values:" FinalValues), + std.forall FinalValues instantiate-coq + ). +} + +% reduce the graph by instantiating variables in the precedence order and updating the graph +% 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] :- + 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. + +% now instantiate for real +pred instantiate-coq i:pair class-id param-class. +instantiate-coq (pr ID (pc M0 N0)) :- + 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. + +} % internal + +} % cstr \ No newline at end of file diff --git a/elpi/constraints/simple-graph.elpi b/elpi/constraints/simple-graph.elpi new file mode 100644 index 0000000..e615d2b --- /dev/null +++ b/elpi/constraints/simple-graph.elpi @@ -0,0 +1,61 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% definition of a directed graph with no annotation on edges +% -------------------------------------------------------------------------------------------------- + +kind simple-graph type -> type. +type simple-graph std.map A (list A) -> simple-graph A. + +namespace simple-graph { + +pred empty i:A -> A -> cmp -> prop, o:simple-graph A. +empty Cmp (simple-graph G) :- + std.map.make Cmp G. + +pred add-node i:A, i:simple-graph A, o:simple-graph A. +add-node X (simple-graph G) (simple-graph G') :- + std.map.add X [] G G'. + +pred add-edge i:A, i:A, i:simple-graph A, o:simple-graph A. +add-edge X Y (simple-graph G) (simple-graph G') :- + util.map.update X (add-edge.aux Y) G G'. +add-edge.aux Y none (some [Y]). +add-edge.aux Y (some L) (some [Y|L]). + +% topological sort +pred toposort i:simple-graph A, o:option (list A). +toposort (simple-graph G) SortedNodes :- + reversed-kahn {std.map.bindings G} [] SortedNodes. + +% Kahn's algorithm +% reversed: we remove exit nodes instead of entry nodes +pred reversed-kahn i:list (pair A (list A)), i:list A, o:option (list A). +reversed-kahn Bindings Stack SortedNodes :- + std.map-filter Bindings (p\ n\ p = pr n []) ExitNodes, + if (ExitNodes = []) ( + if (Bindings = []) + (SortedNodes = some Stack) + (SortedNodes = none) + ) ( + std.map-filter Bindings (p\ p'\ sigma Node Successors Successors'\ + p = pr Node Successors, + not (std.mem! ExitNodes Node), + std.filter Successors (s\ not (std.mem! ExitNodes s)) Successors', + p' = pr Node Successors' + ) Bindings', + reversed-kahn Bindings' {std.append ExitNodes Stack} SortedNodes + ). + +} % simple-graph diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi new file mode 100644 index 0000000..1398cfe --- /dev/null +++ b/elpi/param-class.elpi @@ -0,0 +1,253 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% definition of parametricity classes +% -------------------------------------------------------------------------------------------------- + +% a parametricity class is a pair of map classes (levels in our hierarchy) +kind map-class type. +type map0 map-class. +type map1 map-class. +type map2a map-class. +type map2b map-class. +type map3 map-class. +type map4 map-class. + +kind param-class type. +type pc map-class -> map-class -> param-class. + +pred map-class->term i:map-class, o:term. +map-class->term map0 (pglobal Map0 UI) :- + coq.locate "map0" Map0, + coq.univ-instance UI []. +map-class->term map1 (pglobal Map1 UI) :- + coq.locate "map1" Map1, + coq.univ-instance UI []. +map-class->term map2a (pglobal Map2a UI) :- + coq.locate "map2a" Map2a, + coq.univ-instance UI []. +map-class->term map2b (pglobal Map2b UI) :- + coq.locate "map2b" Map2b, + coq.univ-instance UI []. +map-class->term map3 (pglobal Map3 UI) :- + coq.locate "map3" Map3, + coq.univ-instance UI []. +map-class->term map4 (pglobal Map4 UI) :- + coq.locate "map4" Map4, + coq.univ-instance UI []. + +pred term->map-class i:term, o:map-class. +term->map-class (pglobal Map0 _) map0 :- coq.locate "map0" Map0. +term->map-class (pglobal Map1 _) map1 :- coq.locate "map1" Map1. +term->map-class (pglobal Map2a _) map2a :- coq.locate "map2a" Map2a. +term->map-class (pglobal Map2b _) map2b :- coq.locate "map2b" Map2b. +term->map-class (pglobal Map3 _) map3 :- coq.locate "map3" Map3. +term->map-class (pglobal Map4 _) map4 :- coq.locate "map4" Map4. + +pred map-class->string i:map-class, o:string. +map-class->string map0 "0". +map-class->string map1 "1". +map-class->string map2a "2a". +map-class->string map2b "2b". +map-class->string map3 "3". +map-class->string map4 "4". + +pred param-class->string i:param-class, o:string. +param-class->string (pc M N) S :- + S is {map-class->string M} ^ {map-class->string N}. + +% names of the fields contained in a witness of a given level +pred map-class->fields i:map-class, o:list string. +map-class->fields map0 []. +map-class->fields map1 ["map"]. +map-class->fields map2a ["map", "map_in_R"]. +map-class->fields map2b ["map", "R_in_map"]. +map-class->fields map3 ["map", "map_in_R", "R_in_map"]. +map-class->fields map4 ["map", "map_in_R", "R_in_map", "R_in_mapK"]. + +pred map-class->cofields i:map-class, o:list string. +map-class->cofields map0 []. +map-class->cofields map1 ["comap"]. +map-class->cofields map2a ["comap", "comap_in_R"]. +map-class->cofields map2b ["comap", "R_in_comap"]. +map-class->cofields map3 ["comap", "comap_in_R", "R_in_comap"]. +map-class->cofields map4 ["comap", "comap_in_R", "R_in_comap", "R_in_comapK"]. + +namespace map-class { + +% lower/higher levels at distance 1 from a given level +pred weakenings-from i:map-class, o:list map-class. +weakenings-from map0 []. +weakenings-from map1 [map0]. +weakenings-from map2a [map1]. +weakenings-from map2b [map1]. +weakenings-from map3 [map2a, map2b]. +weakenings-from map4 [map3]. + +pred weakenings-to i:map-class, o:list map-class. +weakenings-to map0 [map1]. +weakenings-to map1 [map2a, map2b]. +weakenings-to map2a [map3]. +weakenings-to map2b [map3]. +weakenings-to map3 [map4]. +weakenings-to map4 []. + +% all possible parametricity classes that can be created by combinations of 2 lists of map classes +pred product i:list map-class, i:list map-class, o:list param-class. +product Ms Ns Classes :- + std.map Ms (m\ cs\ + std.map Ns (n\ c\ c = pc m n) cs + ) ClassesLL, + std.flatten ClassesLL Classes. + +% least upper bound containing all the fields of the two provided map classes +pred union i:map-class, i:map-class, o:map-class. +union map4 _ map4. +union map3 map4 map4 :- !. +union map3 _ map3. +union map2b map4 map4 :- !. +union map2b map3 map3 :- !. +union map2b map2a map3 :- !. +union map2b _ map2b. +union map2a map4 map4 :- !. +union map2a map3 map3 :- !. +union map2a map2b map3 :- !. +union map2a _ map2a. +union map1 map4 map4 :- !. +union map1 map3 map3 :- !. +union map1 map2b map2b :- !. +union map1 map2a map2a :- !. +union map1 _ map1. +union map0 M M. + +% greatest lower bound containing the fields in common in the two provided map classes +pred inter i:map-class, i:map-class, o:map-class. +inter map0 _ map0. +inter map1 map0 map0 :- !. +inter map1 _ map1. +inter map2a map0 map0 :- !. +inter map2a map1 map1 :- !. +inter map2a map2b map1 :- !. +inter map2a _ map2a. +inter map2b map0 map0 :- !. +inter map2b map1 map1 :- !. +inter map2b map2a map1 :- !. +inter map2b _ map2b. +inter map3 map4 map3 :- !. +inter map3 M M. +inter map4 M M. + +% partial order on map classes +pred geq i:map-class, i:map-class. +geq map4 _. +geq map3 M :- std.mem! [map0, map1, map2a, map2b, map3] M. +geq map2a M :- std.mem! [map0, map1, map2a] M. +geq map2b M :- std.mem! [map0, map1, map2b] M. +geq map1 M :- std.mem! [map0, map1] M. +geq map0 map0. + +% minimal dependencies to translate a dependent product, see the table in the article +pred dep-pi i:map-class, o:param-class, o:param-class. +dep-pi map0 (pc map0 map0) (pc map0 map0). +dep-pi map1 (pc map0 map2a) (pc map1 map0). +dep-pi map2a (pc map0 map4) (pc map2a map0). +dep-pi map2b (pc map0 map2a) (pc map2b map0). +dep-pi map3 (pc map0 map4) (pc map3 map0). +dep-pi map4 (pc map0 map4) (pc map4 map0). + +% minimal dependencies to translate an arrow type, see the table in the article +pred dep-arrow i:map-class, o:param-class, o:param-class. +dep-arrow map0 (pc map0 map0) (pc map0 map0). +dep-arrow map1 (pc map0 map1) (pc map1 map0). +dep-arrow map2a (pc map0 map2b) (pc map2a map0). +dep-arrow map2b (pc map0 map2a) (pc map2b map0). +dep-arrow map3 (pc map0 map3) (pc map3 map0). +dep-arrow map4 (pc map0 map4) (pc map4 map0). + +} % map-class + +namespace param-class { + +% extensions of functions over map classes to parametricity classes + +pred weakenings-from i:param-class, o:list param-class. +weakenings-from (pc M N) Classes :- + map-class.weakenings-from M Ms, + map-class.weakenings-from N Ns, + map-class.product Ms Ns Classes. + +pred weakenings-to i:param-class, o:list param-class. +weakenings-to (pc M N) Classes :- + map-class.weakenings-to M Ms, + map-class.weakenings-to N Ns, + map-class.product Ms Ns Classes. + +pred negate i:param-class, o:param-class. +negate (pc M N) (pc N M). + +pred union i:param-class, i:param-class, o:param-class. +union (pc M1 N1) (pc M2 N2) (pc M N) :- + map-class.union M1 M2 M, + map-class.union N1 N2 N. + +pred inter i:param-class, i:param-class, o:param-class. +inter C C' _ :- coq.say C C', fail. +inter (pc M1 N1) (pc M2 N2) (pc M N) :- + map-class.inter M1 M2 M, + map-class.inter N1 N2 N. + +pred geq i:param-class, i:param-class. +geq (pc M1 N1) (pc M2 N2) :- + map-class.geq M1 M2, + map-class.geq N1 N2. + +pred dep-pi i:param-class, o:param-class, o:param-class. +dep-pi (pc M N) ClassA ClassB :- + map-class.dep-pi M ClassAM ClassBM, + map-class.dep-pi N ClassAN ClassBN, + union ClassAM {param-class.negate ClassAN} ClassA, + union ClassBM {param-class.negate ClassBN} ClassB. + +pred dep-arrow i:param-class, o:param-class, o:param-class. +dep-arrow (pc M N) ClassA ClassB :- + map-class.dep-arrow M ClassAM ClassBM, + map-class.dep-arrow N ClassAN ClassBN, + union ClassAM {param-class.negate ClassAN} ClassA, + union ClassBM {param-class.negate ClassBN} ClassB. + +% generate a weakening function from a parametricity class to another, by forgetting fields 1 by 1 +pred forget i:param-class, i:param-class, o:univ-instance -> term -> term -> term -> term. +forget (pc M N) (pc M N) (_\ _\ _\ r\ r) :- !. +forget (pc M N) (pc M N') ForgetF :- !, + std.mem {map-class.weakenings-from N} N1, + forget (pc M N1) (pc M N') ForgetF', !, + map-class->string M MStr, + coq.locate + {calc ("forget_" ^ MStr ^ {map-class->string N} ^ "_" ^ MStr ^ {map-class->string N1})} Forget1, + ForgetF = (ui\ a\ b\ r\ ForgetF' ui a b (app [pglobal Forget1 ui, a, b, r])). +forget (pc M N) (pc M' N') ForgetF :- + std.mem {map-class.weakenings-from M} M1, + forget (pc M1 N) (pc M' N') ForgetF', !, + map-class->string N NStr, + coq.locate + {calc ("forget_" ^ {map-class->string M} ^ NStr ^ "_" ^ {map-class->string M1} ^ NStr)} Forget1, + ForgetF = (ui\ a\ b\ r\ ForgetF' ui a b (app [pglobal Forget1 ui, a, b, r])). + +% succeed if the parametricity class contains a map class over 2b +% this means that a translation of a sort at this class will require univalence, +% and the translation of a dependent product will require funext +pred requires-axiom i:param-class. +requires-axiom (pc M N) :- (std.mem! [map2b, map3, map4] M ; std.mem! [map2b, map3, map4] N). + +} % param-class diff --git a/elpi/param.elpi b/elpi/param.elpi new file mode 100644 index 0000000..9a9ef4e --- /dev/null +++ b/elpi/param.elpi @@ -0,0 +1,261 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% parametricity translation +% -------------------------------------------------------------------------------------------------- + +:before "subst-fun:fail" +coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs. + +% traversing a binder should give information for both typechecking and annotation +macro @annot-pi-decl N T F :- pi x\ [annot.adecl x N T, decl x N T] => F x. + +% param X T X' XR translates X at annotated type T, to X' with witness XR +pred param i:term, i:term, o:term, o:term. + +% locally remember the translation of bound variables +pred param.store o:term, o:term, o:term, o:term. + +% used in order not to typecheck+annotate twice the same term +pred fresh-type. + +% ================================================================================================== + +% ParamSub + ParamConst +param (global GR) T' (global GR') GrefR :- !, + util.when-debug dbg.steps (coq.say "param/const" GR "@" T'), + if (fresh-type) ( + % T' already comes from a call to annot.typecheck in the case for app + % subtyping will be handled there + cstr.dep-gref GR T' GR' GRR, + GrefR = global GRR + ) ( + annot.typecheck (global GR) T, + annot.sub-type T T', + cstr.dep-gref GR T GR' GRR, + weakening T T' (wfun W), + GrefR = (W (global GRR)) + ). + +param (pglobal GR UI) T' (pglobal GR' UI) GrefR :- !, + util.when-debug dbg.steps (coq.say "param/const" GR "@" T'), + if (fresh-type) ( + % T' already comes from a call to annot.typecheck in the case for app + % subtyping will be handled there + cstr.dep-gref GR T' GR' GRR, + GrefR = pglobal GRR UI + ) ( + annot.typecheck (pglobal GR UI) T, + annot.sub-type T T', + cstr.dep-gref GR T GR' GRR, + weakening T T' (wfun W), + GrefR = (W (pglobal GRR UI)) + ). + +% ParamSub + ParamVar +param X T' X' (W XR) :- name X, !, + util.when-debug dbg.steps (coq.say "param/var" X "@" T'), + param.store X T X' XR, + util.when-debug dbg.steps (coq.say "param/var: found" X "@" T "~" X' "by" XR), + annot.sub-type T T', + weakening T T' (wfun W). + +% ParamUniv +param + (app [pglobal (const PType) UI, MR, NR] as Type) (app [pglobal (const PType) _, M, N]) + Type (app [pglobal (const PParamType) UI1|Args]) :- param.db.ptype 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), + cstr.univ-link C M N, + util.when-debug dbg.full (coq.say "param/type:" M N "is linked to" C), + cstr.dep-type C CR, + util.when-debug dbg.full (coq.say "param/type: added dep-type from" C "to" CR), + coq.univ-instance UI [L], + coq.univ.variable U L, + coq.univ-instance UI1 [L, {coq.univ.variable {coq.univ.super U}}], % {coq.univ.new} + param.db.pparam-type C PParamType, + util.when-debug dbg.full (coq.say "param/type: suspending proof on" C), + util.if-suspend C (param-class.requires-axiom C) ( + util.when-debug dbg.full (coq.say "param/type: resuming proof on" C "(univalence needed)"), + coq.univ-instance UI0 [], + Args = [MR, NR, pglobal (const {param.db.univalence}) UI0] + ) ( + util.when-debug dbg.full + (coq.say "param/type: resuming proof on" C "(univalence not needed)"), + Args = [MR, NR] + ) + ]. + +% ParamLam +param (fun N T F) FunTy (fun N' T' F') FunR :- !, + util.when-debug dbg.steps (coq.say "param/fun" N ":" T "@" FunTy), + std.assert-ok! (coq.unify-eq FunTy (prod _ T TF)) {std.string.concat " " + ["type not convertible to Π:", {coq.term->string FunTy}]}, + coq.name-suffix N "'" N', + coq.name-suffix N "R" NR, + map-class->term map0 Map0, + param T (app [pglobal (const {param.db.ptype}) _, Map0, Map0]) T' TR, + util.when-debug dbg.full (coq.say "param/fun:" T "@ 0,0 ~" T' "by" TR), + @annot-pi-decl N T x\ pi x' xR\ param.store x T x' xR => ( + util.when-debug dbg.full (coq.say "param/fun: introducing" x "@" T "~" x' "by" xR), + param (F x) (TF x) (F' x') (FR x x' xR), + util.when-debug dbg.full (coq.say "param/fun:" (F x) "@" (TF x) "~" (F' x') "by" (FR x x' xR)) + ), + param.db.r (pc map0 map0) R, + prune UI [], + FunR = + fun N T x\ fun N' T' x'\ fun NR (app [pglobal (const R) UI, T, T', TR, x, x']) xR\ FR x x' xR. + +% ParamArrow +param + (prod _ A (_\ B)) (app [pglobal (const PType) _, M, N]) + (prod `_` A' (_\ B')) (app [pglobal (const ParamArrow) UI|Args]) :- + param.db.ptype PType, !, std.do! [ + util.when-debug dbg.steps (coq.say "param/arrow" A "->" B "@" 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, + util.when-debug dbg.full (coq.say "param/arrow: added dep-arrow from" C "to" CA "and" CB), + 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, + 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, + util.when-debug dbg.full (coq.say "param/arrow:" B "@" MB NB "~" B' "by" BR), + coq.say "before db param-arrow" C, + param.db.param-arrow C ParamArrow, + coq.say UI, + prune UI [], + util.when-debug dbg.full (coq.say "param/arrow: suspending proof on" C), + util.if-suspend C (param-class.requires-axiom C) ( + util.when-debug dbg.full (coq.say "param/arrow: resuming proof on" C "(funext needed)"), + coq.univ-instance UI0 [], + Args = [pglobal (const {param.db.funext}) UI0, A, A', AR, B, B', BR] + ) ( + util.when-debug dbg.full (coq.say "param/arrow: resuming proof on" C "(funext not needed)"), + Args = [A, A', AR, B, B', BR] + ) + ]. + +% ParamPi +param + (prod N A B) (app [pglobal (const PType) _, M1, M2]) + (prod N' A' B') (app [pglobal (const ParamForall) UI|Args']) :- param.db.ptype PType, !, + 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, + cstr.univ-link C M1 M2, + util.when-debug dbg.full (coq.say "param/forall:" M1 M2 "is linked to" C), + cstr.dep-pi C CA CB, + 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, + 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 => ( + 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)) + ), + param.db.r CA RA, + prune UIA [], + Args = + [ A, A', AR, fun N A B, fun N' A' B', + fun N A a\ fun N' A' a'\ fun NR (app [pglobal (const RA) UIA, A, A', AR, a, a']) aR\ + BR a a' aR ], + param.db.param-forall C ParamForall, + prune UI [], + util.when-debug dbg.full (coq.say "param/forall: suspending proof on" C), + util.if-suspend C (param-class.requires-axiom C) ( + util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext needed)"), + coq.univ-instance UI0 [], + Args' = [pglobal (const {param.db.funext}) UI0|Args] + ) ( + util.when-debug dbg.full (coq.say "param/forall: resuming proof on" C "(funext not needed)"), + Args' = Args + ). + +% ParamSub for F (argument B in param.args) + ParamApp +param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- !, + util.when-debug dbg.steps (coq.say "param/app" F Xs "@" B), + annot.typecheck F FTy, + fresh-type => param F FTy F' FR, + util.when-debug dbg.full (coq.say "param/app:" F "@" FTy "~" F' "by" FR), + param.args FTy B Xs Xs' XsR W, + coq.subst-fun XsR FR AppR. + +pred param.args i:term, i:term, i:list term, o:list term, o:list term, o:term -> term. +param.args T B [] [] [] W :- !, + annot.sub-type T B, + weakening T B (wfun W). +param.args FunTy B [X|Xs] [X'|Xs'] [X, X', XR|XsR] W :- + std.assert-ok! (coq.unify-eq FunTy (prod _ T TF)) {std.string.concat " " + ["type not convertible to Π:", {coq.term->string FunTy}]}, + param X T X' XR, + param.args (TF X) B Xs Xs' XsR W. + +param X T _ _ :- + coq.error "unsupported combination:" X "&" T. + +% ================================================================================================== + +% ad hoc inductive type to represent the suspension in the definition of weakening, see the article +kind weakening type. +type wfun (term -> term) -> weakening. +type wsuspend (term -> term) -> (term -> term) -> weakening. + +% generate the weakening function from a type to a sub-type +pred weakening i:term, i:term, o:weakening. +weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :- + param.db.ptype PType, !, + param.db.weaken Weaken, + prune UI [], + prune Ty [], + % as M, N, M', N' are not known yet, we put a Coq placeholder (see Weaken in Param.v) + W = wfun (xR\ app [pglobal (const Weaken) UI, M, N, M', N', Ty, xR]). +weakening (prod N A B) (prod _ A' B') W :- !, + coq.name-suffix N "'" N', + coq.name-suffix N "R" NR, + weakening A' A (wfun WA), + pi xR a a' aR\ + weakening (B a) (B' a') (wfun (WB a a')), + prune AR [], + prune A2 [], + W = wfun (xR\ fun N A a\ fun N' A2 a'\ fun NR AR aR\ WB a a' (app [xR, a, a', WA aR])). +weakening (app [F|_]) (app [_F'|_]) (wfun (xR\ xR)) :- (name F ; F = global _ ; F = pglobal _ _), !. +weakening (app [F, X|Xs]) (app [F', X'|Xs']) W :- !, + weakening F F' (wsuspend WF WF'), + weakening {coq.mk-app (WF X) Xs} {coq.mk-app (WF' X') Xs'} W. +weakening (fun _ _ F) (fun _ _ F') (wsuspend F F') :- !. +weakening X _ (wfun (xR\ xR)) :- (name X ; X = global _ ; X = pglobal _ _), !. +weakening T _ _ :- coq.error "weakening:" T. + +% replace Weaken placeholders with real weakening functions +pred param.subst-weaken i:term, o:term. +param.subst-weaken T T' :- + param.db.weaken Weaken, + (pi XR XR'\ copy (app [pglobal (const Weaken) _, _, _, _, _, _, _] as XR) XR' :- !, + copy.subst-weaken XR XR') + => copy T T'. +pred copy.subst-weaken i:term, o:term. +copy.subst-weaken (app [_, M, N, M', N', _, XR]) XR'' :- + param-class.forget + (pc {term->map-class M} {term->map-class N}) + (pc {term->map-class M'} {term->map-class N'}) + WeakenF, + copy XR XR', + XR'' = WeakenF _ _ _ XR'. diff --git a/elpi/util.elpi b/elpi/util.elpi new file mode 100644 index 0000000..6eee5b8 --- /dev/null +++ b/elpi/util.elpi @@ -0,0 +1,83 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 the % +% |_| % GNU Lesser General Public License Version 3 % +% % (see LICENSE file for the text of the license) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% -------------------------------------------------------------------------------------------------- +% utility predicates +% -------------------------------------------------------------------------------------------------- + +kind or type -> type -> type. +type inl A -> or A B. +type inr B -> or A B. + +kind debug-level type. +type dbg.none debug-level. +type dbg.steps debug-level. +type dbg.full debug-level. + +pred debug-level->int i:debug-level, o:int. +debug-level->int dbg.none 0. +debug-level->int dbg.steps 1. +debug-level->int dbg.full 2. + +pred debug o:debug-level. + +namespace util { + +pred option.value i:option A, i:A, o:A. +option.value none Default Default. +option.value (some A) _ A. + +pred cmp-int i:int, i:int, o:cmp. +cmp-int A B lt :- A < B, !. +cmp-int A B eq :- A = B, !. +cmp-int _ _ gt. + +pred when i:prop, i:prop. +when Condition Goal :- + if (Condition) Goal true. + +pred when-debug i:debug-level, i:prop. +when-debug L Log :- debug D, !, + when ({debug-level->int D} >= {debug-level->int L}) Log. +when-debug _ _. + +pred unless i:prop, i:prop. +unless Condition Goal :- + if (Condition) true Goal. + +pred if-suspend i:A, i:prop, i:prop, i:prop. +if-suspend V B T E :- var V, !, declare_constraint (if B T E) [V]. +if-suspend _ B T E :- if B T E. + +pred map.find-opt i:A, i:std.map A B, o:option B. +map.find-opt K M (some V) :- std.map.find K M V, !. +map.find-opt _ _ none. + +pred map.update i:A, i:(option B -> option B -> prop), i:std.map A B, o:std.map A B. +map.update K F M M' :- + map.find-opt K M (some V), !, + F (some V) OV', + if (OV' = some V') + (std.map.add K V' M M') % replace + (std.map.remove K M M'). % remove +map.update K F M M' :- + F none (some V'), + std.map.add K V' M M'. % add +map.update _ _ M M. % no-op + +pred delete i:A, i:list A, o:list A. +delete A [A|Xs] Xs :- !. +delete A [X|Xs] [X|Xs'] :- delete A Xs Xs'. +delete _ [] []. + +} % util diff --git a/examples/Example.v b/examples/Example.v new file mode 100644 index 0000000..e20ba17 --- /dev/null +++ b/examples/Example.v @@ -0,0 +1,55 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. + +Set Universe Polymorphism. + +(* Example file on CCω *) +(* 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. + +Param Register Univalence u. +Param Register Funext f. + +Goal + (* Type@{i}. *) + (* Type@{i} -> Type@{i}. *) + (* forall (A : Type@{i}), 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} -> 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. *) + (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}), F A -> forall (B : Type@{i}), F B -> F A. *) + (* forall (A : Type@{i}) (F : A -> Type@{i}) (a : A), F a. *) + (* forall (A : Type@{i}) (F : A -> Type@{i}) (a : A), F a -> F a. *) + (* forall (F : Type@{i} -> Type@{i}) (A : Type@{i}) (H : F A -> Type@{i}) (J : F A), H J. *) + (* forall (F : Type@{i} -> Type@{i}) (A B : Type@{i}) (H : F A -> F B) (J : F A) (K : F B -> Type), K (H J). *) + (* forall + (F : Type@{i} -> Type@{i}) (A : Type@{i}) (H : F A), + F A -> forall (B : Type@{i}) (J : F A -> F B), (forall (K : F B -> Type@{i}), K (J H)) -> + F B -> F A. *) + (* forall (X : forall (A : Type@{i}), A -> Type@{i}) (A : Type@{i}) (a : A), A -> X A a -> A. *) + (* forall (T : (Type@{i} -> Type@{j})) (F : ((Type@{i} -> Type@{j}) -> Type@{k})), F T. *) +Proof. + param. +Abort. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v new file mode 100644 index 0000000..fe8153d --- /dev/null +++ b/examples/int_to_Zp.v @@ -0,0 +1,348 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. + +Set Universe Polymorphism. + +Axiom cheat : forall A, A. +Ltac cheat := apply cheat. + +(* what it can do *) +(* Section Test. *) +Declare Scope int_scope. +Delimit Scope int_scope with int. +Declare Scope Zp_scope. +Delimit Scope Zp_scope with Zp. + +Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int). +Axiom (eqmodp : int -> int -> Type). +Axiom (Zp : Type) (zerop : Zp) (addp : Zp -> Zp -> Zp). + +Context (eqp_refl : Reflexive eqmodp). +Context (eqp_sym : Symmetric eqmodp). +Context (eqp_trans : Transitive eqmodp). +(* Existing Instance eqp_refl. *) +(* Existing Instance eqp_trans. *) + +Context (pmap : Zp -> int) (pcomap : int -> Zp) + (pmapK : forall x, pcomap (pmap x) = x). +Definition Rp x n := pmap x = n. + +Lemma pcomapP :forall (a : int) (b : Zp), sym_rel Rp a b -> pcomap a = b. +Proof. by move=> a b <-; exact: pmapK. Qed. + +Definition Rp42b@{i} : Param42b.Rel Zp@{i} int@{i} := Param42b.BuildRel Zp int Rp + (Map4.BuildHas pmap (fun _ _ => id) (fun _ _ => id) (fun _ _ _ => idpath)) + (Map2b.BuildHas _ _ (sym_rel Rp) pcomap pcomapP). + +Definition Rp00 : Param00.Rel Zp int := Rp42b. +Definition Rp01 : Param01.Rel Zp int := Rp42b. +Definition Rp40 : Param40.Rel Zp int := Rp42b. +Definition Rp10 : Param10.Rel Zp int := Rp42b. +Definition Rp02b : Param02b.Rel Zp int := Rp42b. +Definition Rp2b0 : Param2b0.Rel Zp int := Rp42b. +Definition Rp2a0 : Param2a0.Rel Zp int := Rp42b. + +Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ + (f : X -> Y -> Z) (g : X' -> Y' -> Z') := + forall x x', RX x x' -> forall y y', RY y y' -> RZ (f x y) (g x' y'). + +Variable addp_to_add : binop_param Rp Rp Rp addp add. +Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. + +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%Zp y%Zp) : Zp_scope. + +Definition Radd : forall x x' (xR : Rp x x') y y' (yR : Rp y y'), Rp (x + y)%Zp (x' + y')%int. +Proof. apply addp_to_add. Qed. + +Check Param01_paths. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map4 map0) [] {{:gref int}} {{:gref Rp40}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map0 map0) [] {{:gref int}} {{:gref Rp00}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map0 map1) [] {{:gref int}} {{:gref Rp01}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map1 map0) [] {{:gref int}} {{:gref Rp10}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map0 map2b) [] {{:gref int}} {{:gref Rp02b}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map2b map0) [] {{:gref int}} {{:gref Rp2b0}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map2a map0) [] {{:gref int}} {{:gref Rp2a0}})), + + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref paths}} (pc map0 map1) + [pc map0 map2b] + {{:gref paths}} {{:gref Param01_paths}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref paths}} (pc map1 map0) + [pc map2b map0] + {{:gref paths}} {{:gref Param10_paths}})), + + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref addp}} (pc map0 map0) [] {{:gref add}} {{:gref Radd}})). +}}. + +Axiom u : Univalence. +Axiom f : Funext. + +Param Register Univalence u. +Param Register Funext f. + +Goal + (* Zp@{i}. *) + (* Zp@{i} -> Zp@{i}. *) + (* forall (P : Zp -> Type) (x : Zp), P x. *) + (* forall (P : Zp -> Type) (x : Zp), P x -> P x. *) + (* forall (P : Zp -> Zp -> Type) (x y : Zp), P x y -> P y x. *) + (* forall (P : Zp -> Type) (x : Zp), P x -> forall (y : Zp), P y. *) + (* forall (P : Zp -> Type) (x : Zp), P x -> forall (y : Zp), P y -> P x. *) + (* forall (A : Type) (f : Zp -> A) (P : A -> Type) (x : Zp), P (f x). *) + (* forall (A : Type) (f : Zp -> A) (P : A -> Type) (x : Zp) (H : forall a, P a -> Type) (J : P (f x)), H (f x) J. *) + + (forall x y, x + y = y + x)%Zp. + + (* forall (X : forall (A : Type@{i}), A -> Type@{i}) (x : Zp), Zp -> X Zp x -> Zp. *) +Proof. + param. +Abort. + +Goal (forall x y, x + y = y + x)%int -> + (forall x y z, x + y + z = y + x + z)%Zp. +Proof. + intros addC x y z. + suff addpC: forall x y, (x + y = y + x)%Zp. { + by rewrite (addpC x y). } + param. + exact addC. +Qed. + +Inductive unit@{i} : Type@{i} := tt : unit. + +Module Seq. + Inductive t@{i} (A : Type@{i}) := + | snil : t A + | scons : A -> (unit@{i} -> t A) -> t A. + Arguments snil {_}. + Arguments scons {_} _ _. + + Fixpoint all@{i} {A : Type@{i}} (P : A -> Type@{i}) (s : t A) : Type@{i} := + match s with + | snil => unit@{i} + | scons a s' => P a * all P (s' tt) + end. + + Fixpoint sum@{i} (s : t Zp) : Zp := + match s with + | snil => zerop@{i} + | scons x s' => (x + sum (s' tt))%Zp + end. +End Seq. + +Fixpoint all@{i} {A : Type@{i}} (P : A -> Type@{i}) (l : list A) : Type@{i} := + match l with + | nil => unit@{i} + | cons a l' => P a * all P l' + end. + +Definition sum@{i} (l : list@{i} int) : int := List.fold_left@{i i} _ _ add@{i} l zero. + +Inductive Rseq@{i} + (A A' : Type@{i}) (AR : A -> A' -> Type@{i}) : Seq.t@{i} A -> list@{i} A' -> Type@{i} := + | Rnil : Rseq A A' AR Seq.snil nil + | Rcons : forall a a' (aR : AR a a') s l (r : Rseq A A' AR s l), + Rseq A A' AR (Seq.scons a (fun _ => s)) (cons a' l). + +Fixpoint map_seq@{i} (A A' : Type@{i}) (AR : Param10.Rel A A') (s : Seq.t@{i} A) : list@{i} A' := + match s with + | Seq.snil => nil + | Seq.scons a s' => cons (map AR a) (map_seq A A' AR (s' tt)) + end. + +Definition Param2a0_seq_list@{i} (A A' : Type@{i}) (AR : Param2a0.Rel A A') : + Param2a0.Rel (Seq.t A) (list A'). +Proof. + unshelve econstructor. + - exact (Rseq A A' AR). + - apply cheat@{i}. + - apply cheat@{i}. +Defined. + +Definition Param02b_seq_list@{i} (A A' : Type@{i}) (AR : Param02b.Rel A A') : + Param02b.Rel (Seq.t A) (list A'). +Proof. + unshelve econstructor. + - exact (Rseq A A' AR). + - apply cheat@{i}. + - apply cheat@{i}. +Defined. + +Definition Param44_seq_list@{i} (A A' : Type@{i}) (AR : Param44.Rel A A') : + Param44.Rel (Seq.t A) (list A'). +Proof. + unshelve econstructor. + - exact (Rseq A A' AR). + - apply cheat@{i}. + - apply cheat@{i}. +Defined. + +(* Definition Param01_seq_list@{i} : + forall (A A' : Type@{i}) (AR : Param01.Rel A A'), Param01.Rel (Seq.t A) (list A'). +Proof. + intros A A' AR. + unshelve econstructor. + - exact (Rseq A A' AR). + - constructor. + - cheat. +Defined. *) + +Fixpoint Rall01@{i} + (A A' : Type@{i}) (AR : Param00.Rel A A') + (P : A -> Type@{i}) (P' : A' -> Type@{i}) + (PR : forall a a' (aR : AR a a'), Param01.Rel (P a) (P' a')) + (s : Seq.t A) (l : list A') (slR : Rseq A A' AR s l) : + Param01.Rel (Seq.all P s) (all P' l). +Proof. + unshelve econstructor. + - destruct slR. + + simpl. exact (fun _ _ => unit@{i}). + + simpl. intros (pa, ps) (pa', pl). + exact (PR a a' aR pa pa' * Rall01 A A' AR P P' PR s l slR ps pl). + - constructor. + - unshelve econstructor. + destruct slR. + + simpl. exact (fun u => u). + + simpl. intros (pa', pl). + exact (comap (PR a a' aR) pa', comap (Rall01 A A' AR P P' PR s l slR) pl). +Defined. + +Fixpoint Rall10@{i} + (A A' : Type@{i}) (AR : Param00.Rel A A') + (P : A -> Type@{i}) (P' : A' -> Type@{i}) + (PR : forall a a' (aR : AR a a'), Param10.Rel (P a) (P' a')) + (s : Seq.t A) (l : list A') (slR : Rseq A A' AR s l) : + Param10.Rel (Seq.all P s) (all P' l). +Proof. + unshelve econstructor. + - destruct slR. + + simpl. exact (fun _ _ => unit@{i}). + + simpl. intros (pa, ps) (pa', pl). + exact (PR a a' aR pa pa' * Rall10 A A' AR P P' PR s l slR ps pl). + - unshelve econstructor. + destruct slR. + + simpl. exact (fun u => u). + + simpl. intros (pa, ps). + exact (map (PR a a' aR) pa, map (Rall10 A A' AR P P' PR s l slR) ps). + - constructor. +Defined. + +Definition Rsum : + forall (s : Seq.t Zp) (l : list int) (slR : Rseq Zp int Rp00 s l), + Rp00 (Seq.sum s) (sum l). +Admitted. + +Axiom Rzero : Rp zerop zero. + +Definition Rp02a : Param02a.Rel Zp int. +Proof. + unshelve econstructor. + - exact Rp. + - constructor. + - cheat. +Defined. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Zp}} (pc map0 map2a) [] {{:gref int}} {{:gref Rp02a}})), + + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.t}} (pc map2a map0) + [pc map2a map0] + {{:gref list}} {{:gref Param2a0_seq_list}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.t}} (pc map4 map4) + [pc map4 map4] + {{:gref list}} {{:gref Param44_seq_list}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.t}} (pc map0 map2b) + [pc map0 map2b] + {{:gref list}} {{:gref Param02b_seq_list}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.all}} (pc map0 map1) + [pc map0 map0, pc map0 map1] + {{:gref all}} {{:gref Rall01}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.all}} (pc map1 map0) + [pc map0 map0, pc map1 map0] + {{:gref all}} {{:gref Rall10}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref Seq.snil}} (pc map0 map0) + [pc map0 map0] + {{:gref nil}} {{:gref Rnil}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref zerop}} (pc map0 map0) [] {{:gref zero}} {{:gref Rzero}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Seq.sum}} (pc map0 map0) [] {{:gref sum}} {{:gref Rsum}})). +}}. + +Goal + (* forall (s : Seq.t Zp), s = s. *) + (* Seq.all (fun x : Zp => Zp) Seq.snil. *) + (* forall (s : Seq.t Zp), Seq.all (fun x : Zp => Zp) s. *) + (* forall (P : Zp -> Type), Seq.all P Seq.snil. *) + (* forall (P : Zp -> Type) (s : Seq.t Zp), Seq.all P s. *) + forall (F : (Type@{i} -> Type@{i}) -> Type@{i}), F Seq.t. + (* forall (P : Zp -> Type) (s : Seq.t Zp), + (forall x, P x -> x = zerop) -> Seq.all P s -> Seq.sum s = zerop. *) +Proof. + param. +Abort. diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v new file mode 100644 index 0000000..7b83b5e --- /dev/null +++ b/examples/peano_bin_nat.v @@ -0,0 +1,191 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. + +Set Universe Polymorphism. + +(* definition of binary natural numbers *) + +Inductive positive : Set := + | xI : positive -> positive + | xO : positive -> positive + | xH : positive. + +Declare Scope positive_scope. +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with positive. + +Notation "1" := xH : positive_scope. +Notation "p ~ 1" := (xI p) + (at level 7, left associativity, format "p '~' '1'") : positive_scope. +Notation "p ~ 0" := (xO p) + (at level 7, left associativity, format "p '~' '0'") : positive_scope. + +Module Pos. +Local Open Scope positive_scope. +Fixpoint succ x := + match x with + | p~1 => (succ p)~0 + | p~0 => p~1 + | 1 => 1~0 + end. + +Fixpoint map (x : positive) : nat := + match x with + | p~1 => 1 + (map p + map p) + | p~0 => map p + map p + | 1 => 1 + end. + +Fixpoint add (x y : positive) : positive := + match x, y with + | 1, p | p, 1 => succ p + | p~0, q~0 => (add p q)~0 + | p~0, q~1 | p~1, q~0 => (add p q)~1 + | p~1, q~1 => succ (add p q)~1 + end. +Infix "+" := add : positive_scope. +Notation "p .+1" := (succ p) : positive_scope. + +Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Qed. +Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Qed. +Lemma addpS x y : x + y.+1 = (x + y).+1. +Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Qed. +Lemma addSp x y : x.+1 + y = (x + y).+1. +Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Qed. + +End Pos. +Infix "+" := Pos.add : positive_scope. +Notation "p .+1" := (Pos.succ p) : positive_scope. + +Inductive N : Set := + | N0 : N + | Npos : positive -> N. + +Declare Scope N_scope. +Delimit Scope N_scope with N. +Bind Scope N_scope with N. + +Notation "0" := N0 : N_scope. + +Definition succ_pos (n : N) : positive := + match n with + | N0 => 1%positive + | Npos p => Pos.succ p + end. + +Definition Nsucc (n : N) := Npos (succ_pos n). + +Definition Nadd (m n : N) := match m, n with +| N0, x | x, N0 => x +| Npos p, Npos q => Npos (Pos.add p q) +end. +Infix "+" := Nadd : N_scope. +Notation "n .+1" := (Nsucc n) : N_scope. + +(* various possible proofs to fill the fields of a parametricity witness between N and nat *) + +Definition Nmap (n : N) : nat := + match n with + | N0 => 0 + | Npos p => Pos.map p + end. + +Fixpoint Ncomap (n : nat) : N := + match n with O => 0 | S n => Nsucc (Ncomap n) end. + +Definition RN@{} (m : N) (n : nat) := paths@{Set} (Ncomap n) m. + +Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. +Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed. + +Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N. +Proof. +elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. +rewrite -nat_add_n_Sm/= IHi. +case: (Ncomap i) => // p; case: (Ncomap j) => //=. +- by rewrite /Nsucc/= Pos.addp1. +- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp. +Qed. + +Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0. +Proof. by move=> kp; rewrite NcomapD kp Naddpp. Qed. + +Lemma NmapK (n : N) : Ncomap (Nmap n) = n. +Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed. + +Lemma Nmap_in_R@{} (m : N) (n : nat) : + paths@{Set} (Nmap m) n -> sym_rel@{Set} RN n m. +Proof. by move<-; apply: NmapK. Qed. + +(* the best we can do to link these types is (2a,3) *) + +Definition RN2a3@{} : Param2a3.Rel@{Set} N nat := @Param2a3.BuildRel@{Set} N nat RN@{} + (@Map2a.BuildHas@{Set} _ _ _ Nmap Nmap_in_R) + (@Map3.BuildHas@{Set} _ _ _ Ncomap (fun _ _ p => p) (fun _ _ p => p)). + +(* for brevity, we create witnesses at lower classes by forgetting fields in RN2a3 *) +(* this behaviour can be automated so as to only declare Rn2a3 and get for free all the instances + reachable by forgetting fields *) +(* in the general case, if a field requires an axiom, it is better to manually recreate instances + that do not need this field, so that it is not imported before forgetting, and the lower + instances can be declared without the axiom *) + +Definition RN02b : Param02b.Rel N nat := RN2a3. +Definition RN02a : Param02a.Rel N nat := RN2a3. +Definition RN2a0 : Param2a0.Rel N nat := RN2a3. + +(* as 0 and Nsucc appear in the goal, we need to link them with nat constructors *) +(* NB: as these are not type formers, only class (0,0) is required, so these proofs amount to what + would be done in the context of raw parametricity *) + +Definition RN0 : RN N0 0. Proof. done. Qed. +Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n). +Proof. by move=> _ + <-; case=> //=. Qed. + +Elpi Query param lp:{{ + % register Param N nat + % as said higher, with some automation this can be turned into only one declaration + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref N}} (pc map0 map2b) [] {{:gref nat}} {{:gref RN02b}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref N}} (pc map0 map2a) [] {{:gref nat}} {{:gref RN02a}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref N}} (pc map2a map0) [] {{:gref nat}} {{:gref RN2a0}})), + % register the constants + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref N0}} (pc map0 map0) [] {{:gref O}} {{:gref RN0}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref Nsucc}} (pc map0 map0) [] {{:gref S}} {{:gref RNS}})). +}}. + +Lemma N_Srec : forall (P : N -> Type), P N0 -> + (forall n, P n -> P (Nsucc n)) -> forall n, P n. +Proof. + param. + (* the output sort of P' is (1,1) because of the covariant and contravariant occurrences of P in + the input goal; this annotation was made to be definitionally equal to Type: from there, + the induction principle of nat can be applied directly *) + exact nat_rect. +Defined. + +Print N_Srec. +Print Assumptions N_Srec. \ No newline at end of file diff --git a/examples/setoid_rewrite.v b/examples/setoid_rewrite.v new file mode 100644 index 0000000..295e475 --- /dev/null +++ b/examples/setoid_rewrite.v @@ -0,0 +1,42 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import Prelude. +From Coq Require Import Setoid Morphisms. + +(* what it can do *) +Section Test. +Declare Scope int_scope. +Delimit Scope int_scope with int. +Context (int : Set) (zero : int) (add : int -> int -> int). +Context (eqmodp : int -> int -> Prop). +Hypothesis eqmodp_equiv : Equivalence eqmodp. +Existing Instance eqmodp_equiv. + +Hypothesis add_proper : Proper (eqmodp ==> eqmodp ==> eqmodp) add. +Existing Instance add_proper. + +Notation "x == y" := (eqmodp x y) (format "x == y", at level 70) : int_scope. +Notation "x + y" := (add x%int y%int) : int_scope. + +Goal (forall x y : int, x + y == y + x)%int -> + forall x y z, (x + y + z == y + x + z)%int. +Proof. +intros addC x y z. +rewrite (addC x y). +reflexivity. +Qed. + +End Test. + +(* what it cannot do : handle heterogenous relations *) diff --git a/examples/summable.v b/examples/summable.v new file mode 100644 index 0000000..c2422be --- /dev/null +++ b/examples/summable.v @@ -0,0 +1,246 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. + +Set Universe Polymorphism. + +(* first, we axiomatise non negative reals *) + +Axiom (nnreal : Type). +Declare Scope nnreal_scope. +Delimit Scope nnreal_scope with nnreal. +Bind Scope nnreal_scope with nnreal. + +Axiom (nnreal_zero : nnreal). +Axiom (nnreal_add : nnreal -> nnreal -> nnreal). +Notation "x + y" := (nnreal_add x%nnreal y%nnreal) : nnreal_scope. + +(* the extension is just defined as adding a constructor for infinite reals *) + +Inductive xnnreal : Type := + | Fin : nnreal -> xnnreal + | Inf : xnnreal. + +Declare Scope xnnreal_scope. +Delimit Scope xnnreal_scope with xnnreal. +Bind Scope xnnreal_scope with xnnreal. + +Definition xnnreal_add (re1 re2 : xnnreal) : xnnreal := + match re1, re2 with + | Fin r1, Fin r2 => Fin (r1 + r2)%nnreal + | _, _ => Inf + end. +Notation "x + y" := (xnnreal_add x%xnnreal y%xnnreal) : xnnreal_scope. + +Definition xnnreal_seq := nat -> xnnreal. +Identity Coercion xnnreal_seq_id : xnnreal_seq >-> Funclass. +Declare Scope xnnreal_seq_scope. +Delimit Scope xnnreal_seq_scope with xnnreal_seq. +Bind Scope xnnreal_seq_scope with xnnreal_seq. + +Definition add_xnnreal_seq (u v : xnnreal_seq) : xnnreal_seq := + fun n => (u n + v n)%xnnreal. +Infix "+" := add_xnnreal_seq : xnnreal_seq_scope. + +Definition nnreal_seq := nat -> nnreal. +Identity Coercion nnreal_seq_id : nnreal_seq >-> Funclass. + +(* here we axiomatise the sequence sum and the distributivity lemma *) +(* TODO: expliquer pourquoi? *) + +Axiom (xnnreal_sum : xnnreal_seq -> xnnreal). +Notation "'Σ' ue" := (xnnreal_sum ue) (at level 35) : xnnreal_scope. + +Axiom xnnreal_sumD : + forall u v : xnnreal_seq, (Σ (u + v))%xnnreal = (Σ u + Σ v)%xnnreal. + +(* the explicit cast functions between both types are a trivial extension and a truncation + yielding a default value in the case of infinity *) + +Definition extend (r : nnreal) : xnnreal := Fin r. + +Definition truncate (re : xnnreal) : nnreal := + match re with + | Inf => nnreal_zero + | Fin r => r + end. + +Definition is_finite (re : xnnreal) : Bool := + match re with Inf => false | Fin _ => true end. + +Definition cv_sum (u : nnreal_seq) := is_finite + (Σ (Fin o u))%xnnreal. + +(* TODO: expliquer cet encodage? *) + +Record nnreal_cv_seq := { + cv_to_nnreal_seq :> nnreal_seq; + nnreal_cv_seq_finite_sum : cv_sum cv_to_nnreal_seq = true +}. +Declare Scope nnreal_cv_seq_scope. +Delimit Scope nnreal_cv_seq_scope with nnreal_cv_seq. +Bind Scope nnreal_cv_seq_scope with nnreal_cv_seq. + +Axiom add_nnreal_seq_cv : + forall u v : nnreal_cv_seq, cv_sum (fun n => u n + v n)%nnreal = true. + +Definition add_nnreal_cv_seq (u v : nnreal_cv_seq) := + Build_nnreal_cv_seq _ (add_nnreal_seq_cv u v). +Infix "+" := add_nnreal_cv_seq : nnreal_cv_seq_scope. + +Definition nnreal_sum (u : nnreal_cv_seq) : nnreal := + truncate (xnnreal_sum (Fin o u)). +Notation "'Σ' u" := (nnreal_sum u) (at level 35) : nnreal_scope. + +(* various proofs to be used as fields of the parametricity witness *) + +Definition R_nnreal (r : nnreal) (re : xnnreal) : Type := extend r = re. + +Definition truncate_extend : forall (r : nnreal), truncate (extend r) = r. +Proof. reflexivity. Defined. + +(* in this way, the composition is an identity only conditionally *) +(* this is why truncate_in_R_nnreal is not provable and the maximum provable class is (4,2b) *) +Definition extend_truncate : + forall (re : xnnreal), is_finite re = true -> extend (truncate re) = re. +Proof. by case => //=; discriminate. Defined. + +Definition extend_in_R_nnreal (r : nnreal) (re : xnnreal) (e : extend r = re) : R_nnreal r re := e. +Definition R_in_extend_nnreal (r : nnreal) (re : xnnreal) (w : R_nnreal r re) : extend r = re := w. +Definition R_in_extendK_nnreal (r : nnreal) (re : xnnreal) (w : R_nnreal r re) : + extend_in_R_nnreal r re (R_in_extend_nnreal r re w) = w. +Proof. reflexivity. Defined. +Definition truncate_in_R_nnreal (r : nnreal) (re : xnnreal) (e : truncate re = r) : R_nnreal r re. +Proof. rewrite <- e; unfold R_nnreal. apply extend_truncate. Abort. +Definition R_in_truncate_nnreal (re : xnnreal) (r : nnreal) (w : R_nnreal r re) : truncate re = r. +Proof. rewrite <- w. apply truncate_extend. Defined. + +(* maximum witness between non negative reals and their extended version *) +Definition Param42b_nnreal : Param42b.Rel nnreal xnnreal. +Proof. + unshelve econstructor. + - exact R_nnreal. + - unshelve econstructor. + + exact extend. + + exact extend_in_R_nnreal. + + exact R_in_extend_nnreal. + + exact R_in_extendK_nnreal. + - unshelve econstructor. + + exact truncate. + + exact R_in_truncate_nnreal. +Defined. + +(* the only level we will need to pre-process the distributivity goal is (0,2b) *) +Definition Param02b_nnreal : Param02b.Rel nnreal xnnreal := Param42b_nnreal. + +(* as sequences are encoded with constants, we need to relate them *) + +Definition seq_extend (u : nnreal_cv_seq) : xnnreal_seq := + fun n => extend (u n). +Definition Rrseq (u : nnreal_cv_seq) (v : xnnreal_seq) : Type := + seq_extend u = v. +Definition extend_in_Rrseq + (r : nnreal_cv_seq) (re : xnnreal_seq) (e : seq_extend r = re) : Rrseq r re := e. +Definition R_in_extend_rseq + (r : nnreal_cv_seq) (re : xnnreal_seq) (w : Rrseq r re) : seq_extend r = re := w. +Definition R_in_extendK_rseq (r : nnreal_cv_seq) (re : xnnreal_seq) (w : Rrseq r re) : + extend_in_Rrseq r re (R_in_extend_rseq r re w) = w. +Proof. reflexivity. Defined. + +(* TODO: est-ce que (4,0) est le max ou on ne s'est simplement pas embêté? *) +Definition Param40_rseq : Param40.Rel nnreal_cv_seq xnnreal_seq. +Proof. + unshelve econstructor. + - exact Rrseq. + - unshelve econstructor. + + exact seq_extend. + + exact extend_in_Rrseq. + + exact R_in_extend_rseq. + + exact R_in_extendK_rseq. + - unshelve econstructor. +Defined. + +(* we will only need (2a,0) on sequences to pre-process the distributivity goal *) +Definition Param2a0_rseq : Param2a0.Rel _ _ := Param40_rseq. + +(* now we need to relate the various constants at level (0,0) *) + +Definition R_xnnreal_add : + forall (r1 : nnreal) (re1 : xnnreal), R_nnreal r1 re1 -> + forall (r2 : nnreal) (re2 : xnnreal), R_nnreal r2 re2 -> + R_nnreal (r1 + r2) (re1 + re2). +Proof. +rewrite /R_nnreal /extend. +move=> r1 [_ []|]; last by discriminate. +by move=> r2 [_ []|]; last by discriminate. +Qed. + +Definition R_nnreal_seq_add : + forall (r1 : nnreal_cv_seq) (re1 : xnnreal_seq), Rrseq r1 re1 -> + forall (r2 : nnreal_cv_seq) (re2 : xnnreal_seq), Rrseq r2 re2 -> + Rrseq (r1 + r2) (re1 + re2). +Proof. +move=> [r1 r1cv] re1 <-. +by move=> [r2 r2cv] re2 <-. +Qed. + +Definition R_xnnreal_sum : + forall (u : nnreal_cv_seq) (ue : xnnreal_seq), + Rrseq u ue -> R_nnreal (Σ u) (Σ ue). +Proof. +rewrite /Rrseq /seq_extend /R_nnreal /nnreal_sum. +move=> u _ <-; rewrite extend_truncate//. +by apply nnreal_cv_seq_finite_sum. +Qed. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref + {{:gref paths}} (pc map0 map1) + [pc map0 map2b] + {{:gref paths}} {{:gref Param01_paths}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref nnreal}} (pc map0 map2b) [] {{:gref xnnreal}} + {{:gref Param02b_nnreal}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref nnreal_cv_seq}} (pc map2a map0) [] {{:gref xnnreal_seq}} + {{:gref Param2a0_rseq}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref nnreal_sum}} (pc map0 map0) [] {{:gref xnnreal_sum}} + {{:gref R_xnnreal_sum}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref nnreal_add}} (pc map0 map0) [] {{:gref xnnreal_add}} + {{:gref R_xnnreal_add}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref add_nnreal_cv_seq}} (pc map0 map0) [] {{:gref add_xnnreal_seq}} + {{:gref R_nnreal_seq_add}})). +}}. + +(* we get a proof over non negative reals for free, + from the analogous proof over the extended ones *) +Lemma nnreal_cv_sumD : forall (u v : nnreal_cv_seq), (Σ (u + v) = Σ u + Σ v)%nnreal. +Proof. + param. + exact: xnnreal_sumD. +Qed. + +Print Assumptions nnreal_cv_sumD. diff --git a/examples/trocq_gen_rewrite.v b/examples/trocq_gen_rewrite.v new file mode 100644 index 0000000..08d9dca --- /dev/null +++ b/examples/trocq_gen_rewrite.v @@ -0,0 +1,88 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import HoTT_additions Hierarchy Param Param_paths. + +Set Universe PolymoRinthism. + +Axiom cheat : forall A, A. +Ltac cheat := apply cheat. + +Declare Scope int_scope. +Delimit Scope int_scope with int. + +Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int) (p : int). +Axiom (le@{i} : int@{i} -> int@{i} -> Type@{i}). +Notation "x + y" := (add x%int y%int) : int_scope. +Notation "x <= y" := (le x%int y%int) + (format "x <= y", at level 70) : int_scope. + +Context (le_refl : Reflexive le). +Context (le_trans : Transitive le). + +Variable add_morph : + forall m m' : int, (m <= m')%int -> + forall n n' : int, (n <= n')%int -> + (m + n <= m' + n')%int. + +Lemma le_morph : + forall m m' : int, (m <= m')%int -> + forall n n' : int, (n' <= n)%int -> + (m' <= n')%int -> (m <= n)%int. +Proof. +move=> m m' Rm n n' Rn Rmn. +exact (le_trans _ _ _ Rm (le_trans _ _ _ Rmn Rn)). +Qed. + +Lemma le01 : + forall m m' : int, (m <= m')%int -> + forall n n' : int, (n' <= n)%int -> + 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)). +- constructor. +- by constructor => mn; apply (le_morph _ _ Rm _ _ Rn). +Qed. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref le}} (pc map0 map1) [] {{:gref le}} {{:gref le01}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref add}} (pc map0 map0) [] {{:gref add}} {{:gref add_morph}})). +}}. + +Variables i j : int. +Variable ip : (j <= i)%int. +Definition iid : (i <= i)%int := le_refl i. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref j}} (pc map0 map0) [] {{:gref i}} {{:gref ip}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref i}} (pc map0 map0) [] {{:gref i}} {{:gref iid}})). +}}. + +Example ipi : (j + i + j <= i + i + i)%int. +Proof. +param. +apply le_refl. +Qed. +Print ipi. +Print Assumptions ipi. \ No newline at end of file diff --git a/examples/trocq_setoid_rewrite.v b/examples/trocq_setoid_rewrite.v new file mode 100644 index 0000000..11b5728 --- /dev/null +++ b/examples/trocq_setoid_rewrite.v @@ -0,0 +1,88 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import HoTT_additions Hierarchy Param Param_paths. + +Set Universe PolymoRinthism. + +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}). +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. + +Context (eqp_refl : Reflexive eqmodp). +Context (eqp_sym : Symmetric eqmodp). +Context (eqp_trans : Transitive eqmodp). + +Variable add_morph : + forall m m' : int, (m == m')%int -> + forall n n' : int, (n == n')%int -> + (m + n == m' + n')%int. + +Lemma eqmodp_morph : + forall m m' : int, (m == m')%int -> + forall n n' : int, (n == n')%int -> + (m' == n')%int -> (m == n)%int. +Proof. +move=> m m' Rm n n' Rn Rmn. +exact (eqp_trans _ _ _ Rm (eqp_trans _ _ _ Rmn (eqp_sym _ _ Rn))). +Qed. + +Lemma eqmodp01 : + forall m m' : int, (m == m')%int -> + forall n n' : int, (n == n')%int -> + 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)). +- constructor. +- by constructor => mn; apply (eqmodp_morph _ _ Rm _ _ Rn). +Qed. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref eqmodp}} (pc map0 map1) [] {{:gref eqmodp}} {{:gref eqmodp01}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref add}} (pc map0 map0) [] {{:gref add}} {{:gref add_morph}})). +}}. + +Variables i : int. +Let j := (i + p)%int. +Variable ip : (j == i)%int. +Definition iid : (i == i)%int := eqp_refl i. + +Elpi Query param lp:{{ + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref j}} (pc map0 map0) [] {{:gref i}} {{:gref ip}})), + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-gref") + (param.db.gref {{:gref i}} (pc map0 map0) [] {{:gref i}} {{:gref iid}})). +}}. + +Example ipi : (j + i == i + i)%int. +Proof. +param. +apply eqp_refl. +Qed. + +Print ipi. +Print Assumptions ipi. \ No newline at end of file diff --git a/theories/Database.v b/theories/Database.v new file mode 100644 index 0000000..4e8e002 --- /dev/null +++ b/theories/Database.v @@ -0,0 +1,128 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +Require Import HoTT_additions. +From elpi Require Import elpi. + +(* included to remove Elpi typechecker warnings *) +From Trocq.Elpi.constraints Extra Dependency "simple-graph.elpi" as simple_graph. +From Trocq.Elpi.constraints Extra Dependency "constraint-graph.elpi" as constraint_graph. +From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints. + +From Trocq.Elpi Extra Dependency "annot.elpi" as annot. +From Trocq.Elpi Extra Dependency "util.elpi" as util. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Elpi Db param.db lp:{{ + pred param.db.r o:param-class, o:constant. + :name "default-r" + param.db.r C R :- var C, !, + declare_constraint (param.db.r C R) [C]. + pred param.db.ptype o:constant. + pred param.db.weaken o:constant. + pred param.db.param-type o:param-class, o:param-class, o:constant. + pred param.db.pparam-type o:param-class, o:constant. + param.db.pparam-type C _ :- coq.say "pparam" C, fail. + :name "default-pparam-type" + param.db.pparam-type C PParamType :- var C, !, + declare_constraint (param.db.pparam-type C PParamType) [C]. + pred param.db.param-arrow o:param-class, o:constant. + param.db.param-arrow C _ :- coq.say "arrow" C, fail. + :name "default-param-arrow" + param.db.param-arrow C ParamArrow :- var C, !, + declare_constraint (param.db.param-arrow C ParamArrow) [C]. + pred param.db.param-forall o:param-class, o:constant. + param.db.param-forall C _ :- coq.say "forall" C, fail. + :name "default-param-forall" + param.db.param-forall C ParamForall :- var C, !, + declare_constraint (param.db.param-forall C ParamForall) [C]. + pred param.db.univalence o:constant. + :name "default-univalence" + param.db.univalence _ :- coq.error "univalence axiom required". + pred param.db.funext o:constant. + :name "default-funext" + param.db.funext _ :- coq.error "function extensionality axiom required". + pred param.db.gref o:gref, o:param-class, o:list param-class, o:gref, o:gref. + :name "default-gref" + param.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out. +}}. + +Elpi Command Param. +Elpi Accumulate Db param.db. +Elpi Accumulate File util. +Elpi Accumulate File annot. +Elpi Accumulate File param_class. +Elpi Accumulate File simple_graph. +Elpi Accumulate File constraint_graph. +Elpi Accumulate File constraints. +Elpi Typecheck. +Elpi Accumulate lp:{{ + main [str "Register", str "Univalence", str S] :- !, std.do! [ + std.assert! (coq.locate S GR) "unknown global reference", + coq.univ-instance UI0 [], + @uinstance! UI0 => coq.env.global GR U, + coq.locate "Univalence" GRU, + @uinstance! UI0 => coq.env.global GRU ExpectedUTy, + coq.typecheck U UTy ok, + std.assert-ok! (coq.unify-eq UTy ExpectedUTy) {std.string.concat "" [ + "type mismatch, expected ", + {coq.term->string ExpectedUTy}, + ", got ", + {coq.term->string UTy}, + "." + ]}, + GR = const Const, + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-univalence") (param.db.univalence Const)), + coq.say "Univalence axiom successfully registered." + ]. + + main [str "Register", str "Funext", str S] :- !, std.do! [ + std.assert! (coq.locate S GR) "unknown global reference", + coq.univ-instance UI0 [], + @uinstance! UI0 => coq.env.global GR F, + coq.locate "Funext" GRF, + @uinstance! UI0 => coq.env.global GRF ExpectedFTy, + coq.typecheck F FTy ok, + std.assert-ok! (coq.unify-eq FTy ExpectedFTy) {std.string.concat "" [ + "type mismatch, expected ", + {coq.term->string ExpectedFTy}, + ", got ", + {coq.term->string FTy}, + "." + ]}, + GR = const Const, + coq.elpi.accumulate _ "param.db" + (clause _ (before "default-funext") (param.db.funext Const)), + coq.say "Function extensionality axiom successfully registered." + ]. + + main [str "Usage"] :- !, coq.say {usage-msg}. + main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}. + + pred usage-msg o:string. + usage-msg U :- + std.string.concat "\n" [ + "usage:", + "- Param Register Univalence ", + "- Param Register Funext ", + "", "", + ] U. +}}. +Elpi Typecheck. +Elpi Export Param. diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v new file mode 100644 index 0000000..45158c5 --- /dev/null +++ b/theories/Hierarchy.v @@ -0,0 +1,650 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +Require Import HoTT_additions Database. +From elpi Require Import elpi. + +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Set Polymorphic Inductive Cumulativity. + +(*************************) +(* Parametricity Classes *) +(*************************) + +Module Map0. +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas {}. +End Map0. + +Module Map1. +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas { + map : A -> B +}. +End Map1. + +Module Map2a. +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas { + map : A -> B; + map_in_R : forall (a : A) (b : B), map a = b -> R a b +}. +End Map2a. + +Module Map2b. +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas { + map : A -> B; + R_in_map : forall (a : A) (b : B), R a b -> map a = b +}. +End Map2b. + +Module Map3. +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas { + map : A -> B; + map_in_R : forall (a : A) (b : B), map a = b -> R a b; + R_in_map : forall (a : A) (b : B), R a b -> map a = b +}. +End Map3. + +Module Map4. +(* An alternative presentation of Sozeau, Tabareau, Tanter's univalent parametricity: + symmetrical and transport-free *) +Record Has@{i} {A B : Type@{i}} (R : A -> B -> Type@{i}) := BuildHas { + map : A -> B; + map_in_R : forall (a : A) (b : B), map a = b -> R a b; + R_in_map : forall (a : A) (b : B), R a b -> map a = b; + R_in_mapK : forall (a : A) (b : B) (r : R a b), (map_in_R a b (R_in_map a b r)) = r +}. +End Map4. + +(********************) +(* Record Hierarchy *) +(********************) + +Elpi Command genhierarchy. +Elpi Accumulate Db param.db. +Elpi Accumulate File param_class. +Elpi Accumulate lp:{{ + % generate a module with a record type containing: + % - a relation R : A -> B -> Type; + % - a covariant (A to B) instance of one of the classes of Map listed above; + % - a contravariant (B to A) instance. + % (projections are generated so that all fields are accessible from the top record) + pred generate-module i:param-class, i:univ, i:univ.variable. + generate-module (pc M N as Class) U L :- + map-class->string M MStr, + map-class->string N NStr, + % open module + coq.env.begin-module {calc ("Param" ^ MStr ^ NStr)} none, + % generate record + coq.univ-instance UI [L], + coq.locate {calc ("Map" ^ MStr ^ ".Has")} CovariantSubRecord, + coq.locate {calc ("Map" ^ NStr ^ ".Has")} ContravariantSubRecord, + coq.locate "sym_rel" SymRel, + RelDecl = + parameter "A" _ (sort (typ U)) (a\ + parameter "B" _ (sort (typ U)) (b\ + record "Rel" (sort (typ {coq.univ.super U})) "BuildRel" ( + field [] "R" {{ lp:a -> lp:b -> lp:{{ sort (typ U) }} }} (r\ + field [] "covariant" (app [pglobal CovariantSubRecord UI, a, b, r]) (_\ + 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 _, + coq.locate "Rel" Rel, + coq.locate "R" R, + % add R to database for later use + R = const CR, + coq.elpi.accumulate _ "param.db" (clause _ (after "default-r") (param.db.r Class CR)), + % generate projections on the covariant subrecord + map-class->fields M MFields, + coq.locate "covariant" Covariant, + std.forall MFields (field\ sigma FieldName Field Decl\ + FieldName is "Map" ^ MStr ^ "." ^ field, + coq.locate FieldName Field, + Decl = + (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ fun `P` (app [pglobal Rel UI, a, b]) p\ + app [pglobal Field 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 Decl _ @transparent! _ + ), + % generate projections on the contravariant subrecord + map-class->fields N NFields, + map-class->cofields N NCoFields, + coq.locate "contravariant" Contravariant, + std.forall2 NFields NCoFields (field\ field-name\ sigma FieldName Field Decl\ + FieldName is "Map" ^ NStr ^ "." ^ field, + coq.locate FieldName Field, + Decl = + (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ + fun `P` (app [pglobal Rel UI, a, b]) p\ + app [pglobal Field 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! _ + ), + % close module + coq.env.end-module _. +}}. +Elpi Typecheck. + +(********************) +(* Record Weakening *) +(********************) + +Definition forgetMap43@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map4.Has@{i} R) : Map3.Has@{i} R := + @Map3.BuildHas A B R (@Map4.map A B R m) (@Map4.map_in_R A B R m) (@Map4.R_in_map A B R m). + +Definition forgetMap32a@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2a.Has@{i} R := + @Map2a.BuildHas A B R (@Map3.map A B R m) (@Map3.map_in_R A B R m). + +Definition forgetMap32b@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2b.Has@{i} R := + @Map2b.BuildHas A B R (@Map3.map A B R m) (@Map3.R_in_map A B R m). + +Definition forgetMap2a1@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2a.Has@{i} R) : Map1.Has@{i} R := + @Map1.BuildHas A B R (@Map2a.map A B R m). + +Definition forgetMap2b1@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2b.Has@{i} R) : Map1.Has@{i} R := + @Map1.BuildHas A B R (@Map2b.map A B R m). + +Definition forgetMap10@{i} + {A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map1.Has@{i} R) : Map0.Has@{i} R := + @Map0.BuildHas A B R. + +Elpi Accumulate lp:{{ + % generate 2 functions of weakening per possible weakening: + % one on the left and one on the right, if possible + pred generate-forget i:param-class, i:univ, i:univ.variable. + generate-forget (pc M N) U L :- + coq.univ-instance UI [L], + map-class->string M MStr, + map-class->string N NStr, + ModuleNameMN is "Param" ^ MStr ^ NStr, + coq.locate {calc (ModuleNameMN ^ ".Rel")} RelMN, + coq.locate {calc (ModuleNameMN ^ ".R")} RMN, + coq.locate {calc (ModuleNameMN ^ ".covariant")} CovariantMN, + coq.locate {calc (ModuleNameMN ^ ".contravariant")} ContravariantMN, + % covariant weakening + std.forall {map-class.weakenings-from M} (m1\ + sigma M1Str ModuleNameM1N BuildRelName BuildRelM1N ForgetMapName + ForgetMapM Decl ForgetName Forget RelName RelM1N\ std.do! [ + map-class->string m1 M1Str, + ModuleNameM1N is "Param" ^ M1Str ^ NStr, + BuildRelName is ModuleNameM1N ^ ".BuildRel", + coq.locate BuildRelName BuildRelM1N, + ForgetMapName is "forgetMap" ^ MStr ^ M1Str, + coq.locate ForgetMapName ForgetMapM, + Decl = + (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ + fun `P` (app [pglobal RelMN UI, a, b]) p\ + app [pglobal BuildRelM1N UI, a, b, app [pglobal RMN UI, a, b, p], + app [pglobal ForgetMapM UI, a, b, app [pglobal RMN UI, a, b, p], + app [pglobal CovariantMN UI, a, b, p]], + app [pglobal ContravariantMN UI, a, b, p]]), + ForgetName is "forget_" ^ MStr ^ NStr ^ "_" ^ M1Str ^ NStr, + @udecl! [L] ff [] ff => + coq.env.add-const ForgetName Decl _ @transparent! _, + coq.locate ForgetName Forget, + RelName is ModuleNameM1N ^ ".Rel", + coq.locate RelName RelM1N, + @global! => coq.coercion.declare (coercion Forget 2 RelMN (grefclass RelM1N)) + ]), + % contravariant weakening + coq.locate "sym_rel" SymRel, + std.forall {map-class.weakenings-from N} (n1\ + sigma N1Str ModuleNameMN1 BuildRelName BuildRelMN1 ForgetMapName + ForgetMapN Decl ForgetName Forget RelName RelMN1\ std.do! [ + map-class->string n1 N1Str, + ModuleNameMN1 is "Param" ^ MStr ^ N1Str, + BuildRelName is ModuleNameMN1 ^ ".BuildRel", + coq.locate BuildRelName BuildRelMN1, + ForgetMapName is "forgetMap" ^ NStr ^ N1Str, + coq.locate ForgetMapName ForgetMapN, + Decl = + (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ + fun `P` (app [pglobal RelMN UI, a, b]) p\ + app [pglobal BuildRelMN1 UI, a, b, app [pglobal RMN UI, a, b, p], + app [pglobal CovariantMN UI, a, b, p], + app [pglobal ForgetMapN UI, b, a, + app [pglobal SymRel UI, a, b, app [pglobal RMN UI, a, b, p]], + app [pglobal ContravariantMN UI, a, b, p]]]), + ForgetName is "forget_" ^ MStr ^ NStr ^ "_" ^ MStr ^ N1Str, + @udecl! [L] ff [] ff => + coq.env.add-const ForgetName Decl _ @transparent! _, + coq.locate ForgetName Forget, + RelName is ModuleNameMN1 ^ ".Rel", + coq.locate RelName RelMN1, + @global! => coq.coercion.declare (coercion Forget 2 RelMN (grefclass RelMN1)) + ]). +}}. +Elpi Typecheck. + +(* generate the hierarchy *) +Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall Classes (m\ + std.forall Classes (n\ + generate-module (pc m n) U L, + generate-forget (pc m n) U L + ) + ). +}}. + +(* Set Printing Universes. Print Module Param2a3. *) +(* Set Printing Universes. Print forget_42b_41. *) +(* Check forall (p : Param44.Rel nat nat), @paths (Param12a.Rel nat nat) p p. *) + +(* General projections *) + +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) : + forall (a : A) (b : B), map R a = b -> R a b := + Map2a.map_in_R _ (Param2a0.covariant A B R). +Definition R_in_map {A B} (R : Param2b0.Rel A B) : + forall (a : A) (b : B), R a b -> map R a = b := + Map2b.R_in_map _ (Param2b0.covariant A B R). +Definition R_in_mapK {A B} (R : Param40.Rel A B) : + forall (a : A) (b : B), map_in_R R a b o R_in_map R a b == idmap := + Map4.R_in_mapK _ (Param40.covariant A B R). + +Definition comap {A B} (R : Param01.Rel A B) : B -> A := + Map1.map _ (Param01.contravariant A B R). +Definition comap_in_R {A B} (R : Param02a.Rel A B) : + forall (b : B) (a : A), comap R b = a -> R a b := + Map2a.map_in_R _ (Param02a.contravariant A B R). +Definition R_in_comap {A B} (R : Param02b.Rel A B) : + forall (b : B) (a : A), R a b -> comap R b = a := + Map2b.R_in_map _ (Param02b.contravariant A B R). +Definition R_in_comapK {A B} (R : Param04.Rel A B) : + forall (b : B) (a : A), comap_in_R R b a o R_in_comap R b a == idmap := + Map4.R_in_mapK _ (Param04.contravariant A B R). + +(* Aliasing *) + +Declare Scope param_scope. +Local Open Scope param_scope. +Delimit Scope param_scope with P. + +Notation UParam := Param44.Rel. +Notation MkUParam := Param44.BuildRel. +Notation "A <=> B" := (Param44.Rel A B) : param_scope. +Notation IsUMap := Map4.Has. +Notation MkUMap := Map4.BuildHas. +Arguments Map4.BuildHas {A B R}. +Arguments Param44.BuildRel {A B R}. + +(* 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') -> + 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') -> + 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') -> + Map2a.Has@{i} R' -> Map2a.Has@{i} R. +Proof. + move=> RR' [m mR]; exists m. + move=> a' b /mR /(RR' _ _)^-1%equiv; 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') -> + Map2b.Has@{i} R' -> Map2b.Has@{i} R. +Proof. + move=> RR' [m Rm]; unshelve eexists m. + - move=> a' b /(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') -> + 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. +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. + +(* joined elimination of comap and comap_in_R *) + +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 *) + +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. + +Lemma umap_equiv_isfun `{Funext} {A B : Type@{i}} + (R : A -> B -> Type@{i}) : IsUMap R <~> IsFun 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. +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) := + 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)) := + 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 := + 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 *) + +Definition id_Map0 {A : Type} : Map0.Has (@paths A). +Proof. constructor. Defined. + +Definition id_Map0_sym {A : Type} : Map0.Has (sym_rel (@paths A)). +Proof. constructor. Defined. + +Definition id_Map1 {A : Type} : Map1.Has (@paths A). +Proof. constructor. exact idmap. Defined. + +Definition id_Map1_sym {A : Type} : Map1.Has (sym_rel (@paths A)). +Proof. constructor. exact idmap. Defined. + +Definition id_Map2a {A : Type} : Map2a.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). +Defined. + +Definition id_Map2a_sym {A : Type} : Map2a.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). +Defined. + +Definition id_Map2b {A : Type} : Map2b.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). +Defined. + +Definition id_Map2b_sym {A : Type} : Map2b.Has (sym_rel (@paths A)). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun A B e => e^). +Defined. + +Definition id_Map3 {A : Type} : Map3.Has (@paths A). +Proof. + unshelve econstructor. + - exact idmap. + - exact (fun a b e => e). + - exact (fun a b e => e). +Defined. + +Definition id_Map3_sym {A : Type} : 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 id_Map4 {A : Type} : 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 id_Map4_sym {A : Type} : 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-id-param i:param-class, i:univ, i:univ.variable. + generate-id-param (pc M N) U L :- + map-class->string M MStr, + map-class->string N NStr, + coq.univ-instance UI [L], + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".BuildRel")} BuildRel, + coq.locate "paths" Paths, + coq.locate {calc ("id_Map" ^ MStr)} IdMap, + 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 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! _. +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall Classes (m\ + std.forall Classes (n\ + generate-id-param (pc m n) U L + ) + ). +}}. + +(* Check id_Param00. *) +(* Check id_Param32b. *) + +(* symmetry property for Param *) + +Elpi Accumulate lp:{{ + pred generate-param-sym i:param-class, i:univ, i:univ.variable. + generate-param-sym (pc M N) U L :- + map-class->string M MStr, + map-class->string N NStr, + coq.univ-instance UI [L], + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".Rel")} RelMN, + coq.locate {calc ("Param" ^ NStr ^ MStr ^ ".BuildRel")} BuildRelNM, + coq.locate "sym_rel" SymRel, + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".R")} RMN, + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".covariant")} CovariantMN, + coq.locate + {calc ("Param" ^ MStr ^ NStr ^ ".contravariant")} ContravariantMN, + Decl = + (fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ + fun `P` (app [pglobal RelMN UI, a, b]) p\ + app [pglobal BuildRelNM UI, b, a, + app [pglobal SymRel UI, a, b, app [pglobal RMN UI, a, b, p]], + app [pglobal ContravariantMN UI, a, b, p], + app [pglobal CovariantMN UI, a, b, p] + ]), + ParamSym is "Param" ^ MStr ^ NStr ^ "_sym", + @udecl! [L] ff [] ff => coq.env.add-const ParamSym Decl _ @transparent! _. +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall Classes (m\ + std.forall Classes (n\ + generate-param-sym (pc m n) U L + ) + ). +}}. + +(* Check Param33_sym. +Check Param2a4_sym. *) diff --git a/theories/HoTT_additions.v b/theories/HoTT_additions.v new file mode 100644 index 0000000..8d2c8c0 --- /dev/null +++ b/theories/HoTT_additions.v @@ -0,0 +1,126 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. + +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. + +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. + +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. + +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 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 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 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. diff --git a/theories/Param.v b/theories/Param.v new file mode 100644 index 0000000..6ef2b3a --- /dev/null +++ b/theories/Param.v @@ -0,0 +1,201 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy. +Require Export Database. +Require Export Param_Type Param_arrow Param_forall. + +From Trocq.Elpi Extra Dependency "annot.elpi" as annot. +From Trocq.Elpi Extra Dependency "util.elpi" as util. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. +From Trocq.Elpi Extra Dependency "param.elpi" as param. +From Trocq.Elpi.constraints Extra Dependency "simple-graph.elpi" as simple_graph. +From Trocq.Elpi.constraints Extra Dependency "constraint-graph.elpi" as constraint_graph. +From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4. + +(* PType and weaken *) + +Elpi Command genpparam. +Elpi Accumulate File param_class. +Elpi Accumulate Db param.db. + +Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}. +Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a. + +Elpi Query lp:{{ + coq.locate "PType" (const PType), + coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.ptype PType)), + coq.locate "weaken" (const Weaken), + coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.weaken Weaken)). +}}. + +(* 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 param_class. +Elpi Accumulate Db param.db. +Elpi Accumulate lp:{{ + pred generate-branch i:univ-instance, i:param-class, i:param-class, o:term. + generate-branch UI2 Class RClass (pglobal ParamType UI2) :- + coq.locate + {calc ("Param" ^ {param-class->string Class} ^ "_Type" ^ {param-class->string RClass})} + ParamType. + + pred generate-match2 + i:term, i:univ-instance, i:param-class, i:term, i:map-class, o:term. + generate-match2 RetType UI2 Class QVar P Match :- + std.map [map0, map1, map2a, map2b, map3, map4] + (q\ b\ generate-branch UI2 Class (pc P q) b) Branches, + coq.locate "map_class" MapClass, + coq.univ-instance UI0 [], + Match = (match QVar (fun `_` (pglobal MapClass UI0) _\ RetType) Branches). + + pred generate-match1 + i:term, i:univ-instance, i:param-class, i:term, i:term, o:term. + generate-match1 RetType UI2 Class PVar QVar Match :- + std.map [map0, map1, map2a, map2b, map3, map4] + (p\ b\ generate-match2 RetType UI2 Class QVar p b) Branches, + coq.locate "map_class" MapClass, + coq.univ-instance UI0 [], + Match = (match PVar (fun `_` (pglobal MapClass UI0) _\ RetType) Branches). + + pred generate-pparam-type + i:univ.variable, i:univ.variable, i:param-class. + generate-pparam-type L L1 Class :- + coq.locate {calc ("Param" ^ {param-class->string Class} ^ ".Rel")} ParamRel, + coq.univ-instance UI1 [L1], + RetType = app [pglobal ParamRel UI1, sort (typ U), sort (typ U)], + coq.univ-instance UI2 [L, L1], + (pi p q\ generate-match1 RetType UI2 Class p q (MatchF p q)), + Decl = (fun `p` {{ map_class }} p\ fun `q` {{ map_class }} q\ MatchF p q), + % 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 _ "param.db" (clause _ _ (param.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 => + coq.env.add-const PParamType Decl _ @transparent! Const, + coq.elpi.accumulate _ "param.db" (clause _ _ (param.db.pparam-type Class Const)). +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + coq.univ.super U U1, + coq.univ.variable U1 L1, + Classes1 = [map0, map1, map2a], + Classes2 = [map2b, map3, map4], + Classes = [map0, map1, map2a, map2b, map3, map4], + % 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) + ) + ). +}}. + +Elpi Tactic param. +Elpi Accumulate Db param.db. +Elpi Accumulate File annot. +Elpi Accumulate File util. +Elpi Accumulate File param_class. +Elpi Accumulate File simple_graph. +Elpi Accumulate File constraint_graph. +Elpi Accumulate File constraints. +Elpi Accumulate File param. +Elpi Typecheck. + +Elpi Accumulate lp:{{ + :before "coq-assign-evar" + evar _ _ _ :- !. +}}. + +Elpi Accumulate lp:{{ + solve InitialGoal NewGoals :- debug dbg.full => std.do! [ + InitialGoal = goal _Context _ G _ [], + coq.say "goal" G, + translate-goal G (pc map0 map1) G' GR, + FinalProof = {{ @comap lp:G lp:G' lp:GR (_ : lp:G') }}, + coq.say FinalProof, + + std.assert-ok! (coq.elaborate-skeleton FinalProof G EFinalProof) "proof elaboration error", + std.assert-ok! (coq.typecheck EFinalProof G2) "proof typechecking error", + std.assert-ok! (coq.unify-leq G2 G) "goal unification error", + 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! [ + cstr.init, + T = (app [pglobal (const {param.db.ptype}) _, {map-class->term M}, {map-class->term N}]), + term->annot-term G AG, + util.when-debug dbg.steps ( + coq.say "will translate" AG "at level" T, + coq.say "***********************************************************************************" + ), + param AG T G' GR, + util.when-debug dbg.steps ( + coq.say "***********************************************************************************", + coq.say "after translation:", + coq.say "goal:" G', + coq.say "proof:" GR, + coq.say "***********************************************************************************" + ), + cstr.reduce-graph, + param.subst-weaken GR GR', + util.when-debug dbg.steps ( + coq.say "***********************************************************************************", + coq.say "after reduction:", + coq.say "goal:" {coq.term->string G'}, + coq.say "proof:" {coq.term->string GR'}, + coq.say "***********************************************************************************" + ) + ]. +}}. +Elpi Typecheck. + +Tactic Notation "param" := elpi param. diff --git a/theories/Param44.v b/theories/Param44.v new file mode 100644 index 0000000..db9ce67 --- /dev/null +++ b/theories/Param44.v @@ -0,0 +1,389 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Local Open Scope param_scope. + +(*********************) +(* Proofs for UParam *) +(*********************) + +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. + +Lemma umap_equiv_isfun `{Funext} {A B : Type@{i}} + (R : A -> B -> Type@{i}) : IsUMap R <~> IsFun 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. +Defined. + +Lemma umap_isprop `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : + IsHProp (IsUMap R). +Proof. +apply (istrunc_equiv_istrunc (IsFun R)); last exact: isfun_isprop. +apply symmetric_equiv; apply umap_equiv_isfun. +Qed. + +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) := + 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)) := + 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 := + 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. + +(***********************) +(* Proofs for Universe *) +(***********************) + +Definition umap_Type `{Univalence} : IsUMap@{i} UParam. +Proof. + unshelve refine (MkUMap idmap (fun a b e => e # id_uparam) _ _). + { 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 sym_umap_Type `{Univalence} : + @IsUMap Type@{i} Type@{i} (sym_rel UParam). +Proof. + unshelve refine (MkUMap idmap (fun a b e => e # id_uparam) _ _). + { 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. + +Definition uparam_Type `{Univalence} : Type@{i} <=> Type@{i} := + MkUParam umap_Type sym_umap_Type. + +Lemma R_uparam_Type `{Univalence} : rel uparam_Type = UParam. +Proof. reflexivity. Defined. + +Lemma map_uparam_Type `{Univalence} : map uparam_Type = id. +Proof. reflexivity. Defined. + +Lemma comap_uparam_Type `{Univalence} : comap uparam_Type = id. +Proof. reflexivity. Defined. + +(********************************) +(* Proofs for dependent product *) +(********************************) + +Definition uparam_sym {A A' : Type} : A <=> A' -> A' <=> A := + fun '(MkUParam R m c) => MkUParam c m. +Notation "R ^-1" := (uparam_sym R) : param_scope. + +Definition uparam_sym_val {A A' : Type} (PA : A <=> A') (a : A) (a' : A') : + PA a a' -> PA^-1 a' a. +Proof. by []. Defined. + +Definition uparam_sym_val' {A A' : Type} (PA : A <=> A') (a : A) (a' : A') : + PA^-1 a' a -> PA a a'. +Proof. by []. Defined. + +Definition uparam_sym_val_equiv {A A' : Type} (PA : A <=> A') + (a : A) (a' : A') : PA^-1 a' a = PA a a'. +Proof. by []. 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. + +Definition R_forall {A A' : Type} (PA : Param00.Rel A A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> Param00.Rel (B a) (B' a')) : + (forall a : A, B a) -> (forall a' : A', B' a') -> Type := + fun f f' => forall a a' aR, PB a a' aR (f a) (f' a'). + +(* generic symmetry lemma *) +Definition eq_umap {A A' : Type} {R R' : A -> A' -> Type} : + (forall a a', R a a' <~> R' a a') -> + IsUMap R' -> IsUMap 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 uparam_forall_map1 {A A' : Type} (PA : Param02.Rel A A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> Param10.Rel (B a) (B' a')) : + Map1.Has (R_forall PA PB). +Proof. +constructor. +exact (fun f a' => map (PB _ _ (comap_in_R _ _ _ 1)) (f (comap PA a'))). +Defined. + +Definition uparam_forall_map2 {A A' : Type} (PA : Param04.Rel A A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> Param20.Rel (B a) (B' a')) : + Map2.Has (R_forall PA PB). +Proof. +exists (Map1.map _ (uparam_forall_map1 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): _. +Defined. + +Definition uparam_forall_map3 `{Funext} {A A' : Type} (PA : Param04.Rel A A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> Param30.Rel (B a) (B' a')) : + Map3.Has (R_forall PA PB). +Proof. +exists (Map1.map _ (uparam_forall_map1 PA PB)). +- exact: (Map2.map_in_R _ (uparam_forall_map2 PA PB)). +- move=> f f' fR; apply path_forall => a'. + apply (R_in_map (PB _ _ _)); exact: fR. +Defined. + +Definition uparam_forall_umap `{Funext} {A A' : Type} (PA : Param04.Rel A A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> Param40.Rel (B a) (B' a')) : + IsUMap (R_forall PA PB). +Proof. +exists (Map1.map _ (uparam_forall_map1 PA PB)) + (Map2.map_in_R _ (uparam_forall_map2 PA PB)) + (Map3.R_in_map _ (uparam_forall_map3 PA PB)). +move=> f f' fR /=. +apply path_forall => a. +apply path_forall => 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. + +Definition uparam_forall `{Funext} {A A' : Type} (PA : A <=> A') + {B : A -> Type} {B' : A' -> Type} + (PB : forall (a : A) (a' : A'), PA a a' -> B a <=> B' a') : + (forall a : A, B a) <=> (forall a' : A', B' a'). +Proof. +unshelve econstructor. +- exact: (R_forall PA PB). +- exact: (uparam_forall_umap PA PB). +- apply (eq_umap (fun _ _ => equiv_flip _)). + exact: (uparam_forall_umap PA^-1 (fun a' a r => (PB a a' r)^-1)). +Defined. + +Fact map_uparam_forall `{Funext} A A' (PA : A <=> A') + B B' (PB : forall a a', PA a a' -> B a <=> B' a') : + map (uparam_forall PA PB) = + fun f a' => map (PB _ _ (comap_in_R _ _ _ 1)) (f (comap PA a')). +Proof. reflexivity. Qed. + +Fact comap_uparam_forall `{Funext} A A' (PA : A <=> A') + B B' (PB : forall a a', PA a a' -> B a <=> B' a') : + comap (uparam_forall PA PB) = + fun f a => comap (PB _ _ (map_in_R PA _ _ 1)) (f (map PA a)). +Proof. reflexivity. Qed. + +Definition R_arrow {A A' : Type} (PA : Param00.Rel A A') + {B B' : Type} (PB : Param00.Rel B B') : + (A -> B) -> (A' -> B') -> Type := + fun f f' => forall a a', PA a a' -> PB (f a) (f' a'). + +Definition uparam_arrow_map1 {A A' : Type} (PA : Param01.Rel A A') + {B B' : Type} (PB : Param10.Rel B B') : + Map1.Has (R_arrow PA PB). +Proof. exists; exact (fun f a' => map PB (f (comap PA a'))). Defined. + +Definition uparam_arrow_map2 {A A' : Type} (PA : Param03.Rel A A') + {B B' : Type} (PB : Param20.Rel B B') : + Map2.Has (R_arrow PA PB). +Proof. +exists (Map1.map _ (uparam_arrow_map1 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)^). +Defined. + +Definition uparam_arrow_map3 `{Funext} {A A' : Type} (PA : Param03.Rel A A') + {B B' : Type} (PB : Param30.Rel B B') : + Map3.Has (R_arrow PA PB). +Proof. +exists (Map1.map _ (uparam_arrow_map1 PA PB)). +- exact: (Map2.map_in_R _ (uparam_arrow_map2 PA PB)). +- move=> f f' /= fR; apply path_arrow => a'. + by apply (R_in_map PB); apply fR; apply (comap_in_R PA). +Defined. + +Definition uparam_arrow_umap `{Funext} {A A' : Type} (PA : Param04.Rel A A') + {B B' : Type} (PB : Param40.Rel B B') : + IsUMap (R_arrow PA PB). +Proof. +exists (Map1.map _ (uparam_arrow_map1 PA PB)) + (Map2.map_in_R _ (uparam_arrow_map2 PA PB)) + (Map3.R_in_map _ (uparam_arrow_map3 PA PB)). +move=> f f' fR /=. +apply path_forall => a. +apply path_forall => a'. +apply path_arrow => 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. + +Definition uparam_arrow `{Funext} {A A' : Type} (PA : A <=> A') + {B B' : Type} (PB : B <=> B') : + (A -> B) <=> (A' -> B'). +Proof. +unshelve econstructor. +- exact: (R_arrow PA PB). +- exact: (uparam_arrow_umap PA PB). +- apply (eq_umap (fun _ _ => equiv_flip _)). + exact: (uparam_arrow_umap PA^-1 PB^-1). +Defined. + +Fact map_uparam_arrow `{Funext} A A' (PA : A <=> A') B B' (PB : B <=> B') : + map (uparam_arrow PA PB) = fun f a' => map PB (f (comap PA a')). +Proof. reflexivity. Qed. + +Fact comap_uparam_arrow `{Funext} A A' (PA : A <=> A') B B' (PB : B <=> B') : + comap (uparam_arrow PA PB) = fun f a => comap PB (f (map PA a)). +Proof. reflexivity. Qed. diff --git a/theories/Param_Type.v b/theories/Param_Type.v new file mode 100644 index 0000000..465ccdd --- /dev/null +++ b/theories/Param_Type.v @@ -0,0 +1,256 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Local Open Scope param_scope. + +(* generate MapM_TypeNP@{i} : + MapM.Has Type@{i} Type@{i} ParamNP.Rel@{i}, + for all N P, for M = map2a and below (above, NP is always 44) + + symmetry MapM_Type_symNP *) + +Elpi Command genmaptype. +Elpi Accumulate File param_class. +Elpi Accumulate lp:{{ + pred generate-fields + i:map-class, i:term, i:param-class, i:univ, + i:univ.variable, i:univ.variable, o:list term. + generate-fields map0 R _ _ _ _ [R]. + generate-fields map1 R _ U _ _ [R, Map] :- + Map = (fun `T` (sort (typ U)) t\ t). + generate-fields map2a R RClass U L L1 [R, Map, MapInR] :- + Type = sort (typ U), + coq.univ-instance UI [L], + coq.univ-instance UI1 [L1], + coq.univ-instance UI11 [L1, L1], + Map = (fun `T` Type 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, + MapInR = + (fun `A` Type a\ fun `B` Type b\ + fun `e` (app [pglobal Paths UI1, Type, a, b]) e\ + app [pglobal Transport UI11, Type, RF a, a, b, + e, app [pglobal IdParam UI, a]]). + + pred generate-map-type + i:map-class, i:param-class, i:univ, i:univ.variable, i:univ.variable. + generate-map-type M RClass U L L1 :- + coq.locate {calc ("Param" ^ {param-class->string RClass} ^ ".Rel")} R, + Type = sort (typ U), + coq.univ-instance UI [L], + coq.univ-instance UI1 [L1], + generate-fields M (pglobal R UI) RClass U L L1 Fields, + coq.locate "sym_rel" SymRel, + generate-fields + M (app [pglobal SymRel UI1, Type, Type, pglobal R UI]) + RClass U L L1 FieldsSym, + coq.locate {calc ("Map" ^ {map-class->string M} ^ ".BuildHas")} BuildHas, + Decl = app [pglobal BuildHas UI1, Type, Type | Fields], + DeclSym = app [pglobal BuildHas UI1, Type, Type | FieldsSym], + MapType is + "Map" ^ {map-class->string M} ^ "_Type" ^ {param-class->string RClass}, + MapTypeSym is + "Map" ^ {map-class->string M} ^ "_Type_sym" ^ + {param-class->string RClass}, + % 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 => + coq.env.add-const MapType Decl _ @transparent! _, + @udecl! [L, L1] ff [lt L L1] ff => + coq.env.add-const MapTypeSym DeclSym _ @transparent! _. +}}. +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, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall [map0, map1, map2a] (m\ + std.forall Classes (n\ + std.forall Classes (p\ + generate-map-type m (pc n p) U L L1 + ) + ) + ). +}}. + +(* Check Map0_Type01. +Check Map1_Type_sym32b. +Check Map2a_Type44. *) + +(* now R is always Param44.Rel *) + +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 Db param.db. +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 ^ "_Type" ^ {param-class->string RClass})} MapType, + coq.locate + {calc ("Map" ^ NStr ^ "_Type_sym" ^ {param-class->string RClass})} + MapTypeSym, + coq.locate {calc ("Param" ^ {param-class->string RClass} ^ ".Rel")} R, + if (std.mem! [map2b, map3, map4] M) ( + UnivalentDecl = true, + MapTypeF = (u\ app [pglobal MapType UI2, u]), + if (std.mem! [map2b, map3, map4] N) + (MapTypeSymF = (u\ app [pglobal MapTypeSym UI2, u])) + (MapTypeSymF = (_\ pglobal MapTypeSym UI2)) + ) ( + MapTypeF = (_\ pglobal MapType UI2), + if (std.mem! [map2b, map3, map4] N) ( + MapTypeSymF = (u\ app [pglobal MapTypeSym UI2, u]), + UnivalentDecl = true + ) ( + MapTypeSymF = (_\ pglobal MapTypeSym 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 (typ U), sort (typ U), pglobal R UI, + MapTypeF u, MapTypeSymF u]) + ) ( + Dummy = (fun `x` (sort (typ U)) x\ x), + Decl = + app [pglobal BuildRel UI1, sort (typ U), sort (typ U), pglobal R UI, + MapTypeF Dummy, MapTypeSymF Dummy] + ), + 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 => + coq.env.add-const ParamType Decl _ @transparent! Const, + coq.elpi.accumulate _ "param.db" (clause _ _ (param.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], + Classes44 = [map2b, map3, map4], + 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 + ) + ) + ), + 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 + ) + ). +}}. + +(* Set Printing Universes. About Param00_Type40. +Set Printing Universes. About Param12a_Type31. +Set Printing Universes. About Param30_Type44. +Set Printing Universes. About Param44_Type44. *) diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v new file mode 100644 index 0000000..620ab44 --- /dev/null +++ b/theories/Param_arrow.v @@ -0,0 +1,276 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Local Open Scope param_scope. + +Elpi Command genparamarrow. +Elpi Accumulate Db param.db. +Elpi Accumulate File param_class. + +(* relation for arrow *) + +Definition R_arrow@{i j} + {A A' : Type@{i}} (PA : Param00.Rel@{i} A A') + {B B' : Type@{j}} (PB : Param00.Rel@{j} B B') := + fun f f' => forall a a', PA a a' -> PB (f a) (f' a'). + +(* MapN for arrow *) + +(* (00, 00) -> 00 *) +Definition Map0_arrow@{i j k | i <= k, j <= k} + {A A' : Type@{i}} (PA : Param00.Rel@{i} A A') + {B B' : Type@{j}} (PB : Param00.Rel@{j} B B') : + Map0.Has@{k} (R_arrow PA PB). +Proof. exists. Defined. + +(* (01, 10) -> 10 *) +Definition Map1_arrow@{i j k | i <= k, 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). +Proof. + exists; exact (fun f a' => map PB (f (comap PA a'))). +Defined. + +(* (02b, 2a0) -> 2a0 *) +Definition Map2a_arrow@{i j k | i <= k, 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)^). +Defined. + +(* (02a, 2b0) + funext -> 2b0 *) +Definition Map2b_arrow@{i j k | i <= k, 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). +Proof. + exists (Map1.map@{k} _ (Map1_arrow PA PB)). + move=> f f' /= fR; apply path_forall => a'. + by apply (R_in_map PB); apply fR; apply (comap_in_R PA). +Defined. + +(* (03, 30) + funext -> 30 *) +Definition Map3_arrow@{i j k | i <= k, 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). +Proof. + exists (Map1.map@{k} _ (Map1_arrow PA PB)). + - exact: (Map2a.map_in_R _ (Map2a_arrow PA PB)). + - move=> f f' /= fR; apply path_arrow => a'. + by apply (R_in_map PB); apply fR; apply (comap_in_R PA). +Defined. + +(* (04, 40) + funext -> 40 *) +Definition Map4_arrow@{i j k | i <= k, 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). +Proof. + exists + (Map1.map@{k} _ (Map1_arrow PA PB)) + (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. + +(* Param_arrowMN : forall A A' AR B B' BR, ParamMN.Rel (A -> B) (A' -> B') *) + +Elpi Accumulate lp:{{ + pred generate-param-arrow + i:param-class, i:univ, i:univ, i:univ.variable, i:univ.variable, + i:univ.variable. + generate-param-arrow (pc M N as Class) Ui Uj Li Lj Lk :- + % we need to generate Map in both ways, so we must add the dependencies + % from both sides to get the final classes we shall ask for A and B + map-class.dep-arrow M ClassAM ClassBM, + map-class.dep-arrow N NegClassAN NegClassBN, + param-class.negate NegClassAN ClassAN, + param-class.negate NegClassBN ClassBN, + param-class.union ClassAM ClassAN ClassA, + ClassA = pc MA NA, + param-class.union ClassBM ClassBN ClassB, + ClassB = pc MB NB, + map-class->string M MStr, + map-class->string N NStr, + map-class->string MA MAStr, + map-class->string MB MBStr, + map-class->string NA NAStr, + map-class->string NB NBStr, + coq.univ-instance UIi [Li], + coq.univ-instance UIj [Lj], + coq.univ-instance UIk [Lk], + coq.univ-instance UIij [Li, Lj], + coq.univ-instance UIik [Li, Lk], + coq.univ-instance UIijk [Li, Lj, Lk], + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ ".Rel")} RelA, + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ ".R")} RA, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ ".Rel")} RelB, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ ".R")} RB, + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".BuildRel")} BuildRel, + coq.locate "R_arrow" RArrow, + coq.locate {calc ("Map" ^ MStr ^ "_arrow")} MapM, + coq.locate {calc ("Map" ^ NStr ^ "_arrow")} MapN, + coq.locate {calc ("eq_Map" ^ NStr)} EqMapN, + coq.locate "equiv_flip" EquivFlip, + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ "_sym")} ParamSymA, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ "_sym")} ParamSymB, + % build functions doing several weakenings at once + param-class.forget ClassA (pc map0 map0) ForgetA0F, + param-class.forget ClassB (pc map0 map0) ForgetB0F, + param-class.forget ClassA ClassAM ForgetADepMF, + param-class.forget ClassB ClassBM ForgetBDepMF, + param-class.forget {param-class.negate ClassA} NegClassAN ForgetADepNF, + param-class.forget {param-class.negate ClassB} NegClassBN ForgetBDepNF, + % we cut the proof into multiple parts for readability + RArrowF = (a\ a'\ aR\ b\ b'\ bR\ + app [pglobal RArrow UIij, + a, a', ForgetA0F UIi a a' aR, b, b', ForgetB0F UIj b b' bR] + ), + EqMapR1F = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `_` a' _\ b') f'\ + fun `f` (prod `_` a _\ b) f\ + prod `a` a x\ prod `a'` a' x'\ + prod `_` (app [pglobal RA UIi, a, a', aR, x, x']) _\ + app [pglobal RB UIj, b, b', bR, app [f, x], app [f', x']] + ), + EqMapR2F = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `_` a' _\ b') f'\ + fun `f` (prod `_` a _\ b) f\ + prod `a'` a' x'\ prod `a` a x\ + prod `_` (app [pglobal RA UIi, a, a', aR, x, x']) _\ + app [pglobal RB UIj, b, b', bR, app [f, x], app [f', x']] + ), + EqMapR1R2EquivF = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `_` a' _\ b') f'\ + fun `f` (prod `_` a _\ b) f\ + app [pglobal EquivFlip UIik, a, a', + (fun `a` a x\ fun `a'` a' x'\ + prod `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + app [pglobal RB UIj, b, b', bR, app [f, x], app [f', x']])] + ), + % there is one call to MapM_arrow and one on MapN_arrow on the symmetric + % relation; both can need funext depending on M and N + MapMArgsF = (a\ a'\ aR\ b\ b'\ bR\ [ + a, a', ForgetADepMF UIi a a' aR, b, b', ForgetBDepMF UIj b b' bR + ]), + MapNArgsF = (a\ a'\ aR\ b\ b'\ bR\ [ + a', a, ForgetADepNF UIi a' a (app [pglobal ParamSymA UIi, a, a', aR]), + b', b, ForgetBDepNF UIj b' b (app [pglobal ParamSymB UIj, b, b', bR]) + ]), + if (std.mem! [map2b, map3, map4] M) ( + FunextDecl = true, + MapMF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapM UIijk, funext | MapMArgsF a a' aR b b' bR]), + if (std.mem! [map2b, map3, map4] N) ( + MapNF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk, funext | MapNArgsF a a' aR b b' bR]) + ) ( + MapNF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk | MapNArgsF a a' aR b b' bR]) + ) + ) ( + MapMF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapM UIijk | MapMArgsF a a' aR b b' bR]), + if (std.mem! [map2b, map3, map4] N) ( + FunextDecl = true, + MapNF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk, funext | MapNArgsF a a' aR b b' bR]) + ) ( + FunextDecl = false, + MapNF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk | MapNArgsF a a' aR b b' bR]) + ) + ), + % ParamMN_arrow proof + DeclF = (funext\ + fun `A` (sort (typ Ui)) a\ + fun `A'` (sort (typ Ui)) a'\ + fun `AR` (app [pglobal RelA UIi, a, a']) aR\ + fun `B` (sort (typ Uj)) b\ + fun `B'` (sort (typ Uj)) b'\ + fun `BR` (app [pglobal RelB UIj, b, b']) bR\ + app [pglobal BuildRel UIk, + (prod `_` a _\ b), + (prod `_` a' _\ b'), + RArrowF a a' aR b b' bR, + MapMF funext a a' aR b b' bR, + app [pglobal EqMapN UIk, + (prod `_` a' _\ b'), + (prod `_` a _\ b), + EqMapR1F a a' aR b b' bR, + EqMapR2F a a' aR b b' bR, + EqMapR1R2EquivF a a' aR b b' bR, + MapNF funext a a' aR b b' bR]] + ), + % add an additional binder for funext in case it is needed + if (FunextDecl) ( + coq.locate "Funext" Funext, + Decl = (fun `H` (global Funext) funext\ DeclF funext) + ) ( + Dummy = (fun `x` (sort (typ Ui)) x\ x), + Decl = DeclF Dummy + ), + 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 => + coq.env.add-const ParamArrow Decl _ @transparent! Const, + coq.elpi.accumulate _ "param.db" (clause _ (after "default-param-arrow") + (param.db.param-arrow Class Const)). +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new Ui, + coq.univ.variable Ui Li, + coq.univ.new Uj, + coq.univ.variable Uj Lj, + coq.univ.max Ui Uj Uk, + % cannot have only 2 binders in the declaration because this line creates a fresh level: + coq.univ.variable Uk Lk, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall Classes (m\ + std.forall Classes (n\ + generate-param-arrow (pc m n) Ui Uj Li Lj Lk + ) + ). +}}. + +(* Set Printing Universes. About Param2a1_arrow. +Set Printing Universes. About Param2b1_arrow. +Set Printing Universes. About Param33_arrow. *) diff --git a/theories/Param_forall.v b/theories/Param_forall.v new file mode 100644 index 0000000..c7092bf --- /dev/null +++ b/theories/Param_forall.v @@ -0,0 +1,337 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * 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. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Local Open Scope param_scope. + +Elpi Command genparamforall. +Elpi Accumulate Db param.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}} + (PB : forall (a : A) (a' : A'), PA a a' -> Param00.Rel@{j} (B a) (B' a')) := + fun f f' => forall a a' aR, (PB a a' aR) (f a) (f' a'). + +(* we can also declare everything from Coq-Elpi if we do not trust inference *) +(* Elpi Query lp:{{ + coq.univ.new U, + coq.univ.variable U L, + coq.univ-instance UI [L], + coq.univ.new U', + coq.univ.variable U' L', + coq.univ-instance UI' [L'], + coq.locate "Param00.Rel" Rel00, + coq.locate "Param00.R" R00, + Decl = ( + fun `A` (sort (typ U)) a\ + fun `A'` (sort (typ U)) a'\ + fun `PA` (app [pglobal Rel00 UI, a, a']) pa\ + fun `B` (prod `_` a _\ sort (typ U')) b\ + fun `B'` (prod `_` a' _\ sort (typ U')) b'\ + fun `PB` (prod `a` a x\ prod `a'` a' x'\ + prod `_` (app [pglobal R00 UI, a, a', pa, x, x']) _\ + app [pglobal Rel00 UI', app [b, x], app [b', x']]) pb\ + fun `f` (prod `a` a x\ app [b, x]) f\ + fun `f'` (prod `a'` a' x'\ app [b', x']) f'\ + prod `a` a t\ + prod `a'` a' t'\ + prod `aR` (app [pglobal R00 UI, a, a', pa, t, t']) tR\ + app [pglobal R00 UI', app [b, t], app [b', t'], app [pb, t, t', tR], + app [f, t], app [f', t']] + ), + @udecl! [L, L'] ff [] ff => + coq.env.add-const "R_forall" Decl _ @transparent! _. +}}. *) + +(* MapN for forall *) + +(* (00, 00) -> 00 *) +Definition Map0_forall@{i j k | i <= k, j <= k} + {A A' : Type@{i}} (PA : Param00.Rel@{i} A A') + {B : A -> Type@{j}} {B' : A' -> Type@{j}} + (PB : forall (a : A) (a' : A'), PA a a' -> Param00.Rel@{j} (B a) (B' a')) : + Map0.Has@{k} (R_forall@{i j} PA PB). +Proof. constructor. Defined. + +(* (02a, 10) -> 1 *) +Definition Map1_forall@{i j k | i <= k, 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')) : + Map1.Has@{k} (R_forall@{i j} PA PB). +Proof. + constructor. + exact (fun f a' => map (PB _ _ (comap_in_R _ _ _ 1)) (f (comap PA a'))). +Defined. + +(* (04, 2a0) -> 2a0 *) +Definition Map2a_forall@{i j k | i <= k, 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): _. +Defined. + +(* (02a, 2b0) + funext -> 2b0 *) +Definition Map2b_forall@{i j k | i <= k, 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')) : + Map2b.Has@{k} (R_forall@{i j} PA PB). +Proof. + exists (Map1.map@{k} _ (Map1_forall PA PB)). + - move=> f f' fR; apply path_forall => a'. + apply (R_in_map (PB _ _ _)); exact: fR. +Defined. + +(* (04, 30) + funext -> 30 *) +Definition Map3_forall@{i j k | i <= k, 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')) : + Map3.Has@{k} (R_forall@{i j} PA PB). +Proof. + exists (Map1.map@{k} _ (Map1_forall PA PB)). + - exact: (Map2a.map_in_R _ (Map2a_forall PA PB)). + - move=> f f' fR; apply path_forall => a'. + apply (R_in_map (PB _ _ _)); exact: fR. +Defined. + +(* (04, 40) + funext -> 40 *) +Definition Map4_forall@{i j k | i <= k, 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')) : + Map4.Has@{k} (R_forall@{i j} PA PB). +Proof. + exists + (Map1.map@{k} _ (Map1_forall PA PB)) + (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 => 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. + +(* Param_forallMN : forall A A' AR B B' BR, + ParamMN.Rel (forall a, B a) (forall a', B' a') *) + +Elpi Accumulate lp:{{ + pred generate-param-forall + i:param-class, i:univ, i:univ, i:univ.variable, i:univ.variable, + i:univ.variable. + generate-param-forall (pc M N as Class) Ui Uj Li Lj Lk :- + % we need to generate Map in both ways, so we must add the dependencies + % from both sides to get the final classes we shall ask for A and B + map-class.dep-pi M ClassAM ClassBM, + map-class.dep-pi N NegClassAN NegClassBN, + param-class.negate NegClassAN ClassAN, + param-class.negate NegClassBN ClassBN, + param-class.union ClassAM ClassAN ClassA, + ClassA = pc MA NA, + param-class.union ClassBM ClassBN ClassB, + ClassB = pc MB NB, + map-class->string M MStr, + map-class->string N NStr, + map-class->string MA MAStr, + map-class->string MB MBStr, + map-class->string NA NAStr, + map-class->string NB NBStr, + coq.univ-instance UIi [Li], + coq.univ-instance UIj [Lj], + coq.univ-instance UIk [Lk], + coq.univ-instance UIij [Li, Lj], + coq.univ-instance UIik [Li, Lk], + coq.univ-instance UIijk [Li, Lj, Lk], + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ ".Rel")} RelA, + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ ".R")} RA, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ ".Rel")} RelB, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ ".R")} RB, + coq.locate {calc ("Param" ^ MStr ^ NStr ^ ".BuildRel")} BuildRel, + coq.locate "R_forall" RForall, + coq.locate {calc ("Map" ^ MStr ^ "_forall")} MapM, + coq.locate {calc ("Map" ^ NStr ^ "_forall")} MapN, + coq.locate {calc ("eq_Map" ^ NStr)} EqMapN, + coq.locate "equiv_flip" EquivFlip, + coq.locate {calc ("Param" ^ MAStr ^ NAStr ^ "_sym")} ParamSymA, + coq.locate {calc ("Param" ^ NAStr ^ MAStr ^ ".R")} RSymA, + coq.locate {calc ("Param" ^ MBStr ^ NBStr ^ "_sym")} ParamSymB, + % build functions doing several weakenings at once + param-class.forget ClassA (pc map0 map0) ForgetA0F, + param-class.forget ClassB (pc map0 map0) ForgetB0F, + param-class.forget ClassA ClassAM ForgetADepMF, + param-class.forget ClassB ClassBM ForgetBDepMF, + param-class.forget {param-class.negate ClassA} NegClassAN ForgetADepNF, + param-class.forget {param-class.negate ClassB} NegClassBN ForgetBDepNF, + % we cut the proof into multiple parts for readability + RForallF = (a\ a'\ aR\ b\ b'\ bR\ + app [pglobal RForall UIij, + a, a', ForgetA0F UIi a a' aR, b, b', + fun `a` a x\ fun `a'` a' x'\ + fun `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + ForgetB0F UIj (app [b, x]) (app [b', x']) (app [bR, x, x', xR])] + ), + EqMapR1F = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `a'` a' x'\ app [b', x']) f'\ + fun `f` (prod `a` a x\ app [b, x]) f\ + prod `a` a x\ prod `a'` a' x'\ + prod `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + app [pglobal RB UIj, app [b, x], app [b', x'], app [bR, x, x', xR], + app [f, x], app [f', x']] + ), + EqMapR2F = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `a'` a' x'\ app [b', x']) f'\ + fun `f` (prod `a` a x\ app [b, x]) f\ + prod `a'` a' x'\ prod `a` a x\ + prod `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + app [pglobal RB UIj, app [b, x], app [b', x'], app [bR, x, x', xR], + app [f, x], app [f', x']] + ), + EqMapR1R2EquivF = (a\ a'\ aR\ b\ b'\ bR\ + fun `f'` (prod `a'` a' x'\ app [b', x']) f'\ + fun `f` (prod `a` a x\ app [b, x]) f\ + app [pglobal EquivFlip UIik, a, a', + (fun `a` a x\ fun `a'` a' x'\ + prod `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + app [pglobal RB UIj, app [b, x], app [b', x'], + app [bR, x, x', xR], + app [f, x], app [f', x']])] + ), + % there is one call to MapM_forall and one on MapN_forall on the symmetric + % relation; both can need funext depending on M and N + MapMArgsF = (a\ a'\ aR\ b\ b'\ bR\ [ + a, a', ForgetADepMF UIi a a' aR, b, b', + fun `a` a x\ fun `a'` a' x'\ + fun `aR` (app [pglobal RA UIi, a, a', aR, x, x']) xR\ + ForgetBDepMF UIj (app [b, x]) (app [b', x']) (app [bR, x, x', xR]) + ]), + MapNArgsF = (a\ a'\ aR\ b\ b'\ bR\ [ + a', a, ForgetADepNF UIi a' a (app [pglobal ParamSymA UIi, a, a', aR]), + b', b, + (fun `a'` a' x'\ fun `a` a x\ + fun `aR` (app [pglobal RSymA UIi, a', a, + app [pglobal ParamSymA UIi, a, a', aR], x', x]) xR\ + ForgetBDepNF UIj (app [b', x']) (app [b, x]) + (app [pglobal ParamSymB UIj, app [b, x], app [b', x'], + app [bR, x, x', xR]])) + ]), + if (std.mem! [map2b, map3, map4] M) ( + FunextDecl = true, + MapMF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapM UIijk, funext | MapMArgsF a a' aR b b' bR]), + if (std.mem! [map2b, map3, map4] N) ( + MapNF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk, funext | MapNArgsF a a' aR b b' bR]) + ) ( + MapNF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk | MapNArgsF a a' aR b b' bR]) + ) + ) ( + MapMF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapM UIijk | MapMArgsF a a' aR b b' bR]), + if (std.mem! [map2b, map3, map4] N) ( + FunextDecl = true, + MapNF = (funext\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk, funext | MapNArgsF a a' aR b b' bR]) + ) ( + FunextDecl = false, + MapNF = (_\ a\ a'\ aR\ b\ b'\ bR\ + app [pglobal MapN UIijk | MapNArgsF a a' aR b b' bR]) + ) + ), + % ParamMN_forall proof + DeclF = (funext\ + fun `A` (sort (typ Ui)) a\ + fun `A'` (sort (typ Ui)) a'\ + fun `AR` (app [pglobal RelA UIi, a, a']) aR\ + fun `B` (prod `_` a _\ sort (typ Uj)) b\ + fun `B'` (prod `_` a' _\ sort (typ Uj)) b'\ + fun `BR` + (prod `a` a x\ prod `a'` a' x'\ + prod `_` (app [pglobal RA UIi, a, a', aR, x, x']) _\ + app [pglobal RelB UIj, app [b, x], app [b', x']]) bR\ + app [pglobal BuildRel UIk, + (prod `a` a x\ app [b, x]), + (prod `a'` a' x'\ app [b', x']), + RForallF a a' aR b b' bR, + MapMF funext a a' aR b b' bR, + app [pglobal EqMapN UIk, + (prod `a'` a' x'\ app [b', x']), + (prod `a` a x\ app [b, x]), + EqMapR1F a a' aR b b' bR, + EqMapR2F a a' aR b b' bR, + EqMapR1R2EquivF a a' aR b b' bR, + MapNF funext a a' aR b b' bR]] + ), + % add an additional binder for funext in case it is needed + if (FunextDecl) ( + coq.locate "Funext" Funext, + Decl = (fun `H` (global Funext) funext\ DeclF funext) + ) ( + Dummy = (fun `x` (sort (typ Ui)) x\ x), + Decl = DeclF Dummy + ), + 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 => + coq.env.add-const ParamForall Decl _ @transparent! Const, + coq.elpi.accumulate _ "param.db" (clause _ (after "default-param-forall") + (param.db.param-forall Class Const)). +}}. +Elpi Typecheck. + +Elpi Query lp:{{ + coq.univ.new Ui, + coq.univ.variable Ui Li, + coq.univ.new Uj, + coq.univ.variable Uj Lj, + coq.univ.max Ui Uj Uk, + % cannot have only 2 binders in the declaration because this line creates a fresh level: + coq.univ.variable Uk Lk, + Classes = [map0, map1, map2a, map2b, map3, map4], + std.forall Classes (m\ + std.forall Classes (n\ + generate-param-forall (pc m n) Ui Uj Li Lj Lk + ) + ). +}}. + +(* Set Printing Universes. About Param2a1_forall. +Set Printing Universes. About Param2b1_forall. +Set Printing Universes. About Param33_forall. *) diff --git a/theories/Param_option.v b/theories/Param_option.v new file mode 100644 index 0000000..41d2628 --- /dev/null +++ b/theories/Param_option.v @@ -0,0 +1,163 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Inductive option (A : Type) : Type := + | none + | some : A -> option A. + +Inductive optionR A A' (AR : A -> A' -> Type) : option A -> option A' -> Type := + | noneR : optionR none none + | someR a a' (aR : AR a a') : optionR (some a) (some a'). + +(* *) + +Definition prod_map + (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') : + A * B -> A' * B' := + fun p => + match p with + | (a, b) => (map AR a, map BR b) + end. + +(* *) + +Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) : + (a1, b1) = (a2, b2) -> a1 = a2 := + fun e => + match e in @paths _ _ (a, b) return _ = a with + | @idpath _ _ => @idpath _ a1 + end. + +Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) : + (a1, b1) = (a2, b2) -> b1 = b2 := + fun e => + match e in @paths _ _ (a, b) return _ = b with + | @idpath _ _ => @idpath _ b1 + end. + +Definition prod_map_in_R + (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') : + forall p p', prod_map A A' AR B B' BR p = p' -> prodR A A' AR B B' 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 + a a' (map_in_R AR a a' (pair_inj1 A' B' (map AR a) a' (map BR b) b' e)) + b b' (map_in_R BR b b' (pair_inj2 A' B' (map AR a) a' (map BR b) b' e)) + end + end. + +(* *) + +Definition prod_R_in_map + (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') : + forall p p', prodR A A' AR B B' BR p p' -> prod_map A A' AR B B' BR p = p' := + fun p p' r => + match r with + | pairR a a' aR b b' bR => + @transport _ (fun t => (t, map BR b) = (a', b')) _ _ (R_in_map AR a a' aR)^ + (@transport _ (fun t => (a', t) = (a', b')) _ _ (R_in_map BR b b' bR)^ idpath) + end. + +(* *) + +Definition ap2 : forall {A B C : Type} {a a' : A} {b b' : B} (f : A -> B -> C), + a = a' -> b = b' -> f a b = f a' b' := + fun A B C a a' b b' f e1 e2 => + match e1 with + | idpath => + match e2 with + | idpath => idpath + end + end. + +Definition prod_R_in_mapK + (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') : + forall p p' (r : prodR A A' AR B B' 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. + +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). +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). +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). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). +Defined. + +Definition Map2b_prod A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') : + Map2b.Has (prodR A A' AR B B' BR). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). +Defined. + +Definition Map3_prod A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') : + Map3.Has (prodR A A' AR B B' BR). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). +Defined. + +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). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). + - exact (prod_R_in_mapK A A' AR B B' BR). +Defined. diff --git a/theories/Param_paths.v b/theories/Param_paths.v new file mode 100644 index 0000000..387cd1d --- /dev/null +++ b/theories/Param_paths.v @@ -0,0 +1,181 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +Require Import HoTT_additions Hierarchy. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Inductive pathsR@{i} + (A A' : Type@{i}) (AR : A -> A' -> Type@{i}) (x : A) (x' : A') (xR : AR x x') : + forall (y : A) (y' : A') (yR : AR y y'), x = y -> x' = y' -> Type@{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') + (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') + (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 A A' AR x x' xR y y' yR e = e' -> pathsR A A' AR x x' xR y y' yR e e'. +Proof. + intros e e'. + destruct e. + destruct e'. + exact (fun H => + transport (fun t => pathsR A A' AR x x' xR x x' t 1%path 1%path) + ((R_in_mapK AR x x' xR)^ @ + ap (map_in_R AR x x') + ((inv_V (R_in_map AR x x' xR))^ @ + inverse2 + ((concat_p1 (R_in_map AR x x' xR)^)^ @ + (moveL_1V ((R_in_map AR x x' xR)^ @ 1) (R_in_map AR x x' yR) H)) + @ (inv_V (R_in_map AR x x' yR))) + @ (R_in_mapK AR x x' yR)) + (idpathR A A' AR x x' xR)). +Defined. + +Definition paths_R_in_map@{i} + (A A' : Type@{i}) (AR : Param2b0.Rel 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'), + pathsR A A' AR x x' xR y y' yR e e' -> paths_map A A' AR x x' xR y y' yR e = e'. +Proof. + intros e e' r. + destruct r. + unfold paths_map. + simpl. + apply moveR_pM. + unshelve refine (concat _ _). + - exact (R_in_map AR x x' xR)^. + - apply concat_p1. + - apply inverse. apply concat_1p. +Defined. + +Definition paths_R_in_mapK@{i} + (A A' : Type@{i}) (AR : Param40.Rel 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. +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. + +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') : + Map0.Has (pathsR A A' AR x x' xR y y' yR). +Proof. constructor. Defined. + +Definition Map1_paths + A A' (AR : Param2b0.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : + Map1.Has (pathsR A A' AR x x' xR y y' yR). +Proof. constructor. exact (paths_map A A' AR x x' xR y y' yR). Defined. + +Definition Map2a_paths + A A' (AR : Param40.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : + Map2a.Has (pathsR A A' AR x x' xR y y' yR). +Proof. + unshelve econstructor. + - exact (paths_map A A' AR x x' xR y y' yR). + - exact (paths_map_in_R A A' AR x x' xR y y' yR). +Defined. + +Definition Map2b_paths + A A' (AR : Param2b0.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : + Map2b.Has (pathsR A A' AR x x' xR y y' yR). +Proof. + unshelve econstructor. + - exact (paths_map A A' AR x x' xR y y' yR). + - exact (paths_R_in_map A A' AR x x' xR y y' yR). +Defined. + +Definition Map3_paths + A A' (AR : Param40.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : + Map3.Has (pathsR A A' AR x x' xR y y' yR). +Proof. + unshelve econstructor. + - exact (paths_map A A' AR x x' xR y y' yR). + - exact (paths_map_in_R A A' AR x x' xR y y' yR). + - exact (paths_R_in_map A A' AR x x' xR y y' yR). +Defined. + +Definition Map4_paths + A A' (AR : Param40.Rel A A') (x : A) (x' : A') (xR : AR x x')(y : A) (y' : A') (yR : AR y y') : + Map4.Has (pathsR A A' AR x x' xR y y' yR). +Proof. + unshelve econstructor. + - exact (paths_map A A' AR x x' xR y y' yR). + - exact (paths_map_in_R A A' AR x x' xR y y' yR). + - exact (paths_R_in_map A A' AR x x' xR y y' yR). + - exact (paths_R_in_mapK A A' AR x x' xR y y' yR). +Defined. + +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 <~> + 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. + unshelve econstructor. + - intros []; apply idpathR. + - unshelve econstructor. + + intros []; apply idpathR. + + intros []; reflexivity. + + intros []; reflexivity. + + intros []; reflexivity. +Defined. + +Definition Param01_paths@{i} + (A A' : Type@{i}) (AR : Param02b.Rel@{i} A A') + (a1 : A) (a1' : A') (a1R : AR a1 a1') (a2 : A) (a2' : A') (a2R : AR a2 a2') : + Param01.Rel@{i} (a1 = a2) (a1' = a2'). +Proof. + unshelve econstructor. + - exact (pathsR A A' AR a1 a1' a1R a2 a2' a2R). + - exact (Map0_paths A A' AR a1 a1' a1R a2 a2' a2R). + - apply (@eq_Map1 _ _ _ _ (pathsR_sym A A' AR a1 a1' a1R a2 a2' a2R)). + exact (Map1_paths A' A (Param02b_sym A A' AR) a1' a1 a1R a2' a2 a2R). +Defined. + +Definition Param10_paths@{i} + (A A' : Type@{i}) (AR : Param2b0.Rel@{i} A A') + (a1 : A) (a1' : A') (a1R : AR a1 a1') (a2 : A) (a2' : A') (a2R : AR a2 a2') : + Param10.Rel@{i} (a1 = a2) (a1' = a2'). +Proof. + unshelve econstructor. + - exact (pathsR A A' AR a1 a1' a1R a2 a2' a2R). + - exact (Map1_paths A A' AR a1 a1' a1R a2 a2' a2R). + - constructor. +Defined. + +(* todo generator *) \ No newline at end of file diff --git a/theories/Param_prod.v b/theories/Param_prod.v new file mode 100644 index 0000000..17f03ac --- /dev/null +++ b/theories/Param_prod.v @@ -0,0 +1,159 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +Require Import 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'). + +(* *) + +Definition prod_map + (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') : + A * B -> A' * B' := + fun p => + match p with + | (a, b) => (map AR a, map BR b) + end. + +(* *) + +Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) : + (a1, b1) = (a2, b2) -> a1 = a2 := + fun e => + match e in @paths _ _ (a, b) return _ = a with + | @idpath _ _ => @idpath _ a1 + end. + +Definition pair_inj2 A B (a1 a2 : A) (b1 b2 : B) : + (a1, b1) = (a2, b2) -> b1 = b2 := + fun e => + match e in @paths _ _ (a, b) return _ = b with + | @idpath _ _ => @idpath _ b1 + end. + +Definition prod_map_in_R + (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') : + forall p p', prod_map A A' AR B B' BR p = p' -> prodR A A' AR B B' 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 + a a' (map_in_R AR a a' (pair_inj1 A' B' (map AR a) a' (map BR b) b' e)) + b b' (map_in_R BR b b' (pair_inj2 A' B' (map AR a) a' (map BR b) b' e)) + end + end. + +(* *) + +Definition prod_R_in_map + (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') : + forall p p', prodR A A' AR B B' BR p p' -> prod_map A A' AR B B' BR p = p' := + fun p p' r => + match r with + | pairR a a' aR b b' bR => + @transport _ (fun t => (t, map BR b) = (a', b')) _ _ (R_in_map AR a a' aR)^ + (@transport _ (fun t => (a', t) = (a', b')) _ _ (R_in_map BR b b' bR)^ idpath) + end. + +(* *) + +Definition ap2 : forall {A B C : Type} {a a' : A} {b b' : B} (f : A -> B -> C), + a = a' -> b = b' -> f a b = f a' b' := + fun A B C a a' b b' f e1 e2 => + match e1 with + | idpath => + match e2 with + | idpath => idpath + end + end. + +Definition prod_R_in_mapK + (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') : + forall p p' (r : prodR A A' AR B B' 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. + +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). +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). +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). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). +Defined. + +Definition Map2b_prod A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') : + Map2b.Has (prodR A A' AR B B' BR). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). +Defined. + +Definition Map3_prod A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') : + Map3.Has (prodR A A' AR B B' BR). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). +Defined. + +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). +Proof. + unshelve econstructor. + - exact (prod_map A A' AR B B' BR). + - exact (prod_map_in_R A A' AR B B' BR). + - exact (prod_R_in_map A A' AR B B' BR). + - exact (prod_R_in_mapK A A' AR B B' BR). +Defined. diff --git a/theories/Trocq.v b/theories/Trocq.v new file mode 100644 index 0000000..ec8e117 --- /dev/null +++ b/theories/Trocq.v @@ -0,0 +1,16 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Trocq Require Export + HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param + Param_paths. diff --git a/theories/Uparam.v b/theories/Uparam.v new file mode 100644 index 0000000..f6184fd --- /dev/null +++ b/theories/Uparam.v @@ -0,0 +1,207 @@ +(**************************************************************************************************) +(* * 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 the *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * (see LICENSE file for the text of the license) *) +(**************************************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. + +Require Import HoTT_additions. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +(*****************) +(* Specific Code *) +(*****************) + +Record map_graph (A B : Type@{i}) (R : A -> B -> Type@{i}) := MapGraph{ + _map : A -> B; + _map_in_R : forall (a : A) (b : B), _map a = b -> R a b; + _R_in_map : forall (a : A) (b : B), R a b -> _map a = b; + _R_in_mapK : forall (a : A) (b : B), + _map_in_R a b o _R_in_map a b == idmap}. + +Arguments map_graph {A B} _. +Arguments MapGraph {A B} _. +Arguments _map {A B R} _. +Arguments _map_in_R {A B R} _. +Arguments _R_in_map {A B R} _. +Arguments _R_in_mapK {A B R} _. + +Structure uparam@{i} (A B : Type@{i}) := Uparam { + _R :> A -> B -> Type@{i}; + _covariant : map_graph _R; + _contravariant : map_graph (sym_rel _R); +}. + +Arguments Uparam {_ _}. +Arguments _R {_ _} _. +Arguments _covariant {_ _} _. +Arguments _contravariant {_ _} _. + +Section Uparam. +Context {A B : Type} (r : uparam A B). + +Definition map := _map (_covariant r). +Definition map_in_R := _map_in_R (_covariant r). +Definition R_in_map := _R_in_map (_covariant r). +Definition R_in_mapK := _R_in_mapK (_covariant r). + +Definition comap := _map (_contravariant r). +Definition comap_in_R := _map_in_R (_contravariant r). +Definition R_in_comap := _R_in_map (_contravariant r). +Definition R_in_comapK := _R_in_mapK (_contravariant r). + +End Uparam. + +Lemma map_graph_equiv_sigma (A B : Type@{i}) (R : A -> B -> Type@{i}) : + map_graph 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. + +Lemma map_graph_equiv_isfun `{Funext} {A B : Type@{i}} + (R : A -> B -> Type@{i}) : map_graph R <~> IsFun R. +Proof. +apply (equiv_composeR' (map_graph_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. +Defined. + +Lemma map_graph_isprop `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : + IsHProp (map_graph R). +Proof. +apply (istrunc_equiv_istrunc (IsFun R)); last exact: isfun_isprop. +apply symmetric_equiv; apply map_graph_equiv_isfun. +Qed. + +Lemma uparam_equiv `{Univalence} {A B : Type} : uparam A B <~> (A <~> B). +Proof. +apply (equiv_compose' equiv_sig_relequiv^-1). +unshelve eapply equiv_adjointify. +- move=> [R mR msR]; exists R; exact: map_graph_equiv_isfun. +- move=> [R mR msR]; exists R; exact: (map_graph_equiv_isfun _)^-1%equiv. +- by move=> [R mR msR]; rewrite !equiv_invK. +- by move=> [R mR msR]; rewrite !equiv_funK. +Defined. + +Definition id_map_graph {A : Type} : @map_graph A A (@paths A) := + MapGraph _ idmap (fun a b r => r) (fun a b r => r) (fun a b r => 1%path). + +Definition id_sym_map_graph {A : Type} : @map_graph A A (sym_rel (@paths A)) := + MapGraph _ idmap (fun a b r => r^) (fun a b r => r^) (fun a b r => inv_V r). + +Definition id_uparam {A : Type} : uparam A A := + Uparam (@paths A) id_map_graph id_sym_map_graph. + +Lemma uparam_induction `{Univalence} A (P : forall B, uparam 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. Qed. + +Definition map_graph_Type `{Univalence} : @map_graph Type@{i} Type@{i} uparam. +Proof. +unshelve refine (MapGraph _ idmap (fun a b e => e # id_uparam) _ _). + { 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 sym_map_graph_Type `{Univalence} : @map_graph Type@{i} Type@{i} (sym_rel uparam). +Proof. +unshelve refine (MapGraph _ idmap (fun a b e => e # id_uparam) _ _). + { 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. + +Definition uparam_Type `{Univalence} : uparam Type@{i} Type@{i} := + Uparam _ map_graph_Type sym_map_graph_Type. + +Lemma R_uparam_Type `{Univalence} : (uparam_Type : _ -> _ -> _) = uparam. +Proof. reflexivity. Defined. + +Lemma map_uparam_Type `{Univalence} : map uparam_Type = id. +Proof. reflexivity. Defined. + +Lemma comap_uparam_Type `{Univalence} : comap uparam_Type = id. +Proof. reflexivity. Defined.