fix the bug

Author: namasikanam

src/phl/ecPhlRnd.ml

@@ -467,7 +467,7 @@ module Core = struct
         (* Goal: dmap d1 g = d2 /\ forall a b, b = g(a) => psi[x -> a, y -> b] *)
         let dmap_op = EcPath.extend EcCoreLib.p_top ["Distr"; "dmap"] in
         let dmap_ty = tfun (tdistr tyL) (tfun (tfun tyL tyR) (tdistr tyR)) in
-        let dmap_pred = f_eq (f_app (f_op dmap_op [tyL; tyR] dmap_ty) [muL; g] tyR) muR in
+        let dmap_pred = f_eq (f_app (f_op dmap_op [tyL; tyR] dmap_ty) [muL; g] (tdistr tyR)) muR in
 
         let a_id = EcIdent.create "a" in
         let b_id = EcIdent.create "b" in

tests/coupling-rnd.ec

@@ -87,16 +87,15 @@ proc.
 coupling{1} f.
 wp; skip => @/predT /=.
 + split.
-  + admit.
-(*   + apply eq_distr. *)
-(* rewrite dbiased1E. *)
-(* rewrite clamp_id. *)
-(* + exact mu_bounded. *)
-(* rewrite dmap1E /pred1 /(\o) /=. *)
-(* case b => _. *)
-(* + by apply mu_eq => x /#. *)
-(* rewrite (mu_eq _ _ (predC test)). *)
-(* + by smt(). *)
-(* by rewrite mu_not D_ll. *)
-  + by rewrite /f //.
+  + apply eq_distr => b.
+    rewrite dbiased1E.
+    rewrite clamp_id.
+    + exact mu_bounded.
+    rewrite dmap1E /pred1 /(\o) /=.
+    case b => _.
+    + by apply mu_eq => x /#.
+    rewrite (mu_eq _ _ (predC test)).
+    + by smt().
+    by rewrite mu_not D_ll.
+  + by move => @/f //.
 qed.