Compress

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') :=
@@ -43,6 +45,8 @@ Definition eqmodp (x y : int) := modp x = modp y.
 (* 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,14 +58,11 @@ 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.
+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.
+Trocq Use Rp Rmul Rzero Param10_paths.
 
 Definition eq_Zmodp (x y : Zmodp) := (x = y).
 (* Bug if we inline the previous def in the following axiom *)
@@ -70,15 +71,13 @@ Axiom Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x ->
 Trocq Use Reqmodp01.
 Arguments eq_Zmodp /.
 
-Hypothesis RedZmodpEq0 :
-  (forall (m n p : Zmodp), (m = n * n)%Zmodp -> m = (p * p * p)%Zmodp ->
-    m = zerop).
-
-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 *) *)

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.spy-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}]}.