Commit 11e082f4 authored by charguer's avatar charguer

progress_tactics

parent 3d98a723
Set Implicit Arguments.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(** * Polymorphic let demos *)
(** Demo top-level polymorphic let. *)
Lemma poly_top_spec : forall A,
poly_top = @nil A.
Proof using. xcf. Qed.
(** Demo local polymorphic let. *)
Lemma poly_let_1_spec : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval. subst. xrets. auto. Qed.
(** Demo [xval_st P] *)
Lemma poly_let_1_spec' : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil). extens~. xrets. subst~. Qed.
(** Demo [xval_st P as x Hx] *)
Lemma poly_let_1_spec'' : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil) as p Hp. extens~. xrets. subst~. Qed.
(** Demo for partially-polymorphic values. *)
Lemma poly_let_2_spec : forall A1 A2,
Spec poly_let_2 () |B>>
B \[] (fun '(x,y) : list A1 * list A2 => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.
Lemma poly_let_2_same_spec : forall A,
Spec poly_let_2_same () |B>>
B \[] (fun '(x,y) : list A * list A => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.
Lemma poly_let_2_partial_spec : forall A,
Spec poly_let_2_partial () |B>>
B \[] (fun '(x,y) : list A * list int => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
(*************************************************************************)
(* If demo *)
(**)
(* data base demo => tlc
Definition mydatabase := True.
Definition mykey := 3.
Lemma mylemma : True -> True. auto. Qed.
Hint Extern 1 (Register mydatabase mykey) => Provide mylemma.
Lemma ltac_database_demo : True.
ltac_database_get mydatabase mykey. intros _.
try ( ltac_database_get mydatabase 3 ). (* fails --no conversion *)
auto.
Qed.
*)
(*
Ltac auto_tilde ::= try solve [ intros; auto with maths ].
*)
Lemma if_demo_spec :
Spec if_demo (b:bool) |B>>
B \[] (fun (x:int) => \[0 <= x <= 1]).
Proof.
xcf. intros. xapp. xapps.
xseq (Hexists (x:int), r ~~> x \* \[x = 0 \/ x = 1] \* s ~~> 5).
xif. xapp~. hsimpl~. xrets~.
introv C. xgc. xapps. intros M. hsimpl. subst. invert C; math.
Qed.
(*
let if_demo b =
let r = ref 0 in
let s = ref 5 in
if b
then incr r;
!r
*)
(*
(*************************************************************************)
(* Arrays as sequences *)
Ltac index_solve := subst; rew_arr; math.
Hint Extern 1 (index _ _) => index_solve.
Lemma array_demo_spec :
Spec array_demo () |B>>
B \[] (fun n => \[n = 3]).
Proof.
xcf.
xapp. xapp. hnf. math. intros L (LL&LV).
xapp. math. intros Ex.
(* xapp. math. sets_eq L': (L[2:=4]). *)
(* xapp_spec ml_array_set_named_spec. math. intros L' EL'. *)
xapp_by named. math. intros L' EL'.
xapp. subst. rew_arr. math. intros Ey. rewrite EL' in Ey. (*rewrite read_write_eq in Ey.*) rew_arrs.
xapp. auto. (* index_solve. *) (* subst. rew_arr. math. *) intros Ez.
rewrite EL' in Ez. rew_arrs. case_if.
xapp. hsimpl. subst. rew_arrs. math.
Qed.
(*
let array_demo () =
let t = Array.make 3 0 in
let x = t.(1) in
t.(2) <- 4;
let y = t.(2) in
let z = t.(1) in
Array.length t
*)
(*************************************************************************)
(* Simple records *)
(* this definition will later not be needed *)
Notation "'RMyrec'" := (Myrec Id Id).
(* "r ~> RMyrec n L" asserts that at location "r"
we find a record of type "myrec" with field "nb"
storing "n" and the field "items" storing "L". *)
(* Note that "myrec A" is a type equivalent to "loc" *)
(*
let myrec_incr_nb r =
r.nb <- r.nb + 1
*)
Lemma myrec_incr_nb_spec : forall A,
Spec myrec_incr_nb (r:myrec A) |B>>
forall n (L:list A),
B (r ~> RMyrec n L) (# r ~> RMyrec (n+1) L).
Proof.
xcf. intros.
xapp. intro_subst. (* read *)
xapps. (* write *)
hsimpl.
Qed.
(* below, "keep B H Q" is the same as "B H (Q \*+ H)";
here, it is the same as
"B (r ~> RMyrec n L)
(fun (k:int) => \[k = LibList.length L] \* r ~> RMyrec n L)."
*)
(*
let myrec_length_items r =
List.length r.items
*)
Lemma myrec_length_items : forall A,
Spec myrec_length_items (r:myrec A) |B>>
forall n (L:list A),
keep B (r ~> RMyrec n L)
(fun (k:int) => \[k = LibList.length L]).
Proof.
xcf. intros. xapps. xrets. auto.
Qed.
(* Definition of an invariant on the record, in the form
of a representation predicate. The predicate
"r ~> SizedList Q" asserts that at location "r" we find
a record with fields "n" and "Q" such that "n" is always
equal to the length of the list Q. *)
Definition SizedList A (Q:list A) (r:myrec A) :=
Hexists n, r ~> RMyrec n Q \* \[n = LibList.length Q].
Lemma SizedList_unfocus : forall A (r:myrec A) (Q:list A) (n:int),
n = LibList.length Q ->
(r ~> RMyrec n Q) ==> (r ~> SizedList Q).
Proof.
introv E. hunfold SizedList. hsimpl. auto.
Qed.
Implicit Arguments SizedList_unfocus [A].
(* remark: the following definition is equivalent ot the above.
*)
Definition SizedList' A (Q:list A) (r:myrec A) :=
Hexists n L, r ~> RMyrec n L \*
\[n = LibList.length L /\ L = Q].
Lemma SizedList_equiv : forall A (Q:list A) (r:myrec A),
r ~> SizedList Q ==> r ~> SizedList' Q.
Proof.
intros. hunfold SizedList. (* at 1 *)
(* unfold SizedList. hdata_simpl. *)
hunfold SizedList'.
hextract as n En. hsimpl. auto.
Qed.
Lemma SizedList_equiv2 : forall A (Q:list A) (r:myrec A),
r ~> SizedList' Q ==> r ~> SizedList Q.
Proof.
intros. hunfold SizedList. hunfold SizedList'.
hextract as n L (En&EL). hsimpl. subst~.
Qed.
Lemma myrec_inv_length_items : forall A,
Spec myrec_inv_length_items (r:myrec A) |B>>
forall (Q:list A),
keep B (r ~> SizedList Q)
(fun (k:int) => \[k = LibList.length Q]).
Proof.
xcf. intros. hunfold SizedList at 1.
xextract as n En. xapp. intros x. hextract as Ex. subst.
hchange (SizedList_unfocus r). auto.
hsimpl. auto.
(*
(* if we run "xapp" here, we're stuck; try it! *)
(* xapp. *)
(* use "hunfold" to unfold SizedList in the heap predicate *)
hunfold SizedList at 1.
(* note that we added "at 1" to avoid unfolding the definition
in the post-condition as well; but it would be fine to just
do "hunfold SizedList" if we didn't care for readability *)
(* extract the existential that appears in the pre-condition *)
xextract as n En.
(* read the field nb *)
xapp.
(* if we run "hsimpl" here, we're stuck: try it! *)
(* hsimpl. *)
(* unfold "SizedList" in the post-condition *)
hunfold SizedList.
(* simplify *)
hsimpl. subst~. subst~.
*)
Qed.
(* here, we show that by adding an item to "items" and by
incrementing "nb", we correctly preserve the invariant. *)
Lemma myrec_inv_push : forall A,
Spec myrec_inv_push (x:A) (r:myrec A) |B>>
forall (Q:list A),
B (r ~> SizedList Q) (# r ~> SizedList (x::Q)).
Proof.
xcf. intros.
(* hunfold SizedList. xapps.
xapp. xapps. xapp. hsimpl. rew_list. math. *)
hunfold SizedList at 1. xapps.
xapp. xapps. xapp.
(* hunfold SizedList. hsimpl. rew_list. math. *)
hchange (SizedList_unfocus r). rew_list. math. hsimpl.
Qed.
*)
(*************************************************************************)
(*************************************************************************)
(*
(*************************************************************************)
(* Partial recursive function *)
(** Step-by-step proof, by induction on [n] *)
Lemma half_spec_1 :
forall n x, n >= 0 -> x = n+n ->
(App half x;) \[] (fun x => \[x = n]).
Proof.
intros n. induction_wf IH: (int_downto_wf 0) n.
introv P D. xcf_app.
xif.
xret. hsimpl. math.
xif.
xfail. math.
xlet.
xapply (IH (n-1)).
hnf. math. (* or auto with maths. *)
math.
math.
hsimpl.
xok.
xextract as E. xret. hsimpl. math.
Qed.
(** Step-by-step proof, by induction on [x] *)
Lemma half_spec_2 :
forall x n, n >= 0 -> x = n+n ->
(App half x;) \[] (fun x => \[x = n]).
Proof.
intros x. induction_wf IH: (int_downto_wf 0) x.
introv P D. xcf_app.
xif.
xret. hsimpl. math.
xif.
xfail. math.
xlet.
xapply (>> IH (x-2) (n-1)).
hnf. math. (* or auto with maths. *)
math.
math.
hsimpl.
xok.
xextract as E. xret. hsimpl. math.
Qed.
(** A better proofs, by induction on [x] *)
(* TODO: fix this
Lemma half_spec_3 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R \[] (\= n).
Proof.
xinduction (downto 0). xcf.
introv IH P D.
repeat xif.
xrets. math.
xfail. math.
xapp (n-1).
auto with maths.
math.
math.
intro_subst. xrets. math.
Qed.
*)
(** An optimized proofs, by induction on [x] *)
Ltac auto_tilde ::= auto with maths.
(*
TODO: fix this
Lemma half_spec_4 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R \[] (\= n).
Proof.
xinduction (downto 0). xcf. introv IH P D.
repeat xif. xgo~. xgo~. xapp~ (n-1). xgo~.
Qed.
*)
(** An optimized proofs, by induction on [n] *)
Lemma half_spec_5 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R \[] (fun x => \[x = n]).
Proof.
xinduction_heap (unproj21 int (downto 0)).
xcf. intros x n IH P D.
repeat xif. xgo~. xgo~. xapp~ (n-1). xgo~.
Qed.
(*************************************************************************)
(* Partial apps *)
Lemma add_spec :
Spec add x y |R>> R \[] (fun z => \[z = x + y]).
Proof. xgo*. Qed.
Hint Extern 1 (RegisterSpec add) => Provide add_spec.
Lemma hof_spec : forall A B,
Spec hof (x:A) (f:func) |R>> forall (H:hprop) (Q:B->hprop),
(App f x; H Q) -> R H Q.
Proof. xcf. auto. Qed.
Hint Extern 1 (RegisterSpec hof) => Provide hof_spec.
Lemma test_partial_app_1_spec :
Spec test_partial_app_1 () |R>> R \[] (fun x => \[x = 3]).
Proof.
xcf. xapp_partial. intros Sg. xapp. hsimpl*.
(* or: xcf. xlet. xframe - \[]. xapp_partial. xok. xextract. intros Sg. xapp. hsimpl*. *)
Qed.
Lemma test_partial_app_1_spec' : forall x,
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => \[r = 3] \* x ~~> 4).
Proof.
xcf. xapp_partial. intros Sg. xapp. hsimpl*.
Qed.
Lemma test_partial_app_1_spec'' : forall x,
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => \[r = 3] \* x ~~> 4).
Proof.
xcf. xlet. (* how to execute xapp_partial step by step *)
eapply local_wframe. xlocal.
xapp_show_spec.
let arity_goal := spec_goal_arity tt in
let arity_hyp := spec_term_arity H in
let lemma := get_spec_elim_x_y arity_hyp arity_goal in
lets K: lemma;
lets K': (>> lemma H).
apply K'.
hsimpl.
try xok.
xextract.
intros Sg. xapp. hsimpl*.
Qed.
Lemma test_partial_app_2_spec :
Spec test_partial_app_2 () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf. xapp_partial as P1. intros HP1.
xapp \[]. (* effectively inline the code of the function [hof] *)
(* -> the empty heap is used to instantiate the variable [H] from [hof_spec] *)
xapp. (* reason about the application of function [P1] *)
hsimpl*.
Qed.
Lemma test_partial_app_2_spec' :
Spec test_partial_app_2 () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf. xapp_partial as P1. intros HP1.
xapp. (* if we do not provide the argument [H] *)
xapp.
instantiate (1 := \[]). hsimpl. (* then we later need to instantiate it manually *)
(* even though in this particular example, a more powerful version of
hsimpl should be able to do the unification properly *)
hsimpl*.
Qed.
Lemma func4_spec :
Spec func4 a b c d |R>> R \[] (fun x => \[x = a + b + c + d]).
Proof. xgo*. Qed.
Hint Extern 1 (RegisterSpec func4) => Provide func4_spec.
Lemma test_partial_app_3_spec :
Spec test_partial_app_3 () |R>> R \[] (fun x => \[x = 30]).
Proof.
xcf.
xapp_partial. intros Hf1.
xapp_partial. intros Hf2.
xapp_partial. intros Hf3.
xapps.
xapps.
xapps.
xret*.
Qed.
(*************************************************************************)
(* Inlining *)
Lemma test_inlining_spec :
Spec test_inlining () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf.
xfun f. (* use the most-general spec for specifying the local function *)
simpl in Sf. (* optional clean up *)
xcf_app. (* reason on [hof] using directly its caracteristic formula *)
xcf_app. (* reason on [f] using [Sf] *)
xret*.
Qed.
(*************************************************************************)
(* Linked lists *)
(*
(* [cell A] is equivalent to [loc] *)
Print cell.
(* [Cell] is the representation predicate,
so you can write [x ~> Cell T1 T2 V1 V2]. *)
Check Cell.
(* Focus and unfocus operations *)
Check Cell_focus.
Check Cell_unfocus.
(* Specification of creation and accessors for fields *)
Check _new_cell_spec.
Check _get_next_spec.
Check _set_next_spec.
Check _get_content_spec.
Check _set_content_spec.
*)
(* We can define our own representation on top of [Cell] *)
Fixpoint CList a A (T:A->a->hprop) (L:list A) (l:loc) : hprop :=
match L with
| nil => \[]
| X::L' => l ~> Cell T (CList T) X L'
end.
(* We can show that allocating a Cell extends a CList *)
Lemma CList_from_Cell : forall l a x q A (T:A->a->hprop) X Q,
l ~> Cell Id Id x q \* x ~> T X \* q ~> CList T Q
==> l ~> CList T (X::Q).
Proof. intros. hchange (Cell_unfocus l). hsimpl. Qed.
Lemma CList_to_Cell : forall l a A (T:A->a->hprop) X Q,
l ~> CList T (X::Q) ==> Hexists x q,
l ~> Cell Id Id x q \* x ~> T X \* q ~> CList T Q.
Proof. intros. hdata_simpl CList. fold CList. hchange (Cell_focus l). hsimpl. Qed.
Implicit Arguments CList_from_Cell [a A].
Implicit Arguments CList_to_Cell [a A].
Opaque CList.
(** From there, we can prove the function [newx] *)
(*
let newx x q1 q2 =
let machin = {content = x; next = q1} in
machin.next <- q2
*)
Lemma newx_spec : forall a,
Spec newx (x:a) (q1:loc) (q2:loc) |R>>
forall A (T:A->a->hprop) (X:A) (L1 L2 : list A),
R (x ~> T X \* q1 ~> CList T L1 \* q2 ~> CList T L2)
(fun l => l ~> CList T (X::L2)).
Proof.
xcf. (* apply the characteristic formula *)
intros. (* introduces the arguments *)
xapp. (* reason on application *)
(* at this point we could call [xapp] directly, but let's
first see how we can build a clean CList first *)
xchange (CList_from_Cell machin).
(* at this point we cannot call [xapp] because
updating the record requires a [Cell] *)
xchange (CList_to_Cell machin). xextract as y q.
(* now we can continue *)
xapp. (* reason on application *)
(* We could be tempted to conclude with [xret], but that
would not work since we need to do some garbage collection *)
xret. (* conclude and create an existential for the discarded heap *)
(* finally we need to rebuild the CList as earlier on *)
hchange (CList_from_Cell machin).
hsimpl.
Qed.
(** A specification proof is always followed with a line of the
following form, for registering the specification so that it
can be automatically used to reason about a call to the function *)
Hint Extern 1 (RegisterSpec newx) => Provide newx_spec.
*)
......@@ -8,47 +8,6 @@ open Pervasives
*)
(********************************************************************)
(* ** Top-level values *)
let top_val_int = 5
let top_val_int_list : int list = []
let top_val_poly_list = []
let top_val_poly_list_pair = ([],[])
(********************************************************************)
(* ** Polymorphic functions *)
let top_fun_poly_id x =
x
let top_fun_poly_proj1 (x,y) =
x
let top_fun_poly_pair_homogeneous (x:'a) (y:'a) =
(x,y)
(********************************************************************)
(* ** Infix functions *)
let (+++) x y = x + y