From 793e10106326943d132ec0ed13a621894dcbfc60 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 12 Jan 2024 11:18:57 +0100 Subject: [PATCH] example of transfer of nat_rec to an abtract type + bugfix --- _CoqProject | 1 + artifact-doc/CLAIMS.md | 1 + elpi/constraints/constraint-graph.elpi | 11 +++--- elpi/constraints/constraints.elpi | 13 ++++--- elpi/param.elpi | 16 ++++---- elpi/util.elpi | 5 ++- examples/nat_ind.v | 53 ++++++++++++++++++++++++++ 7 files changed, 79 insertions(+), 21 deletions(-) create mode 100644 examples/nat_ind.v diff --git a/_CoqProject b/_CoqProject index 12de94b..61d974e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -33,3 +33,4 @@ examples/summable.v examples/trocq_setoid_rewrite.v examples/Vector_tuple.v examples/misc.v +examples/nat_ind.v \ No newline at end of file diff --git a/artifact-doc/CLAIMS.md b/artifact-doc/CLAIMS.md index 65bf8d9..2afd76e 100644 --- a/artifact-doc/CLAIMS.md +++ b/artifact-doc/CLAIMS.md @@ -25,6 +25,7 @@ As explained in the paper, univalent parametricity makes use of the univalence a ### Trocq handles non-bijective relations. In the `int_to_Zp.v` file, we present proof transfer done by Trocq on a goal featuring integers modulo a hypothetical constant $p$, which is not equivalent to the whole set of integers, but a weaker relation — a split surjection — can still be stated between them. Whereas tools like univalent parametricity propagate type equivalences everywhere, Trocq can handle more diverse relations in a finer-grained way. +Another supporting evidence is in `nat_ind.v` where we show any type `I` with abstract zero and successor and a split surjection from `nat` compatible with zero and successor, can be endowed with an induction principle similar to the one of `nat`. ### Trocq supports polymorphism and dependent types. diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi index 4d5ca30..5e9d94b 100644 --- a/elpi/constraints/constraint-graph.elpi +++ b/elpi/constraints/constraint-graph.elpi @@ -38,7 +38,7 @@ 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.gref gref -> term -> term -> gref -> constraint-type. type ct.geq constraint-type. typeabbrev @@ -75,13 +75,13 @@ add-dep-type ID IDR (constraint-graph G) (constraint-graph G') :- % 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, + i:class-id, i:gref, i:term, i:term, 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') :- +add-dep-gref ID GR T Tm' 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 % TODO: rename utility functions to add-earlier-node / add-later-node? - util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T GR' GRR) IDs)) G G1, + util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T Tm' 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'. @@ -156,13 +156,14 @@ instantiate.aux ID Class (node.var ct.type [IDR]) G G' :- 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' :- +instantiate.aux ID Class (node.var (ct.gref GR T Tm' 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 trocq.db.gref GR Class Cs GR' GRR, !, + coq.env.global GR' Tm', % make sure the classes are consistent instantiate.gref IDs TCs Cs G1 G'. pred instantiate.gref diff --git a/elpi/constraints/constraints.elpi b/elpi/constraints/constraints.elpi index 46b0cfc..41f3d0f 100644 --- a/elpi/constraints/constraints.elpi +++ b/elpi/constraints/constraints.elpi @@ -65,16 +65,17 @@ dep-type C CR :- (geq CR (pc map4 map4)). % D_K(C, C_1, ..., C_n) -pred dep-gref i:gref, i:term, o:gref, o:gref. -dep-gref GR T GR' GRR :- +pred dep-gref i:gref, i:term, o:term, o:gref. +dep-gref GR T Tm' 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) [_] + declare_constraint (internal.c.dep-gref ID GR T Tm' GRR IDs) [_] ) ( trocq.db.gref GR Out Cs GR' GRR, !, + coq.env.global GR' Tm', !, std.forall2 TCs Cs eq ). @@ -188,7 +189,7 @@ pred c.graph o: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.dep-gref o:class-id, o:gref, o:term, o:term, 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 @@ -207,8 +208,8 @@ constraint c.graph c.dep-pi c.dep-arrow c.dep-type c.dep-gref c.geq c.reduce-gra 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', + rule \ (c.graph G) (c.dep-gref ID GR T Tm' GRR IDs) <=> ( + cstr-graph.add-dep-gref ID GR T Tm' GRR IDs G G', declare_constraint (c.graph G') [_] ). rule \ (c.graph G) (c.geq IDorC1 IDorC2) <=> ( diff --git a/elpi/param.elpi b/elpi/param.elpi index eee90fe..5e2b8df 100644 --- a/elpi/param.elpi +++ b/elpi/param.elpi @@ -33,33 +33,33 @@ pred fresh-type. % ================================================================================================== % TrocqConv + TrocqConst -param (global GR) T' (global GR') GrefR :- !, +param (global GR) T' Tm' 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 % (we do not want to annot.typecheck several times a same constant, because it creates % fresh class variables twice, which would split the information) - cstr.dep-gref GR T' GR' GRR, - GrefR = global GRR + cstr.dep-gref GR T' Tm' GRR, + GrefR = pglobal GRR _ ) ( annot.typecheck (global GR) T, annot.sub-type T T', - cstr.dep-gref GR T GR' GRR, + cstr.dep-gref GR T Tm' GRR, weakening T T' (wfun W), - GrefR = (W (global GRR)) + GrefR = (W (pglobal GRR _)) ). % universe-polymorphic case -param (pglobal GR UI) T' (pglobal GR' UI) GrefR :- !, +param (pglobal GR UI) T' Tm' GrefR :- !, util.when-debug dbg.steps (coq.say "param/const" GR "@" T'), if (fresh-type) ( - cstr.dep-gref GR T' GR' GRR, + cstr.dep-gref GR T' Tm' GRR, GrefR = pglobal GRR UI ) ( annot.typecheck (pglobal GR UI) T, annot.sub-type T T', - cstr.dep-gref GR T GR' GRR, + cstr.dep-gref GR T Tm' GRR, weakening T T' (wfun W), GrefR = (W (pglobal GRR UI)) ). diff --git a/elpi/util.elpi b/elpi/util.elpi index fb512f9..569c3f8 100644 --- a/elpi/util.elpi +++ b/elpi/util.elpi @@ -88,8 +88,9 @@ delete _ [] []. % subst-gref T GR' T' % substitutes GR for GR' in T if T = (global GR) or (pglobal GR I) pred subst-gref i:term, i:gref, o:term. -subst-gref (global _) GR' (global GR'). -subst-gref (pglobal _ I) GR' (pglobal GR' I). +subst-gref (global _) GR' Tm' :- !, coq.env.global GR' Tm'. +subst-gref (pglobal _ I) GR' Tm' :- !, + @uinstance! I => coq.env.global GR' Tm'. subst-gref T _ _ :- coq.error T "is not a gref". } % util diff --git a/examples/nat_ind.v b/examples/nat_ind.v new file mode 100644 index 0000000..86d6838 --- /dev/null +++ b/examples/nat_ind.v @@ -0,0 +1,53 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 Inria & MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * This file is distributed under the terms of *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * see LICENSE file for the text of the license *) +(*****************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. + +Set Universe Polymorphism. + +Section IndType. +Variables (I : Type) (I0 : I) (IS : I -> I). +Variables (to_nat : I -> nat) (of_nat : nat -> I). + +Hypothesis to_natK : forall x, of_nat (to_nat x) = x. +Hypothesis of_nat0 : of_nat O = I0. +Hypothesis of_natS : forall x n, of_nat n = x -> of_nat (S n) = IS x. + +(* We only need/ (2a,3) which is morally that Nmap is a split injection *) +Definition RI : Param2a3.Rel I nat := + SplitSurj.toParamSym (SplitSurj.Build to_natK). + +Definition RI0 : RI I0 O. Proof. exact of_nat0. Qed. +Definition RIS m n : RI m n -> RI (IS m) (S n). Proof. exact: of_natS. Qed. + +Trocq Use RI. +Trocq Use RI0. +Trocq Use RIS. + +Lemma I_Srec : forall (P : I -> Type), P I0 -> + (forall n, P n -> P (IS n)) -> forall n, P n. +Proof. + trocq. + (* 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. + +End IndType. + +Check I_Srec. +Print I_Srec. +Print Assumptions I_Srec.