example of transfer of nat_rec to an abtract type + bugfix

_CoqProject

@@ -33,3 +33,4 @@ examples/summable.v
 examples/trocq_setoid_rewrite.v
 examples/Vector_tuple.v
 examples/misc.v
+exmaples/nat_ind.v

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.
 

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,12 +75,12 @@ 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
-  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'.
@@ -155,13 +155,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

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) <=> (

elpi/param.elpi

@@ -33,32 +33,32 @@ pred fresh-type.
 % ==================================================================================================
 
 % ParamSub + ParamConst
-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
-    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 _))
   ).
 
-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) (
     % 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,
+    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))
   ).

elpi/util.elpi

@@ -86,8 +86,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

examples/nat_ind.v

@@ -0,0 +1,53 @@
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *       Copyright (C) 2023 Inria & MERCE       *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <[email protected]>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <[email protected]>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <[email protected]>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * 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.