Merge pull request #34 from coq-community/list-finegrained

Finer-grained hierarchy for list

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$.

examples/stuck.v

@@ -0,0 +1,49 @@
+(*****************************************************************************)
+(*                            *                    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 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.
+

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.
+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.