Skip to content

Commit b2a4c86

Browse files
oskgooskgo
authored
Merge branch 'main' into softcode-memories2
2 parents 0eb3285 + 50a3039 commit b2a4c86

File tree

2 files changed

+132
-86
lines changed

2 files changed

+132
-86
lines changed

‎src/phl/ecPhlPrRw.ml

Lines changed: 96 additions & 86 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,140 @@ 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 =
7675
f_and_simpl
7776
pr.pr_event
7877
(f_eq (f_pvar EcTypes.pv_res xty EcFol.mhr).inv fx)
79-
in f_pr pr.pr_mem pr.pr_fun pr.pr_args event in
78+
in
79+
f_pr pr.pr_mem pr.pr_fun pr.pr_args event in
8080

8181
let prx =
8282
EcFol.f_app
83-
(EcFol.f_op
84-
EcCoreLib.CI_Sum.p_sum
85-
[xty]
83+
(EcFol.f_op EcCoreLib.CI_Sum.p_sum [ xty ]
8684
(EcTypes.tfun (EcTypes.tfun xty EcTypes.treal) EcTypes.treal))
87-
[EcFol.f_lambda [x, GTty xty] prx]
85+
[ EcFol.f_lambda [ (x, GTty xty) ] prx ]
8886
EcTypes.treal
8987
in
9088

9189
f_eq (f_pr_r pr) prx
9290

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

96103
let select_pr on_ev sid f =
97104
match f.f_node with
98105
| Fpr { pr_event = ev } ->
99-
if on_ev ev && Mid.set_disjoint f.f_fv sid
100-
then raise (FoundPr f)
106+
if on_ev ev && Mid.set_disjoint f.f_fv sid then raise (FoundPr f)
101107
else false
102108
| _ -> false
103109

104110
let select_pr_cmp on_cmp sid f =
105111
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
112+
| Fapp
113+
({ f_node = Fop (op, _) }, [ { f_node = Fpr pr1 }; { f_node = Fpr pr2 } ])
114+
->
115+
if on_cmp op
116+
&& EcIdent.id_equal pr1.pr_mem pr2.pr_mem
117+
&& EcPath.x_equal pr1.pr_fun pr2.pr_fun
118+
&& f_equal pr1.pr_args pr2.pr_args
119+
&& Mid.set_disjoint f.f_fv sid
115120
then raise (FoundPr f)
116121
else false
117-
118122
| _ -> false
119123

120124
let select_pr_ge0 sid f =
121125
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
126+
| Fapp ({ f_node = Fop (op, _) }, [ f'; { f_node = Fpr _ } ]) ->
127+
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
128+
&& f_equal f' f_r0
129+
&& Mid.set_disjoint f.f_fv sid
126130
then raise (FoundPr f)
127131
else false
128-
129132
| _ -> false
130133

131134
let select_pr_le1 sid f =
132135
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
136+
| Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr _ }; f' ]) ->
137+
if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op
138+
&& f_equal f' f_r1
139+
&& Mid.set_disjoint f.f_fv sid
137140
then raise (FoundPr f)
138141
else false
139-
140142
| _ -> false
141143

142144
(* -------------------------------------------------------------------- *)
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-
]
145+
let pr_rewrite_lemma =
146+
[
147+
("mu1_le_eq_mu1", `Mu1LeEqMu1);
148+
("muE", `MuSum);
149+
("mu_disjoint", `MuDisj);
150+
("mu_eq", `MuEq);
151+
("mu_false", `MuFalse);
152+
("mu_ge0", `MuGe0);
153+
("mu_le1", `MuLe1);
154+
("mu_not", `MuNot);
155+
("mu_or", `MuOr);
156+
("mu_split", `MuSplit);
157+
("mu_sub", `MuSub);
158+
]
155159

156160
(* -------------------------------------------------------------------- *)
157-
let t_pr_rewrite_low (s,dof) tc =
161+
let t_pr_rewrite_low (s, dof) tc =
158162
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
163+
try List.assoc s pr_rewrite_lemma
164+
with Not_found ->
165+
tc_error !!tc "Pr-rewrite: `%s` is not a suitable probability lemma" s
166+
in
161167

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;
168+
let expect_arg = function `MuSplit | `Mu1LeEqMu1 -> true | _ -> false in
169+
(if not (is_some dof = expect_arg kind) then
170+
let neg = if is_some dof then "no " else "" in
171+
tc_error !!tc "Pr-rewrite: %sargument expected for `%s`" neg s);
169172

170173
let select =
171174
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)
175+
| `Mu1LeEqMu1 -> select_pr is_eq
176+
| `MuDisj | `MuOr -> select_pr is_or
177+
| `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq)
174178
| `MuFalse -> select_pr is_false
175-
| `MuNot -> select_pr is_not
176-
| `MuOr
177-
| `MuDisj -> select_pr is_or
179+
| `MuGe0 -> select_pr_ge0
180+
| `MuLe1 -> select_pr_le1
181+
| `MuNot -> select_pr is_not
178182
| `MuSplit -> select_pr (fun _ev -> true)
179-
| `MuGe0 -> select_pr_ge0
180-
| `MuLe1 -> select_pr_le1
181-
| `MuSum -> select_pr (fun _ev -> true)
183+
| `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le)
184+
| `MuSum -> select_pr (fun _ev -> true)
182185
in
183186

184187
let select xs fp = if select xs fp then `Accept (-1) else `Continue in
185-
let env, _, concl = FApi.tc1_eflat tc in
188+
let env, hyps, concl = FApi.tc1_eflat tc in
186189
let torw =
187190
try
188191
ignore (EcMatching.FPosition.select select concl);
189-
tc_error !!tc "cannot find a pattern for %s" s
192+
tc_error !!tc "Pr-rewrite: cannot find a pattern for `%s`" s
190193
with FoundPr f -> f in
191194

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

226236
| `MuSplit ->
227237
let pr = destr_pr torw in
228-
let ev' = (oget dof) tc torw in
238+
let ev' = (oget dof) tc torw EcTypes.tbool in
229239
(pr_split pr.pr_mem pr.pr_fun pr.pr_args pr.pr_event ev', 0)
230240

231241
| `MuGe0 -> begin
@@ -255,16 +265,16 @@ let t_pr_rewrite_low (s,dof) tc =
255265
(t_pr_lemma lemma)
256266
(t_rewrite rwpt (`LtoR, None) tc)
257267

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
268+
let t_pr_rewrite_i (s, f) tc =
269+
let do_ev = omap (fun f _ _ _ -> f) f in
270+
t_pr_rewrite_low (s, do_ev) tc
271+
272+
let t_pr_rewrite (s, f) tc =
273+
let to_env f tc torw ty =
274+
let env, hyps, _ = FApi.tc1_eflat tc in
275+
let pr = destr_pr torw in
276+
let mp = EcEnv.Fun.prF_memenv EcFol.mhr pr.pr_fun env in
277+
let hyps = LDecl.push_active mp hyps in
278+
EcProofTyping.process_form hyps f ty
279+
in
280+
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)