Commit 2e477059 by charguer

### tuto

parent 66aab3ab
 ... ... @@ -2,7 +2,7 @@ (***********************************************************************) (* Basic operations *) (** Basic operations *) let example_let n = let a = n+1 in ... ... @@ -22,11 +22,11 @@ let example_two_ref n = (***********************************************************************) (* For loops *) (** For loops *) let facto_for n = let r = ref 0 in for i = 0 to pred n do let r = ref 1 in for i = 1 to n do r := !r * i; done; !r ... ... @@ -43,7 +43,7 @@ let fib_for n = (***********************************************************************) (* While loops *) (** While loops *) let example_while n = let i = ref 0 in ... ... @@ -52,7 +52,7 @@ let example_while n = incr i; incr r; done; r !r let facto_while n = let r = ref 0 in ... ... @@ -64,19 +64,32 @@ let facto_while n = !r let is_prime n = let d = ref 2 in let x = ref 2 in let p = ref true in while !p && (!d * !d <= n) do if (n mod !d) = 0 while !p && (!x * !x <= n) do if (n mod !x) = 0 then p := false; incr d; incr x; done; !p (***********************************************************************) (** 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) (***********************************************************************) (* Stack *) (** Stack *) module StackList = struct ... ... @@ -110,15 +123,13 @@ end (***********************************************************************) (* Array *) (** Array *) (* 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 *) let example_array () = let t = Array.make 3 true in ... ... @@ -128,7 +139,7 @@ let example_array () = (***********************************************************************) (* Vector *) (** Vector *) module Vector = struct ... ... @@ -176,15 +187,3 @@ end *) (***********************************************************************) (* 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)
 Set Implicit Arguments. Require Import CFLib Exo_ml. Require Import LibListZ Buffer. Require Import CFLib Pervasives_ml Pervasives_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. ... ... @@ -14,10 +13,238 @@ Hint Resolve index_length_unfold int_index_prove : maths. Hint Extern 1 (length (?l[?i:=?v]) = _) => rewrite length_update. Hint Resolve length_make : maths. Hint Extern 1 (length ?M = _) => subst M : maths. Hint Constructors Forall. Global Opaque Z.mul. *) (***********************************************************************) (** Mathematical definitions *) (** Factorial *) Parameter facto : int -> int. Parameter facto_zero : facto 0 = 1. Parameter facto_one : facto 1 = 1. Parameter facto_succ : forall n, n >= 1 -> facto n = n * facto(n-1). (** Fibonnaci *) Parameter fib : int -> int. Parameter fib_base : forall n, n <= 1 -> fib n = n. Parameter fib_succ : forall n, n > 1 -> fib n = fib(n-1) + fib(n-2). (** Primes *) Parameter prime : int -> Prop. Parameter divide_not_prime : forall n d, 1 < d < n -> Z.rem n d = 0 -> ~ (prime n). Parameter not_divide_prime : forall n, (forall d, 1 < d < n -> Z.rem n d <> 0) -> (prime n). Parameter not_divide_prime_sqrt : forall n r, (forall d, 1 < d <= r -> Z.rem n d <> 0) -> (r * r >= n) -> (prime n). (***********************************************************************) (** Basic operations *) (*---------------------------------------------------------------------*) (*---- let example_let n = let a = n+1 in let b = n-1 in a + b ----*) Lemma example_let_spec : forall n, app example_let [n] PRE \[] POST (fun (v:int) => \[v = 2*n]). Proof using. dup 2. { xcf. xlet. xret. xpull. intros. xlet. xret. xpull. intros. xret. xsimpl. math. } { xcf. xret. intros. xret. intros. xret. xsimpl. math. } (* use: [xcf], [xret], [xsimpl], [math]; [xlet] is optional; if used then [xpull] is also needed. *) Qed. (*---------------------------------------------------------------------*) (*---- let example_incr r = r := !r + 1 ----*) Lemma example_incr_spec : forall r n, app example_incr [r] PRE (r ~~> n) POST (fun (_:unit) => (r ~~> (n+1))). Proof using. dup 2. { xcf. xapp. intros. subst. xapp. } { xcf. xapps. xapp. } (* use: [xcf], [xapp]; [xapps] is a shortand for [xapp] followed with [subst] *) Qed. (*---------------------------------------------------------------------*) (*---- let example_two_ref n = let i = ref 0 in let r = ref n in decr r; incr i; r := !i + !r; !i + !r ----*) Lemma example_two_ref_spec : forall n, app example_two_ref [n] PRE \[] POST (fun (v:int) => \[v = n+1]). Proof using. dup. { xcf. xapps. xapps. xapps. xapps. xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math. } { xcf. xgo~. } Qed. (***********************************************************************) (** For loops *) (*---------------------------------------------------------------------*) (*---- let facto_for n = let r = ref 1 in for i = 0 to pred n do r := !r * i; done; !r ----*) Lemma facto_for_spec : forall n, n >= 1 -> app facto_for [n] PRE \[] POST (fun (v:int) => \[v = facto n]). Proof using. xcf. xapps. xfor_inv (fun i => r ~~> (facto (i-1))). { math. } { xsimpl. forwards~: facto_zero. } { introv Hi. xapps. xapps. xsimpl. math_rewrite ((i+1)-1=i). rewrite~ (@facto_succ i). ring. } xapps. xsimpl. math_rewrite ((n+1)-1 = n) in *. auto. Qed. (*---------------------------------------------------------------------*) (*---- let fib_for n = let a = ref 0 in let b = ref 1 in for i = 0 to n-1 do let c = !a + !b in a := !b; b := c; done; !a ----*) Lemma fib_for_spec : forall n, n >= 1 -> app fib_for [n] PRE \[] POST (fun (v:int) => \[v = fib n]). Proof using. xcf. xapps. xapps. xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1))). { math. } { xsimpl. { forwards~: fib_base. math. } { forwards~: fib_base. math. } } { introv Hi. xapps. xapps. xret. intros. xapps. xapps. xapps. xsimpl. rewrite fib_succ. math_rewrite ((i+1)+1-1 = i+1). math_rewrite ((i+1)+1-2=i). math. math. } xapps. xsimpl. auto. Qed. (***********************************************************************) (** 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 r := !i * !r; incr i; done; !r let is_prime n = let x = ref 2 in let p = ref true in while !p && (!x * !x <= n) do if (n mod !x) = 0 then p := false; incr x; done; !p (***********************************************************************) (** 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) (***********************************************************************) (***********************************************************************) (***********************************************************************) ... ... @@ -69,59 +296,7 @@ Shortcut: Definition prime k := k > 1 /\ forall r d, 1 < d < k -> k <> r * d. (*--------------------------------------------------------*) (*---- let example_let n = let a = n+1 in let b = n-1 in a + b ----*) Lemma example_let_spec : forall n, App example_let n; \[] (fun (v:int) => \[v = 2*n]). Proof using. skip. (* use: [math], [xextract], [xsimpl], [xcf], [xret] *) Qed. (*--------------------------------------------------------*) (*---- let example_incr r = r := !r + 1 ----*) Lemma example_incr_spec : forall r n, App example_incr r; (r ~~> n) (fun (_:unit) => (r ~~> (n+1))). Proof using. skip. (* use also: [xapp] or [xapp as x] or [xapps] (try them all) *) Qed. (*--------------------------------------------------------*) (*---- let example_incr_2 n = let i = ref 0 in let r = ref n in decr r; incr i; r := !i + !r; !i + !r ----*) Lemma example_incr_2_spec : forall n, App example_incr_2 n; \[] (fun (v:int) => \[v = n+1]). Proof using. skip. Qed. (*--------------------------------------------------------*) ... ...
 ... ... @@ -317,7 +317,7 @@ Qed. (** Union *) Lemma state_union_idempotent : idempotent2 state_union. Lemma ostate_union_idempotent : idempotent2 state_union. Proof using. intros [f F]. apply~ state_eq. simpl. intros x. unfold pfun_union. cases~ (f x). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!