Merge pull request #49 from 4ever2/mathcomp-2.3.0

Compatibility with mathcomp 2.3.0
SSProve · Dec 3, 2024 · cb4a367 · cb4a367
2 parents d199572 + 1967aed
commit cb4a367
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 19 deletions.
diff --git a/theories/Crypt/Prelude.v b/theories/Crypt/Prelude.v
@@ -131,7 +131,7 @@ Proof.
   - rewrite expnS. rewrite mulSnr. rewrite mulSnr.
     change (0 * ?n) with 0.
     set (m := 2^n) in *. clearbody m. cbn.
-    rewrite -addnE. rewrite -plusE.
+    rewrite -?addnE. rewrite -plusE.
     lia.
 Qed.
 

diff --git a/theories/Crypt/choice_type.v b/theories/Crypt/choice_type.v
@@ -508,7 +508,8 @@ Section choice_typeTypes.
       destruct n.
       + discriminate.
       + cbn.
-        rewrite -subnE subn0. repeat f_equal. apply eq_irrelevance.
+        rewrite ?subnE /= -subnE subn0.
+        repeat f_equal. apply eq_irrelevance.
   Defined.
 
   HB.instance Definition _ := Choice.copy choice_type (pcan_type codeK).

diff --git a/theories/Crypt/examples/PRFPRG.v b/theories/Crypt/examples/PRFPRG.v
@@ -263,7 +263,7 @@ Proof.
     ssprove_restore_mem;
       last by apply: r_ret.
     ssprove_invariant.
-    2: by rewrite -subnE subSnn.
+    2: by rewrite -?subnE subSnn.
     move {Hinv k Heq} => s0 s1 [[[Hinv _] _] _] loc H.
     rewrite (get_set_heap_neq _ k_loc) -?in_fset1 //.
     case: (eq_dec loc count_loc)=> Heq.
@@ -282,10 +282,10 @@ Proof.
     all: move=> s0 s1 [[Hinv _] H] /=.
     all: rewrite /couple_rhs get_set_heap_eq get_set_heap_neq //.
     all: move /eqP in Hlt.
-    + rewrite Hinv // H -subnE eqnE.
+    + rewrite Hinv // H -?subnE eqnE.
       by rewrite subn_eq0 ltnW // -subn_eq0 Hlt.
     + move /eqP /negPf in Hlt.
-      by rewrite -subnE eqnE Hlt.
+      by rewrite -?subnE eqnE Hlt.
 Qed.
 
 (**
@@ -328,7 +328,7 @@ Proof.
     ssprove_restore_mem;
       last by apply: r_ret.
     ssprove_invariant.
-    2: by rewrite -subnE subSnn.
+    2: by rewrite -?subnE subSnn.
     move {Hinv T Heq} => s0 s1 [[[Hinv A] B] C] loc H /=.
     rewrite !(get_set_heap_neq _ T_loc) -?in_fset1 //.
     case: (eq_dec loc count_loc)=> Heq.
@@ -349,10 +349,10 @@ Proof.
     all: move=> s0 s1 [[Hinv H] _] /=.
     all: rewrite /couple_lhs get_set_heap_eq get_set_heap_neq //.
     all: move /eqP in Hlt.
-    + rewrite Hinv // H -subnE eqnE.
+    + rewrite Hinv // H -?subnE eqnE.
       by rewrite subn_eq0 ltnW // -subn_eq0 Hlt.
     + move /eqP /negPf in Hlt.
-      by rewrite -subnE eqnE Hlt.
+      by rewrite -?subnE eqnE Hlt.
 Qed.
 
 Local Open Scope ring_scope.

diff --git a/theories/Crypt/examples/Schnorr.v b/theories/Crypt/examples/Schnorr.v
@@ -375,7 +375,7 @@ Proof.
                    (@otf Challenge s2))))
        q) =
     (@nat_of_ord (S (S (Zp_trunc q)))
-                   (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))).
+                   (@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
   { simpl.
     rewrite modnDmr.
     destruct (otf s2) as [a Ha].
@@ -400,14 +400,14 @@ Proof.
                       (GRing.opp
                          (@otf Challenge s2)))))
           (@nat_of_ord (S (S (Zp_trunc q)))
-             (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2))))) q) =
+             (@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2))))) q) =
     (Zp_mul
        (GRing.inv
           (GRing.add
              (@otf Challenge s1)
              (GRing.opp
                 (@otf Challenge s2))))
-       (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))).
+       (@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
   { simpl.
     rewrite modnDmr.
     rewrite <- order_ge1 at 9.
@@ -514,7 +514,7 @@ Proof.
            unfold "\notin".
            rewrite in_fset1.
            done.
-        ++ 
+        ++
            rewrite -!fset1E.
            rewrite fdisjoint1s.
             unfold "\notin".
@@ -554,7 +554,7 @@ Proof.
            unfold "\notin".
            rewrite in_fset1.
            done.
-        ++ 
+        ++
            rewrite -!fset1E.
            rewrite fdisjoint1s.
             unfold "\notin".

diff --git a/theories/Crypt/examples/ShamirSecretSharing.v b/theories/Crypt/examples/ShamirSecretSharing.v
@@ -833,7 +833,7 @@ Proof.
 Qed.
 
 Instance p_pow_positive t:
-  Positive (p^t).
+  Positive (p ^ t).
 Proof.
   by rewrite /Positive expn_gt0 prime_gt0.
 Qed.
@@ -851,7 +851,7 @@ Qed.
   Finally we combine all three bijections to create a bijection from [PolyEnc t]
   to [PolyEnc t] that we can use to prove security of the protocol.
 *)
-Definition PolyEnc t := 'fin (p^t).
+Definition PolyEnc t := 'fin (p ^ t).
 
 #[program] Definition mod_p (a: nat): Word :=
   @Ordinal _ (a %% p) _.
@@ -889,7 +889,7 @@ Proof.
 Qed.
 
 Lemma size_poly_to_nat (t: nat) (q: {poly Word}):
-  poly_to_nat t q < p^t.
+  poly_to_nat t q < p ^ t.
 Proof.
   elim: t => [// | t IHt] /= in q*.
   apply: (@leq_trans (poly_to_nat t (tail_poly q) * p + p)).
@@ -899,7 +899,7 @@ Proof.
 Qed.
 
 Lemma nat_poly_nat (t a: nat):
-  a < p^t ->
+  a < p ^ t ->
   poly_to_nat t (nat_to_poly t a) = a.
 Proof.
   elim: t a => [|t IHt] a H.
@@ -991,7 +991,7 @@ Definition SHARE_pkg_tt:
     #def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'seq 'share {
       if size (domm U) >= t then ret emptym
       else
-      q <$ uniform (p^t') ;;
+      q <$ uniform (p ^ t') ;;
       let q := nat_to_poly t' q in
       let sh := make_shares ml q (domm U) in
       ret (fmap_of_seq sh)
@@ -1005,7 +1005,7 @@ Definition SHARE_pkg_ff:
     #def #[shares] ('(ml, mr, U): ('word × 'word) × 'set 'party): 'seq 'share {
       if size (domm U) >= t then ret emptym
       else
-      q <$ uniform (p^t') ;;
+      q <$ uniform (p ^ t') ;;
       let q := nat_to_poly t' q in
       let sh := make_shares mr q (domm U) in
       ret (fmap_of_seq sh)