From d6a0fbc9903023cd0661dff00666fbdbe8bf3c70 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 23 Jan 2024 17:23:31 +0100 Subject: [PATCH 1/4] Finer-grained hierarchy for list --- theories/Param_list.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/theories/Param_list.v b/theories/Param_list.v index 199eeae..2488d0e 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,16 @@ 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 Param33_list (A A' : Type) (AR : Param33.Rel A A') : Param33.Rel (list A) (list A'). Proof. unshelve econstructor. From b542c99e0069f7cfef90182520f45414fe268235 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 23 Jan 2024 17:49:35 +0100 Subject: [PATCH 2/4] Stuck translation --- examples/stuck.v | 57 +++++++++++++++++++++++++++++++++++++++++++ theories/Param_list.v | 28 ++++++++++++++++++++- 2 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 examples/stuck.v diff --git a/examples/stuck.v b/examples/stuck.v new file mode 100644 index 0000000..f0ff441 --- /dev/null +++ b/examples/stuck.v @@ -0,0 +1,57 @@ +(*****************************************************************************) +(* * 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. + +Module Stuck. + +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. +Trocq Use Param44_list Param_cons Param_nil. + +Goal forall (l : list Zmodp), l = l. +Fail trocq. +Abort. + +End Stuck. + +Module Works. + +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. +Trocq Use Param2a4_list Param_cons Param_nil. + +Goal forall (l : list Zmodp), l = l. +trocq. +Abort. + +End Works. + + diff --git a/theories/Param_list.v b/theories/Param_list.v index 2488d0e..b77608c 100644 --- a/theories/Param_list.v +++ b/theories/Param_list.v @@ -153,6 +153,23 @@ Proof. + 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. @@ -172,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 From 85296576dfa90a9f25f7d77ebe697ee23e5571c3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 23 Jan 2024 17:54:11 +0100 Subject: [PATCH 3/4] refactoring --- examples/stuck.v | 22 +++++++--------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/examples/stuck.v b/examples/stuck.v index f0ff441..08f2974 100644 --- a/examples/stuck.v +++ b/examples/stuck.v @@ -20,17 +20,17 @@ Set Universe Polymorphism. Local Open Scope int_scope. Local Open Scope Zmodp_scope. -Module Stuck. - 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. -Trocq Use Param44_list Param_cons Param_nil. +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. @@ -39,19 +39,11 @@ End Stuck. Module Works. -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. -Trocq Use Param2a4_list Param_cons Param_nil. - +Trocq Use Param2a4_list. Goal forall (l : list Zmodp), l = l. trocq. -Abort. +reflexivity. +Qed. End Works. - From 766a5d26f0081fb229cd7e6d3919c570f84db7aa Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 24 Jan 2024 16:54:38 +0100 Subject: [PATCH 4/4] adding claim --- artifact-doc/CLAIMS.md | 4 ++++ 1 file changed, 4 insertions(+) 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$.