cleanup

examples/N.v

@@ -43,10 +43,10 @@ Fixpoint succ x :=
     | 1 => 1~0
   end.
 
-Fixpoint map (x : positive) : nat :=
+Fixpoint to_nat (x : positive) : nat :=
   match x with
-    | p~1 => 1 + (map p + map p)
-    | p~0 => map p + map p
+    | p~1 => 1 + (to_nat p + to_nat p)
+    | p~0 => to_nat p + to_nat p
     | 1 => 1
   end.
 
@@ -78,57 +78,58 @@ Inductive N : Set :=
 Declare Scope N_scope.
 Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
+Coercion Npos : positive >-> N.
 
 Notation "0" := N0 : N_scope.
 
-Definition succ_pos (n : N) : positive :=
+Module N.
+Local Definition succ_subdef (n : N) : positive :=
  match n with
    | N0 => 1%positive
    | Npos p => Pos.succ p
  end.
+Arguments succ_subdef /.
+Definition succ : N -> N := succ_subdef.
 
-Definition Nsucc (n : N) := Npos (succ_pos n).
-
-Definition Nadd (m n : N) := match m, n with
+Definition add (m n : N) := match m, n with
 | N0, x | x, N0 => x
-| Npos p, Npos q => Npos (Pos.add p q)
+| Npos p, Npos q => 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 *)
+Infix "+" := add : N_scope.
+Notation "n .+1" := (succ n) : N_scope.
 
-Definition Nmap (n : N) : nat :=
-  match n with
-  | N0 => 0
-  | Npos p => Pos.map p
-  end.
+Lemma addpp p : (Npos p + Npos p)%N = Npos p~0.
+Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Defined.
 
-Fixpoint Ncomap (n : nat) : N :=
-  match n with O => 0 | S n => Nsucc (Ncomap n) end.
+Definition to_nat (n : N) : nat :=
+  match n with N0 => 0 | Npos p => Pos.to_nat p end.
 
-Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0.
-Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Defined.
+Fixpoint of_nat (n : nat) : N :=
+  match n with O => 0 | S n => succ (of_nat n) end.
 
-Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N.
+Lemma of_natD i j : of_nat (i + j) = (of_nat i + of_nat 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.
+case: (of_nat i) => // p; case: (of_nat j) => //=.
+- by rewrite /succ/= Pos.addp1.
+- by move=> q; rewrite /succ/= 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.
+Local Definition of_nat_double p k :
+  of_nat k = Npos p -> of_nat (k + k) = Npos p~0.
+Proof. by move=> kp; rewrite of_natD kp addpp. Defined.
 
-Lemma NmapK (n : N) : Ncomap (Nmap n) = n.
-Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Defined.
+Lemma to_natK (n : N) : of_nat (to_nat n) = n.
+Proof. by case: n => //= ; elim=> //= p /of_nat_double/= ->. Defined.
 
-Lemma NcomapK (n : nat) : Nmap (Ncomap n) = n.
+Lemma of_natK (n : nat) : to_nat (of_nat n) = n.
 Proof.
 elim: n => //= n IHn; rewrite -[in X in _ = X]IHn.
-by case: (Ncomap n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm.
+by case: (of_nat n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm.
 Defined.
 
-Definition Niso := Iso.Build NcomapK NmapK.
+Definition of_nat_iso := Iso.Build of_natK to_natK.
+End N.
+Infix "+" := N.add : N_scope.
+Notation "n .+1" := (N.succ n) : N_scope.

examples/artifact_paper_example.v

@@ -20,12 +20,12 @@ 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.
+Definition RN44 : (N <=> nat)%P := Iso.toParamSym N.of_nat_iso.
 
 (* 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).
+Definition RNS m n : RN44 m n -> RN44 (N.succ m) (S n).
 Proof. by move: m n => _ + <-; case=> //=. Defined.
 
 (* We now register all these informations in a database known to the tactic: *)
@@ -34,7 +34,7 @@ Trocq Use RN44.
 
 (* We can now make use of the tactic to prove an induction principle on N *)
 Lemma N_Srec : forall (P : N -> Type), P N0 ->
- (forall n, P n -> P (Nsucc n)) -> forall n, P n.
+ (forall n, P n -> P (N.succ 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
@@ -43,4 +43,4 @@ 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).
+Eval compute in N_Srec (fun _ => N) (0%N) N.add 1~0~1~1~0~1%positive.

examples/peano_bin_nat.v

@@ -20,32 +20,23 @@ Set Universe Polymorphism.
 
 (* 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} {|
-   SplitSurj.retract := Ncomap;
-   SplitSurj.section := Nmap;
-   SplitSurj.sectionK := NmapK |}.
-
-(* for brevity, we create witnesses at lower classes by forgetting fields in RN2a3 *)
-(* this behaviour can be automated so as to only declare Rn2a3 and get for free all the instances
-   reachable by forgetting fields *)
-(* in the general case, if a field requires an axiom, it is better to manually recreate instances
-   that do not need this field, so that it is not imported before forgetting, and the lower
-   instances can be declared without the axiom *)
+Definition RN : Param2a3.Rel N nat :=
+ SplitSurj.toParamSym (SplitSurj.Build N.to_natK).
 
 (* as 0 and Nsucc appear in the goal, we need to link them with nat constructors *)
 (* NB: as these are not type formers, only class (0,0) is required, so these proofs amount to what
    would be done in the context of raw parametricity *)
 
-Definition RN0 : RN N0 0%nat. Proof. done. Qed.
-Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n).
+Definition RN0 : RN 0%N 0%nat. Proof. done. Qed.
+Definition RNS : forall m n, RN m n -> RN m.+1%N n.+1%nat.
 Proof. by move=> _ + <-; case=> //=. Qed.
 
 Trocq Use RN.
 Trocq Use RN0.
 Trocq Use RNS.
 
 Lemma N_Srec : forall (P : N -> Type), P N0 ->
- (forall n, P n -> P (Nsucc n)) -> forall n, P n.
+ (forall n, P n -> P n.+1%N) -> forall n, P n.
 Proof.
   trocq.
   (* the output sort of P' is (1,1) because of the covariant and contravariant occurrences of P in