Automatic weakening of constants

_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

elpi/param-class.elpi

@@ -102,6 +102,15 @@ weakenings-to map2b [map3].
 weakenings-to map3  [map4].
 weakenings-to map4  [].
 
+% lower/higher levels at distance 1 from a given level
+pred all-weakenings-from i:map-class, o:list map-class.
+all-weakenings-from map0  [].
+all-weakenings-from map1  [map0].
+all-weakenings-from map2a [map1, map0].
+all-weakenings-from map2b [map1, map0].
+all-weakenings-from map3  [map2a, map2b, map1, map0].
+all-weakenings-from map4  [map3, map2a, map2b, map1, map0].
+
 % all possible parametricity classes that can be created by combinations of 2 lists of map classes
 pred product i:list map-class, i:list map-class, o:list param-class.
 product Ms Ns Classes :-
@@ -176,10 +185,6 @@ dep-arrow map4  (pc map0 map4)  (pc map4 map0).
 
 } % map-class
 
-pred do-not-fail.
-:before "term->gref:fail"
-coq.term->gref _ _ :- do-not-fail, !, false.
-
 namespace param-class {
 
 % extensions of functions over map classes to parametricity classes
@@ -196,6 +201,15 @@ weakenings-to (pc M N) Classes :-
   map-class.weakenings-to N Ns,
   map-class.product Ms Ns Classes.
 
+pred all-weakenings-from i:param-class, o:list param-class.
+all-weakenings-from (pc M N) Classes :-
+  map-class.all-weakenings-from M Ms,
+  map-class.all-weakenings-from N Ns,
+  map-class.product Ms Ns StrictClasses,
+  map-class.product [M] Ns MClasses,
+  map-class.product Ms [N] NClasses,
+  std.flatten [StrictClasses, MClasses, NClasses] Classes.
+
 pred negate i:param-class, o:param-class.
 negate (pc M N) (pc N M).
 
@@ -229,6 +243,13 @@ dep-arrow (pc M N) ClassA ClassB :-
   union ClassAM {param-class.negate ClassAN} ClassA,
   union ClassBM {param-class.negate ClassBN} ClassB.
 
+pred to-string i:param-class, o:string.
+to-string (pc M N) String :- std.do! [
+  map-class->string M MStr,
+  map-class->string N NStr,
+  String is MStr ^ NStr
+].
+
 % generate a weakening function from a parametricity class to another, by forgetting fields 1 by 1
 pred forget i:param-class, i:param-class, o:univ-instance -> term -> term -> term -> term.
 forget (pc M N) (pc M N) (_\ _\ _\ r\ r) :- !.
@@ -247,6 +268,29 @@ forget (pc M N) (pc M' N') ForgetF :-
     {calc ("forget_" ^ {map-class->string M} ^ NStr ^ "_" ^ {map-class->string M1} ^ NStr)} Forget1,
   ForgetF = (ui\ a\ b\ r\ ForgetF' ui a b (app [pglobal Forget1 ui, a, b, r])).
 
+% weaking of the out class of a gref.
+% e.g. if GR has type `forall A B, R A B -> Param21 X Y`
+% then `weaken-out (pc map1 map0) GR T`
+% where `T` has type `forall A B, R A B -> Param10 X Y`
+pred weaken-out i:param-class, i:gref, o:term.
+weaken-out OutC GR WT :- std.do! [
+  coq.env.global GR T,
+  coq.env.typeof GR Ty,
+  replace-out-ty OutC Ty WTy,
+  std.assert-ok! (coq.elaborate-skeleton T WTy WT)
+    "weaken-out: failed to weaken"
+].
+
+pred replace-out-ty i:param-class, i:term, o:term.
+replace-out-ty OutC (prod N A B) (prod N A B') :- !,
+   pi x\ replace-out-ty OutC (B x) (B' x).
+replace-out-ty OutC InT OutT :- std.do! [
+  coq.safe-dest-app InT HD Ts,
+  trocq.db.gref->class OutGRClass OutC,
+  util.subst-gref HD OutGRClass HD',
+  coq.mk-app HD' Ts OutT
+  ].
+
 % succeed if the parametricity class contains a map class over 2b
 % this means that a translation of a sort at this class will require univalence,
 % and the translation of a dependent product will require funext

elpi/util.elpi

@@ -14,6 +14,10 @@
 % utility predicates
 % -----------------------------------------------------------------------------
 
+pred do-not-fail.
+:before "term->gref:fail"
+coq.term->gref _ _ :- do-not-fail, !, false.
+
 kind or type -> type -> type.
 type inl A -> or A B.
 type inr B -> or A B.
@@ -79,4 +83,11 @@ delete A [A|Xs] Xs :- !.
 delete A [X|Xs] [X|Xs'] :- delete A Xs Xs'.
 delete _ [] [].
 
+% subst-gref T GR' T'
+% substitutes GR for GR' in T if T = (global GR) or (pglobal GR I)
+pred subst-gref i:term, i:gref, o:term.
+subst-gref (global _) GR' (global GR').
+subst-gref (pglobal _ I) GR' (pglobal GR' I).
+subst-gref T _ _ :- coq.error T "is not a gref".
+
 } % util

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/Vector_tuple.v

@@ -209,7 +209,6 @@ Defined.
 
 Module AppendConst.
 
-Trocq Use Param00_nat.
 Trocq Use Param2a0_nat.
 Trocq Use Param_add.
 Trocq Use Param02b_tuple_vector.
@@ -240,19 +239,14 @@ Axiom Param_head : forall
 Module HeadConst.
 
 Axiom (int : Type) (Zp : Type) (Rp42b : Param42b.Rel Zp int).
-Definition Rp00 : Param00.Rel Zp int := Rp42b.
-Definition Rp2a0 : Param2a0.Rel Zp int := Rp42b.
-Definition Rp02b : Param02b.Rel Zp int := Rp42b.
+Definition Rp2a2b : Param2a2b.Rel Zp int := Rp42b.
 
 Lemma head_const {n : nat} : forall (i : int), Vector.hd (Vector.const i (S n)) = i.
 Proof. destruct n; simpl; reflexivity. Qed.
 
-Trocq Use Param00_nat.
 Trocq Use Param2a0_nat.
 Trocq Use SR.
-Trocq Use Rp00.
-Trocq Use Rp2a0.
-Trocq Use Rp02b.
+Trocq Use Rp2a2b.
 Trocq Use Param_head.
 Trocq Use Param_const.
 Trocq Use Param01_paths.
@@ -464,13 +458,9 @@ Axiom setBitThenGetSame :
   forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool),
     (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b.
 
-Definition Param2a0_Bool : Param2a0.Rel Bool Bool := Param44_Bool.
-Definition Param02b_Bool : Param02b.Rel Bool Bool := Param44_Bool.
 
-Trocq Use Param00_nat.
 Trocq Use Param2a0_nat.
-Trocq Use Param2a0_Bool.
-Trocq Use Param02b_Bool.
+Trocq Use Param44_Bool.
 Trocq Use Param2a0_bnat_bv.
 Trocq Use getBitR.
 Trocq Use setBitR.

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).