Skip to content

Commit 50a3039

Browse files
loutrstrub
loutr
authored and
strub
committed
feat(Pr-rewrite): Support for the new mu1_leq_eq_mu1 lemma
1 parent 3501e37 commit 50a3039

File tree

2 files changed

+134
-89
lines changed

2 files changed

+134
-89
lines changed

‎src/phl/ecPhlPrRw.ml‎

Lines changed: 98 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,17 @@ let t_pr_lemma lemma tc =
1818
(* -------------------------------------------------------------------- *)
1919
let pr_eq env m f args p1 p2 =
2020
let mem = Fun.prF_memenv mhr f env in
21-
let hyp = f_forall_mems [mem] (f_iff p1 p2) in
21+
let hyp = f_forall_mems [ mem ] (f_iff p1 p2) in
2222
let concl = f_eq (f_pr m f args p1) (f_pr m f args p2) in
23-
f_imp hyp (f_eq concl f_true)
23+
f_imp hyp (f_eq concl f_true)
2424

2525
let pr_sub env m f args p1 p2 =
2626
let mem = Fun.prF_memenv mhr f env in
27-
let hyp = f_forall_mems [mem] (f_imp p1 p2) in
27+
let hyp = f_forall_mems [ mem ] (f_imp p1 p2) in
2828
let concl = f_real_le (f_pr m f args p1) (f_pr m f args p2) in
29-
f_imp hyp (f_eq concl f_true)
29+
f_imp hyp (f_eq concl f_true)
3030

31-
let pr_false m f args =
32-
f_eq (f_pr m f args f_false) f_r0
31+
let pr_false m f args = f_eq (f_pr m f args f_false) f_r0
3332

3433
let pr_not m f args p =
3534
f_eq
@@ -41,18 +40,18 @@ let pr_or m f args por p1 p2 =
4140
let pr2 = f_pr m f args p2 in
4241
let pr12 = f_pr m f args (f_and p1 p2) in
4342
let pr = f_real_sub (f_real_add pr1 pr2) pr12 in
44-
f_eq (f_pr m f args (por p1 p2)) pr
43+
f_eq (f_pr m f args (por p1 p2)) pr
4544

4645
let pr_disjoint env m f args por p1 p2 =
4746
let mem = Fun.prF_memenv mhr f env in
48-
let hyp = f_forall_mems [mem] (f_not (f_and p1 p2)) in
47+
let hyp = f_forall_mems [ mem ] (f_not (f_and p1 p2)) in
4948
let pr1 = f_pr m f args p1 in
5049
let pr2 = f_pr m f args p2 in
51-
let pr = f_real_add pr1 pr2 in
52-
f_imp hyp (f_eq (f_pr m f args (por p1 p2)) pr)
50+
let pr = f_real_add pr1 pr2 in
51+
f_imp hyp (f_eq (f_pr m f args (por p1 p2)) pr)
5352

5453
let pr_split m f args ev1 ev2 =
55-
let pr = f_pr m f args ev1 in
54+
let pr = f_pr m f args ev1 in
5655
let pr1 = f_pr m f args (f_and ev1 ev2) in
5756
let pr2 = f_pr m f args (f_and ev1 (f_not ev2)) in
5857
f_eq pr (f_real_add pr1 pr2)
@@ -68,129 +67,139 @@ let pr_le1 m f args ev =
6867
let pr_sum env pr =
6968
let prf = EcEnv.Fun.by_xpath pr.pr_fun env in
7069
let xty = prf.f_sig.fs_ret in
71-
let x = EcIdent.create "x" in
72-
let fx = f_local x xty in
70+
let x = EcIdent.create "x" in
71+
let fx = f_local x xty in
7372

7473
let prx =
7574
let event =
76-
f_and_simpl
77-
pr.pr_event
78-
(f_eq (f_pvar EcTypes.pv_res xty EcFol.mhr) fx)
79-
in f_pr pr.pr_mem pr.pr_fun pr.pr_args event in
75+
f_and_simpl pr.pr_event (f_eq (f_pvar EcTypes.pv_res xty EcFol.mhr) fx)
76+
in
77+
f_pr pr.pr_mem pr.pr_fun pr.pr_args event
78+
in
8079

8180
let prx =
8281
EcFol.f_app
83-
(EcFol.f_op
84-
EcCoreLib.CI_Sum.p_sum
85-
[xty]
82+
(EcFol.f_op EcCoreLib.CI_Sum.p_sum [ xty ]
8683
(EcTypes.tfun (EcTypes.tfun xty EcTypes.treal) EcTypes.treal))
87-
[EcFol.f_lambda [x, GTty xty] prx]
84+
[ EcFol.f_lambda [ (x, GTty xty) ] prx ]
8885
EcTypes.treal
8986
in
9087

9188
f_eq (f_pr_r pr) prx
9289

90+
let pr_mu1_le_eq_mu1 m f args resv k fresh_id d =
91+
let kfresh = f_local fresh_id k.f_ty in
92+
let f_ll = f_bdHoareF f_true f f_true FHeq f_r1
93+
and f_le_mu1 = f_forall [ (fresh_id, gtty k.f_ty) ]
94+
(f_real_le (f_pr m f args (f_eq resv kfresh)) (f_mu_x d kfresh))
95+
and concl =
96+
f_eq (f_pr m f args (f_eq resv k)) (f_mu_x d k) in
97+
f_imp f_ll (f_imp f_le_mu1 concl)
98+
9399
(* -------------------------------------------------------------------- *)
94100
exception FoundPr of form
95101

96102
let select_pr on_ev sid f =
97103
match f.f_node with
98104
| Fpr { pr_event = ev } ->
99-
if on_ev ev && Mid.set_disjoint f.f_fv sid
100-
then raise (FoundPr f)
105+
if on_ev ev && Mid.set_disjoint f.f_fv sid then raise (FoundPr f)
101106
else false
102107
| _ -> false
103108

104109
let select_pr_cmp on_cmp sid f =
105110
match f.f_node with
106-
| Fapp({f_node = Fop(op,_)},
107-
[{f_node = Fpr pr1};
108-
{f_node = Fpr pr2}]) ->
109-
110-
if on_cmp op
111-
&& EcIdent.id_equal pr1.pr_mem pr2.pr_mem
112-
&& EcPath.x_equal pr1.pr_fun pr2.pr_fun
113-
&& f_equal pr1.pr_args pr2.pr_args
114-
&& Mid.set_disjoint f.f_fv sid
111+
| Fapp
112+
({ f_node = Fop (op, _) }, [ { f_node = Fpr pr1 }; { f_node = Fpr pr2 } ])
113+
->
114+
if on_cmp op
115+
&& EcIdent.id_equal pr1.pr_mem pr2.pr_mem
116+
&& EcPath.x_equal pr1.pr_fun pr2.pr_fun
117+
&& f_equal pr1.pr_args pr2.pr_args
118+
&& Mid.set_disjoint f.f_fv sid
115119
then raise (FoundPr f)
116120
else false
117-
118121
| _ -> false
119122

120123
let select_pr_ge0 sid f =
121124
match f.f_node with
122-
| Fapp({f_node = Fop(op,_)}, [f'; {f_node = Fpr _}]) ->
123-
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
124-
&& f_equal f' f_r0
125-
&& Mid.set_disjoint f.f_fv sid
125+
| Fapp ({ f_node = Fop (op, _) }, [ f'; { f_node = Fpr _ } ]) ->
126+
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
127+
&& f_equal f' f_r0
128+
&& Mid.set_disjoint f.f_fv sid
126129
then raise (FoundPr f)
127130
else false
128-
129131
| _ -> false
130132

131133
let select_pr_le1 sid f =
132134
match f.f_node with
133-
| Fapp({f_node = Fop(op,_)}, [{f_node = Fpr _}; f']) ->
134-
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
135-
&& f_equal f' f_r1
136-
&& Mid.set_disjoint f.f_fv sid
135+
| Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr _ }; f' ]) ->
136+
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
137+
&& f_equal f' f_r1
138+
&& Mid.set_disjoint f.f_fv sid
137139
then raise (FoundPr f)
138140
else false
139-
140141
| _ -> false
141142

142143
(* -------------------------------------------------------------------- *)
143-
let pr_rewrite_lemma = [
144-
"mu_eq" , `MuEq;
145-
"mu_sub" , `MuSub;
146-
"mu_false" , `MuFalse;
147-
"mu_not" , `MuNot;
148-
"mu_or" , `MuOr;
149-
"mu_disjoint", `MuDisj;
150-
"mu_split" , `MuSplit;
151-
"mu_ge0" , `MuGe0;
152-
"mu_le1" , `MuLe1;
153-
"muE" , `MuSum;
154-
]
144+
let pr_rewrite_lemma =
145+
[
146+
("mu1_le_eq_mu1", `Mu1LeEqMu1);
147+
("muE", `MuSum);
148+
("mu_disjoint", `MuDisj);
149+
("mu_eq", `MuEq);
150+
("mu_false", `MuFalse);
151+
("mu_ge0", `MuGe0);
152+
("mu_le1", `MuLe1);
153+
("mu_not", `MuNot);
154+
("mu_or", `MuOr);
155+
("mu_split", `MuSplit);
156+
("mu_sub", `MuSub);
157+
]
155158

156159
(* -------------------------------------------------------------------- *)
157-
let t_pr_rewrite_low (s,dof) tc =
160+
let t_pr_rewrite_low (s, dof) tc =
158161
let kind =
159-
try List.assoc s pr_rewrite_lemma with Not_found ->
160-
tc_error !!tc "do not reconize %s as a probability lemma" s in
162+
try List.assoc s pr_rewrite_lemma
163+
with Not_found ->
164+
tc_error !!tc "Pr-rewrite: `%s` is not a suitable probability lemma" s
165+
in
161166

162-
let check_f dof =
163-
match kind, dof with
164-
| `MuSplit, None -> tc_error !!tc "argument expected for %s" s
165-
| `MuSplit, Some _ -> ()
166-
| _, Some _ -> tc_error !!tc "no argument expected for %s" s
167-
| _, _ -> () in
168-
check_f dof;
167+
let expect_arg = function `MuSplit | `Mu1LeEqMu1 -> true | _ -> false in
168+
(if not (is_some dof = expect_arg kind) then
169+
let neg = if is_some dof then "no " else "" in
170+
tc_error !!tc "Pr-rewrite: %sargument expected for `%s`" neg s);
169171

170172
let select =
171173
match kind with
172-
| `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq)
173-
| `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le)
174+
| `Mu1LeEqMu1 -> select_pr is_eq
175+
| `MuDisj | `MuOr -> select_pr is_or
176+
| `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq)
174177
| `MuFalse -> select_pr is_false
175-
| `MuNot -> select_pr is_not
176-
| `MuOr
177-
| `MuDisj -> select_pr is_or
178+
| `MuGe0 -> select_pr_ge0
179+
| `MuLe1 -> select_pr_le1
180+
| `MuNot -> select_pr is_not
178181
| `MuSplit -> select_pr (fun _ev -> true)
179-
| `MuGe0 -> select_pr_ge0
180-
| `MuLe1 -> select_pr_le1
181-
| `MuSum -> select_pr (fun _ev -> true)
182+
| `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le)
183+
| `MuSum -> select_pr (fun _ev -> true)
182184
in
183185

184186
let select xs fp = if select xs fp then `Accept (-1) else `Continue in
185-
let env, _, concl = FApi.tc1_eflat tc in
187+
let env, hyps, concl = FApi.tc1_eflat tc in
186188
let torw =
187189
try
188190
ignore (EcMatching.FPosition.select select concl);
189-
tc_error !!tc "cannot find a pattern for %s" s
191+
tc_error !!tc "Pr-rewrite: cannot find a pattern for `%s`" s
190192
with FoundPr f -> f in
191193

192194
let lemma, args =
193195
match kind with
196+
| `Mu1LeEqMu1 ->
197+
let { pr_mem; pr_fun; pr_args; pr_event } = destr_pr torw in
198+
let (resv, k) = destr_eq pr_event in
199+
let k_id = EcEnv.LDecl.fresh_id hyps "k" in
200+
let d = (oget dof) tc torw (EcTypes.tdistr k.f_ty) in
201+
(pr_mu1_le_eq_mu1 pr_mem pr_fun pr_args resv k k_id d, 2)
202+
194203
| (`MuEq | `MuSub as kind) -> begin
195204
match torw.f_node with
196205
| Fapp(_, [{f_node = Fpr ({ pr_event = ev1 } as pr) };
@@ -225,7 +234,7 @@ let t_pr_rewrite_low (s,dof) tc =
225234

226235
| `MuSplit ->
227236
let pr = destr_pr torw in
228-
let ev' = (oget dof) tc torw in
237+
let ev' = (oget dof) tc torw EcTypes.tbool in
229238
(pr_split pr.pr_mem pr.pr_fun pr.pr_args pr.pr_event ev', 0)
230239

231240
| `MuGe0 -> begin
@@ -255,16 +264,16 @@ let t_pr_rewrite_low (s,dof) tc =
255264
(t_pr_lemma lemma)
256265
(t_rewrite rwpt (`LtoR, None) tc)
257266

258-
let t_pr_rewrite_i (s,f) tc =
259-
let do_ev = omap (fun f _ _ -> f) f in
260-
t_pr_rewrite_low (s,do_ev) tc
261-
262-
let t_pr_rewrite (s,f) tc =
263-
let do_ev =
264-
omap (fun f tc torw ->
265-
let env,hyps,_ = FApi.tc1_eflat tc in
266-
let pr = destr_pr torw in
267-
let mp = EcEnv.Fun.prF_memenv EcFol.mhr pr.pr_fun env in
268-
let hyps = LDecl.push_active mp hyps in
269-
EcProofTyping.process_formula hyps f) f in
270-
t_pr_rewrite_low (s,do_ev) tc
267+
let t_pr_rewrite_i (s, f) tc =
268+
let do_ev = omap (fun f _ _ _ -> f) f in
269+
t_pr_rewrite_low (s, do_ev) tc
270+
271+
let t_pr_rewrite (s, f) tc =
272+
let to_env f tc torw ty =
273+
let env, hyps, _ = FApi.tc1_eflat tc in
274+
let pr = destr_pr torw in
275+
let mp = EcEnv.Fun.prF_memenv EcFol.mhr pr.pr_fun env in
276+
let hyps = LDecl.push_active mp hyps in
277+
EcProofTyping.process_form hyps f ty
278+
in
279+
t_pr_rewrite_low (s, omap to_env f) tc

‎theories/distributions/Distr.ec‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -376,6 +376,42 @@ qed.
376376
lemma mu_le_weight ['a] (d : 'a distr) p : mu d p <= weight d.
377377
proof. by apply/mu_le. qed.
378378
379+
lemma mu_le_eq ['a] (d1 d2 : 'a distr) :
380+
is_lossless d1 =>
381+
(forall p, mu d1 p <= mu d2 p) =>
382+
d1 = d2.
383+
proof.
384+
rewrite eq_distr => d1_ll d1_leq_d2 x.
385+
case (mu1 d1 x = mu1 d2 x) => // *.
386+
suff: (weight d1 < weight d2) by smt(mu_bounded).
387+
have weight_decomp : forall d,
388+
weight d = mu1 d x + mu d (predC (pred1 x)) by smt(mu_not).
389+
do 2 ! rewrite weight_decomp.
390+
by apply ltr_le_add => /#.
391+
qed.
392+
393+
lemma mu1_le_eq ['a] (d1 d2 : 'a distr) :
394+
is_lossless d1 =>
395+
(forall x, mu1 d1 x <= mu1 d2 x) =>
396+
d1 = d2.
397+
proof.
398+
move => d1_ll d1_leq_d2.
399+
apply mu_le_eq => // p.
400+
rewrite muE muE.
401+
apply RealSeries.ler_sum; 2,3: exact summable_mu1_cond.
402+
move => x. case: (p x) => /> *.
403+
exact d1_leq_d2.
404+
qed.
405+
406+
lemma mu1_le_eq_mu1 ['a] (d1 d2 : 'a distr) :
407+
is_lossless d1 =>
408+
(forall x, mu1 d1 x <= mu1 d2 x) =>
409+
forall x, mu1 d1 x = mu1 d2 x.
410+
proof.
411+
move => d1_ll d1_le_d2.
412+
by rewrite (mu1_le_eq d1_ll d1_le_d2).
413+
qed.
414+
379415
(* -------------------------------------------------------------------- *)
380416
381417
lemma mu_has_le ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) :

0 commit comments

Comments
 (0)