replace fsdist_convA by its generic version convA0 (#122)

affeldt-aist · Jan 3, 2025 · a640c19 · a640c19
1 parent ed161f2
commit a640c19
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 21 deletions.
diff --git a/theories/applications/smallstep.v b/theories/applications/smallstep.v
@@ -34,8 +34,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Bullet Behavior "Strict Subproofs".
-
 Obligation Tactic := idtac.
 
 Reserved Notation "'p_do' x <- m ; e"
@@ -198,10 +196,10 @@ induction Hss1 as [
   | sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
   ].
   + subst sk1' l2 sk2.
-    do 3 eexists.
-    split; [ apply ss_refl | ].
-    split; [ eapply ss_step_None; eassumption | ].
-    rewrite cats0; reflexivity.
+    exists [::], l1, sk3.
+    split; first exact: ss_refl.
+    split; first exact: (ss_step_None Hstep1 Hss1).
+    by rewrite cats0.
   + subst sk1' l2' sk2'''.
     specialize (step_deterministic Hstep1 Hstep2).
     intros [ [] Heq2].
@@ -210,18 +208,18 @@ induction Hss1 as [
     exact Hss2'.
   + subst sk1' l2 sk2'''.
     specialize (step_deterministic Hstep1 Hstep2).
-    intros [ [=] ?].
+    by move=> [].
 - intros l2 sk2 Hss2.
   inversion Hss2 as [
     sk1' Hsk1 Hl2 Hsk2
   | sk1' sk2'' sk2''' l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
   | sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
   ].
   + subst sk1' l2 sk2.
-    do 3 eexists.
-    split; [ apply ss_refl | ].
-    split; [ eapply ss_step_Some; eassumption | ].
-    rewrite cats0; reflexivity.
+    exists [::], (t1 :: l1),  sk3.
+    split; first exact: ss_refl.
+    split; first exact: (ss_step_Some Hstep1).
+    by rewrite cats0.
   + subst sk1' l2' sk2'''.
     specialize (step_deterministic Hstep1 Hstep2).
     intros [ [=] ?].
@@ -231,11 +229,8 @@ induction Hss1 as [
     subst t2 sk2''.
     apply IH in Hss2'.
     destruct Hss2' as (l1' & l2'' & skf & Hss3 & Hss4 & Heq).
-    do 3 eexists.
-    do 2 (split; [ eassumption | ]).
-    cbn.
-    f_equal.
-    exact Heq.
+    exists l1', l2'', skf; split => //; split => //.
+    by rewrite /= Heq.
 Qed.
 
 Lemma step_star_deterministic ski l1 l2 s1 s2 A1 A2 a1 a2 :

diff --git a/theories/models/proba_monad_model.v b/theories/models/proba_monad_model.v
@@ -3,7 +3,7 @@
 Require Import Reals.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
-From mathcomp Require Import reals Rstruct.
+From mathcomp Require Import mathcomp_extra reals Rstruct.
 From infotheo Require Import Reals_ext realType_ext ssr_ext fsdist.
 From infotheo Require Import convex.
 From HB Require Import structures.
@@ -62,12 +62,13 @@ Let choicemm : forall (T : Type) p, idempotent (@choice p T).
 Proof. by move=> ? ? ?; exact: convmm. Qed.
 
 Let choiceA : forall (T : Type) (p q r s : {prob R}) (a b c : acto T),
-    choice p _ a (choice q _ b c) = choice [s_of p, q] _ (choice [r_of p, q] _ a b) c.
+  choice p _ a (choice q _ b c) = choice [s_of p, q] _ (choice [r_of p, q] _ a b) c.
 Proof.
 move=> ? p q r s a b c.
-rewrite /choice.
-rewrite [LHS](_ : _ = conv p a (conv q b c))//. (* NB: this is slow *)
-by rewrite convA.
+rewrite /choice -/(conv p a (conv q b c)) -/(conv s (conv r a b) c).
+apply: convA0 => /=; rewrite RmultE.
+  by rewrite -p_is_rs.
+by rewrite s_of_pqE onemK.
 Qed.
 
 HB.instance Definition _ := isMonadConvex.Build R