From 7ede4519cc89fef27cdac28bdfc6493cd01bae86 Mon Sep 17 00:00:00 2001
From: Enzo Crance <enzo.crance@inria.fr>
Date: Fri, 5 Jan 2024 16:53:32 +0100
Subject: [PATCH] :memo: Example int Zp

---
 artifact-doc/TUTORIAL.md | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/artifact-doc/TUTORIAL.md b/artifact-doc/TUTORIAL.md
index e6e6812..3a8ab1e 100644
--- a/artifact-doc/TUTORIAL.md
+++ b/artifact-doc/TUTORIAL.md
@@ -73,28 +73,19 @@ The `peano_bin_nat.v` file contains this example but remarks that the isomorphis
 
 #### Modular arithmetic (`int_to_Zp.v`)
 
-todo
-
-<!-- ```coq
-Lemma Radd : forall (x : Zp) (x' : int) (xR : Rp x x') (y : Zp) (y' : int) (yR : Rp y y'), Rp (x + y)%Zp (x' + y')%int.
-Proof. (...) Qed.
-
-Trocq Use Radd.
+In this example, we study a *directed* relation between unary integers (`int`) and integers modulo a constant $p$. Indeed, it is directed because the types are not fully equivalent and thus a relation at level $(4, 4)$ of the hierarchy cannot be stated between them. We know that two functions `modp : Zmodp -> int` and `reprp : Zmodp -> int` can be defined and the following property holds:
+```coq
+forall x, modp (reprp x) = x
 ```
-will enable the translation of the addition over type Zp (integers mod p) to type int (integers) because Rp is defined as the embedding of an integer mod p into int via a suitable `pmap` function:
-
+The graph of `modp` is therefore a surjective relation, and through the `SplitSurj` module we can build a parametricity relation `Rp : Param2a4.Rel Zmodp int`, which can be added to Trocq with the following command:
 ```coq
-Definition Rp (x : Zp) (n : int) := pmap x = n.
+Trocq Use Rp.
 ```
-
-As soon as Rp is equipped with the suitable structure (which is not an equivalence in this case!), we can use it to transfer to Zp the obvious consequences of the arithemtic on integers. For instance:
+After adding to Trocq a proof relating additions in both encodings and a proof relating equality to itself at level $(0,1)$, with 2 further calls to `Trocq Use`, we can transfer the following goal to the statement of commutativity of addition over `int`:
 ```coq
-Goal (forall x y, x + y = y + x)%Zp.
-Proof.
-trocq. (* here we obtain the corresponding goal type int *)
-apply int_add_comm. (* here we use the commutativity of addition on  type int *)
-Qed.
-``` -->
+(forall x y, x + y = y + x)%Zmodp.
+```
+As `int` is defined in the MathComp library, this property is already proved and comes under the name `addC`. We can therefore close the goal and get commutativity of addition over `Zmodp` "for free".
 
 #### Bitwise arithmetic (`Vector_tuple.v`)