Commit 121713ba authored by charguer's avatar charguer

stable ML example

parent 32db123c
Definition p := 0%nat.
Lemma test : forall p, p = 0 -> p = Top.p.
Proof using. intros p. intros. replace Top.p with p. auto. Qed.
coqc Test.v
File "./Test.v", line 5, characters 36-41:
Error: The reference Top.p was not found in the current environment.
......@@ -46,9 +46,9 @@ Inductive prim : Type :=
| prim_alloc : prim
| prim_get : prim
| prim_set : prim
| prim_op : (int -> int -> int) -> prim.
| prim_op : (int -> int -> int) -> prim
Inductive val : Type :=
with val : Type :=
| val_unit : val
| val_int : int -> val
| val_pair : val -> val -> val
......@@ -220,6 +220,9 @@ Ltac state_red_base tt ::=
(********************************************************************)
(* * Notations *)
Bind Scope trm_scope with trm.
Delimit Scope trm_scope with trm.
(** Core terms *)
Notation "'If_' x 'Then' F1 'Else' F2" :=
......@@ -248,7 +251,7 @@ Notation "'While' F1 'Do' F2 'Done_'" :=
: trm_scope.
(** Applications *)
(* LATER
Notation "'App' f x1 ;" :=
(trm_app f [x1])
(at level 68, f at level 0, x1 at level 0) : trm_scope.
......@@ -267,26 +270,27 @@ Notation "'App' f x1 x2 x3 x4 ;" :=
(trm_app f [x1; x2; x3; x4])
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0, x4 at level 0) : trm_scope.
*)
(** Functions *)
(** Recursive functions *)
Notation "'Fun' f [ x1 ] ':=' K" :=
Notation "'Fix' f [ x1 ] ':=' K" :=
(val_fix f (x1:nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 ] ':=' K" :=
Notation "'Fix' f [ x1 ] ':=' K" :=
(val_fix f (x1::nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 ] ':=' K" :=
Notation "'Fix' f [ x1 x2 ] ':=' K" :=
(val_fix f (x1::x2::nil) K)
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 ] ':=' K" :=
Notation "'Fix' f [ x1 x2 x3 ] ':=' K" :=
(val_fix f (x1::x2::x3::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 x4 ] ':=' K" :=
Notation "'Fix' f [ x1 x2 x3 x4 ] ':=' K" :=
(val_fix f (x1::x2::x3::x4::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident) : trm_scope.
......
......@@ -13,48 +13,8 @@ Open Scope heap_scope.
Ltac auto_star ::= jauto.
Tactic Notation "xunfold" "~" constr(E) := xunfold E; auto_tilde.
Tactic Notation "xunfold" "*" constr(E) := xunfold E; auto_star.
Tactic Notation "xunfold" constr(E) :=
change repr with repr';
let h := fresh "temp" in
set (h := repr');
repeat (
unfold h at 1;
let ok := match goal with
| |- context [ repr' (E) _ ] => constr:(true)
| |- context [ repr' (E _) _ ] => constr:(true)
| |- context [ repr' (E _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ repr' (E _ _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| _ => constr:(false)
end in
match ok with
| true => unfold repr'
| false => change repr' with repr
end);
clear h;
simpl E.
(*
unfold E;
try fold E.
*)
Global Opaque repr Record.
(********************************************************************)
(* * Nonlifted mutable lists *)
(* * Mutable lists *)
(** Layout in memory:
......@@ -63,9 +23,6 @@ Global Opaque repr Record.
*)
Module MList.
Definition hd : field := 0.
Definition tl : field := 1.
......@@ -142,9 +99,135 @@ Qed.
End Properties.
Implicit Arguments MList_null_keep [].
Implicit Arguments MList_cons [].
Implicit Arguments MList_uncons [].
Implicit Arguments MList_not_null [].
Implicit Arguments MList_not_null_keep [].
Global Opaque MList.
End MList.
(********************************************************************)
(* * Additional constructs, TODO: realize them *)
Parameter val_neq : val.
Parameter val_add : val.
Parameter rule_neq : forall p1 p2,
triple (trm_app val_neq [val_loc p1; val_loc p2])
\[]
(fun (r:val) => \[r = val_int (If (p1 <> p2) then 1 else 0)]).
Parameter rule_add : forall n1 n2,
triple (trm_app val_add [val_int n1; val_int n2])
\[]
(fun (r:val) => \[r = val_int (n1 + n2)]).
Parameter rule_get_hd : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> Record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> Record `{ hd := x; tl := p'}).
(********************************************************************)
(* * Mutable list increment verification *)
(** Program variables *)
Definition Mlist_length : var := 1%nat.
Definition P : var := 2%nat.
Definition Q : var := 3%nat.
Definition N : var := 6%nat.
(** Program code *)
Definition mlist_length : val :=
Fix Mlist_length [P] :=
If_ trm_app val_neq [val_var P; val_loc null] Then (
Let Q := prim_get [val_var P; val_field tl] in
Let N := trm_app (val_var Mlist_length) [val_var Q] in
trm_app val_add [val_var N; val_int 1]
) Else val_int 0.
(** Program specification and verification *)
Lemma mlist_incr_spec : forall L p,
triple (trm_app mlist_length [val_loc p])
(p ~> MList L)
(fun r => \[r = val_int (length L)] \* p ~> MList L).
Proof using.
intros L. induction_wf: list_sub_wf L.
intros p.
applys rule_app; try reflexivity.
skip_rewrite ( (* TODO: implement a substitution that computes *)
subst_trm (List.combine [Mlist_length; P] [mlist_length; val_loc p])
(If_ (val_neq [val_var P; val_loc null]%list) Then
Let Q := prim_get [val_var P; val_field tl] in
Let N := (val_var Mlist_length) [val_var Q]%list in
trm_app val_add [val_var N; val_int 1]
Else val_int 0)
=
If_ (val_neq [val_loc p; val_loc null]%list)
Then Let Q := prim_get [val_loc p; val_field tl] in
Let N := mlist_length [val_var Q]%list in
trm_app val_add [val_var N; val_int 1]
Else val_int 0).
applys rule_if. { xapplys rule_neq. }
intros c. xpull. intros C.
applys rule_if_val. subst c.
case_if as C1; case_if as C2; tryfalse.
{ subst p. xchange MList_null_keep.
xpull. intros EL. applys rule_val. hsimpl. subst~. }
{ xchange~ (MList_not_null p). xpull. intros x p' L' EL.
applys rule_let.
{ xapplys rule_get_hd. }
{ intros p''. xpull. intros E. subst p''.
skip_rewrite (* TODO: implement a substitution that computes *)
(subst_trm [(Q,val_loc p')] (Let N := mlist_length [val_var Q]%list in
trm_app val_add [val_var N; val_int 1])
= Let N := mlist_length [val_loc p']%list in
trm_app val_add [val_var N; val_int 1]).
applys rule_let.
{ xapplys IH. { subst~. } }
{ intros r. xpull. intros Er. xchange (MList_uncons p).
skip_rewrite (* TODO: implement a substitution that computes *)
(subst_trm [(N,r)] (trm_app val_add [val_var N; val_int 1])
= trm_app val_add [r; val_int 1]).
subst r. xapplys rule_add. subst. rew_length. fequals. math. } } }
Qed.
......
......@@ -388,6 +388,15 @@ Qed.
Implicit Arguments rule_extract_prop_from_extract_exists [T].
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(* TODO: move the remaining of this file to a different file *)
(*------------------------------------------------------------------*)
(* ** [rew_heap] tactic to normalize expressions with [hprop_star] *)
......@@ -631,17 +640,14 @@ Abort.
(*------------------------------------------------------------------*)
(* ** Tactic [hpull_check] tests whetherit would be useful
(* ** Tactic [hpull_check] tests whether it would be useful
to call [hpull] to extract things from the precondition.
- [hpull_check_himpl tt] for a goal of the form [H ==> H']
- [hpull_check_pre tt] for a goal of the form [F H Q].
*)
Applies to a goal of the form [H ==> H']. *)
(** Raises an error indicating the need to extract information *)
Ltac hpull_check_error tt :=
fail 100 "need to first call xpull.".
fail 100 "need to first call hpull or xpull.".
(** [hpull_check_rec H] raises an error if the heap predicate [H]
contains existentials or non-empty pure facts. *)
......@@ -668,11 +674,11 @@ Ltac hpull_check_rec H :=
| _ => idtac
end.
(** [hpull_check_himpl tt] applies to a goal of the form (H ==> H')
(** [hpull_check tt] applies to a goal of the form (H ==> H')
and raises an error if [H] contains extractible quantifiers
or facts *)
Ltac hpull_check_himpl tt :=
Ltac hpull_check tt :=
match goal with |- ?H ==> ?H' => hpull_check_rec H end.
(*-- Demo --*)
......@@ -680,20 +686,11 @@ Ltac hpull_check_himpl tt :=
Lemma hpull_check_demo_1 : forall H1 H3 H,
let H2 := Hexists (y:int), \[y = y] in
(H1 \* H2 \* H3) ==> H.
Proof using. intros. hpull_check_himpl tt. (* --> accepts *) Abort.
Proof using. intros. hpull_check tt. (* --> accepts *) Abort.
Lemma hpull_check_demo_2 : forall H1 H2 H3 H,
(H1 \* \[] \* (H2 \* Hexists (y:int), \[y = y]) \* H3) ==> H.
Proof using. intros. (* hpull_check_himpl tt. --> blocks *) Abort.
(** [hpull_check_pre tt] applies to a goal of the form (F H Q)
and raises an error if [H] contains extractible quantifiers
or facts *)
Ltac hpull_check_pre tt :=
let H := xprecondition tt in
hpull_check_rec H.
Proof using. intros. (* hpull_check tt. --> blocks *) Abort.
(*------------------------------------------------------------------*)
......@@ -1387,7 +1384,12 @@ Tactic Notation "xunfold" constr(E) :=
| false => change repr' with repr
end);
clear h;
unfold E.
simpl E.
(* TODO: was "unfold E", but this fails for recursive definitions. *)
Tactic Notation "xunfold" "~" constr(E) := xunfold E; auto_tilde.
Tactic Notation "xunfold" "*" constr(E) := xunfold E; auto_star.
(** [xunfold E] unfolds a specific occurence of the representation
predicate [E]. TODO: still needs to unfold [E] by hand. *)
......@@ -1678,6 +1680,16 @@ Tactic Notation "xlocal" :=
xlocal_core tt.
(*------------------------------------------------------------------*)
(* ** Tactic [xpull_check] tests whether it would be useful
to call [xpull] to extract things from the precondition.
Applies to a goal of the form [F H Q]. *)
Ltac xpull_check tt :=
let H := xprecondition tt in
hpull_check_rec H.
(*------------------------------------------------------------------*)
(* ** Tactic [xpull] to extract existentials and pure facts from
pre-conditions. *)
......@@ -1724,6 +1736,8 @@ Proof using.
Qed.
Ltac xpull_setup tt :=
try match goal with |- ?H ==> ?H' =>
fail 100 "you should call hpull, not xpull" end;
pose ltac_mark;
apply xpull_start; [ try xlocal | ].
......@@ -1781,11 +1795,11 @@ Ltac xapply_core H cont1 cont2 :=
end).
Ltac xapply_base H :=
hpull_check_pre tt;
xpull_check tt;
xapply_core H ltac:(fun tt => idtac) ltac:(fun tt => idtac).
Ltac xapplys_base H :=
hpull_check_pre tt;
xpull_check tt;
xapply_core H ltac:(fun tt => hcancel) ltac:(fun tt => hsimpl).
Tactic Notation "xapply" constr(H) :=
......@@ -1803,10 +1817,103 @@ Tactic Notation "xapplys" "*" constr(H) :=
xapplys H; auto_star.
(*--------------------------------------------------------*)
(* ** [xchange] *)
(** [xchange E] applies to a goal of the form [F H Q]
and to a lemma [E] of type [H1 ==> H2] or [H1 = H2].
It replaces the goal with [F H' Q], where [H']
is computed by replacing [H1] with [H2] in [H].
The substraction is computed by solving [H ==> H1 \* ?H']
with [hsimpl]. If you need to solve this implication by hand,
use [xchange_no_simpl E] instead.
[xchange <- E] is useful when [E] has type [H2 = H1]
instead of [H1 = H2].
[xchange_show E] is useful to visualize the instantiation
of the lemma used to implement [xchange].
*)
(* Lemma used by [xchange] *)
Lemma xchange_lemma : forall H1 H1' H2 B H Q (F:~~B),
is_local F ->
(H1 ==> H1') ->
(H ==> H1 \* H2) ->
F (H1' \* H2) Q ->
F H Q.
Proof using.
introv W1 L W2 M. applys local_frame __ \[]; eauto.
hsimpl. hchange~ W2. hsimpl~. rew_heap~.
Qed.
Ltac xchange_apply L cont :=
eapply xchange_lemma;
[ try xlocal | applys L | cont tt | (*xtag_pre_post*) ].
(* Note: the term modif should be either himpl_proj1 or himpl_proj2 *)
Ltac xchange_forwards L modif cont :=
forwards_nounfold_then L ltac:(fun K =>
match modif with
| __ =>
match type of K with
| _ = _ => xchange_apply (@himpl_proj1 _ _ _ K) cont
| _ => xchange_apply K cont
end
| _ => xchange_apply (@modif _ _ _ K) cont
end).
Ltac xchange_with_core cont H H' :=
eapply xchange_lemma with (H1:=H) (H1':=H');
[ try xlocal | | cont tt | (* xtag_pre_post*) ].
Ltac xchange_core cont E modif :=
match E with
| ?H ==> ?H' => xchange_with_core cont H H'
| _ => xchange_forwards E modif ltac:(fun _ => instantiate; cont tt)
end.
Ltac xchange_base cont E modif :=
xpull_check tt;
match goal with
| |- _ ==> _ => hchange_base E modif
| |- _ ===> _ => hchange_base E modif
| _ => xchange_core cont E modif
end.
Tactic Notation "xchange" constr(E) :=
xchange_base ltac:(fun tt => hsimpl) E __.
Tactic Notation "xchange" "~" constr(E) :=
xchange E; auto_tilde.
Tactic Notation "xchange" "*" constr(E) :=
xchange E; auto_star.
Tactic Notation "xchange" "<-" constr(E) :=
xchange_base ltac:(fun tt => hsimpl) E himpl_proj2.
Tactic Notation "xchange" "~" "<-" constr(E) :=
xchange <- E; auto_tilde.
Tactic Notation "xchange" "*" "<-" constr(E) :=
xchange <- E; auto_star.
Tactic Notation "xchange_no_simpl" constr(E) :=
xchange_base ltac:(idcont) E __.
Tactic Notation "xchange_no_simpl" "<-" constr(E) :=
xchange_base ltac:(idcont) E himpl_proj2.
Tactic Notation "xchange_show" constr(E) :=
xchange_forwards E __ ltac:(idcont).
Tactic Notation "xchange_show" "<-" constr(E) :=
xchange_forwards himpl_proj2 ltac:(idcont).
(*------------------------------------------------------------------*)
Global Opaque repr.
End SepLogicSetup.
......
This diff is collapsed.
......@@ -238,6 +238,7 @@ Fixpoint Record (L:record_descr) (r:loc) : hprop :=
| (f, v)::L' => (r `.` f ~> v) \* (r ~> Record L')
end.
Global Opaque Record.
(********************************************************************)
......@@ -500,6 +501,8 @@ End RulesPrimitiveOps.
(*------------------------------------------------------------------*)
(* ** Derived big-step specifications for get and set on records *)
(* TODO: update
Definition field_eq_dec := Z.eq_dec.
Fixpoint record_get_compute_dyn (f:field) (L:record_descr) : option val :=
......@@ -524,7 +527,7 @@ Lemma record_get_compute_spec_correct : forall f L (P:Prop),
record_get_compute_spec f L = Some P -> P.
Proof using.
Admitted.
(* TODO: update
(*
introv M. unfolds record_get_compute_spec.
sets_eq <- do E: (record_get_compute_dyn f L).
destruct do as [[T v]|]; inverts M.
......@@ -625,6 +628,9 @@ Ltac xspec_record_set_compute tt :=
*)
(********************************************************************)
(* * Bonus *)
......@@ -647,6 +653,11 @@ Proof using.
rewrite (hprop_star_comm_assoc \GC H'). hsimpl. }
Qed.
(** Make [xlocal] aware that triples are local *)
Ltac xlocal_core tt ::=
try first [ assumption | applys is_local_triple ].
(*------------------------------------------------------------------*)
(* ** Practical notation for triples *)
......
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