Compress

examples/Vector_tuple.v

@@ -209,12 +209,8 @@ Defined.
 
 Module AppendConst.
 
-Trocq Use Param2a0_nat.
-Trocq Use Param_add.
-Trocq Use Param02b_tuple_vector.
-Trocq Use Param_append.
-Trocq Use Param_const.
-Trocq Use Param01_paths.
+Trocq Use Param2a0_nat Param_add Param02b_tuple_vector.
+Trocq Use Param_append Param_const Param01_paths.
 
 Lemma append_const : forall {A : Type} (a : A) (n1 n2 : nat),
   append (const a n1) (const a n2) = const a (n1 + n2).
@@ -244,12 +240,7 @@ 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 Param2a0_nat.
-Trocq Use SR.
-Trocq Use Rp2a2b.
-Trocq Use Param_head.
-Trocq Use Param_const.
-Trocq Use Param01_paths.
+Trocq Use Param2a0_nat SR Rp2a2b Param_head Param_const Param01_paths.
 
 Lemma head_const' : forall {n : nat} (z : Zp), head (const z (S n)) = z.
 Proof. trocq. exact @head_const. Qed.
@@ -277,14 +268,9 @@ Proof.
     + exact vv'R.
 Defined.
 
-Trocq Use SR.
-Trocq Use Param_cons.
-Trocq Use Param_add.
-Trocq Use Param_append.
-Trocq Use Param01_paths.
-Trocq Use Param2a0_tuple_vector.
-Trocq Use Param02b_tuple_vector.
-Trocq Use Param2a0_nat.
+Trocq Use SR Param_cons Param_add Param_append Param01_paths.
+Trocq Use Param2a0_tuple_vector Param02b_tuple_vector Param2a0_nat.
+
 Lemma append_comm_cons : forall {A : Type} {n1 n2 : nat}
     (v1 : tuple A n1) (v2 : tuple A n2) (a : A),
   @paths (tuple A (S (n1 + n2))) (cons a (append v1 v2)) (append (cons a v1) v2).
@@ -449,13 +435,8 @@ Axiom setBitThenGetSame :
     (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b.
 
 
-Trocq Use Param2a0_nat.
-Trocq Use Param44_Bool.
-Trocq Use Param2a0_bnat_bv.
-Trocq Use getBitR.
-Trocq Use setBitR.
-Trocq Use Param01_paths.
-Trocq Use Param10_lt.
+Trocq Use Param2a0_nat Param44_Bool Param2a0_bnat_bv getBitR setBitR.
+Trocq Use Param01_paths Param10_lt.
 
 Lemma setBitThenGetSame' :
   forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool),

examples/artifact_paper_example.v

@@ -30,7 +30,7 @@ Trocq Use RN. (* registering related types *)
   types: *)
 Definition RN0 : RN 0%N 0%nat. Proof. done. Defined.
 Definition RNS m n : RN m n -> RN (N.succ m) (S n). Proof. by case. Defined.
-Trocq Use RN0. Trocq Use RNS. (* registering related constants *)
+Trocq Use RN0 RNS. (* registering related constants *)
 
 (** We can now make use of the tactic to prove an induction principle on `N` *)
 Lemma N_Srec : forall (P : N -> Type), P 0%N ->

examples/int_to_Zp.v

@@ -18,8 +18,10 @@ Set Universe Polymorphism.
 
 Declare Scope int_scope.
 Delimit Scope int_scope with int.
+Local Open Scope int_scope.
 Declare Scope Zmodp_scope.
 Delimit Scope Zmodp_scope with Zmodp.
+Local Open Scope Zmodp_scope.
 
 Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ
    (f : X -> Y -> Z) (g : X' -> Y' -> Z') :=
@@ -39,10 +41,16 @@ Axiom (modp : int -> Zmodp) (reprp : Zmodp -> int)
 
 Definition eqmodp (x y : int) := modp x = modp y.
 
+(* for now translations need the support of a global reference: *)
+Definition eq_Zmodp (x y : Zmodp) := (x = y).
+Arguments eq_Zmodp /.
+
 (* Axiom (eqp_refl : Reflexive eqmodp). *)
 (* Axiom (eqp_sym : Symmetric eqmodp). *)
 (* Axiom (eqp_trans : Transitive eqmodp). *)
 
+Notation "0" := zero : int_scope.
+Notation "0" := zerop : Zmodp_scope.
 Notation "x == y" := (eqmodp x%int y%int)
   (format "x  ==  y", at level 70) : int_scope.
 Notation "x + y" := (add x%int y%int) : int_scope.
@@ -54,31 +62,21 @@ Module IntToZmodp.
 
 Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
 
-Axiom Rzero' : Rp zero zerop.
-Variable Radd' : binop_param Rp Rp Rp add addp.
-Variable Rmul' : binop_param Rp Rp Rp mul mulp.
-
-Trocq Use Rmul'.
-Trocq Use Rzero'.
-Trocq Use Param10_paths.
-Trocq Use Rp.
-
-Definition eq_Zmodp (x y : Zmodp) := (x = y).
-(* Bug if we inline the previous def in the following axiom *)
-Axiom Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x ->
+Axiom Rzero : Rp zero zerop.
+Variable Radd : binop_param Rp Rp Rp add addp.
+Variable Rmul : binop_param Rp Rp Rp mul mulp.
+Variable Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x ->
   forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y).
-Trocq Use Reqmodp01.
-Arguments eq_Zmodp /.
 
-Hypothesis RedZmodpEq0 :
-  (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = (p * p * p)%Zmodp ->
-    m = zerop).
+Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01.
 
-Lemma IntRedModZp : forall (m n p : int),
-  (m = n * n)%int -> m = (p * p * p)%int -> eqmodp m zero.
+Lemma IntRedModZp :
+ (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = 0) ->
+ forall (m n p : int), (m = n * n)%int -> (m == 0)%int.
 Proof.
+move=> Hyp.
 trocq; simpl.
-exact @RedZmodpEq0.
+exact: Hyp.
 Qed.
 
 (* Print Assumptions IntRedModZp. (* No Univalence *) *)
@@ -93,11 +91,7 @@ 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 Rp.
-Trocq Use Param01_paths.
-Trocq Use Param10_paths.
-Trocq Use Radd.
-Trocq Use Rzero.
+Trocq Use Rp Param01_paths Param10_paths Radd Rzero.
 
 Goal (forall x y, x + y = y + x)%Zmodp.
 Proof.

examples/nat_ind.v

@@ -32,9 +32,7 @@ Definition RI : Param2a3.Rel I nat :=
 Definition RI0 : RI I0 O. Proof. exact of_nat0. Qed.
 Definition RIS m n : RI m n -> RI (IS m) (S n). Proof. exact: of_natS. Qed.
 
-Trocq Use RI.
-Trocq Use RI0.
-Trocq Use RIS.
+Trocq Use RI RI0 RIS.
 
 Lemma I_Srec : forall (P : I -> Type), P I0 ->
  (forall n, P n -> P (IS n)) -> forall n, P n.

examples/peano_bin_nat.v

@@ -30,9 +30,7 @@ Definition RN : Param2a3.Rel N nat :=
 Definition RN0 : RN 0%N 0%nat. Proof. done. Qed.
 Definition RNS m n : RN m n -> RN m.+1%N n.+1%nat. Proof. by case. Qed.
 
-Trocq Use RN.
-Trocq Use RN0.
-Trocq Use RNS.
+Trocq Use RN RN0 RNS.
 
 Lemma N_Srec : forall (P : N -> Type), P N0 ->
  (forall n, P n -> P n.+1%N) -> forall n, P n.

examples/summable.v

@@ -203,12 +203,8 @@ move=> u _ <-; rewrite extend_truncate//.
 by apply isSummableP.
 Qed.
 
-Trocq Use Param01_paths.
-Trocq Use Param02b_nnR.
-Trocq Use Param2a0_rseq.
-Trocq Use R_sum_xnnR.
-Trocq Use R_add_xnnR.
-Trocq Use seq_nnR_add.
+Trocq Use Param01_paths Param02b_nnR Param2a0_rseq.
+Trocq Use R_sum_xnnR R_add_xnnR seq_nnR_add.
 
 (* we get a proof over non negative reals for free,
    from the analogous proof over the extended ones *)

examples/trocq_gen_rewrite.v

@@ -54,15 +54,13 @@ apply: (@Param01.BuildRel (m <= n)%int (m' <= n')%int (fun _ _ => Unit)).
 - by constructor => mn; apply (le_morph _ _ Rm _ _ Rn).
 Qed.
 
-Trocq Use le01.
-Trocq Use add_morph.
+Trocq Use le01 add_morph.
 
 Variables i j : int.
 Variable ip : (j <= i)%int.
 Definition iid : (i <= i)%int := le_refl i.
 
-Trocq Use ip.
-Trocq Use iid.
+Trocq Use ip iid.
 
 Example ipi : (j + i + j <= i + i + i)%int.
 Proof.

examples/trocq_setoid_rewrite.v

@@ -55,16 +55,14 @@ apply: (@Param01.BuildRel (m == n)%int (m' == n')%int (fun _ _ => Unit)).
 - by constructor => mn; apply (eqmodp_morph _ _ Rm _ _ Rn).
 Qed.
 
-Trocq Use eqmodp01.
-Trocq Use add_morph.
+Trocq Use eqmodp01 add_morph.
 
 Variables i : int.
 Let j := (i + p)%int.
 Variable ip : (j == i)%int.
 Definition iid : (i == i)%int := eqp_refl i.
 
-Trocq Use ip.
-Trocq Use iid.
+Trocq Use ip iid.
 
 Example ipi : (j + i == i + i)%int.
 Proof.

theories/Vernac.v

@@ -111,6 +111,10 @@ Elpi Accumulate lp:{{
   %   (clause _ (before "default-gref")
   %     (trocq.db.gref GR (pc map4 map2b) [] {{:gref int}} {{:gref Rp42b}})),
 
+  % serveral use in one go!
+  main [str "Use", X, Y | Rest] :- !, std.do![
+      main [str "Use", X], main [str "Use", Y | Rest]].
+
   main [str "Usage"] :- !, coq.say {usage-msg}.
   main _ :- coq.error {std.string.concat "\n" ["command syntax error", {usage-msg}]}.