Tuto_proof.v 18.8 KB
Newer Older
1
Set Implicit Arguments.
2 3 4 5 6
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import Tuto_ml.
Require Import TLC.LibListZ.
charguer's avatar
charguer committed
7

charguer's avatar
charguer committed
8

charguer's avatar
charguer committed
9 10
(***********************************************************************)
(** Cheat list *)
charguer's avatar
charguer committed
11

charguer's avatar
charguer committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
(**
Specification syntax:
   - [app f [x y]
        PRE H
        POST (fun (x:T) => H']

Heap syntax H :  heap -> Prop ::=
   - \[]
   - \[P]
   - H \* H'
   - r ~~> v        r ~> Ref v       Ref v r
   - r ~~> (v+1)
   - Hexists x, H
   - r ~> Stack L       Stack L r

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]
charguer's avatar
charguer committed
37 38
   - [xclean] sometimes needed to do simplifications
   - [xret], or [xrets] for substitution/simplification
charguer's avatar
charguer committed
39 40 41 42 43 44 45 46 47 48 49
   - [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; eauto with maths]
50
*)
charguer's avatar
tuto  
charguer committed
51

charguer's avatar
charguer committed
52

charguer's avatar
tuto  
charguer committed
53 54 55 56 57 58
(***********************************************************************)
(** Mathematical definitions *)

(** Factorial *)

Parameter facto : int -> int.
59
Parameter facto_zero : facto 0 = 1.
charguer's avatar
tuto  
charguer committed
60 61 62 63 64 65 66 67 68 69 70 71
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.
72
Parameter divide_not_prime : forall n d,
charguer's avatar
tuto  
charguer committed
73 74 75
  1 < d < n ->
  Z.rem n d = 0 ->
  ~ (prime n).
76
Parameter not_divide_prime : forall n,
charguer's avatar
tuto  
charguer committed
77 78
  (forall d, 1 < d < n -> Z.rem n d <> 0) ->
  (prime n).
79
Parameter not_divide_prime_sqrt : forall n r,
charguer's avatar
charguer committed
80 81
  (forall d, 1 < d < r -> Z.rem n d <> 0) ->
  (r * r > n) ->
charguer's avatar
tuto  
charguer committed
82 83 84
  (prime n).


charguer's avatar
charguer committed
85 86 87 88 89 90
(***********************************************************************)
(** Automation for mathematical subgoals *)

Ltac auto_tilde ::= try solve [ intuition eauto with maths ].

Hint Extern 1 (index ?M _) => subst M : maths.
charguer's avatar
stable  
charguer committed
91 92 93
Hint Resolve LibListZ.index_make : maths.
Hint Resolve index_of_inbound : maths.
Hint Resolve index_of_index_length int_index_prove : maths.
charguer's avatar
charguer committed
94 95 96
Hint Resolve index_update : maths.

(** Tactic [rew_maths] for simplifying math expressions *)
charguer's avatar
charguer committed
97 98 99 100 101 102 103 104 105

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.
106
Hint Rewrite math_plus_one_twice math_minus_same
charguer's avatar
charguer committed
107 108 109 110
  math_two_minus_one math_plus_minus_same : rew_maths.



charguer's avatar
charguer committed
111 112


charguer's avatar
tuto  
charguer committed
113 114 115 116
(***********************************************************************)
(** Basic operations *)

(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
117 118 119 120 121 122 123 124 125

(**
[[
  let example_let n =
    let a = n+1 in
    let b = n-1 in
    a + b
]]
*)
charguer's avatar
tuto  
charguer committed
126 127 128 129

Lemma example_let_spec : forall n,
  app example_let [n]
    PRE \[]
charguer's avatar
charguer committed
130 131
    POST (fun (v:int) => \[v = 2*n]). 
   (* post-condition also written: POST \[= (2 * n)]  *)
charguer's avatar
tuto  
charguer committed
132
Proof using.
charguer's avatar
charguer committed
133 134 135 136 137
  (* Hint: the proof uses [xcf], [xret], [xsimpl], [math].
     [xlet] is optional; if used then [xpull] is also needed. *)
  dup 3.
  { (* detailed proof *)
    xcf.
138
    xlet. xret. simpl. xpull. intros Ha.
charguer's avatar
charguer committed
139 140
    xlet. xret. simpl. xpull. intros Hb.
    xret. (*hnf.*) xsimpl. math. }
charguer's avatar
charguer committed
141 142 143 144
  { (* shorter proof *)
    xcf. xret ;=> Ha. xret ;=> Hb. xret. xsimpl. math. }
  { (* real proof *)
    xcf. xrets. xrets. xrets. math. }
charguer's avatar
tuto  
charguer committed
145 146
Qed.

charguer's avatar
charguer committed
147

charguer's avatar
tuto  
charguer committed
148
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
149

charguer's avatar
charguer committed
150 151 152 153 154 155 156 157 158 159 160 161 162 163
(**
[[
  let example_incr r =
    r := !r + 1
]]

normalized to:

[[
  let example_incr r =
    let x0__ := get r in
    set r (x0__ + 1)
]]
*)
charguer's avatar
tuto  
charguer committed
164 165 166 167

Lemma example_incr_spec : forall r n,
  app example_incr [r]
    PRE (r ~~> n)
charguer's avatar
charguer committed
168 169
    POST (fun (_:unit) => (r ~~> (n+1))). 
    (* post-condition also written: POST (# r ~~> (n+1)). *)
charguer's avatar
tuto  
charguer committed
170
Proof using.
charguer's avatar
charguer committed
171 172
  (* Hint: the proof uses [xcf], [xapp].
     [xapps] is a shortand for [xapp] followed with [subst]. *)
charguer's avatar
charguer committed
173 174
  dup 3.
  { xcf. xlet. xapp. simpl. xpull. intros. subst. xapp. }
charguer's avatar
tuto  
charguer committed
175 176 177 178
  { xcf. xapp. intros. subst. xapp. }
  { xcf. xapps. xapp. }
Qed.

charguer's avatar
charguer committed
179
(* Note: recall the specifications of get and set from Pervasives_proof:
charguer's avatar
charguer committed
180

charguer's avatar
charguer committed
181
  Lemma get_spec : forall A (v:A) r,
182
    app get [r]
charguer's avatar
charguer committed
183 184 185 186 187
      PRE (r ~~> v)
      POST (fun x => \[x = v] \* r ~~> v)

  Lemma set_spec : forall A (v w:A) r,
    app set [r w] (r ~~> v) (# r ~~> w).
charguer's avatar
charguer committed
188 189

*)
charguer's avatar
tuto  
charguer committed
190 191

(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
192 193 194

(**
[[
charguer's avatar
tuto  
charguer committed
195
let example_two_ref n =
196 197
  let i = ref 0 in
  let r = ref n in
charguer's avatar
tuto  
charguer committed
198 199 200 201
  decr r;
  incr i;
  r := !i + !r;
  !i + !r
charguer's avatar
charguer committed
202 203
]]
*)
charguer's avatar
tuto  
charguer committed
204

charguer's avatar
charguer committed
205
Lemma example_two_ref_spec : forall n: int,
charguer's avatar
charguer committed
206
  (* <EXO> *)
charguer's avatar
charguer committed
207 208 209
  app example_two_ref [n]
     PRE \[]
     POST (fun x: int => \[ x = n+1 ]).
charguer's avatar
charguer committed
210
  (* </EXO *)
charguer's avatar
charguer committed
211
Proof using.
charguer's avatar
charguer committed
212
  (* Hint: the proof uses [xcf], [xapp], [xapps], and [xret] or [xrets]. *)
charguer's avatar
charguer committed
213
  dup 3.
charguer's avatar
charguer committed
214 215 216 217 218 219 220
  { (* detailed proof *)
    xcf. 
    xapp. (* details: xlet. xapp. simpl. *)
    xapp. xapp. xapp. 
    xapps. (* details: xapp. intro. subst. *)
    xapps. xapps. xapps. xapps.
    xrets. (* details: xret. xsimpl. *) 
charguer's avatar
tuto  
charguer committed
221
    math. }
charguer's avatar
charguer committed
222 223 224 225
  { (* shorter proof, not recommended for nontrivial code *)
    xcf. xgo. subst. math. }
  { (* real proof *)
    xcf. xgo~. }
charguer's avatar
tuto  
charguer committed
226
Qed.
charguer's avatar
charguer committed
227

charguer's avatar
tuto  
charguer committed
228 229 230 231 232 233


(***********************************************************************)
(** For loops *)

(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255

(**
[[
  let facto_for n =
    let r = ref 1 in
    for i = 1 to n do
      r := !r * i;
    done;
    !r
]]
*)

(* Reasoning principle for the loop [for i = a to b to t done] when [b+1>=a]
   implemented by tactic [xfor_inv I].

  I a               initial invariant

  I i -> I (i+1)    when executing [t] on some [i] in the range from [a] to [b]

  I (b+1)           final invariant

*)
charguer's avatar
tuto  
charguer committed
256 257 258 259 260 261 262

Lemma facto_for_spec : forall n,
  n >= 1 ->
  app facto_for [n]
    PRE \[]
    POST (fun (v:int) => \[v = facto n]).
Proof using.
charguer's avatar
charguer committed
263
  =>> Hn. xcf. xapps.
charguer's avatar
tuto  
charguer committed
264 265
  xfor_inv (fun i => r ~~> (facto (i-1))).
  { math. }
charguer's avatar
charguer committed
266
  { xsimpl. forwards: facto_zero. easy. }
267
  { =>> Hi. xapps. xapps. xsimpl.
charguer's avatar
charguer committed
268 269
    rew_maths. rewrite (@facto_succ i). ring. math. }
  xapps. xsimpl. rew_maths. auto.
charguer's avatar
tuto  
charguer committed
270 271 272
Qed.


273

charguer's avatar
charguer committed
274
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
275

charguer's avatar
charguer committed
276 277 278 279 280 281 282 283 284 285 286 287
(**
[[
  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
]]
charguer's avatar
charguer committed
288 289
*)

charguer's avatar
tuto  
charguer committed
290 291 292 293 294 295
Lemma fib_for_spec : forall n,
  n >= 1 ->
  app fib_for [n]
    PRE \[]
    POST (fun (v:int) => \[v = fib n]).
Proof using.
charguer's avatar
charguer committed
296
  (* Hint: follow the pattern from the previous example *)
charguer's avatar
charguer committed
297
  (* <EXO> *)
298
  =>> Hn. xcf. xapps. xapps.
299
  xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
charguer's avatar
charguer committed
300
  { math. }
charguer's avatar
charguer committed
301 302 303
  { xsimpl.
    rewrite~ fib_base. (* details: math. math. rewrite fib_base. *) 
    rewrite~ fib_base. }
304
  { =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
charguer's avatar
charguer committed
305 306 307
    rew_maths. rewrite~ (@fib_succ (i+2)). rew_maths.
    math_rewrite ((i + 2)-1 = i+1). math. }
  xapps. xsimpl~.
charguer's avatar
charguer committed
308 309 310
  (* </EXO> *)
Qed.

charguer's avatar
charguer committed
311

charguer's avatar
charguer committed
312
(*----Alternative script:
charguer's avatar
charguer committed
313

314
  =>> Hn. xcf. xapps. xapps.
charguer's avatar
tuto  
charguer committed
315 316 317 318 319 320
  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.
charguer's avatar
charguer committed
321
    rewrite fib_succ. rew_maths. math. math. }
charguer's avatar
tuto  
charguer committed
322
  xapps. xsimpl. auto.
charguer's avatar
charguer committed
323
*)
324

325

charguer's avatar
tuto  
charguer committed
326 327 328 329

(***********************************************************************)
(** While loops *)

charguer's avatar
charguer committed
330
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361

(**
[[
  let example_while n =
    let i = ref 0 in
    let r = ref 0 in
    while !i < n do
      incr i;
      incr r;
    done;
    !r
]]
*)

(* Reasoning principle for the loop [while t1 do t2] using an invariant
   implemented by tactic [xwhile_inv_basic J W].

  J b i             true for some boolean [b] and some initial index [k]

  J b i             when executing [t1] on some [i]
   ->
  J b' i

  J true i          when executing [t2] on some [i], should restablish the
   ->               invariant for some [b'] and some [i'] smaller than [i]
  J b' i'           w.r.t. [W], that is [W i' i].

  J false i         for some [i] describes the final state

*)

charguer's avatar
charguer committed
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380

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.

charguer's avatar
tuto  
charguer committed
381

charguer's avatar
charguer committed
382
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
383 384 385 386 387 388 389 390 391 392 393 394 395

(**
[[
  let facto_while n =
    let r = ref 1 in
    let i = ref 1 in
    while !i <= n do
      r := !i * !r;
      incr i;
    done;
    !r
]]
*)
charguer's avatar
charguer committed
396 397 398 399 400 401 402

Lemma facto_while_spec : forall n,
  n >= 2 ->
  app facto_while [n]
    PRE \[]
    POST (fun (v:int) => \[v = facto n]).
Proof using.
charguer's avatar
charguer committed
403
  (* Hint: follow the pattern from previous example *)
charguer's avatar
charguer committed
404 405
  (* <EXO> *)
  introv Hn. xcf. xapps. xapps.
406
  xwhile_inv_basic (fun b k => \[b = isTrue (k <= n)] \* \[2 <= k <= n+1]
charguer's avatar
charguer committed
407 408 409 410 411 412 413 414 415 416 417 418 419
                               \* 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.

charguer's avatar
tuto  
charguer committed
420

charguer's avatar
charguer committed
421
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439

(* TODO: add demos using the other xfor and xwhile approach *)   

(*---------------------------------------------------------------------*)

(**
[[
  let is_prime n =
    let i = ref 2 in
    let p = ref true in
    while !p && (!i * !i <= n) do
      if (n mod !i) = 0
        then p := false;
      incr i;
    done;
    !p
]]
*)
charguer's avatar
charguer committed
440

charguer's avatar
stable  
charguer committed
441 442 443
Require Import Psatz.
Tactic Notation "math_nia" := math_setup; nia.

charguer's avatar
charguer committed
444 445 446 447 448 449 450 451 452 453
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)]
454 455
       \* \[2 <= k]
       \* i ~~> k
charguer's avatar
charguer committed
456 457 458 459 460 461 462
       \* 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.
charguer's avatar
charguer committed
463 464
    xclean. (* cleans up results of boolean tests *)
    destruct Hb as (Hvp&Hkk).
charguer's avatar
charguer committed
465
    xapps. xapps. math.
charguer's avatar
charguer committed
466 467 468
    xrets. 
    xseq. (* TODO: later try to change xif to remove xseq *)
    xif (# Hexists (vp':bool), i ~~> k \* p ~~> vp' \*
charguer's avatar
charguer committed
469 470 471 472 473 474 475 476 477
       \[if vp' then (forall d, 1 < d < (k+1) -> Z.rem n d <> 0) else (~ prime n)]).
      { 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.
charguer's avatar
stable  
charguer committed
478
  xapps. xsimpl. subst. case_if; rew_bool_eq.
charguer's avatar
charguer committed
479 480 481
  { destruct Hb; tryfalse. applys* not_divide_prime_sqrt. math. }
  { auto. }
Qed.
charguer's avatar
tuto  
charguer committed
482 483 484 485 486


(***********************************************************************)
(** Recursion *)

charguer's avatar
charguer committed
487
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
488 489 490 491 492 493 494 495 496

(**
[[
  let rec facto_rec n =
    if n <= 1
      then 1
      else n * facto_rec(n-1)
]]
*)
charguer's avatar
charguer committed
497

charguer's avatar
charguer committed
498 499 500 501 502
Lemma facto_rec_spec : forall n,
  n >= 1 ->
  app facto_rec [n]
    PRE \[]
    POST (fun (v:int) => \[v = facto n]).
charguer's avatar
charguer committed
503
Proof using.
charguer's avatar
charguer committed
504
  => n. induction_wf IH: (downto 0) n. unfolds downto. => Hn.
505
  xcf. xif.
charguer's avatar
charguer committed
506
  { xrets. math_rewrite (n=1). rewrite~ facto_one. }
charguer's avatar
charguer committed
507
  { xapps. math. math. (* optimization: could be written [xapps~] *)
508
    xrets. rewrite~ (@facto_succ n). }
charguer's avatar
charguer committed
509 510 511
Qed.


charguer's avatar
charguer committed
512
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
513 514 515 516 517 518 519 520 521

(**
[[
  let rec fib_rec n =
    if n <= 1
      then 1
      else fib_rec(n-1) + fib_rec(n-2)
]]
*)
charguer's avatar
charguer committed
522

charguer's avatar
charguer committed
523 524 525 526 527
Lemma fib_rec_spec : forall n,
  n >= 0 ->
  app fib_rec [n]
    PRE \[]
    POST (fun (v:int) => \[v = fib n]).
528
Proof using.
charguer's avatar
charguer committed
529
  (* Hint: follow the pattern for the previous example *)
charguer's avatar
charguer committed
530 531
  (* <EXO> *)
  => n. induction_wf IH: (downto 0) n. => Hn.
532
  xcf. xif.
charguer's avatar
charguer committed
533
  { xrets. rewrite~ fib_base. }
534
  { xapps~. xapps~. xrets. rewrite~ (@fib_succ n). }
charguer's avatar
charguer committed
535
  (* </EXO> *)
charguer's avatar
charguer committed
536 537 538
Qed.


charguer's avatar
charguer committed
539 540 541 542 543 544

(***********************************************************************)
(** Stack *)

(*---------------------------------------------------------------------*)

charguer's avatar
charguer committed
545 546 547 548 549 550 551
(*
[[
  module StackList = struct

    type 'a t = {
       mutable items : 'a list;
       mutable size : int }
charguer's avatar
charguer committed
552

charguer's avatar
charguer committed
553 554 555
    let create () =
      { items = [];
        size = 0 }
charguer's avatar
charguer committed
556

charguer's avatar
charguer committed
557 558
    let size s =
      s.size
charguer's avatar
charguer committed
559

charguer's avatar
charguer committed
560 561
    let is_empty s =
      s.size = 0
charguer's avatar
charguer committed
562

charguer's avatar
charguer committed
563 564 565
    let push x s =
      s.items <- x :: s.items;
      s.size <- s.size + 1
charguer's avatar
charguer committed
566

charguer's avatar
charguer committed
567 568 569 570 571 572 573
    let pop s =
      match s.items with
      | hd::tl ->
          s.items <- tl;
          s.size <- s.size - 1;
          hd
      | [] -> assert false
charguer's avatar
charguer committed
574

charguer's avatar
charguer committed
575 576 577
  end
]]
*)
charguer's avatar
charguer committed
578 579 580 581 582

Module StackListProof.

Import StackList_ml.

charguer's avatar
charguer committed
583

charguer's avatar
charguer committed
584
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
charguer's avatar
charguer committed
585

586 587 588
Definition Stack A (L:list A) r :=
  Hexists n,
      r ~> `{ items' := L; size' := n }
charguer's avatar
charguer committed
589 590
   \* \[ n = length L ].

charguer's avatar
charguer committed
591 592 593 594 595 596
(** Unfolding and folding lemmas paraphrasing the definition of [Stack] *)

Lemma Stack_open : forall r A (L:list A),
  r ~> Stack L ==>
  Hexists n, r ~> `{ items' := L; size' := n } \* \[ n = length L ].
Proof using. intros. xunfolds~ Stack. Qed.
charguer's avatar
charguer committed
597

charguer's avatar
charguer committed
598 599 600 601 602
Lemma Stack_close : forall r A (L:list A) (n:int),
  n = length L ->
  r ~> `{ items' := L; size' := n } ==>
  r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
charguer's avatar
charguer committed
603

charguer's avatar
charguer committed
604
Arguments Stack_close : clear implicits.
charguer's avatar
charguer committed
605 606


charguer's avatar
charguer committed
607 608 609
(** Customization of [xopen] and [xclose] tactics for [Stack].
    These tactics avoid the need to call [hchange] or [xchange]
    by providing explicitly the lemmas [Stack_open] and [Stack_close]. *)
charguer's avatar
charguer committed
610

charguer's avatar
charguer committed
611 612 613 614
Hint Extern 1 (RegisterOpen (Stack _)) =>
  Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
  Provide Stack_close.
charguer's avatar
charguer committed
615

charguer's avatar
charguer committed
616
(** Verification of the code *)
charguer's avatar
charguer committed
617 618

Lemma create_spec : forall (A:Type),
619
  app create [tt]
charguer's avatar
charguer committed
620 621 622
    PRE \[]
    POST (fun r => r ~> Stack (@nil A)).
Proof using.
charguer's avatar
charguer committed
623 624 625 626
  xcf.
  xapp ;=> r. (* ddetails: xapp. intros r. *)
  xclose r. (* details: xchange (@Stack_close r). *)
  auto. xsimpl.
charguer's avatar
charguer committed
627 628 629
Qed.

Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
630
  app size [s]
charguer's avatar
charguer committed
631 632
    INV (s ~> Stack L)
    POST (fun n => \[n = length L]).
charguer's avatar
charguer committed
633
(* Remark: the above is a notation for:
634
  app size [s]
charguer's avatar
charguer committed
635 636 637
    PRE (s ~> Stack L)
    POST (fun n => \[n = length L] \* s ~> Stack L).
*)
charguer's avatar
charguer committed
638
Proof using.
639
  xcf.
charguer's avatar
charguer committed
640 641 642 643 644 645 646
  xopen s. (* details: xchange (@Stack_open s). *)
  xpull ;=> n Hn. xapp. => m. xpull ;=> E.
  xclose s. (* details: xchange (@Stack_close s). *)
  auto. xsimpl. math.
  (* Here we have an issue because Coq is a bit limited.
     Workaround to discharge the remaining type: *)
  Unshelve. solve_type. (* TODO: support [xcf A] in the beginning *)
charguer's avatar
charguer committed
647 648 649 650 651
Qed.

Lemma length_zero_iff_nil : forall A (L:list A),
  length L = 0 <-> L = nil.
Proof using.
charguer's avatar
charguer committed
652 653
  =>. subst. destruct L; rew_list. (* [rew_list] normalizes list expressions *) 
  autos*. iff M; false; math.
charguer's avatar
charguer committed
654 655 656 657
Qed.

Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
  (* <EXO> *)
658
  app is_empty [s]
charguer's avatar
charguer committed
659 660 661 662
    INV (s ~> Stack L)
    POST (fun b => \[b = isTrue (L = nil)]).
  (* </EXO> *)
Proof using.
charguer's avatar
charguer committed
663 664 665
  (* Hint: use [xopen] then [xclose] like in [size_spec].
     Also use [xcf], [xpull], [xapps], [xrets],
     and lemma [length_zero_iff_nil] from above. *)
charguer's avatar
charguer committed
666 667 668 669
  (* <EXO> *)
  xcf. xopen s. xpull ;=> n Hn. xapps. xclose~ s. xrets.
  subst. apply length_zero_iff_nil.
  (* </EXO> *)
charguer's avatar
charguer committed
670
  Unshelve. solve_type.
charguer's avatar
charguer committed
671 672 673
Qed.

Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A),
674
  app push [x s]
charguer's avatar
charguer committed
675 676 677
    PRE (s ~> Stack L)
    POST (# s ~> Stack (x::L)).
Proof using.
charguer's avatar
charguer committed
678 679
  (* Hint: use [xcf], [xapp], [xapps], [xpull], [xsimpl],
     [xopen], [xclose] and [rew_list] *)
charguer's avatar
charguer committed
680
  (* <EXO> *)
charguer's avatar
charguer committed
681
  xcf.
charguer's avatar
charguer committed
682
  xopen s. (* details: xchange (@Stack_open s) *)
683
  xpull ;=> n Hn.
charguer's avatar
charguer committed
684
  xapps. xapps. xapps. xapp.
charguer's avatar
charguer committed
685
  xclose s. (* details: xchange (@Stack_close s) *)
charguer's avatar
charguer committed
686 687
  rew_list. math.
  xsimpl.
charguer's avatar
charguer committed
688 689 690 691 692
  (* </EXO> *)
Qed.

Lemma pop_spec : forall (A:Type) (L:list A) (s:loc),
  L <> nil ->
693
  app pop [s]
charguer's avatar
charguer committed
694 695 696
    PRE (s ~> Stack L)
    POST (fun x => Hexists L', \[L = x::L'] \* s ~> Stack L').
Proof using.
charguer's avatar
charguer committed
697
  (* Hint: also use [rew_list in H] *)
charguer's avatar
charguer committed
698 699 700 701 702 703 704 705
  (* <EXO> *)
  =>> HL. xcf. xopen s. xpull ;=> n Hn. xapps. xmatch.
  xapps. xapps. xapps. xret. xclose~ s. rew_list in Hn. math.
  (* </EXO> *)
Qed.



charguer's avatar
charguer committed
706 707
(***********************************************************************)
(** Array *)
charguer's avatar
charguer committed
708

charguer's avatar
charguer committed
709
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
710 711 712 713 714 715 716 717 718
(*
[[
  let demo_array () =
    let t = Array.make 3 true in
    t.(0) <- false;
    t.(1) <- false;
    t
]]
*)
charguer's avatar
charguer committed
719

720
Lemma demo_array_spec :
charguer's avatar
charguer committed
721 722
  app demo_array [tt]
    PRE \[]
723
    POST (fun (t:loc) => Hexists M, (t ~> Array M)
charguer's avatar
charguer committed
724
       \* \[forall k, 0 <= k < 3 -> M[k] = isTrue(k > 1)]).
charguer's avatar
tuto  
charguer committed
725
Proof using.
charguer's avatar
charguer committed
726
  dup 2.
charguer's avatar
charguer committed
727 728
  { (* Detailed proof: *)
    xcf.
charguer's avatar
charguer committed
729 730 731 732 733
    xapp. math. => M EM.
    xapp. autos.
    xapp. autos.
    xret. xsimpl. =>> Hk. subst M. rew_array; autos.
     case_ifs. math. math. math. }
charguer's avatar
charguer committed
734 735
  { (* Shorter proof *)
    xcf. xapp~. => M EM. xapp~. xapp~. xrets.
charguer's avatar
charguer committed
736
    =>> Hk. subst M. rew_array~. case_ifs; math. }
charguer's avatar
tuto  
charguer committed
737
Qed.
charguer's avatar
sieve  
charguer committed
738

charguer's avatar
charguer committed
739

charguer's avatar
charguer committed
740

charguer's avatar
charguer committed
741
(*---------------------------------------------------------------------*)
charguer's avatar
charguer committed
742 743 744 745 746 747 748 749
(*
[[
  let exercise_array () =
    let t = Array.make 3 true in
    t.(2) <- false;
    t.(1) <- t.(2);
    t
]]
charguer's avatar
charguer committed
750
*)
charguer's avatar
tuto  
charguer committed
751

charguer's avatar
charguer committed
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777
Lemma exercise_array_spec :
  App exercise_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.


charguer's avatar
charguer committed
778

charguer's avatar
charguer committed
779 780


charguer's avatar
charguer committed
781 782 783
(***********************************************************************)
(***********************************************************************)
(***********************************************************************)
784 785

End StackListProof.
charguer's avatar
charguer committed
786 787 788 789 790 791 792 793 794 795 796



(* LATER
  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.
  Hint Constructors Forall.
  Global Opaque Z.mul.
*)