fix Nat.Div0 references for CI

logsem · Jan 25, 2024 · 09721cd · 09721cd
1 parent 425d15b
commit 09721cd
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 17 deletions.
diff --git a/theories/examples/approximate_samplers/approx_rejection_sampler_presampled.v b/theories/examples/approximate_samplers/approx_rejection_sampler_presampled.v
@@ -34,14 +34,10 @@ Section presampled_flip2.
     iAssert (flip2_junk_inv _ _ _ (length (junk ++ block_pad (Z.to_nat 0) 2 junk) `div` 2) _) with "[Hα]" as "Hinv".
     { rewrite /flip2_junk_inv app_assoc.
       iExists _; iFrame; iPureIntro.
-
-      (* Works but breaks CI
-      apply Nat.Div0.div_exact.
+      apply Nat.div_exact; [lia|].
       rewrite app_length.
       apply (blocks_aligned (Z.to_nat 0%nat) 2%nat).
       lia.
-       *)
-      admit.
     }
     do 11 wp_pure.
     iInduction (length (junk ++ block_pad (Z.to_nat 0) 2 junk) `div` 2) as [|k'] "IH".
@@ -68,5 +64,5 @@ Section presampled_flip2.
       + wp_pures; iModIntro; iExists _; auto.
       + wp_pure. iApply "IH".
       + do 2 wp_pure; iApply "IH".
-  Admitted.
+  Qed.
 End presampled_flip2.
diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
@@ -1153,18 +1153,13 @@ Proof.
   intros Hblocksize junk.
   rewrite /block_pad.
   rewrite repeat_length.
-
-  (* This proof works, but it breaks CI *)
-  (*
-  rewrite -PeanoNat.Nat.Div0.add_mod_idemp_l -PeanoNat.Nat.Div0.add_mod -PeanoNat.Nat.Div0.add_mod_idemp_l.
-  rewrite -Nat.le_add_sub; [apply PeanoNat.Nat.Div0.mod_same|].
-  edestruct Nat.mod_bound_pos as [? H]; last first.
-  - eapply Nat.lt_le_incl, H.
-  - lia.
-  - lia.
+  rewrite -PeanoNat.Nat.add_mod_idemp_l; [|lia].
+  rewrite -PeanoNat.Nat.add_mod; [|lia].
+  rewrite -PeanoNat.Nat.add_mod_idemp_l; [|lia].
+  rewrite -Nat.le_add_sub; [apply Nat.mod_same; lia|].
+  apply Nat.lt_le_incl.
+  apply Nat.mod_bound_pos; [apply Nat.le_0_l | done].
 Qed.
-  *)
-Admitted.
 
 Lemma block_pad_ub N blocksize : (0 < blocksize) -> forall junk, (length (block_pad N blocksize junk) <= blocksize)%nat.
 Proof.