Commit feb353fb authored by charguer's avatar charguer
Browse files

tuto_loops

parent 2e477059
......@@ -55,21 +55,21 @@ let example_while n =
!r
let facto_while n =
let r = ref 0 in
let i = ref 0 in
while !i < n do
let r = ref 1 in
let i = ref 2 in
while !i <= n do
r := !i * !r;
incr i;
done;
!r
let is_prime n =
let x = ref 2 in
let i = ref 2 in
let p = ref true in
while !p && (!x * !x <= n) do
if (n mod !x) = 0
while !p && (!i * !i <= n) do
if (n mod !i) = 0
then p := false;
incr x;
incr i;
done;
!p
......
......@@ -45,11 +45,26 @@ 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) ->
(forall d, 1 < d < r -> Z.rem n d <> 0) ->
(r * r > n) ->
(prime n).
(** [rew_maths] for simplifying math expressions *)
Lemma math_plus_one_twice : forall n, ((n+1)+1) = n+2.
Proof using. math. Qed.
Lemma math_minus_same : forall n, n-n = 0.
Proof using. math. Qed.
Lemma math_two_minus_one : 2-1 = 1.
Proof using. math. Qed.
Lemma math_plus_minus_same : forall n m, (n+m)-m = n.
Proof using. math. Qed.
Hint Rewrite math_plus_one_twice math_minus_same
math_two_minus_one math_plus_minus_same : rew_maths.
(***********************************************************************)
(** Basic operations *)
......@@ -107,10 +122,13 @@ let example_two_ref n =
----*)
Lemma example_two_ref_spec : forall n,
(* <EXO> *)
app example_two_ref [n]
PRE \[]
POST (fun (v:int) => \[v = n+1]).
(* </EXO> *)
Proof using.
(* <EXO> *)
dup.
{ xcf.
xapps.
......@@ -126,6 +144,7 @@ Proof using.
xsimpl.
math. }
{ xcf. xgo~. }
(* </EXO> *)
Qed.
......@@ -148,14 +167,13 @@ Lemma facto_for_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = facto n]).
Proof using.
xcf.
xapps.
=>> Hn. 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.
rew_maths. rewrite~ (@facto_succ i). ring. }
xapps. xsimpl. rew_maths. auto.
Qed.
......@@ -178,16 +196,17 @@ Lemma fib_for_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = fib n]).
Proof using.
xcf. xapps. xapps.
(* <EXO> *)
=>> Hn. 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. }
rewrite fib_succ. rew_maths. math. math. }
xapps. xsimpl. auto.
(* </EXO> *)
Qed.
......@@ -195,6 +214,8 @@ Qed.
(***********************************************************************)
(** While loops *)
(*---------------------------------------------------------------------*)
(*----
let example_while n =
let i = ref 0 in
let r = ref 0 in
......@@ -203,25 +224,111 @@ let example_while n =
incr r;
done;
!r
----*)
Lemma example_while_spec : forall n,
n >= 0 ->
app example_while [n]
PRE \[]
POST (fun (v:int) => \[v = n]).
Proof using.
introv Hn. xcf. xapps. xapps.
xwhile_inv_basic (fun b k => \[b = isTrue (k < n)] \* \[k <= n] \* i ~~> k \* r ~~> k)
(upto n).
{ xsimpl. eauto. eauto. }
{ => b k. xpull. => Hb Hk. xapps. xrets. auto. autos*. } (* short for: xret; xsimpl. *)
{ => k. xpull. => Hb Hk. xapps. xapps. xsimpl.
{ math. }
{ eauto. }
{ hnf. math. } }
=>> Hb Hk. xclean. xapps. xsimpl. subst. math.
Qed.
(*---------------------------------------------------------------------*)
(*----
let facto_while n =
let r = ref 0 in
let i = ref 0 in
while !i < n do
let r = ref 1 in
let i = ref 1 in
while !i <= n do
r := !i * !r;
incr i;
done;
!r
----*)
Lemma facto_while_spec : forall n,
n >= 2 ->
app facto_while [n]
PRE \[]
POST (fun (v:int) => \[v = facto n]).
Proof using.
(* <EXO> *)
introv Hn. xcf. xapps. xapps.
xwhile_inv_basic (fun b k => \[b = isTrue (k <= n)] \* \[2 <= k <= n+1]
\* i ~~> k \* r ~~> (facto (k-1)))
(upto (n+1)).
{ xsimpl. rew_maths. rewrite~ facto_one. math. eauto. }
{ => b k. xpull. => Hb Hk. xapps. xrets. auto. autos*. } (* short for: xret; xsimpl. *)
{ => k. xpull. => Hb Hk. xapps. xapps. xapps. xapps. xsimpl.
{ rew_maths. rewrite (@facto_succ k). ring. math. }
{ math. }
{ eauto. }
{ math. } }
=>> Hb Hk. xclean. xapps. xsimpl. subst. fequal. math.
(* </EXO> *)
Qed.
(*---------------------------------------------------------------------*)
(*----
let is_prime n =
let x = ref 2 in
let i = ref 2 in
let p = ref true in
while !p && (!x * !x <= n) do
if (n mod !x) = 0
while !p && (!i * !i <= n) do
if (n mod !i) = 0
then p := false;
incr x;
incr i;
done;
!p
----*)
Lemma is_prime_spec : forall n,
n >= 2 ->
app is_prime [n]
PRE \[]
POST (fun (b:bool) => \[b = isTrue (prime n)]).
Proof using.
introv Hn. xcf. xapps. xapps.
xwhile_inv_basic (fun b k => Hexists vp,
\[b = isTrue (vp = true /\ k*k <= n)]
\* \[if vp then (forall d, 1 < d < k -> Z.rem n d <> 0) else (~ prime n)]
\* \[2 <= k]
\* i ~~> k
\* p ~~> vp)
(upto n).
{ xsimpl. math. math. eauto. }
{ => b k. xpull ;=> vp Hb Hp Hk. xapps. xand.
{ xapps. xapps. xrets*. }
{ xsimpl*. } }
{ => k. xpull ;=> vp Hb Hp Hk.
(* TODO: xclean. *) xclean. destruct Hb as (Hvp&Hkk).
xapps. xapps. math.
xrets. xseq. xif (# Hexists (vp':bool), i ~~> k \* p ~~> vp' \*
\[if vp' then (forall d, 1 < d < (k+1) -> Z.rem n d <> 0) else (~ prime n)]).
(* TODO: remove xseq *)
{ xapps. xsimpl. applys~ divide_not_prime. math_nia. }
{ xrets. rewrite Hvp in *. =>> Hd. tests: (d = k). auto. applys~ Hp. }
xpull ;=> vp' Hvp'. xapps. xsimpl.
{ math. }
{ auto. }
{ eauto. }
{ math_nia. } }
=> k vp Hb Hvp Hk. xclean. rew_logic in Hb.
xapps. xsimpl. subst. case_if.
{ destruct Hb; tryfalse. applys* not_divide_prime_sqrt. math. }
{ auto. }
Qed.
(***********************************************************************)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment