require import AllCore Distr DBool.

type input. 

module type A = {
  proc main(x:input) : bool
}.

module RandomLR(L:A) (R:A) = {
  proc main (x:input) = { 
    var b,r : bool;
    b <${0,1};
    if (b)  r <@ L.main(x);
    else r <@ R.main(x);
    return (b = r);
  }
}.

section.

  declare module L <: A.
  declare module R <: A.

  local module Aux = {
    var b,r : bool
    proc main (x:input) = { 
      b <${0,1};
      if (b)  r <@ L.main(x);
      else r <@ R.main (x);
      return (b = r);
    }
  }.

  lemma pr_AdvLR_AdvRndLR &m (x' : input): 
     Pr[R.main(x') @ &m : true] = 1%r =>
     `| Pr[L.main (x') @ &m : res] - Pr[R.main (x') @ &m : res] | =
     2%r * `| Pr[RandomLR(L, R).main(x') @ &m : res] - 1%r/2%r |.
  proof.
    move => Hll.
    have -> : Pr[RandomLR(L, R).main(x') @ &m : res] = Pr[Aux.main(x') @ &m : res].
    + by byequiv => //; proc; sim=> /#.
    have -> : Pr[Aux.main(x') @ &m : res] = 
              Pr[Aux.main(x') @ &m : res /\ Aux.b] +  
              Pr[Aux.main(x') @ &m : res /\ !Aux.b].
    + by rewrite Pr [mu_split Aux.b].
    have -> : Pr[Aux.main(x') @ &m : res /\ Aux.b] = 1%r/2%r * Pr[L.main (x') @ &m : res].
    + byphoare (_: (glob L) = (glob L){m} /\ x = x' ==> res /\ Aux.b) => //.
      proc; pose p := Pr[L.main(x') @ &m : res]. (* FIXME assert false without the pose *)
      seq 1 : (Aux.b = true /\ x = x') (1%r/2%r) p  _ 0%r (glob L = (glob L){m} /\ x = x'); 1:by auto.
      + by rnd (pred1 true); skip => />; rewrite dbool1E.
      + if; last by (conseq (_: false ==> _); 1:by smt()); auto.
        conseq (_ : _ ==> Aux.r) => //; 1:by smt().
        call (_: x = x' /\ glob L = (glob L){m} ==> res); last by auto.  
        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true).    
      + by (conseq (_: _ ==> false); 1:smt()); auto.
      smt().
    have -> : Pr[Aux.main(x') @ &m : res /\ !Aux.b] = 1%r/2%r * Pr[R.main (x') @ &m : !res].
    + byphoare (_: (glob R) = (glob R){m} /\ x = x' ==> res /\ !Aux.b) => //.
      proc; pose p := Pr[R.main(x') @ &m : !res]. 
      seq 1 : (Aux.b = false /\ x = x') (1%r/2%r) p  _ 0%r (glob R = (glob R){m} /\ x = x'); 1:by auto.
      + by rnd (pred1 false); skip => />; rewrite dbool1E.
      + if; first by (conseq (_: false ==> _); 1:by smt()); auto.
        conseq (_ : _ ==> !Aux.r) => //; 1:by smt().
        call (_: x = x' /\ glob R = (glob R){m} ==> !res); last by auto.
        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true). 
      + by (conseq (_: _ ==> false); 1:smt()); auto.
      smt().
    rewrite Pr [mu_not] Hll /#.
  qed.

end section.