Commit 56017d01 by charguer

democode

parent 4bd8252e
 -- 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' ... ...
 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 *) { intros E. applys E2 d'; math_nia. } { applys~ E1. } } { split. { unfolds~ no_factor. } { introv Hd E. applys (proj2 E1) iv d; math_nia. } } } } { xrets~. introv Hk. rewrite~ HM. logics. iff (L&G). { split~. intros r' d' R1 R2. tests: (r' = iv). (* for SMT extraction Ltac generalize_all tt := repeat match goal with H: _ |- _ => gen H end. generalize_all tt. autorewrite with rew_maths rew_int_comp rew_nat_comp. *) (* subgoals provable by SMT *) { intros E. rewrite~ HM in C. logics. unfold no_factor in C. rew_logic in C. destruct C as [|(a&C)]. math. rew_logic in C. destruct C as (b&C). rew_logic in C. destruct C as (C1&C2&C3). applys G a (b*d'); math_nia. } { applys~ G. } } { split. math. intros r' d' R1 R2 E. applys~ G r' d'. } } } { clears M. intros M LM HM. xapps~. xsimpl~. } } { xextract as m iv M Hi LM HM N Em. xrets. (* subgoals provable by SMT *) introv Hk. rewrite~ HM. logics. unfold prime. iff (L&G). { split. autos. introv Hd E. applys G r d; math_nia. } { split. autos. intros r d Hr1 Hr2 E. applys G r d; math_nia. } } Qed.
 include ../Makefile.example common: .coqide cf Buffer.vio exo: common Exo_ml.vio Exo_proof.vio # common: .coqide cf Buffer.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
 (* axiomatization of fib and facto *) (* Definition prime k := k > 1 /\ forall r d, 1 < d < k -> k <> r * d. *) (***********************************************************************) (* Basic operations *) let example_let n = let a = n+1 in let b = n-1 in a + b let example_incr r = let x = !r in let i = ref x in incr i; r := !r + 1 let example_two_ref n = let i = ref 0 in let r = ref n in decr r; let y = !i in y incr i; r := !i + !r; !i + !r let example_array n = let t = Array.make n true in t.(0) <- false; t.(1) <- false; t let example_loop n = (***********************************************************************) (* For loops *) let facto_for n = let r = ref 0 in for i = 0 to pred n do r := !r * i; done; !r let fib_for n = let a = ref 0 in let b = ref 1 in for i = 1 to n do let c = !a + !b in a := !b; b := c; done; !a (***********************************************************************) (* While loops *) let example_while n = let i = ref 0 in let r = ref 0 in while !i < n do incr i; incr r; done; r let facto_while n = let r = ref 0 in let i = ref 0 in while !i < n do incr i; r := !i * !r; incr i; done; !r let is_prime n = let d = ref 2 in let p = ref true in while !p && (!d * !d <= n) do if (n mod !d) = 0 then p := false; incr d; done; i !p (***********************************************************************) (* Stack *) module StackList = struct let example_cross_even n t = let r = ref 0 in while 2 * !r < n do t.(2 * !r) <- false; incr r; done type 'a t = { mutable items : 'a list; mutable size : int } let sieve n = let create () = { items = []; size = 0 } let length s = s.size let is_empty s = s.size = 0 let push x s = s.items <- x :: s.items; s.size <- s.size + 1 let pop s = match s.items with | hd::tl -> s.items <- tl; s.size <- s.size - 1; hd | [] -> assert false end (***********************************************************************) (* Array *) (* let example_array 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 *) let example_array () = let t = Array.make 3 true in t.(2) <- false; t.(1) <- t.(2); t (***********************************************************************) (* Vector *) module Vector = struct type 'a t = { mutable data : 'a array; mutable size : int; default: 'a; } let create size def = { data = Array.make size def; size = size; default = def; } let length t =