Commit 9aa3600c authored by POTTIER Francois's avatar POTTIER Francois
Browse files
parents 7232de3d 56017d01
-- while loop invariant : when b is false, should not prove decrease
Lemma xwhile_inv_basic_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists b X0, I b X0) \* \GC) ->
(forall b X, F1 (I b X) (fun b' => I b' X)) ->
(forall X, F2 (I true X) (# Hexists b X', \[b -> R X' X] \* I b X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I false X).
-- xfor_inv prefers to use b-1 as upper bound if possible
-- xapp as b'
......
(*************************************************************)
(* Common constructs *)
type var = string
and vars = var list
type cstr = string
type pat =
| Pvar of var
(* x *)
| Pcst of int
(* n *)
| Pconstr of cstr * pat
(* C(p1, .., pN) *)
let fresh_var =
let r = ref 0 in
(fun () -> incr r; string_of_int !r)
(*************************************************************)
(* Source language *)
type etrm =
| Evar of var
(* x *)
| Ecst of int
(* n *)
| Econstr of cstr * etrms
(* C(e1, ..., en) *)
| Eapp of etrm * etrm
(* (e1 e2) *)
| Elet of var * etrm * etrm
(* let(rec) x = e1 in e2 *)
| Eif of etrm * etrm * etrm
(* if e1 then e2 else e3 *)
| Ematch of etrm * ebranches
(* match e1 with bes *)
| Efun of var * etrm
(* fun x -> e1 *)
and etrms = etrm list
and ebranch = pat * etrm
(* pi -> ei *)
and ebranches = ebranch list
(* p1 -> e1 | .. | pn -> en *)
(*************************************************************)
(* Target language *)
type aval =
| Avar of var
(* x *)
| Acst of int
(* n *)
| Aconstr of cstr * avals
(* C(v1, ..., vn) *)
(* Note: at runtime, type aval also includes closures,
but there are no closures in the source code.
Same applies for program locations. *)
and avals = aval list
type atrm =
| Aval of aval
(* v *)
| Aapp of aval * aval
(* (v1 v2) *)
| Alet of var * atrm * atrm
(* let x = t1 in t2 *)
| Aletfun of var * var * atrm * atrm
(* let rec f x = t1 in t2 *)
| Aif of aval * atrm * atrm
(* if v1 then t2 else t3 *)
| Amatch of aval * abranches
(* match v with bas *)
and atrms = atrm list
and abranch = pat * atrm
(* pi -> ti *)
and abranches = abranch list
(* p1 -> t1 | .. | pn -> tn *)
(*************************************************************)
(* Translation auxiliary definitions *)
(* Internally, the translation of a term of type [etrm]
produces a [res], which is either a value or a term. *)
type res =
| ResVal of aval
| ResTrm of atrm
(* A [res] can always be viewed as a term. *)
let atrm_of_res r =
match r with
| ResVal v -> Aval v
| ResTrm t -> t
(* Bindings, used internally by the translation. *)
type binding =
| BindingTrm of var * atrm
(* let x = t *)
| BindingFun of var * var * atrm
(* let rec f x = t *)
and bindings = binding list
(** [apply_binding b t0] computes, e.g.,
[let x = t t0]. *)
let apply_binding b t0 =
match b with
| BindingTrm (x, t) -> Alet (x, t, t0)
| BindingFun (f, x, t) -> Aletfun (f, x, t, t0)
(** [apply_bindings bs t0] computes, e.g.,
[let x1 = t1 in .. let xn = tn in t0],
where [bs = (x1,t1)::...::(xn,tn)]. *)
let apply_bindings bs t0 =
List.fold_right apply_binding bs t0
(*************************************************************)
(* Translation *)
(* There are five mutually recursive functions
- [tr_any e] produces a pair (r, bs), made
of a result of type [res] (a value or a term),
and a list of bindings.
- [tr_val e] produces a pair (v, bs), made of a
value of type [aval] and a list of bindings.
- [tr_trm e] produces a term t of type [atrm]
- [tr_anys es] produces a (rs, bs) made of a list of
results of type [res], and a list of bindings.
- [tr_vals es] produces a (vs, bs) made of a list of
results of type [aval], and a list of bindings.
*)
let rec tr_val e =
let (r,bs) = tr_any e in
match r with
| ResVal v -> (v, bs)
| ResTrm t ->
let x = fresh_var() in
let v = Avar x in
let bs2 = bs @ [BindingTrm (x,t)] in
(v, bs2)
and tr_trm e =
let (r,bs) = tr_any e in
let t0 = atrm_of_res r in
apply_bindings bs t0
and tr_any e =
match e with
| Evar x ->
(ResVal(Avar x), [])
| Ecst n ->
(ResVal(Acst n), [])
| Econstr (c,es) ->
let (vs,bs) = tr_vals es in
(ResVal(Aconstr(c, vs)), bs)
| Eapp (e1,e2) ->
let (vs,bs) = tr_vals [e1;e2] in
begin match vs with
| [v1;v2] -> (ResTrm(Aapp(v1, v2)), bs)
| _ -> assert false
end
| Elet (f,Efun(x,e1),e2) ->
let t1 = tr_trm e1 in
let t2 = tr_trm e2 in
(ResTrm(Aletfun(f, x, t1, t2)), [])
| Efun (x,e1) ->
(* only for anonymous functions *)
let f = fresh_var() in
let t1 = tr_trm e1 in
(ResVal(Avar f), [BindingFun(f, x, t1)])
| Elet (x,e1,e2) ->
let (r1,bs1) = tr_any e1 in
let t1 = atrm_of_res r1 in
let t2 = tr_trm e2 in
(ResTrm(Alet(x, t1, t2)), bs1)
| Eif (e1,e2,e3) ->
let (v1,bs1) = tr_val e1 in
let t2 = tr_trm e2 in
let t3 = tr_trm e3 in
(ResTrm(Aif(v1,t2,t3)), bs1)
| Ematch (e1,bes) ->
let (v1,bs1) = tr_val e1 in
let bas = List.map (fun (p,e) -> (p, tr_trm e)) bes in
(ResTrm(Amatch(v1,bas)), bs1)
and tr_anys es =
(* assume here right-to-left evaluation order, as in OCaml;
otherwise, replace [bs @ bs2] with [bs2 @ bs]. *)
List.fold_right (fun e (rs,bs) ->
let (r,bs2) = tr_any e in
(r::rs, bs @ bs2)
) es ([],[])
and tr_vals es =
(* idem. *)
List.fold_right (fun e (vs,bs) ->
let (v,bs2) = tr_val e in
(v::vs, bs @ bs2)
) es ([],[])
include ../Makefile.example
common: .coqide cf Buffer.vio
exo: common Exo_ml.vio Exo_proof.vio
tuto: common Tuto_ml.vio Tuto_proof.vio
perso: common Perso_ml.vio Perso_proof.vio
all: exo tuto test Exo_proof.vq Tuto_proof.vq Test_proof.vq
full: all Tuto_extra.vq Exo_extra.vq
let example_incr r =
let x = !r in
let i = ref x in
incr i;
decr r;
let y = !i in
y
let example_array n =
let t = Array.make n true in
t.(0) <- false;
t.(1) <- false;
t
let example_loop n =
let i = ref 0 in
while !i < n do
incr i;
done;
i
let example_cross_even n t =
let r = ref 0 in
while 2 * !r < n do
t.(2 * !r) <- false;
incr r;
done
let sieve n =
let t = Array.make n true in
t.(0) <- false;
t.(1) <- false;
let i = ref 2 in
while !i < n do
if t.(!i) then begin
let r = ref !i in
while !r * !i < n do
t.(!r * !i) <- false;
incr r;
done;
end;
incr i;
done;
t
Set Implicit Arguments.
Require Import CFLib Tuto_ml.
Require Import LibListZ Buffer.
Ltac auto_tilde ::= try solve [ intuition eauto with maths ].
(*--------------------------------------------------------*)
(*----
let example_incr r =
let x = !r in
let i = ref x in
incr i;
decr r;
let y = !i in
y
----*)
Lemma example_cf_show : True.
Proof using. pose example_incr_cf. auto. Qed.
Lemma example_incr_spec : forall r n,
(App example_incr r;)
(r ~~> n)
(fun (v:int) => \[v = n+1] \* (r ~~> (n-1))).
Proof using.
intros.
xcf.
xapp. intros Ex.
xapp.
xapp.
xapp.
xapp. intros Ey.
xret.
xsimpl. math.
Qed.
(*--------------------------------------------------------*)
(*----
let example_array n =
let t = Array.make n true in
t.(0) <- false;
t.(1) <- false;
t
----*)
Lemma example_array_spec : forall n,
n >= 2 ->
App example_array n;
\[]
(fun (t:loc) => Hexists M, (t ~> Array M)
\* \[forall k, 0 <= k < n -> M[k] = isTrue(k > 1)]).
Proof using.
introv Hn. xcf.
xapp. autos. intros M EM.
xapp. autos.
xapp. autos.
xret. xsimpl. introv Hk. subst M. rew_array; autos.
case_ifs. math. math. math.
Qed.
(* same, in shorter *)
Lemma example_array_spec' : forall n,
n >= 2 ->
App example_array n;
\[]
(fun (t:loc) => Hexists M, (t ~> Array M)
\* \[forall k, 0 <= k < n -> M[k] = isTrue(k > 1)]).
Proof using.
introv Hn. xcf. xapp~. intros M EM. xapp~. xapp~. xrets.
introv Hk. subst M. rew_array~. case_ifs; math.
Qed.
(*--------------------------------------------------------*)
(*----
let example_loop n =
let i = ref 0 in
while !i < n do
incr i;
done;
i
----*)
Lemma example_loop_spec : forall n,
n >= 0 ->
App example_loop n;
\[]
(fun (i:loc) => Hexists v, \[v >= n] \* (i ~~> v)).
Proof using.
introv Hn. xcf. xapp.
xwhile_inv (fun b m =>
Hexists iv, (i ~~> iv) \* \[iv <= n] \*
\[b = isTrue(iv < n)] \* \[m = n - iv]).
{ (* loop invariant initialization *)
exists_all. xsimpl. autos. autos. autos. }
{ (* loop conditional *)
intros. xextract as iv Hi Eb Em.
xapps.
xret.
xsimpl. autos. autos. autos. }
{ (* loop body *)
intros. xextract as iv Hi Eb Em.
xapps.
xsimpl. autos. autos. autos. autos. }
xextract as m iv Ei Ei' Em. xret. xsimpl. autos.
Qed.
(** Same, with more automation *)
Lemma example_loop_spec_2 : forall n,
n >= 0 ->
App example_loop n;
\[]
(fun (i:loc) => Hexists v, \[v >= n] \* (i ~~> v)).
Proof using.
introv Hn. xcf. xapp.
xwhile_inv (fun b m =>
Hexists iv, (i ~~> iv) \* \[iv <= n] \*
\[b = isTrue(iv < n)] \* \[m = n - iv]).
{ exists_all. xsimpl~. }
{ intros. xextract as iv Hi Eb Em. xapps. xrets~. }
{ intros. xextract as iv Hi Eb Em. xapps. xsimpl~. }
xextract as m iv Ei Ei' Em. xrets~.
Qed.
(** Same, giving the intermediate state. *)
Lemma example_loop_spec_3 : forall n,
n >= 0 ->
App example_loop n;
\[]
(fun (i:loc) => Hexists v, \[v >= n] \* (i ~~> v)).
Proof using.
introv Hn. xcf. xapp.
xseq (i ~~> n). (* give the intermediate state *)
xwhile_inv (fun b m =>
Hexists iv, (i ~~> iv) \* \[iv <= n] \*
\[b = isTrue(iv < n)] \* \[m = n - iv]).
{ exists_all. xsimpl~. }
{ intros. xextract as iv Hi Eb Em. xapps. xrets~. }
{ intros. xextract as iv Hi Eb Em. xapps. xsimpl~. }
{ xsimpl~. }
xrets~.
Qed.
(*--------------------------------------------------------*)
(*----
let example_cross_even n t =
let r = ref 0 in
while 2 * !r < n do
t.(2 * !r) <- false;
incr r;
done
----*)
Definition odd k :=
exists r, k = 2*r+1.
Lemma odd_or_ge_next : forall rv k,
k <> rv*2 ->
(odd k \/ k >= rv*2)
<-> (odd k \/ k >= (rv + 1)*2).
Proof using.
introv N. iff [E1|E2]; autos.
{ tests_nosubst E: (k = 2*rv+1).
{ left. exists rv. math. }
{ right. math. } }
Qed.
Lemma example_cross_even_spec : forall n t M,
length M = n ->
(forall k, 0 <= k < n -> M[k] = true) ->
App example_cross_even n t;
(t ~> Array M)
(fun (_:unit) => Hexists M', t ~> Array M'
\* \[forall k, 0 <= k < n -> M'[k] = isTrue(odd k)]).
Proof using.
intros n t M0 LM0 HM0. xcf. xapp.
xwhile_inv (fun b m =>
Hexists rv M, (r ~~> rv) \* (t ~> Array M) \*
\[rv >= 0] \* \[length M = n] \*
\[forall k, 0 <= k < n ->
M[k] = isTrue(odd k \/ k >= rv*2) ] \*
\[b = isTrue(rv*2 < n)] \* \[m = n - rv]);
try clear M0 LM0 HM0.
{ exists_all. xsimpl~.
introv Hk. rewrite~ HM0. logics. right. math. }
{ intros. xextract as rv M Hr LM HM Eb Em.
xapps. xret. xsimpl~. }
{ intros. xextract as rv M Hr LM HM Eb Em.
xapps. xapps~. xapps. xsimpl~.
introv Hk. rew_array~. case_if.
{ unfold odd. rew_logic. math. }
{ rewrite~ HM. logics. applys~ odd_or_ge_next. } }
xextract as m rv M Hr LM HM Eb Em. xsimpl~.
introv Hk. rewrite~ HM. logics. iff [E1|E2] E1; autos~. math.
Qed.
(*--------------------------------------------------------*)
(*----
let sieve n =
let t = Array.make n true in
t.(0) <- false;
t.(1) <- false;
let i = ref 2 in
while !i < n do
if t.(!i) then begin
let r = ref !i in
while !r * !i < n do
t.(!r * !i) <- false;
incr r;
done;
end;
incr i;
done;
t
----*)
Definition prime k :=
k > 1 /\ forall r d, 1 < d < k -> k <> r * d.
Definition no_factor i n k :=
k > 1 /\ (forall r d, 1 < r < i -> 1 < d < n -> k <> r*d).
Lemma sieve_spec : forall n,
n >= 2 ->
App sieve n; \[]
(fun (t:loc) => Hexists M', t ~> Array M' \*
\[forall k, 0 <= k < n -> M'[k] = isTrue (prime k)]).
Proof using.
introv Hn. xcf.
xapp~. intros M0 HM0. xapp~. xapp~.
xapp~. xwhile_inv (fun b m =>
Hexists iv M, (i ~~> iv) \* (t ~> Array M) \*
\[1 < iv <= n] \* \[length M = n] \*
\[forall k, 0 <= k < n -> M[k] = isTrue(no_factor iv n k) ] \*
\[b = isTrue(iv < n)] \* \[m = n - iv]); try clear M0 HM0.
{ exists_all. xsimpl~. introv Hk. subst M0. rew_array~.
unfold no_factor. case_ifs; rew_logic~. }
{ intros. xextract as iv M Hi LM HM Eb Em. xapps. xrets~. }
{ intros. xextract as iv M Hi LM HM Eb Em. xapps. xapps~.
xseq (Hexists M', (i ~~> iv) \* (t ~> Array M') \* \[length M' = n] \*
\[forall k, 0 <= k < n -> M'[k] = isTrue(no_factor (iv+1) n k)]).
{ xif.
{ xapps. xapps.
xwhile_inv (fun b m =>
Hexists rv M', (i ~~> iv) \* (r ~~> rv) \* (t ~> Array M') \*
\[1 < rv <= n] \* \[length M' = n] \*
\[forall k, 0 <= k < n ->
M'[k] = isTrue(no_factor iv n k /\
(forall d, 1 < d < rv -> k <> d*iv)) ] \*
\[b = isTrue(rv*iv < n)] \* \[m = n + iv - rv*iv]).
{ exists_all. xsimpl~. introv Hk. rewrite~ HM.
logics. iff (L&G) (G1&G2); unfolds~ no_factor. }
{ clears M. intros. xextract as rv M Hr LM HM Eb' Em'.
xapps. xapps. xrets~. }
{ clears M. intros. xextract as rv M Hr LM HM Eb' Em'.
xapps. xapps~. asserts: (rv*iv>=0). math_nia. xapps~.
xapps~. xsimpl~.
{ introv Hk. rew_array~. case_if.
{ sets_eq k: (rv * iv). rew_logic.
right. exists rv. rew_logic~. }
{ rewrite~ HM. logics. iff (G1&G2).
{ split. autos~. introv Hd.
unfolds no_factor. tests~: (d = rv). }
{ split. autos~. intros. applys~ G2. } } }
{ math_nia. }
{ math_nia. } }
{ clears M. xextract as m' rv M Hr LM HM Eb' Em'. xsimpl~.
(* not provable by SMT before the case analysis *)
introv Hk. rewrite~ HM. logics. iff ((G&E1)&E2) E1.
{ split. math. intros r' d' H1 H2. tests: (r' = iv).
(* next 5 lines provable by SMT *)