fix build

Author: simongregersen

theories/approxis/examples/prf_cpa.v

@@ -311,7 +311,9 @@ we can split off q/N credits to spend on sampling a fresh element, as required.
       1: { iExists 0.
            iFrame. iSplitL. 2: iPureIntro ; set_solver.
            iApply (ec_eq with "[$]").
-           field_simplify_eq ; try real_solver. nify_r. nat_solver. }
+           field_simplify_eq.
+           - nify_r. nat_solver.
+           - rewrite S_INR. real_solver. }
       iIntros "#Hinv".
       rel_arrow_val ; lrintro "msg"...
       iApply (refines_na_inv with "[$Hinv]"); [done|].

theories/approxis/examples/prf_cpa_combined_sem_typ.v

@@ -512,7 +512,9 @@ Hypothesis refines_tape_couple_avoid : forall `{!approxisRGS Σ} (N:nat) α l z
       assert (q * (q + 1) <= (Q - 1) * Q)%R.
       {
         rewrite -INR_1.
-        apply Rmult_le_compat ; try real_solver.
+        apply Rmult_le_compat.
+        - real_solver.
+        - rewrite -S_INR. real_solver.
         - rewrite -minus_INR. 2: lia. apply le_INR. lia.
         - rewrite -plus_INR. apply le_INR. lia.
       }

theories/approxis/examples/prf_cpa_with_dec.v

@@ -584,7 +584,9 @@ we can split off q/N credits to spend on sampling a fresh element, as required.
       1: { iExists 0.
            iFrame. iSplitL. 2: iPureIntro ; set_solver.
            iApply (ec_eq with "[$]").
-           field_simplify_eq ; try real_solver. nify_r. nat_solver. }
+           field_simplify_eq.
+           - nify_r. nat_solver.
+           - rewrite S_INR. real_solver. }
       iIntros "#Hinv".
       rel_arrow_val ; lrintro "msg"...
       iApply (refines_na_inv with "[$Hinv]"); [done|].

theories/approxis/examples/rejection_samplers.v

@@ -242,7 +242,8 @@ Proof.
     do 3 tp_pure.
     wp_pures.
     iRevert "Hα Hαₛ Hspec".
-    iApply (ec_ind_amp _ (S N / (S N - S M)) with "[] Hε"); [done|real_solver|].
+    iApply (ec_ind_amp _ (S N / (S N - S M)) with "[] Hε"); [done| |].
+    { apply NM1. }
     iIntros "!#" (??) "#IH ????".
     iApply (wp_simpl_rejection_ind_aux with "[$][$][$][$]"); [done|].
     iIntros (? H1) "? Hε ? ?". subst.