Commit d7487085 by charguer

### array_tuto

parent feb353fb
 ... ... @@ -131,7 +131,7 @@ let demo_array () = t.(1) <- false; t let example_array () = let exercise_array () = let t = Array.make 3 true in t.(2) <- false; t.(1) <- t.(2); ... ...
 Set Implicit Arguments. Require Import CFLib Pervasives_ml Pervasives_proof Tuto_ml. Require Import CFLib Pervasives_ml Pervasives_proof Array_proof Tuto_ml. Require Import LibListZ. Ltac auto_tilde ::= try solve [ intuition eauto with maths ]. (* Hint Resolve length_nonneg : maths. Hint Extern 1 (index ?M _) => subst M : maths. Hint Resolve index_update : maths. Hint Resolve index_zmake : maths. Hint Resolve index_bounds_impl : maths. Hint Resolve index_length_unfold int_index_prove : maths. Hint Resolve index_update : maths. (* Hint Resolve length_nonneg : maths. Hint Extern 1 (length (?l[?i:=?v]) = _) => rewrite length_update. Hint Resolve length_make : maths. Hint Extern 1 (length ?M = _) => subst M : maths. ... ... @@ -17,7 +19,6 @@ Hint Constructors Forall. Global Opaque Z.mul. *) (***********************************************************************) (** Mathematical definitions *) ... ... @@ -65,6 +66,49 @@ Hint Rewrite math_plus_one_twice math_minus_same (***********************************************************************) (** Cheat list *) (** Specification syntax: - [app f [x y] PRE H POST (fun (x:T) => H'] Heap syntax - \[] - \[P] - H \* H' - r ~~> v - r ~~> (v+1) - Hexists x, H Coq tactics: - [=> x], [=>> H], [exists v] - [rew_maths] for normalizing math expressions - [rew_list] for normalizing list operations - [autos], [math], [ring], [math_nia] CFML tactics: - [xcf] - [xsimpl], or [xsimpl X1 .. X2] (to instantiate Hexists) - [xpull] - [xret], or [xapps] for substitution/simplification - [xapp], or [xapps] for substitution - [xfor_inv (fun i => H)] - [xwhile_inv_basic (fun b k => [b = isTrue(..)] \* H) (downto n)] - [xif Q] - [xmatch] Shortcut: - [xextracts] like [xextract; intros x; subst x] - [xrets] like [xret; xsimpl] - [xapps] like [xapp; xextracts] - [tactic~] like [tactic; autos] - [exists_all] like [exists __ .. __] *) (***********************************************************************) (** Basic operations *) ... ... @@ -334,426 +378,121 @@ Qed. (***********************************************************************) (** Recursion *) (*---------------------------------------------------------------------*) (*---- let rec facto_rec n = if n <= 1 then 1 else n * facto_rec(n-1) let rec fib_rec n = if n <= 1 then n else fib_rec(n-1) + fib_rec(n-2) (***********************************************************************) (***********************************************************************) (***********************************************************************) (* axiomatization of fib and facto *) (* Definition prime k := k > 1 /\ forall r d, 1 < d < k -> k <> r * d. *) (*--------------------------------------------------------*) (** Mini-manual *) (** Specification syntax: - [App f x; H (fun (x:T) => H'] Heap syntax - \[] - \[P] - H \* H' - r ~~> v - Hexists x, H Tactics: - [intros], [exists v] - [rew_list], [rew_list_mul] for normalizing list operations - [autos], [math], [ring], [math_nia] - [xcf] - [xsimpl], or [xsimpl X1 .. X2] (to instantiate Hexists) - [xextract] or [xextract as E] - [xret], [xapp]. - [xwhile_inv (fun b m => H \* [b = isTrue(..)] \* \[m = ..]] - [xseq H] - others: [xif], [xmatch] Shortcut: - [xextracts] like [xextract; intros x; subst x] - [xrets] like [xret; xsimpl] - [xapps] like [xapp; xextracts] - [tactic~] like [tactic; autos] - [exists_all] like [exists __ .. __] *) (*--------------------------------------------------------*) (** Prime numbers *) Definition prime k := k > 1 /\ forall r d, 1 < d < k -> k <> r * d. (*--------------------------------------------------------*) (*---- let example_loop n = let i = ref 0 in let r = ref 0 in while !i < n do incr i; incr r; done; r ----*) Lemma example_loop_spec : forall (n:int), n >= 0 -> App example_loop n; \[] (fun (r:loc) => (r ~~> n)). Lemma facto_rec_spec : forall n, n >= 1 -> app facto_rec [n] PRE \[] POST (fun (v:int) => \[v = facto n]). Proof using. skip. (* use: [xcf], [xsimpl], [xextract], [xapp], [xapps], [xret] and also: xwhile_inv (fun b m => Hexists .., (.. ~~> ..) \* \[...] \* \[b = isTrue(...)] \* \[m = ...]). *) => n. induction_wf IH: (downto 0) n. => Hn. xcf. xif. { xrets. math_rewrite (n=1). rewrite~ facto_one. } { xapps. math. math. (* could be written [xapps~] *) xrets. rewrite~ (@facto_succ n). } Qed. (*--------------------------------------------------------*) (*---------------------------------------------------------------------*) (*---- let example_array () = let t = Array.make 3 true in t.(2) <- false; t.(1) <- t.(2); t let rec fib_rec n = if n <= 1 then 1 else fib_rec(n-1) + fib_rec(n-2) ----*) Lemma example_array_spec : App example_array tt; \[] (fun (t:loc) => Hexists M, (t ~> Array M) \* \[length M = 3 /\ forall k, 0 <= k < 3 -> M[k] = isTrue(k<1)]). Proof using. skip. (* to reason about arrays, use [rew_array] and [case_if]. *) Lemma fib_rec_spec : forall n, n >= 0 -> app fib_rec [n] PRE \[] POST (fun (v:int) => \[v = fib n]). Proof using. (* *) => n. induction_wf IH: (downto 0) n. => Hn. xcf. xif. { xrets. rewrite~ fib_base. } { xapps~. xapps~. xrets. rewrite~ (@fib_succ n). } (* *) Qed. (***********************************************************************) (** Array *) 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 let demo_array () = let t = Array.make 3 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)]). Lemma demo_array_spec : app demo_array [tt] PRE \[] POST (fun (t:loc) => Hexists M, (t ~> Array M) \* \[forall k, 0 <= k < 3 -> 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. dup 2. { xcf. xapp. math. => M EM. xapp. autos. xapp. autos. xret. xsimpl. =>> Hk. subst M. rew_array; autos. case_ifs. math. math. math. } { xcf. xapp~. => M EM. xapp~. xapp~. xrets. =>> Hk. subst M. rew_array~. case_ifs; 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 let exercise_array () = let t = Array.make 3 true in t.(2) <- false; t.(1) <- t.(2); t ----*) 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. (*--------------------------------------------------------*) Lemma example_let_spec : forall n, App example_let n; \[] (fun (v:int) => \[v = 2*n]). Proof using. intros. xcf. xret. xextract as Ea. xret. xextract as Eb. xret. xsimpl. math. Qed. (*--------------------------------------------------------*) Lemma example_incr_spec : forall r n, App example_incr r; (r ~~> n) (fun (_:unit) => (r ~~> (n+1))). Proof using. intros. xcf. xapp as v. intros Ev. xapp. intros _. xsimpl. math. Qed. (** Same, with more direct tactic calls *) Lemma example_incr_spec_2 : forall r n, App example_incr r; (r ~~> n) (fun (_:unit) => (r ~~> (n+1))). Proof using. xcf. xapps. xapp. xsimpl. Qed. (*--------------------------------------------------------*) Lemma example_incr_2_spec : forall n, App example_incr_2 n; \[] (fun (v:int) => \[v = n+1]). Proof using. xcf. xapp. xapp. xapp. xapp. xapps. xapps. xapp. xapps. xapps. xret. xsimpl. math. Qed. (*--------------------------------------------------------*) Lemma example_loop_spec : forall (n:int), n >= 0 -> App example_loop n; \[] (fun (r:loc) => (r ~~> n)). Proof using. xcf. xapp. xapp. xwhile_inv (fun b m => Hexists iv, (i ~~> iv) \* (r ~~> iv) \* \[iv <= n] \* \[b = isTrue(iv < n)] \* \[m = n - iv]). { exists_all. xsimpl~. } { intros. xextract as iv Hi Eb Em. xapps. xret. xsimpl~. } { intros. xextract as iv Hi Eb Em. xapps. xapps. xsimpl~. } xextract as m iv Hi Eb Em. xrets~. Qed. (* alternative, specifying the end of the loop *) Lemma example_loop_spec_2 : forall (n:int), n >= 0 -> App example_loop n; \[] (fun (r:loc) => (r ~~> n)). Proof using. xcf. xapp. xapp. xseq (i ~~> n \* r ~~> n). (* new: specify the end of the loop *) xwhile_inv (fun b m => Hexists iv, (i ~~> iv) \* (r ~~> iv) \* \[iv <= n] \* \[b = isTrue(iv < n)] \* \[m = n - iv]). { exists __ __. xsimpl~. } { intros. xextract as iv Hi Eb Em. xapps. xret. xsimpl~. } { intros. xextract as iv Hi Eb Em. xapps. xapps. xsimpl~. } { xsimpl~. } xrets~. Qed. (* LATER Lemma example_array_spec : App example_array tt; \[] (fun (t:loc) => Hexists M, (t ~> Array M) \* \[length M = 3 /\ forall k, 0 <= k < 3 -> M[k] = isTrue(k<1)]). Proof using. xcf. xapp. autos. intros M EM. subst M. xapp. autos. xapp~ as v. intros Ev. xapp~. xret. xsimpl. split. rew_array~. introv Hk. rew_array~. case_ifs. subst v. rew_array~. case_if~. math. math. math. (* Optional forward reasoning after [intros Ev]: asserts Ev': (v = false). subst. rew_array~. case_if~. clear Ev. subst v. *) Qed. *) (*--------------------------------------------------------*) Lemma example_array_spec : App example_array tt; \[] (fun (t:loc) => Hexists M, (t ~> Array M) \* \[length M = 3 /\ forall k, 0 <= k < 3 -> M[k] = isTrue(k<1)]). Proof using. xcf. xapp. autos. intros M EM. subst M. xapp. autos. xapp~ as v. intros Ev. xapp~. xret. xsimpl. split. rew_array~. introv Hk. rew_array~. case_ifs. subst v. rew_array~. case_if~. math. math. math. (* Optional forward reasoning after [intros Ev]: asserts Ev': (v = false). subst. rew_array~. case_if~. clear Ev. subst v. *) Qed. (***********************************************************************) (***********************************************************************) (***********************************************************************)
 ... ... @@ -2924,7 +2924,7 @@ Ltac xspec_in_hyps_core f := Ltac xspec_app_in_hyps f := match goal with | H: context [ app f _ _ _ ] |- _ => generalize H | H: context [ app f _ ] |- _ => generalize H end.