Commit f373f3b2 authored by POTTIER Francois's avatar POTTIER Francois

Fix 3 examples so that they compile again.

parent a0436157
Set Implicit Arguments.
Require Import CFLib CFLibCredits.
Require Import CFML.CFLib CFML.CFLibCredits.
(* Require Import RandomAccessListSig_ml. *)
Require Import BinaryRandomAccessList_ml.
Require Import LibListZ.
Require Import TLC.LibListZ.
Module BinaryRandomAccessListSpec (* <: RandomAccessListSigSpec *).
......@@ -149,7 +149,7 @@ Qed.
Lemma inv_ts_len : forall A ts p (L:list A),
inv p ts L ->
ts <> nil ->
ts <> nil ->
2 ^ (p + (length ts) - 1) <= length L.
Proof.
induction ts as [|d ts].
......@@ -208,8 +208,8 @@ Qed.
(** verification *)
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
and tactic rew_div pour optimiser. *)
Lemma pow2_succ_div : forall p, p >= 0 -> 2 ^ (p+1) ÷ 2 = 2 ^ p.
......@@ -301,7 +301,7 @@ Proof. xcf. xapp~. Qed.
Hint Extern 1 (RegisterSpec cons) => Provide cons_spec.
Lemma uncons_tree_spec : forall A (ts: rlist_ A) p L,
inv p ts L ->
inv p ts L ->
ts <> nil ->
app uncons_tree [ts]
PRE \[]
......@@ -359,7 +359,7 @@ Qed.
Hint Extern 1 (RegisterSpec tail) => Provide tail_spec.
Require Import LibInt.
Require Import TLC.LibInt.
Lemma lookup_tree_spec :
forall a i (t: tree_ a) p L,
......@@ -382,7 +382,7 @@ Qed.
Hint Extern 1 (RegisterSpec lookup_tree) => Provide lookup_tree_spec.
Lemma update_tree_spec :
Lemma update_tree_spec :
forall a i (x: a) (t: tree_ a) p L,
btree p t L ->
ZInbound i L ->
......@@ -405,7 +405,7 @@ Qed.
Hint Extern 1 (RegisterSpec update_tree) => Provide update_tree_spec.
Ltac xapp_xapply_no_simpl K ::=
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
Lemma lookup_spec_ind :
......@@ -421,7 +421,7 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
......@@ -444,30 +444,30 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
(*
-- strategy 2.
-- strategy 2.
introv. unfold Rlist. generalize 0 as p. revert i L.
induction ts; introv I Bi; inverts I; xcf.
- xgo. apply~ ZInbound_nil_inv.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
-- strategy 3.
-- strategy 3.
assert ( de toute la spec )
-- strategy 4
lemme séparée
-- strategy 4
lemme séparée
*)
Qed.
(* OLD
......
Set Implicit Arguments.
Require Import CFLib.
Require Import CFML.CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Import ZsubNoSimpl.
......@@ -1188,7 +1188,7 @@ Abort.
(********************************************************************)
(* ** Recursive function *)
Require Import LibInt.
Require Import TLC.LibInt.
Lemma rec_partial_half_spec : forall k n,
n = 2 * k -> k >= 0 ->
......@@ -1426,7 +1426,7 @@ Qed.
(********************************************************************)
(* ** Arrays *)
Require Import Array_proof LibListZ.
Require Import Array_proof TLC.LibListZ.
Section Array.
......
Set Implicit Arguments.
Require Import CFLib Pervasives_ml Pervasives_proof Array_proof Tuto_ml.
Require Import LibListZ.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import Tuto_ml.
Require Import TLC.LibListZ.
(***********************************************************************)
......@@ -43,7 +46,7 @@ Shortcut:
- [xrets] like [xret; xsimpl]
- [xapps] like [xapp; xextracts]
- [tactic~] like [tactic; eauto with maths]
*)
*)
(***********************************************************************)
......@@ -52,7 +55,7 @@ Shortcut:
(** Factorial *)
Parameter facto : int -> int.
Parameter facto_zero : facto 0 = 1.
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).
......@@ -122,13 +125,13 @@ Lemma example_let_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = 2*n]). (* POST \[= (2 * n)] *)
Proof using.
dup 2.
{ xcf.
xlet. xret. simpl. xpull. intros Ha.
dup 2.
{ xcf.
xlet. xret. simpl. xpull. intros Ha.
xlet. xret. simpl. xpull. intros Hb.
xret. (*hnf.*) xsimpl. math. }
{ xcf. xret ;=> Ha. xret. intros Hb. xret. xsimpl. math. }
(* use: [xcf], [xret], [xsimpl], [math];
(* use: [xcf], [xret], [xsimpl], [math];
[xlet] is optional; if used then [xpull] is also needed. *)
Qed.
......@@ -140,7 +143,7 @@ let example_incr r =
let example_incr r =
let x0__ := get r in
set r (x0__ + 1)
set r (x0__ + 1)
----*)
......@@ -159,13 +162,13 @@ Qed.
(*
Let x0__ := app get [r] in
app set [r (x0__ + 1)]
app set [r (x0__ + 1)]
*)
(* Remark: here are the specifications of get and set from Pervasives_proof.
Lemma get_spec : forall A (v:A) r,
app get [r]
app get [r]
PRE (r ~~> v)
POST (fun x => \[x = v] \* r ~~> v)
......@@ -193,13 +196,13 @@ Lemma example_two_ref_spec : forall n: int,
Proof using.
(*
dup 3.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
xapp.
xapp.
xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
}
{xcf. xgo. subst. math. }
}
{xcf. xgo. subst. math. }
*)
......@@ -207,15 +210,15 @@ Proof using.
xcf. xapp. xapp. xapp. xapp. xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
Qed.
(*
(*
app example_two_ref [n]
PRE \[]
POST (fun (v:int) => \[v = n+1]).
(* </EXO> *)
Proof using.
(* <EXO> *)
dup.
dup.
{ xcf.
xapps.
xapps.
......@@ -258,7 +261,7 @@ Proof using.
xfor_inv (fun i => r ~~> (facto (i-1))).
{ math. }
{ xsimpl. forwards: facto_zero. easy. }
{ =>> Hi. xapps. xapps. xsimpl.
{ =>> Hi. xapps. xapps. xsimpl.
rew_maths. rewrite (@facto_succ i). ring. math. }
xapps. xsimpl. rew_maths. auto.
Qed.
......@@ -269,7 +272,7 @@ Qed.
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
*)
......@@ -326,19 +329,19 @@ Proof using.
(* <EXO> *)
=>> Hn. xcf. xapps. xapps.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
{ math. }
{ xsimpl. rewrite fib_base. math. math. rewrite~ fib_base. (*math. math.*) }
{ =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
{ =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
rew_maths. rewrite~ (@fib_succ (i+2)). rew_maths. math_rewrite ((i + 2)-1 = i+1). math. }
xapps. xsimpl~.
xapps. xsimpl~.
(* </EXO> *)
Qed.
(*----Alternative script:
=>> Hn. xcf. xapps. xapps.
=>> Hn. xcf. xapps. xapps.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1))).
{ math. }
{ xsimpl.
......@@ -349,7 +352,7 @@ Qed.
xapps. xsimpl. auto.
*)
(***********************************************************************)
(** While loops *)
......@@ -547,8 +550,8 @@ module StackList = struct
let pop s =
match s.items with
| hd::tl ->
s.items <- tl;
| hd::tl ->
s.items <- tl;
s.size <- s.size - 1;
hd
| [] -> assert false
......@@ -562,9 +565,9 @@ Import StackList_ml.
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
Definition Stack A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
Definition Stack A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
......@@ -599,12 +602,12 @@ Proof using.
Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
app size [s]
app size [s]
INV (s ~> Stack L)
POST (fun n => \[n = length L]).
(* Remark: the above is a notation for:
app size [s]
app size [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L).
*)
......@@ -613,7 +616,7 @@ Proof using.
xcf.
xopen s. xpull ;=> n Hn. xapp. => m. xpull ;=> E.
xclose s. auto. xsimpl. math.
Unshelve. solve_type. (* todo: xcf A *)
Unshelve. solve_type. (* todo: xcf A *)
Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
......@@ -644,7 +647,7 @@ Proof using.
(* <EXO> *)
xcf.
xopen s. (* Same as [xchange (@Stack_open s)] *)
xpull ;=> n Hn.
xpull ;=> n Hn.
xapps. xapps. xapps. xapp.
xclose s. (* Same as [xchange (@Stack_close s)] *)
rew_list. math.
......
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