Merge pull request rocq-community#58 from rocq-community/minor-tutorial-updates

Minor tutorial updates

Author: CohenCyril

README.md

@@ -77,7 +77,7 @@ in the [INSTALL.md file](INSTALL.md).
 
 ## Documentation
 
-See the [tutorial](artifact-doc/TUTORIAL.md) for concrete use cases.
+See the [tutorial](https://rocq-community.org/trocq/index.html#/quick-start) for concrete use cases.
 
 In short, the plugin provides a tactic:
 - `trocq` (without arguments) which attempts to run a translation on

docs/home.md

@@ -45,13 +45,7 @@ and readable code with respect to a sequent-style theoretical presentation.
 
 ## Building and installation instructions
 
-As **Trocq** is a prototype, it is currently unreleased, and depends on a
-[custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat)
-of **Coq-Elpi**. It is not yet packaged in **Opam** or **Nix**, but will be in
-the near future.
-
-There are however three ways to develop it and experiment with it,
-they are documented in the [INSTALL.md file](https://github.com/coq-community/trocq/blob/master/INSTALL.md) of the repository.
+See the [INSTALL.md file](https://github.com/coq-community/trocq/blob/master/INSTALL.md) of the repository.
 
 ## Documentation
 

docs/quick-start.md

@@ -5,6 +5,11 @@ First, we present the use of Trocq to perform proof transfer along type equivale
 Then, we handle the case of weaker, directed relations.
 Finally, we give several examples of multiple transfer featuring polymorphic and dependent containers.
 
+## Installation
+
+See the [INSTALL.md file](https://github.com/coq-community/trocq/blob/master/INSTALL.md) of the repository.
+We recommend the Nix or OPAM solutions, other solutions mentionned in that file may be outdated.
+
 ## Proof transfer with type isomorphisms
 
 In this first section, we show two examples of isomorphisms: natural numbers with unary and binary representations, and bitvectors.
@@ -34,6 +39,8 @@ Inductive N : Set :=
   | Npos : positive -> N.
 ```
 
+?> These definitions, along with a few results to be used later, are available in file [N.v](https://github.com/coq-community/trocq/blob/master/examples/std/N.v).
+
 A binary natural number of type `N` is either zero (`N0`) or a `positive` binary number (`Npos`) composed of a sequence of digits (`xI` and `xO`), starting from the least significant byte and always ending with a one (`xH`).
 
 Both `nat` and `N` types come with an induction principle generated by Coq.
@@ -62,6 +69,8 @@ Lemma N_Srect : forall (P : N -> Type),
 Proof. Fail apply nat_rect. Abort.
 ```
 
+?> See file [artifact_paper_example.v](https://github.com/coq-community/trocq/blob/master/examples/std/artifact_paper_example.v).
+
 Unfortunately, `nat_rect` cannot be used directly to prove `N_Srect` here, since the types of the induction principles cannot be unified.
 Indeed, by default, Coq does not know `N` and `nat` represent the same concept, and that the zero and successors of `N` are associated to the ones of `nat`.
 
@@ -117,10 +126,17 @@ Such functions and properties can be packed into an `Iso` record and given to Tr
 ```coq
 Definition N_nat_iso : Iso.type N nat := Iso.Build N_to_natK N_of_natK.
 
-Definition N_nat_R : Param44.Rel N nat := Iso.toParam N_nat_iso.
+Definition N_nat_R : Param44.Rel N nat := Iso.toParamSym N_nat_iso.
 Trocq Use N_nat_R.
 ```
 
+?> See files
+[N.v](https://github.com/coq-community/trocq/blob/master/examples/std/N.v)
+and
+[artifact_paper_example.v](https://github.com/coq-community/trocq/blob/master/examples/std/artifact_paper_example.v)
+where `N_to_natK` and `N_of_natK` are named respectively `to_natK` and
+`of_natK` and the notation `(N <=> nat)%P` stands for `Param44.Rel N nat`.
+
 In order to perform proof transfer for `N_Srect`, we need to declare in Trocq all the remaining constants appearing in the goal, that is, `N0` and `N_succ`.
 
 #### Operations and constants
@@ -157,6 +173,8 @@ Proof.
 Qed.
 ```
 
+?> See file [artifact_paper_example.v](https://github.com/coq-community/trocq/blob/master/examples/std/artifact_paper_example.v)
+
 ?> A careful analysis shows that in order to transfer this goal to `nat`, only information up to level `(2a,3)` in `N_nat_R` was used. It means that we could have only proved `N_to_natK` and the transfer would still have been possible. A way to declare the minimal amount of information is to run `trocq` without adding any information, and follow the error message asking for a specific level, until all the requirements are met and the tactic succeeds.
 
 ### Bounded natural numbers and bitvectors
@@ -168,6 +186,9 @@ Definition bounded_nat (k : nat) := {n : nat & n < 2^k}.
 Definition bitvector (k : nat) := Vector.t bool k.
 ```
 
+?> See file
+[Vector_tuple.v](https://github.com/coq-community/trocq/blob/master/examples/std/Vector_tuple.v).
+
 The required type of the Trocq relation between these type formers is the following:
 ```coq
 forall (k k' : nat) (kR : natR k k'), ParamXY.Rel (bounded_nat k) (bitvector k')
@@ -342,6 +363,9 @@ Definition Z_Zmodp_R : Param42a.Rel Z Zmodp := SplitSurj.toParam Z_Zmodp_surj.
 Trocq Use Z_Zmodp_R.
 ```
 
+?> See file
+[flt3_step.v](https://github.com/coq-community/trocq/blob/master/examples/std/flt3_step.v).
+
 ?> To give a slightly different example, here we relate `Z` to `Zmodp`, aiming to rephrase a goal expressed with the bigger type `Z` as a goal expressed with `Zmodp`, instead of pulling the goal in the subtype back to a more general goal, as it was done for `positive` and `N` above.
 
 If we define an equality over `Z` checking whether both values are congruent to each other modulo `p`, and use it in a general goal expressed with `Z`, if we relate it to a classic equality over `Zmodp`, Trocq can rephrase the general goal as a goal over `Zmodp` (we omit the details about multiplication and the zero here, as they have been covered in the previous examples):
@@ -369,6 +393,9 @@ Qed.
 
 !> Coming soon...
 
+?> Meanwhile, one can look into file
+[summable.v](https://github.com/coq-community/trocq/blob/master/examples/std/summable.v).
+
 ## Polymorphic and dependent container types
 
 As shown in the first section of this tutorial, as Trocq has support for the whole syntax of CCω, in particular, it supports dependent types.
@@ -532,6 +559,9 @@ Definition option_list_inj (A : Type) : @SplitInj.type (option A) (list A) :=
 Definition Param_option_list_d (A : Type) : Param42b.Rel (option A) (list A) :=
   SplitInj.toParam (option_list_inj A).
 ```
+?> See file
+[list_option.v](https://github.com/coq-community/trocq/blob/master/examples/std/list_option.v).
+
 ?> Note that again, we assume we are in a setup where relations linking the target standard type were defined previously. Here, it allows relating `option A` to `list A` and leaving the step changing the parameter `A` to an `A'` to the parametricity lemma over lists.
 
 By transitivity, we can state the full relation and add it to Trocq:
@@ -590,4 +620,4 @@ Such an approach enables refinement-like transfer, by expressing the statements
 
 Consider the encoding of matrices in the [MathComp library](https://github.com/math-comp/math-comp), where `'M[T](m,n)` denotes a matrix of size `m`X`n` with elements in `T`.
 
-!> To be continued...
+!> To be continued...

examples/N.v

@@ -11,8 +11,8 @@
 (*                            * see LICENSE file for the text of the license *)
 (*****************************************************************************)
 
+Require Import ssreflect.
 From Trocq Require Import Stdlib Common.
-From mathcomp Require Import ssreflect.
 
 Set Universe Polymorphism.
 Set Bullet Behavior "Strict Subproofs".
@@ -109,18 +109,11 @@ Fixpoint of_nat (n : nat) : N :=
 
 (* from ssrnat, inlined because ssrnat clashes with HoTT. *)
 Lemma addn0 : forall n, (n + 0)%nat = n.
-Proof.
-  move=> n; induction n as [|n IHn] => //= ;
-  rewrite IHn ;
-  done.
-Qed.
+Proof. by move=> n; induction n as [|n IHn] => //=; rewrite IHn. Qed.
 Lemma addSn : forall n m, (S n + m)%nat = S (n + m)%nat.
-Proof. done. Qed.  
+Proof. by []. Qed.
 Lemma addnS : forall n m, (n + S m)%nat = S (n + m)%nat.
-Proof.
-  move=> n m; induction n as [|n IHn] => /= [//|].
-  by rewrite IHn //.
-Qed.
+Proof. by move=> n m; induction n as [|n IHn] => /= [//|]; rewrite IHn //. Qed.
 
 Lemma of_natD i j : of_nat (i + j) = (of_nat i + of_nat j)%N.
 Proof.

examples/artifact_paper_example.v

@@ -14,12 +14,9 @@
 Require Import ssreflect.
 From Trocq Require Import Stdlib Trocq.
 From Trocq_examples Require Import N.
-From elpi Require Import elpi.
 
 Set Universe Polymorphism.
 
-(*Elpi Trace.*)
-
 (** In this example, we transport the induction principle on natural numbers
   from two equivalent representations of `N`: the unary one `nat` and the binary
   one `N`. We introduce the `Trocq Use` command to register such translations.
@@ -45,4 +42,3 @@ Proof. trocq. (* replaces N by nat in the goal *) exact nat_rect. Defined.
     independence. *)
 Set Printing Depth 20.
 Print Assumptions N_Srec.
-

examples/std/Vector_tuple.v

@@ -362,7 +362,7 @@ Definition Param44_bnat_bv (k k' : nat) (kR : natR k k') :
   Param44.Rel (bounded_nat k) (bitvector k').
 Proof.
   unshelve eapply (@Param44_trans _ (bitvector k) _).
-  - exact Param44_bnat_bv_d.  
+  - exact Param44_bnat_bv_d.
   - exact (Vector.Param44 bool bool Param44_Bool k k' kR).
 Defined.
 
@@ -382,7 +382,7 @@ Axiom getBit_bnat : forall {k : nat}, bounded_nat k -> nat -> bool.
 Axiom setBitR :
   forall
     (k k' : nat) (kR : natR k k')
-    (bn : bounded_nat k) (bv' : bitvector k') 
+    (bn : bounded_nat k) (bv' : bitvector k')
     (r : R_trans
           (@R_bnat_bv k) (Vector.Param44 bool bool Param44_Bool k k' kR) bn bv')
     (n n' : nat) (nR : natR n n')
@@ -395,7 +395,7 @@ Axiom setBitR :
 Axiom getBitR :
   forall
     (k k' : nat) (kR : natR k k')
-    (bn : bounded_nat k) (bv' : bitvector k') 
+    (bn : bounded_nat k) (bv' : bitvector k')
     (r : R_trans
           (@R_bnat_bv k) (Vector.Param44 bool bool Param44_Bool k k' kR) bn bv')
     (n n' : nat) (nR : natR n n'),

examples/std/flt3_step.v

@@ -11,7 +11,6 @@
 (*                            * see LICENSE file for the text of the license *)
 (*****************************************************************************)
 
-Require Import ssreflect.
 From mathcomp Require Import all_ssreflect all_algebra.
 From Trocq Require Import Stdlib Trocq.
 
@@ -164,7 +163,7 @@ Trocq Use Param01_Empty.
 Trocq Use Param10_Empty.
 
 Lemma flt3_step : forall (m n p : ℤ),
-  ((m * n * p)%Z % 3)%Z ≢ 0 -> (m³ + n³)%ℤ  ≠ p³%ℤ.
+  ((m * n * p)%Z % 3)%Z ≢ 0 -> (m³ + n³)%ℤ ≠ p³%ℤ.
 Proof.
 trocq=> /=.
 

examples/std/square_and_cube_mod7.v

@@ -11,7 +11,6 @@
 (*                            * see LICENSE file for the text of the license *)
 (*****************************************************************************)
 
-Require Import ssreflect.
 From mathcomp Require Import all_ssreflect all_algebra.
 From Trocq Require Import Stdlib Trocq.
 

examples/std/stuck.v

@@ -68,4 +68,3 @@ reflexivity.
 Qed.
 
 End Works.
-

examples/std/trocq_setoid_rewrite.v

@@ -32,23 +32,23 @@ Existing Instance eqp_sym.
 #[local] Axiom (eqp_trans : Transitive eqmodp).
 Existing Instance eqp_trans.
 
-#[local] Axiom add_morph : 
-  forall m m' : int, (m == m')%int ->  
-  forall n n' : int, (n == n')%int ->  
-  (m + n == m' + n')%int. 
+#[local] Axiom add_morph :
+  forall m m' : int, (m == m')%int ->
+  forall n n' : int, (n == n')%int ->
+  (m + n == m' + n')%int.
 
-Definition eqmodp_morph : 
-  forall m m' : int, (m == m')%int ->  
-  forall n n' : int, (n == n')%int ->  
+Definition eqmodp_morph :
+  forall m m' : int, (m == m')%int ->
+  forall n n' : int, (n == n')%int ->
   (m' == n')%int -> (m == n)%int.
 Proof.
 move=> m m' Rm n n' Rn Rmn.
 exact (eqp_trans _ _ _ Rm (eqp_trans _ _ _ Rmn (eqp_sym _ _ Rn))).
 Qed.
 
-Lemma eqmodp01 : 
-  forall m m' : int, (m == m')%int ->  
-  forall n n' : int, (n == n')%int ->  
+Lemma eqmodp01 :
+  forall m m' : int, (m == m')%int ->
+  forall n n' : int, (n == n')%int ->
   Param01.Rel (m == n)%int (m' == n')%int.
 Proof.
 move=> m m' Rm n n' Rn.