Commit 0429b12c authored by POTTIER Francois's avatar POTTIER Francois
Browse files
parents 701baac2 bf06a855
-- 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'
-- xapp on a leaf does not do xpull
- xfor_inv tag goal
-- case_if checking single goal
-- xmatch_no_intros should do the inversion.
-- improve xauto spec
-- xcf_show without argument should put at head of goal
-- xunfold at fait pas le unfold
-- Ouvrir liblistZ à la fin de cflib
-- Demo de la notation pour les records
-- Array : compléter.
-- LibListZ.sub
-- Array.iter forall l, Array xs \c I l
-- renommer Array.of_list
-- utiliser "of_list []" à la place de make_empty
-- régler le "==>"
-- avoir un flag pour _output
-- external sur une constante, passe pas le typeur
-- ajouter
- documenter la faiblesse de Array.make
- remettre les vrais noms des external
- xclose with args for the change.
......
(*************************************************************)
(* 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 *)
| Ebool of bool
(* b *)
| Eint of int
(* n *)
| Econstr of cstr * etrms
(* C(e1, ..., en) *)
| Eapp of etrm * etrms
(* (e0 e1 .. en) *)
| 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 *)
| Elazyand of etrm * etrm
(* e1 && e2 *)
| Elazyor of etrm * etrm
(* e1 || e2 *)
and etrms = etrm list
and ebranch = pat * etrm
(* pi -> ei *)
and ebranches = ebranch list
(* p1 -> e1 | .. | pn -> en *)
(*************************************************************)
(* Target language *)
type logic_fct =
| Logic_add (* + *)
| Logic_and (* && *)
| Logic_or (* || *)
type aval =
| Avar of var
(* x *)
| Abool of bool
(* b *)
| Aint of int
(* n *)
| Aconstr of cstr * avals
(* C(v1, ..., vn) *)
| Alogic of logic_fct * avals
(* 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 * avals
(* (v0 v1 .. vn) *)
| 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
(** [apply_bindings_to_res (r,bs)] is like the above,
except that it converts the result [r] into a term [t0],
using [atrm_of_res]. *)
let apply_bindings_to_res (r,bs) =
let t0 = atrm_of_res r in
apply_bindings bs t0
(** [val_bindings_of_res_bindings (r,bs)] produces
a pair [(v,bs')]. When the result [r] is a term [t]
and not a value, it is replaced with a variable[x],
and [x] is bound to [t] is [bs']. *)
let val_bindings_of_res_bindings (r,bs) =
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)
(*************************************************************)
(* 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 =
val_bindings_of_res_bindings (tr_any e)
and tr_trm e =
apply_bindings_to_res (tr_any e)
and tr_any e =
match e with
| Evar x ->
(ResVal(Avar x), [])
| Ebool b ->
(ResVal(Abool b), [])
| Eint n ->
(ResVal(Aint n), [])
| Econstr (c,es) ->
let (vs,bs) = tr_vals es in
(ResVal(Aconstr(c, vs)), bs)
| Eapp (e0,es) ->
let (vs,bs) = tr_vals es in
begin match e0 with
| Evar "+" -> (* total function directly reflected in the logic *)
(ResVal(Alogic(Logic_add, vs)), bs)
| _ ->
let (v0,b0) = tr_val e0 in
(ResTrm(Aapp(v0, vs)), bs @ b0)
(* assuming right-to-left evaluation, else use [b0 @ bs] *)
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)
| Elazyand (e1,e2) ->
let (r1,bs1) = tr_any e1 in
let (r2,bs2) = tr_any e2 in
begin match r1, bs2, r2 with
| ResVal v1, [], ResVal v2 ->
(ResVal (Alogic (Logic_and, [v1;v2])), bs1)
(* let bs1 in Val(v1 && v2) *)
| _ ->
let (v1,bs1') = val_bindings_of_res_bindings (r1,bs1) in
let t2 = apply_bindings_to_res (r2,bs2) in
(ResTrm(Aif(v1,t2,Aval(Abool false))), bs1')
(* let bs1 in if v1 then t2 else false *)
end
| Elazyor (e1,e2) -> (* in practice, factorized with previous case *)
let (r1,bs1) = tr_any e1 in
let (r2,bs2) = tr_any e2 in
begin match r1, bs2, r2 with
| ResVal v1, [], ResVal v2 ->
(ResVal (Alogic (Logic_or, [v1;v2])), bs1)
(* let bs1 in Val(v1 || v2) *)
| _ ->
let (v1,bs1') = val_bindings_of_res_bindings (r1,bs1) in
let t2 = apply_bindings_to_res (r2,bs2) in
(ResTrm(Aif(v1,Aval(Abool true),t2)), bs1')
(* let bs1 in if v1 then true else t2 *)
end
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 ([],[])
......@@ -4,6 +4,19 @@ Require Import Demo_ml.
Require Import Stdlib.
Open Scope tag_scope.
(*
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 55,
format "'[' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation "Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
*)
(********************************************************************)
......
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).