dpexp

dpexp.ec

require import List.
require import OldMonoid.
require import RealExp.
require import RealExtra.
require import FSet.

type R = int.
type util = int list * R -> real.
op du : real.
axiom dupos : du > 0%r.
op eps : real.
axiom epspos : eps > 0%r.
op sum : real list -> real.

module type EXP = {
  proc m(x : int list, u : util, rs : int list) : int
  }.


  
lemma expdp
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
    Pr[Exp.m(x, u, rs) @&m : res = r]
  / Pr[Exp.m(y, u, rs) @&m : res = r]
      <= exp(eps) by admit.

lemma denom (a b x y): (a / b) / (x / y) = (a / x) * (y / b) by smt.
    
lemma expandpr  :
  forall &m,
  forall ( Exp <: EXP) ,
  forall( r : R, x : int list, u : util, rs : int list),
    Pr[Exp.m(x, u, rs) @&m : res = r]
  = exp(eps * u(x, r) / (2%r * du))
  / sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs) by admit.
    
lemma step1
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
  Pr[Exp.m(x, u, rs) @&m : res = r]
/ Pr[Exp.m(y, u, rs) @&m : res = r]
= (exp(eps * u(x, r) / (2%r * du))
  / sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs))
/ (exp(eps * u(y, r) / (2%r * du))
  / sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs)).
  rewrite (expandpr &m Exp r x u rs).
  rewrite (expandpr &m Exp r y u rs).
trivial.
qed.

lemma step2
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
  (exp(eps * u(x, r) / (2%r * du))
  / sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs))
/ (exp(eps * u(y, r) / (2%r * du))
    / sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs))
  = (exp(eps * u(x, r) / (2%r * du))
    /exp(eps * u(y, r) / (2%r * du)))
  * (sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)) by smt.
  
lemma step3
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
  (exp(eps * u(x, r) / (2%r * du))
  /exp(eps * u(y, r) / (2%r * du)))
* (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs))
  = exp(eps * (u(x,r) - u(y,r)) / (2%r * du))
  * (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs)).
  rewrite - expN.
  rewrite - expD.
  rewrite -StdRing.RField.mulrBl.
  rewrite - StdRing.RField.mulrBr.
  trivial.
qed.

lemma dumax (u : util, x : int list, y : int list, r : R):
    u(x, r) - u(y, r) <= du by admit.
    (* missing premise: norm (x, y) <= 1*)   

lemma leq_drist :
 forall (x : real),
    x > 0%r => forall (y z : real), y <= z => x * y <= x * z.
    search (<=>).
    move => a b c d.
    
    apply iffRL.
      apply StdOrder.RealOrder.ler_pmul2l.
    trivial.
qed.   

lemma drist_leq :
 forall (x : real),
    x > 0%r => forall (y z : real), x * y <= x * z => y <= z.
    search (<=>).
    move => a b c d.
    
    apply iffLR.
      apply StdOrder.RealOrder.ler_pmul2l.
    trivial.
qed.   

lemma div_gt1 (x, y: real): 0%r < x => y <= x => y / x <= 1%r by smt.

lemma cancel (x, y, z : real) : x <>0%r => x * y / (z * x) = y / z by smt.
    
lemma duxy_leq_du (x : int list, y : int list, r:R, u : util) :
    exp(eps * ((u(x,r) - u(y,r)) / (2%r * du)))
    <= exp(eps / 2%r).
      apply exp_mono.
      apply (leq_drist eps _ _).
    apply epspos.
    rewrite StdRing.RField.invrM.
      trivial.
      smt(dupos).
   rewrite StdRing.RField.mulrA.
    apply (drist_leq 2%r).
    trivial.
    simplify.
    search ( * ).
    rewrite cancel.
trivial.
      apply div_gt1.
apply dupos.  
apply dumax.
  qed.

lemma sumratio_leq_exp (x, y : int list, r:R, rs: R list, u : util):
    (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
      /sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs))
      <= exp(eps / 2%r)
      * (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
      /sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)) by admit.
  
lemma step4
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
  exp(eps * (u(x,r) - u(y,r)) / (2%r * du))
  * (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(y, r') / (2%r * du))) rs))
 <= exp(eps / 2%r) * exp(eps / 2%r)
  * (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)) by admit.

lemma sum_fun (x) : sum(x) = sum(x) by admit.

lemma n_div (x, y) : x <> 0%r => x = y => x / y = 1%r by smt.
    
lemma step5
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
  exp(eps / 2%r) * exp(eps / 2%r)
  * (sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs)
    /sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs))
  = exp(eps) .
rewrite {1} sum_div.    
smt(epspos).
    rewrite StdRing.RField.unitrE.
  smt.
    progress.