diff --git a/artifact-doc/CLAIMS.md b/artifact-doc/CLAIMS.md index 2afd76e..f7cd95a 100644 --- a/artifact-doc/CLAIMS.md +++ b/artifact-doc/CLAIMS.md @@ -27,6 +27,10 @@ As explained in the paper, univalent parametricity makes use of the univalence a 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 can get stuck if the wrong translation is picked + +In the `stuck.v` file, we show that assuming that lists preserves equivalences `Param44_list` is too strong and that we need to have other preservation properties such as `Param2a4_list`, that are thus incomparable between themselves through the weakening relation. + ### Trocq supports polymorphism and dependent types. The `Vector_tuple.v` file defines a type equivalence between fixed-size vectors and iterated tuples, which are both implemented in Coq using polymorphism — elements inside these data structures can be anything — and dependent types — to ensure the size is a fixed integer $n$. diff --git a/examples/stuck.v b/examples/stuck.v new file mode 100644 index 0000000..08f2974 --- /dev/null +++ b/examples/stuck.v @@ -0,0 +1,49 @@ +(*****************************************************************************) +(* * 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 Trocq Require Import Trocq Param_list. +From Trocq_examples Require Import int_to_Zp. + +Set Universe Polymorphism. + +Local Open Scope int_scope. +Local Open Scope Zmodp_scope. + +Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). + +Axiom Rzero : Rp zerop zero. +Variable Radd : binop_param Rp Rp Rp addp add. +Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. + +Trocq Use Rp Param01_paths Param10_paths Radd Rzero Param_cons Param_nil. + +Module Stuck. + +Trocq Use Param44_list. +Goal forall (l : list Zmodp), l = l. +Fail trocq. +Abort. + +End Stuck. + +Module Works. + +Trocq Use Param2a4_list. +Goal forall (l : list Zmodp), l = l. +trocq. +reflexivity. +Qed. + +End Works. + diff --git a/theories/Param_list.v b/theories/Param_list.v index 199eeae..b77608c 100644 --- a/theories/Param_list.v +++ b/theories/Param_list.v @@ -62,6 +62,20 @@ Definition R_in_map_list (A A' : Type) (AR : Param2b0.Rel A A') : end end. +Definition Map2a_list (A A' : Type) (AR : Param2a0.Rel A A') : Map2a.Has (listR A A' AR). +Proof. + unshelve econstructor. + - exact (map_list A A' AR). + - exact (map_in_R_list A A' AR). +Defined. + +Definition Map2b_list (A A' : Type) (AR : Param2b0.Rel A A') : Map2b.Has (listR A A' AR). +Proof. + unshelve econstructor. + - exact (map_list A A' AR). + - exact (R_in_map_list A A' AR). +Defined. + Definition Map3_list (A A' : Type) (AR : Param30.Rel A A') : Map3.Has (listR A A' AR). Proof. unshelve econstructor. @@ -129,6 +143,33 @@ Proof. - constructor. Defined. +Definition Param42a_list (A A' : Type) (AR : Param42a.Rel A A') : Param42a.Rel (list A) (list A'). +Proof. + unshelve econstructor. + - exact (listR A A' AR). + - exact (Map4_list A A' AR). + - refine (eq_Map2a _ _). + + apply listR_sym. + + exact (Map2a_list A' A (Param2a2a_sym _ _ AR)). +Defined. + + +Definition Param42b_list (A A' : Type) (AR : Param42b.Rel A A') : Param42b.Rel (list A) (list A'). +Proof. + unshelve econstructor. + - exact (listR A A' AR). + - exact (Map4_list A A' AR). + - refine (eq_Map2b _ _). + + apply listR_sym. + + exact (Map2b_list A' A (Param2b2b_sym _ _ AR)). +Defined. + +Definition Param2a4_list (A A' : Type) (AR : Param2a4.Rel A A') : + Param2a4.Rel (list A) (list A') := Param42a_sym _ _ (Param42a_list _ _ (Param2a4_sym _ _ AR)). + +Definition Param2b4_list (A A' : Type) (AR : Param2b4.Rel A A') : + Param2b4.Rel (list A) (list A') := Param42b_sym _ _ (Param42b_list _ _ (Param2b4_sym _ _ AR)). + Definition Param33_list (A A' : Type) (AR : Param33.Rel A A') : Param33.Rel (list A) (list A'). Proof. unshelve econstructor. @@ -148,4 +189,13 @@ Proof. - refine (eq_Map4 _ _). + apply listR_sym. + exact (Map4_list A' A (Param44_sym _ _ AR)). -Defined. \ No newline at end of file +Defined. + + +Definition Param_nil : forall (A A' : Type) (AR : Param00.Rel A A'), + listR A A' AR (@nil A) (@nil A') := @nilR. + +Definition Param_cons : forall (A A' : Type) (AR : Param00.Rel A A') + (a : A) (a' : A') (aR : AR a a') + (l : list A) (l' : list A') (lR : listR A A' AR l l'), + listR A A' AR (cons a l) (cons a' l') := @consR. \ No newline at end of file