Update CertRL for new version of Rocq

Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>

Author: shinnar

coq/CertRL/mdp.v

@@ -96,8 +96,6 @@ Proof.
   eapply FiniteType_fun_dep ; eauto.
   - apply fs.
   - apply fa.
- Unshelve.
- apply st_eqdec.
 Qed.
 
 Global Instance act_finite (M : MDP) : FiniteType (sigT M.(act))
@@ -407,12 +405,19 @@ Proof.
   lra.
 Qed.
 
+
+Definition Rfct_AbelianMonoid_mixin :=
+  AbelianMonoid.Mixin (Rfct A) Rfct_plus Rfct_zero Rfct_plus_comm
+   Rfct_plus_assoc Rfct_plus_zero_r.
+
+Canonical Rfct_AbelianMonoid :=
+  AbelianMonoid.Pack (Rfct A) (Rfct_AbelianMonoid_mixin) (Rfct A).
+
 Definition Rfct_AbelianGroup_mixin :=
-  AbelianGroup.Mixin (Rfct A) Rfct_plus Rfct_opp Rfct_zero Rfct_plus_comm
-   Rfct_plus_assoc Rfct_plus_zero_r Rfct_plus_opp_r.
+  AbelianGroup.Mixin Rfct_AbelianMonoid Rfct_opp Rfct_plus_opp_r.
 
 Canonical Rfct_AbelianGroup :=
-  AbelianGroup.Pack (Rfct A) (Rfct_AbelianGroup_mixin) (Rfct A).
+  AbelianGroup.Pack (Rfct A) (AbelianGroup.Class _ (Rfct_AbelianMonoid_mixin) Rfct_AbelianGroup_mixin) (Rfct A).
 
 End Rfct_AbelianGroup.
 

coq/CertRL/mdp_turtle.v

@@ -253,7 +253,7 @@ End optimal_path.
   Section to_string.
     Section utils.
 
-      Definition newline := String (Ascii.ascii_of_N 10) EmptyString.
+      Definition newline := String (Ascii.ascii_of_N (Npos 10%positive)) EmptyString.
 
       Definition string_bracket (sstart send:string) (smiddle:string)
         := String.append sstart (String.append smiddle send).

coq/CertRL/pmf_prob.v

@@ -127,7 +127,7 @@ Section Pmf_PMF.
              rewrite Forall_forall; intros lmu.
              specialize (lmu _ inn).
              lia.
-          -- destruct (in_dec eq_nat_dec a l); trivial.
+          -- destruct (in_dec Peano_dec.eq_nat_dec a l); trivial.
              specialize (nin _ n).
              unfold nequiv_decb, negb, equiv_decb in non0.
              destruct (equiv_dec (coll a) 0); congruence.
@@ -283,7 +283,7 @@ Section Pmf_PMF.
            (map (fun x : nonnegreal * A => nonneg (fst x))
               (filter (fun x : nonnegreal * A => if equiv_dec a (snd x) then true else false) outcomes))
      | None => 0
-     end) (nodup eq_nat_dec (map countable_index (map snd outcomes))))).
+     end) (nodup Peano_dec.eq_nat_dec (map countable_index (map snd outcomes))))).
     - apply infinite_sum'_finite
       ; intros.
       + match_case; intros.
@@ -389,7 +389,7 @@ Section pmf_prob.
                             (exist (fun _ : pre_event A => True)
                                    (fun omega : A => pre_event_singleton c (rv_X omega))
                                    (sa_preimage_singleton rv_X c)))
-                 (nodup eq_nat_dec (map countable_index (map snd pmf.(outcomes)))))
+                 (nodup Peano_dec.eq_nat_dec (map countable_index (map snd pmf.(outcomes)))))
    ; intros HH.
    cut_to HH.
    - rewrite (infinite_sum'_unique i HH).