code refactoring: isolating example of artifact paper

_CoqProject

@@ -3,6 +3,7 @@
 
 -R theories/ Trocq
 -R elpi/ Trocq.Elpi
+-R examples/ Trocq_examples
 
 theories/HoTT_additions.v
 theories/Hierarchy.v
@@ -23,10 +24,12 @@ theories/Param_prod.v
 theories/Param_option.v
 theories/Param_vector.v
 
-examples/Example.v
+examples/artifact_paper_example.v
+examples/N.v
 examples/int_to_Zp.v
 examples/peano_bin_nat.v
 examples/setoid_rewrite.v
 examples/summable.v
 examples/trocq_setoid_rewrite.v
 examples/Vector_tuple.v
+examples/misc.v

examples/N.v

@@ -0,0 +1,134 @@
+(*****************************************************************************)
+(*                            *                    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 HoTT Require Import HoTT.
+From Trocq Require Import Common.
+
+Set Universe Polymorphism.
+
+(* definition of binary natural numbers *)
+
+Inductive positive : Set :=
+  | xI : positive -> positive
+  | xO : positive -> positive
+  | xH : positive.
+
+Declare Scope positive_scope.
+Delimit Scope positive_scope with positive.
+Bind Scope positive_scope with positive.
+
+Notation "1" := xH : positive_scope.
+Notation "p ~ 1" := (xI p)
+ (at level 7, left associativity, format "p '~' '1'") : positive_scope.
+Notation "p ~ 0" := (xO p)
+ (at level 7, left associativity, format "p '~' '0'") : positive_scope.
+
+Module Pos.
+Local Open Scope positive_scope.
+Fixpoint succ x :=
+  match x with
+    | p~1 => (succ p)~0
+    | p~0 => p~1
+    | 1 => 1~0
+  end.
+
+Fixpoint map (x : positive) : nat :=
+  match x with
+    | p~1 => 1 + (map p + map p)
+    | p~0 => map p + map p
+    | 1 => 1
+  end.
+
+Fixpoint add (x y : positive) : positive :=
+  match x, y with
+  | 1, p | p, 1 => succ p
+  | p~0, q~0 => (add p q)~0
+  | p~0, q~1 | p~1, q~0 => (add p q)~1
+  | p~1, q~1 => succ (add p q)~1
+  end.
+Infix "+" := add : positive_scope.
+Notation "p .+1" := (succ p) : positive_scope.
+
+Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Defined.
+Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Defined.
+Lemma addpS x y : x + y.+1 = (x + y).+1.
+Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Defined.
+Lemma addSp x y : x.+1 + y = (x + y).+1.
+Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Defined.
+
+End Pos.
+Infix "+" := Pos.add : positive_scope.
+Notation "p .+1" := (Pos.succ p) : positive_scope.
+
+Inductive N : Set :=
+  | N0 : N
+  | Npos : positive -> N.
+
+Declare Scope N_scope.
+Delimit Scope N_scope with N.
+Bind Scope N_scope with N.
+
+Notation "0" := N0 : N_scope.
+
+Definition succ_pos (n : N) : positive :=
+ match n with
+   | N0 => 1%positive
+   | Npos p => Pos.succ p
+ end.
+
+Definition Nsucc (n : N) := Npos (succ_pos n).
+
+Definition Nadd (m n : N) := match m, n with
+| N0, x | x, N0 => x
+| Npos p, Npos q => Npos (Pos.add p q)
+end.
+Infix "+" := Nadd : N_scope.
+Notation "n .+1" := (Nsucc n) : N_scope.
+
+(* various possible proofs to fill the fields of a parametricity witness between N and nat *)
+
+Definition Nmap (n : N) : nat :=
+  match n with
+  | N0 => 0
+  | Npos p => Pos.map p
+  end.
+
+Fixpoint Ncomap (n : nat) : N :=
+  match n with O => 0 | S n => Nsucc (Ncomap n) end.
+
+Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0.
+Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Defined.
+
+Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N.
+Proof.
+elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//.
+rewrite -nat_add_n_Sm/= IHi.
+case: (Ncomap i) => // p; case: (Ncomap j) => //=.
+- by rewrite /Nsucc/= Pos.addp1.
+- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp.
+Defined.
+
+Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0.
+Proof. by move=> kp; rewrite NcomapD kp Naddpp. Defined.
+
+Lemma NmapK (n : N) : Ncomap (Nmap n) = n.
+Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Defined.
+
+Lemma NcomapK (n : nat) : Nmap (Ncomap n) = n.
+Proof.
+elim: n => //= n IHn; rewrite -[in X in _ = X]IHn.
+by case: (Ncomap n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm.
+Defined.
+
+Definition Niso := Iso.Build NcomapK NmapK.

examples/artifact_paper_example.v

@@ -0,0 +1,46 @@
+(*****************************************************************************)
+(*                            *                    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 HoTT Require Import HoTT.
+From Trocq Require Import Trocq.
+From Trocq_examples Require Import N.
+
+Set Universe Polymorphism.
+
+(* Let us first prove that type nat , of unary natural numbers, and type N , of
+binary ones, are equivalent *)
+Definition RN44 : (N <=> nat)%P := Iso.toParamSym Niso.
+
+(* This equivalence proof coerces to a relation of type N -> nat -> Type , which
+relates the respective zero and successor constants of these types: *)
+Definition RN0 : RN44 0%N 0%nat. Proof. done. Defined.
+Definition RNS m n : RN44 m n -> RN44 (Nsucc m) (S n).
+Proof. by move: m n => _ + <-; case=> //=. Defined.
+
+(* We now register all these informations in a database known to the tactic: *)
+Trocq Use RN0. Trocq Use RNS.
+Trocq Use RN44.
+
+(* We can now make use of the tactic to prove a recurrence principle on N *)
+Lemma N_Srec : forall (P : N -> Type), P N0 ->
+ (forall n, P n -> P (Nsucc n)) -> forall n, P n.
+Proof. trocq. (* N replaces nat in the goal *) exact nat_rect. Defined.
+
+(* Inspecting the proof term atually reveals that univalence was not needed
+in the proof of N_Srec.  *)
+Print N_Srec.
+Print Assumptions N_Srec.
+
+(* Indeed this computes *)
+Eval compute in N_Srec (fun n => N) (0%N) Nadd (Npos 1~0~1~1~1~0).

examples/int_to_Zp.v

@@ -52,8 +52,7 @@ Notation "x * y" := (mulp x%Zmodp y%Zmodp) : Zmodp_scope.
 
 Module IntToZmodp.
 
-Definition Rp := SplitSurj.toParam
-  (SplitSurj.Build_type modp reprp reprpK).
+Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
 
 Axiom Rzero' : Rp zero zerop.
 Variable Radd' : binop_param Rp Rp Rp add addp.
@@ -88,25 +87,13 @@ End IntToZmodp.
 
 Module ZmodpToInt.
 
-Definition Rp x n := eqmodp (reprp x) n.
-
-Definition Rp2a2b@{i} : Param2a2b.Rel Zmodp@{i} int@{i}.
-Proof.
-unshelve econstructor.
-- exact Rp.
-- unshelve econstructor.
-  + exact reprp.
-  + move=> a b; move=> /(ap modp); exact.
-- unshelve econstructor.
-  + exact modp.
-  + by move=> a b; rewrite /Rp/sym_rel/eqmodp reprpK => <-.
-Defined.
+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 Rp2a2b.
+Trocq Use Rp.
 Trocq Use Param01_paths.
 Trocq Use Param10_paths.
 Trocq Use Radd.

examples/peano_bin_nat.v

@@ -14,117 +14,10 @@
 From Coq Require Import ssreflect.
 From HoTT Require Import HoTT.
 From Trocq Require Import Trocq.
+From Trocq_examples Require Import N.
 
 Set Universe Polymorphism.
 
-(* definition of binary natural numbers *)
-
-Inductive positive : Set :=
-  | xI : positive -> positive
-  | xO : positive -> positive
-  | xH : positive.
-
-Declare Scope positive_scope.
-Delimit Scope positive_scope with positive.
-Bind Scope positive_scope with positive.
-
-Notation "1" := xH : positive_scope.
-Notation "p ~ 1" := (xI p)
- (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p)
- (at level 7, left associativity, format "p '~' '0'") : positive_scope.
-
-Module Pos.
-Local Open Scope positive_scope.
-Fixpoint succ x :=
-  match x with
-    | p~1 => (succ p)~0
-    | p~0 => p~1
-    | 1 => 1~0
-  end.
-
-Fixpoint map (x : positive) : nat :=
-  match x with
-    | p~1 => 1 + (map p + map p)
-    | p~0 => map p + map p
-    | 1 => 1
-  end.
-
-Fixpoint add (x y : positive) : positive :=
-  match x, y with
-  | 1, p | p, 1 => succ p
-  | p~0, q~0 => (add p q)~0
-  | p~0, q~1 | p~1, q~0 => (add p q)~1
-  | p~1, q~1 => succ (add p q)~1
-  end.
-Infix "+" := add : positive_scope.
-Notation "p .+1" := (succ p) : positive_scope.
-
-Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Qed.
-Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Qed.
-Lemma addpS x y : x + y.+1 = (x + y).+1.
-Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Qed.
-Lemma addSp x y : x.+1 + y = (x + y).+1.
-Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Qed.
-
-End Pos.
-Infix "+" := Pos.add : positive_scope.
-Notation "p .+1" := (Pos.succ p) : positive_scope.
-
-Inductive N : Set :=
-  | N0 : N
-  | Npos : positive -> N.
-
-Declare Scope N_scope.
-Delimit Scope N_scope with N.
-Bind Scope N_scope with N.
-
-Notation "0" := N0 : N_scope.
-
-Definition succ_pos (n : N) : positive :=
- match n with
-   | N0 => 1%positive
-   | Npos p => Pos.succ p
- end.
-
-Definition Nsucc (n : N) := Npos (succ_pos n).
-
-Definition Nadd (m n : N) := match m, n with
-| N0, x | x, N0 => x
-| Npos p, Npos q => Npos (Pos.add p q)
-end.
-Infix "+" := Nadd : N_scope.
-Notation "n .+1" := (Nsucc n) : N_scope.
-
-(* various possible proofs to fill the fields of a parametricity witness between N and nat *)
-
-Definition Nmap (n : N) : nat :=
-  match n with
-  | N0 => 0
-  | Npos p => Pos.map p
-  end.
-
-Fixpoint Ncomap (n : nat) : N :=
-  match n with O => 0 | S n => Nsucc (Ncomap n) end.
-
-Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0.
-Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed.
-
-Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N.
-Proof.
-elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//.
-rewrite -nat_add_n_Sm/= IHi.
-case: (Ncomap i) => // p; case: (Ncomap j) => //=.
-- by rewrite /Nsucc/= Pos.addp1.
-- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp.
-Qed.
-
-Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0.
-Proof. by move=> kp; rewrite NcomapD kp Naddpp. Qed.
-
-Lemma NmapK (n : N) : Ncomap (Nmap n) = n.
-Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed.
-
 (* the best we can do to link these types is (4,4), but
 we only need (2a,3) which is morally that Nmap is a split injection *)
 Definition RN := SplitSurj.toParamSym@{Set} {|