Commit 8c4b2deb authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Notations: use `` instead of ` for enc, in order to avoid compatibility with...

Notations: use `` instead of ` for enc, in order to avoid compatibility with proj1_sig notation defined in Coq's Program.Util.
parent af3458d2
......@@ -26,7 +26,7 @@ Implicit Types n : int.
(** [val_swap] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_swap_neq : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} (v:A1) (w:A2) p q,
Triple (val_swap `p `q)
Triple (val_swap ``p ``q)
PRE (p ~~> v \* q ~~> w)
POST (fun (r:unit) => p ~~> w \* q ~~> v).
Proof using.
......@@ -34,7 +34,7 @@ Proof using.
Qed.
Lemma Rule_swap_eq : forall A1 `{EA1:Enc A1} (v:A1) p,
Triple (val_swap `p `p)
Triple (val_swap ``p ``p)
PRE (p ~~> v)
POST (fun (r:unit) => p ~~> v).
Proof using.
......
......@@ -25,8 +25,8 @@ Definition val_apply : val :=
Lemma Rule_apply : forall (f:func) `{EA:Enc A} (x:A),
forall (H:hprop) `{EB:Enc B} (Q:B->hprop),
Triple (f `x) H Q ->
Triple (val_apply `f `x) H Q.
Triple (f ``x) H Q ->
Triple (val_apply ``f ``x) H Q.
Proof using.
introv M. xcf. (* todo why not simplified? *)
unfold Substs; simpl; rew_enc_dyn.
......@@ -35,8 +35,8 @@ Qed.
Lemma Rule_apply' : forall (f:func) `{EA:Enc A} (x:A),
forall (H:hprop) `{EB:Enc B} (Q:B->hprop),
Triple (val_apply f `x)
PRE (\[Triple (f `x) H Q] \* H)
Triple (val_apply f ``x)
PRE (\[Triple (f ``x) H Q] \* H)
POST Q.
Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed.
......@@ -53,11 +53,11 @@ Definition val_refapply : val :=
Lemma Rule_refapply_pure : forall (f:func) `{EA:Enc A} (r:loc) (x:A),
forall `{EB:Enc B} (P:A->B->Prop),
Triple (f `x)
Triple (f ``x)
PRE \[]
POST (fun y => \[P x y])
->
Triple (val_refapply `f `r)
Triple (val_refapply ``f ``r)
PRE (r ~~> x)
POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y).
Proof using.
......@@ -66,11 +66,11 @@ Qed.
Lemma Rule_refapply_effect : forall (f:func) `{EA:Enc A} (r:loc) (x:A),
forall `{EB:Enc B} (P:A->B->Prop) (H H':hprop),
Triple (f `x)
Triple (f ``x)
PRE H
POST (fun y => \[P x y] \* H')
->
Triple (val_refapply `f `r)
Triple (val_refapply ``f ``r)
PRE (r ~~> x \* H)
POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y \* H').
Proof using.
......@@ -88,9 +88,9 @@ Definition val_twice : val :=
'f '().
Lemma Rule_twice : forall (f:func) (H H':hprop) `{EB:Enc B} (Q:B->hprop),
Triple (f `tt) H (fun (_:unit) => H') ->
Triple (f `tt) H' Q ->
Triple (val_twice `f) H Q.
Triple (f ``tt) H (fun (_:unit) => H') ->
Triple (f ``tt) H' Q ->
Triple (val_twice ``f) H Q.
Proof using.
introv M1 M2. xcf. xseq. xapp M1. xapp M2. hsimpl~.
Qed.
......@@ -127,16 +127,16 @@ Proof using. math. Qed.
Lemma Rule_repeat : forall (I:int->hprop) (f:func) (n:int),
n >= 0 ->
(forall i, 0 <= i < n ->
Triple (f `tt)
Triple (f ``tt)
PRE (I i)
POST (fun (_:unit) => I (i+1)))
->
Triple (val_repeat `n `f)
Triple (val_repeat ``n ``f)
PRE (I 0)
POST (fun (_:unit) => I n).
Proof using.
introv N M. xcf.
asserts_rewrite (`n = val_int n). auto. (* todo: investigate *)
asserts_rewrite (``n = val_int n). auto. (* todo: investigate *)
applys local_weaken_post. xlocal.
applys local_erase. applys xfor_inv_lemma (fun i => (I (i-1))).
{ math. }
......@@ -195,7 +195,7 @@ Definition val_mkcounter : val :=
(** Verification *)
Lemma Rule_mkcounter :
Triple (val_mkcounter `val_unit)
Triple (val_mkcounter ``val_unit)
\[]
(fun g => g ~> MCount 0).
Proof using.
......
......@@ -216,7 +216,7 @@ Definition val_new_cell :=
*)
Lemma Rule_new_cell : forall `{EA:Enc A} (x:A) (q:loc),
Triple (val_new_cell `x `q)
Triple (val_new_cell ``x ``q)
PRE \[]
POST (fun p => (p ~> MCell x q)).
Proof using. xrule_new_record. Qed.
......@@ -296,7 +296,7 @@ Definition val_mlist_copy :=
).
Lemma Rule_mlist_copy : forall p (L:list int),
Triple (val_mlist_copy `p)
Triple (val_mlist_copy ``p)
PRE (p ~> MList L)
POST (fun (p':loc) => (p ~> MList L) \* (p' ~> MList L)).
Proof using.
......@@ -328,7 +328,7 @@ Definition val_mlist_length : val :=
).
Lemma Rule_mlist_length : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length `p)
Triple (val_mlist_length ``p)
PRE (p ~> MList L)
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
......@@ -356,7 +356,7 @@ Definition val_mlist_append : val :=
).
Lemma Rule_mlist_append : forall (L1 L2:list int) (p1 p2:loc),
Triple (val_mlist_append `p1 `p2)
Triple (val_mlist_append ``p1 ``p2)
PRE (p1 ~> MList L1 \* p2 ~> MList L2)
POST (fun (p:loc) =>
p ~> MList (L1++L2) \* p1 ~> MList L1 \* p2 ~> MList L2).
......@@ -376,13 +376,13 @@ Qed.
(* * Out-of-place append of two aliased mutable lists *)
Lemma Rule_mlist_append_aliased : forall (L:list int) (p1:loc),
Triple (val_mlist_append `p1 `p1)
Triple (val_mlist_append ``p1 ``p1)
PRE (p1 ~> MList L)
POST (fun (p:loc) => p ~> MList (L++L) \* p1 ~> MList L).
Proof using.
cuts K: (forall (L L1 L2:list int) (p1 p3:loc),
L = L1++L2 ->
Triple (val_mlist_append `p3 `p1)
Triple (val_mlist_append ``p3 ``p1)
PRE (p1 ~> MListSeg p3 L1 \* p3 ~> MList L2)
POST (fun (p:loc) => p ~> MList (L2++L) \* p1 ~> MList L)).
{ intros. xchange (MListSeg_nil p1). xapplys (K L nil L). rew_list~. }
......@@ -416,17 +416,17 @@ Definition val_mlist_iter : val :=
Lemma Rule_mlist_iter : forall `{EA:Enc A} (I:list A->hprop) (L:list A) (f:func) (p:loc),
(forall x K,
Triple (f `x)
Triple (f ``x)
PRE (I K)
POST (fun (_:unit) => I (K&x)))
->
Triple (val_mlist_iter `f `p)
Triple (val_mlist_iter ``f ``p)
PRE (p ~> MList L \* I nil)
POST (fun (_:unit) => p ~> MList L \* I L).
Proof using.
introv M.
cuts G: (forall L1 L2,
Triple (val_mlist_iter `f `p)
Triple (val_mlist_iter ``f ``p)
PRE (p ~> MList L2 \* I L1)
POST (fun (_:unit) => p ~> MList L2 \* I (L1++L2))).
{ applys G. }
......@@ -442,17 +442,17 @@ Qed.
Lemma Rule_mlist_iter_general : forall `{EA:Enc A} (I:list A->hprop) (L:list A) (f:func) (p:loc),
(forall x L1 L2, L = L1++x::L2 ->
Triple (f `x)
Triple (f ``x)
PRE (I L1)
POST (fun (_:unit) => I (L1&x)))
->
Triple (val_mlist_iter `f `p)
Triple (val_mlist_iter ``f ``p)
PRE (p ~> MList L \* I nil)
POST (fun (_:unit) => p ~> MList L \* I L).
Proof using.
introv M.
cuts G: (forall L1 L2, L = L1++L2 ->
Triple (val_mlist_iter `f `p)
Triple (val_mlist_iter ``f ``p)
PRE (p ~> MList L2 \* I L1)
POST (fun (_:unit) => p ~> MList L2 \* I L)).
{ applys~ G. }
......@@ -478,7 +478,7 @@ Definition val_mlist_length_using_iter : val :=
val_get 'r.
Lemma Rule_mlist_length_using_iter : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length_using_iter `p)
Triple (val_mlist_length_using_iter ``p)
PRE (p ~> MList L)
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
......@@ -509,7 +509,7 @@ Definition val_mlist_length_loop : val :=
val_get 'n.
Lemma Rule_mlist_length_loop : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length_loop `p)
Triple (val_mlist_length_loop ``p)
PRE (p ~> MList L)
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
......@@ -550,7 +550,7 @@ Definition val_mlist_incr : val :=
) End.
Lemma Rule_mlist_incr : forall (L:list int) (p:loc),
Triple (val_mlist_incr `p)
Triple (val_mlist_incr ``p)
PRE (p ~> MList L)
POST (fun (r:unit) => p ~> MList (LibList.map (fun x => x+1) L)).
Proof using.
......@@ -582,7 +582,7 @@ Definition val_mlist_in_place_rev : val :=
val_get 's.
Lemma Rule_mlist_in_place_rev : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_in_place_rev `p)
Triple (val_mlist_in_place_rev ``p)
PRE (p ~> MList L)
POST (fun (p':loc) => p' ~> MList (rev L)).
Proof using.
......@@ -623,10 +623,10 @@ Definition val_mlist_cps_append : val :=
Lemma Rule_mlist_cps_append : forall A `{EA:Enc A} (L M:list A) (p q:loc) (k:func),
forall `{EB: Enc B} (H:hprop) (Q:B->hprop),
(forall (r:loc), Triple (k `r)
(forall (r:loc), Triple (k ``r)
PRE (r ~> MList (L ++ M) \* H)
POST Q) ->
Triple (val_mlist_cps_append `p `q `k)
Triple (val_mlist_cps_append ``p ``q ``k)
PRE (p ~> MList L \* q ~> MList M \* H)
POST Q.
Proof using.
......@@ -644,7 +644,7 @@ Proof using.
Qed.
(* Note that K' could be given the following spec, rather than inlining its code:
Triple (k' `r)
Triple (k' ``r)
PRE (p ~~> (x,p') \* r ~> Mlist (L'++M) \* H)
POST Q.
*)
......
......@@ -188,7 +188,7 @@ Definition val_new_node :=
*)
Lemma Rule_new_node : forall x p1 p2,
Triple (val_new_node `x `p1 `p2)
Triple (val_new_node ``x ``p1 ``p2)
PRE \[]
POST (fun p => (p ~> Cell x p1 p2)).
Proof using. xrule_new_record. Qed.
......@@ -213,7 +213,7 @@ Definition val_tree_copy :=
Hint Constructors tree_sub.
Lemma Rule_tree_copy : forall p T,
Triple (val_tree_copy `p)
Triple (val_tree_copy ``p)
PRE (p ~> MTree T)
POST (fun (p':loc) => (p ~> MTree T) \* (p' ~> MTree T)).
Proof using.
......@@ -277,7 +277,7 @@ Qed.
(* ** Copy of a complete binary tree *)
Lemma Rule_tree_copy_complete : forall p T,
Triple (val_tree_copy `p)
Triple (val_tree_copy ``p)
PRE (p ~> MTreeComplete T)
POST (fun (p':loc) => (p ~> MTreeComplete T) \* (p' ~> MTreeComplete T)).
Proof using.
......
......@@ -770,7 +770,7 @@ Additional heap predicates:
- r ~> S notation for [S r]
Specification syntax:
- [Triple (f `x `y) PRE H POST (fun (r:typ) => H')]
- [Triple (f ``x ``y) PRE H POST (fun (r:typ) => H')]
Tactic for representation predicates [x ~> R X]:
- [xunfold R]
......@@ -798,7 +798,7 @@ Additional relevant files:
(** Demo: verification of [incr] *)
Lemma Rule_incr : forall (p:loc) (n:int),
Triple (val_incr `p)
Triple (val_incr ``p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n+1)).
Proof using.
......@@ -812,7 +812,7 @@ Hint Extern 1 (Register_Spec val_incr) => Provide Rule_incr.
(** Exercise: [incr2] *)
Lemma Rule_incr2 : forall (p:loc) (n:int),
Triple (Basic.val_incr_twice `p)
Triple (Basic.val_incr_twice ``p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n+2)).
Proof using.
......@@ -979,7 +979,7 @@ Definition val_mlist_length : val :=
).
Lemma Rule_mlist_length : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length `p)
Triple (val_mlist_length ``p)
PRE (p ~> MList L)
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
......@@ -996,7 +996,7 @@ Qed.
Definition val_new_cell : val := val_new_record 2%nat.
Lemma Rule_new_cell : forall `{EA:Enc A} (x:A) (q:loc),
Triple (val_new_cell `x `q)
Triple (val_new_cell ``x ``q)
PRE \[]
POST (fun p => (p ~> Record`{ hd := x; tl := q })).
Proof using. xrule_new_record. Qed.
......@@ -1019,7 +1019,7 @@ Definition val_mlist_copy :=
).
Lemma Rule_mlist_copy : forall p (L:list int),
Triple (val_mlist_copy `p)
Triple (val_mlist_copy ``p)
PRE (p ~> MList L)
POST (fun (p':loc) => (p ~> MList L) \* (p' ~> MList L)).
Proof using.
......
......@@ -1095,7 +1095,7 @@ Proof using.
Abort.
Lemma rule_neq_3'' : forall (v1 v2:int),
Spec val_neq `[ v1, v2 ]
Spec val_neq ``[ v1, v2 ]
\[]
(fun (r:int) => \[r = (If v1 = v2 then 0 else 1)]).
Proof using.
......@@ -1106,7 +1106,7 @@ Proof using.
Abort.
Lemma rule_neq_3'' : forall (v1 v2:int),
App val_neq '[ `v1, `v2 ]
App val_neq '[ ``v1, ``v2 ]
\[]
(fun (r:int) => \[r = (If v1 = v2 then 0 else 1)]).
Proof using.
......@@ -1122,7 +1122,7 @@ Abort.
(* DEPRECATED
Lemma Rule_eq_int : forall (v1 v2 : int),
Spec val_eq `[v1, v2]
Spec val_eq ``[v1, v2]
\[]
(fun (b:bool) => \[b = isTrue (v1 = v2 :> int)]).
Proof using.
......@@ -1139,7 +1139,7 @@ Hint Extern 1 (RegisterSpec (val_prim val_eq)) =>
(* ---------------------------------------------------------------------- *)
(*
Notation "` V" := (enc V) (at level 8, format "` V").
Notation "`` V" := (enc V) (at level 8, format "`` V").
*)
......@@ -1294,19 +1294,19 @@ Section SpecBasic.
Transparent trm_apps apps. (* TODO: fix *)
Lemma Spec_ref : forall A `{EA:Enc A} (v:A),
Spec val_ref `[v]
Spec val_ref ``[v]
\[]
(fun (l:loc) => l ~~~> v).
Proof using. intros. applys~ @Rule_ref. Qed.
Lemma Spec_get : forall A `{EA:Enc A} (v:A) l,
Spec val_get `[l]
Spec val_get ``[l]
(l ~~~> v)
(fun (x:A) => \[x = v] \* (l ~~~> v)).
Proof using. intros. applys~ Rule_get. Qed.
Lemma Spec_set : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} l (v:A1) (w:A2),
Spec val_set `[l,w]
Spec val_set ``[l,w]
(l ~~~> v)
(fun (_:unit) => l ~~~> w).
Proof using. intros. applys~ Rule_set. Qed.
......@@ -1891,21 +1891,21 @@ Proof using. auto. Qed.
(* DEPRECATED
Notation "`[ x1 ]" :=
Notation "``[ x1 ]" :=
((Dyn x1)::nil)
(at level 0, format "`[ x1 ]")
(at level 0, format "``[ x1 ]")
: dyns.
Notation "``[ x1 , x2 ]" :=
Notation "```[ x1 , x2 ]" :=
((Dyn x1)::(Dyn x2)::nil)
(at level 0, format "`[ x1 , x2 ]")
(at level 0, format "``[ x1 , x2 ]")
: dyns.
Notation "``[ x1 , x2 , x3 ]" :=
Notation "```[ x1 , x2 , x3 ]" :=
((Dyn x1)::(Dyn x2)::(Dyn x3)::nil)
(at level 0, format "`[ x1 , x2 , x3 ]")
(at level 0, format "``[ x1 , x2 , x3 ]")
: dyns.
Notation "``[ x1 , x2 , x3 , x4 ]" :=
Notation "```[ x1 , x2 , x3 , x4 ]" :=
((Dyn x1)::(Dyn x2)::(Dyn x3)::(Dyn x4)::nil)
(at level 0, format "`[ x1 , x2 , x3 , x4 ]")
(at level 0, format "``[ x1 , x2 , x3 , x4 ]")
: dyns.
*)
......@@ -1913,21 +1913,21 @@ Notation "``[ x1 , x2 , x3 , x4 ]" :=
(* annotated
Notation "`[ ]" := ((@nil dyn) : dyns) (format "`[ ]") : dyns_scope.
Notation "``[ ]" := ((@nil dyn) : dyns) (format "``[ ]") : dyns_scope.
Notation "`[ x ]" := ((cons (Dyn x) nil) : dyns) : dyns_scope.
Notation "``[ x ]" := ((cons (Dyn x) nil) : dyns) : dyns_scope.
Notation "`[ x1 , x2 ]" :=
Notation "``[ x1 , x2 ]" :=
(((Dyn x1)::(Dyn x2)::nil) : dyns)
(at level 0, format "`[ x1 , x2 ]")
(at level 0, format "``[ x1 , x2 ]")
: dyns_scope.
Notation "`[ x1 , x2 , x3 ]" :=
Notation "``[ x1 , x2 , x3 ]" :=
(((Dyn x1)::(Dyn x2)::(Dyn x3)::nil) : dyns)
(at level 0, format "`[ x1 , x2 , x3 ]")
(at level 0, format "``[ x1 , x2 , x3 ]")
: dyns_scope.
Notation "`[ x1 , x2 , x3 , x4 ]" :=
Notation "``[ x1 , x2 , x3 , x4 ]" :=
(((Dyn x1)::(Dyn x2)::(Dyn x3)::(Dyn x4)::nil) : dyns)
(at level 0, format "`[ x1 , x2 , x3 , x4 ]")
(at level 0, format "``[ x1 , x2 , x3 , x4 ]")
: dyns_scope.
*)
......@@ -2009,7 +2009,7 @@ Qed.
(*
Lemma Spec_eq_int : forall (v1 v2 : int),
Spec val_eq `[v1, v2]
Spec val_eq ``[v1, v2]
\[]
(fun (b:bool) => \[b = isTrue (v1 = v2 :> int)]).
Proof using.
......@@ -2283,22 +2283,22 @@ Definition Apps (f:val) (Vs:dyns) :=
(* ** Specification of primitive operations *)
Lemma Spec_ref : forall A `{EA:Enc A} (v:A),
App val_ref `[v] \[] (fun (l:loc) => l ~~~> v).
App val_ref ``[v] \[] (fun (l:loc) => l ~~~> v).
Proof using. intros. applys~ Rule_ref. Qed.
Lemma app_get : forall A `{EA:Enc A} (v:A) l,
App val_get `[l] (l ~~~> v) (fun (x:A) => \[x = v] \* (l ~~~> v)).
App val_get ``[l] (l ~~~> v) (fun (x:A) => \[x = v] \* (l ~~~> v)).
Proof using. intros. applys~ Rule_get. Qed.
Lemma app_set : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} l (v:A1) (w:A2),
App val_set `[l,w] (l ~~~> v) (fun (_:unit) => l ~~~> w).
App val_set ``[l,w] (l ~~~> v) (fun (_:unit) => l ~~~> w).
Proof using. intros. applys~ Rule_set. Qed.
*)
(*
Lemma Spec_get' : forall A `{EA:id Enc A} (v:A) l,
@Spec val_get `[l] A EA
@Spec val_get ``[l] A EA
(@Hsingle A EA l v)
(fun (x:A) => \[x = v] \* (@Hsingle A EA l v)).
Proof using. intros. applys~ Spec_get. Qed.
......
......@@ -44,7 +44,7 @@ Definition func := val.
Class Enc (A:Type) :=
make_Enc { enc : A -> val }.
Notation "` V" := (enc V) (at level 8, format "` V").
Notation "`` V" := (enc V) (at level 8, format "`` V").
(* TEMPORARY: this is patch of a TLC tactic to prevent undesired
......@@ -60,11 +60,11 @@ Ltac app_evar t A cont ::=
(** Notation for lists of encoded values *)
Notation "`[ ]" :=
(@nil val) (format "`[ ]") : enc_scope.
Notation "`[ x ]" :=
Notation "``[ ]" :=
(@nil val) (format "``[ ]") : enc_scope.
Notation "``[ x ]" :=
(cons (enc x) nil) : enc_scope.
Notation "`[ x , y , .. , z ]" :=
Notation "``[ x , y , .. , z ]" :=
(cons (enc x) (cons (enc y) .. (cons (enc z) nil) ..)) : enc_scope.
Open Scope enc_scope.
......@@ -251,11 +251,11 @@ Hint Resolve Enc_injective_loc Enc_injective_unit Enc_injective_bool
Definition dyns := list dyn.
(** Notation for lists of dynamic values *)
Notation "`[ ]" :=
(@nil dyn) (format "`[ ]") : dyns_scope.
Notation "`[ x ]" :=
Notation "``[ ]" :=
(@nil dyn) (format "``[ ]") : dyns_scope.
Notation "``[ x ]" :=
(cons (Dyn x) nil) : dyns_scope.
Notation "`[ x , y , .. , z ]" :=
Notation "``[ x , y , .. , z ]" :=
(cons (Dyn x) (cons (Dyn y) .. (cons (Dyn z) nil) ..)) : dyns_scope.
Open Scope dyns_scope.
......@@ -646,13 +646,13 @@ Section RulesStateOps.
Transparent Hsingle.
Lemma Rule_ref : forall A `{EA:Enc A} (V:A),
Triple (val_ref `V)
Triple (val_ref ``V)
\[]
(fun l => l ~~> V).
Proof using. intros. applys_eq rule_ref 1. subst~. Qed.
Lemma Rule_get : forall A `{EA:Enc A} (V:A) l,
Triple (val_get `l)
Triple (val_get ``l)
(l ~~> V)
(fun x => \[x = V] \* (l ~~> V)).
Proof using.
......@@ -660,7 +660,7 @@ Proof using.
Qed.
Lemma Rule_set' : forall v1 A2 `{EA2:Enc A2} (V2:A2) l,
Triple (val_set `l `V2)
Triple (val_set ``l ``V2)
(l ~~> v1)
(fun u => l ~~> V2).
Proof using.
......@@ -669,7 +669,7 @@ Proof using.
Qed.
Lemma Rule_set : forall A1 A2 `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l,
Triple (val_set l `V2)
Triple (val_set l ``V2)
(l ~~> V1)
(fun u => l ~~> V2).
Proof using. intros. applys~ Rule_set'. Qed.
......@@ -703,7 +703,7 @@ Proof using. intros. unfold Triple, Post. xapplys~ rule_eq. Qed.
Lemma Rule_eq : forall `{EA:Enc A},
Enc_injective EA ->
forall (v1 v2 : A),
Triple (val_eq `v1 `v2)
Triple (val_eq ``v1 ``v2)
\[]
(fun (b:bool) => \[b = isTrue (v1 = v2)]).
Proof using.
......
......@@ -102,7 +102,7 @@ Qed.
(* ** Increment *)
Lemma Rule_incr : forall (p:loc) (n:int),
Triple (val_incr `p)
Triple (val_incr ``p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n+1)).
Proof using.
......@@ -118,7 +118,7 @@ Hint Extern 1 (Register_Spec val_incr) => Provide Rule_incr.
(** [val_decr] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_decr : forall (p:loc) (n:int),
Triple (val_decr `p)
Triple (val_decr ``p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n-1)).
Proof using.
......@@ -148,7 +148,7 @@ Hint Extern 1 (Register_Spec val_not) => Provide Rule_not.
Lemma Rule_neq : forall `{EA:Enc A} (v1 v2:A),
Enc_injective EA ->
Triple (val_neq `v1 `v2)
Triple (val_neq ``v1 ``v2)
PRE \[]
POST (fun (b:bool) => \[b = isTrue (v1 <> v2)]).
Proof using.
......@@ -199,7 +199,7 @@ Proof using. auto. Qed.
Lemma Record_cons : forall p x (V:dyn) L,
(p ~> Record ((x, V)::L)) =
(p`.`x ~~> (`V) \* p ~> Record L).
(p`.`x ~~> ``V \* p ~> Record L).
Proof using. intros. destruct~ V. Qed.
Lemma Record_not_null : forall (r:loc) (L:Record_fields),
......@@ -254,7 +254,7 @@ Proof using.
Qed.
Lemma Rule_set_field : forall `{EA1:Enc A1} (V1:A1) (l:loc) f `{EA2:Enc A2} (V2:A2),
Triple ((val_set_field f) l `V2)
Triple ((val_set_field f) l ``V2)
PRE (l `.` f ~~> V1)
POST (fun (r:unit) => l `.` f ~~> V2).
Proof using.
......@@ -283,7 +283,7 @@ Definition record_get_compute_spec (f:field) (L:Record_fields) : option Prop :=
match record_get_compute_dyn f L with
| None => None
| Some (Dyn V) => Some (forall r,
Triple (val_get_field f `r) (r ~> Record L) (fun x => \[x = V] \* r ~> Record L))
Triple (val_get_field f ``r) (r ~> Record L) (fun x => \[x = V] \* r ~> Record L))
end.
Lemma record_get_compute_spec_correct : forall (f:field) L (P:Prop),
......@@ -316,7 +316,7 @@ Definition record_set_compute_spec (f:field) `{EA:Enc A} (W:A) (L:Record_fields)
match record_set_compute_dyn f (Dyn W) L with
| None => None
| Some L' => Some (forall r,
Triple (val_set_field f `r `W) (r ~> Record L) (fun (_:unit) => r ~> Record L'))
Triple (val_set_field f ``r ``W) (r ~> Record L) (fun (_:unit) => r ~> Record L'))
end.
Lemma record_set_compute_spec_correct : forall (f:field) `{EA:Enc A} (W:A) L (P:Prop),
......@@ -454,7 +454,7 @@ Definition val_new_record_2 :=
'p.
Lemma Rule_new_record_2 : forall `{EA1:Enc A1} `{EA2:Enc A2} (v1:A1) (v2:A2),
Triple (val_new_record_2 `v1 `v2)
Triple (val_new_record_2 ``v1 ``v2)
PRE \[]
POST (fun p => p ~> Record`{ 0%nat := v1 ; 1%nat := v2 }).
Proof using.
......@@ -504,12 +504,12 @@ Proof using.
= val_set_field f N (enc V)).
{ unfold Subst. simpl. case_if. case_if~. }
rewrite~ Substs_seq.
asserts_rewrite (Substs xs' Vs' (val_set_field f N `V)
= (val_set_field f N `V)).
asserts_rewrite (Substs xs' Vs' (val_set_field f N ``V)
= (val_set_field f N ``V)).
{ do 2 rewrite~ Substs_app. do 2 rewrite~ Substs_val. rewrite~ Substs_var_neq.
{ rewrite Exs'. applys var_fresh_var_seq_ge. math. } }
rewrite~ Subst_seq.
asserts_rewrite (Subst N (Dyn p) (val_set_field f N `V) = val_set_field f p `V).
asserts_rewrite (Subst N (Dyn p) (val_set_field f N ``V) = val_set_field f p ``V).
{ unfold Subst; simpl. case_if~. } (* todo: lemma Subst_var *)
fequals.
match goal with |- context [Subst x V ?t'] => set (t:=t') end.
......@@ -681,7 +681,7 @@ Global Opaque Array.
Lemma Rule_alloc_array : forall n,
n >= 0 ->
Triple (val_alloc `n)
Triple (val_alloc ``n)
PRE \[]
POST (fun p => Hexists (L:list val), \[length L = n :> int] \* p ~> Array L).
Proof using.
......@@ -702,7 +702,7 @@ Hint Resolve index_map.
Lemma Rule_array_get : forall p i L,
index L i ->
Triple (val_array_get `p `i)
Triple (val_array_get ``p ``i)
PRE (p ~> Array L)
POST (fun (r:A) => \[r = L[i]] \* p ~> Array L).
Proof using.
......@@ -716,7 +716,7 @@ Hint Extern 1 (Register_Spec val_array_get) => Provide Rule_array_get.
Lemma Rule_array_set : forall p i v L,
index L i ->
Triple (val_array_set `p `i `v)
Triple (val_array_set ``p ``i ``v)
PRE (p ~> Array L)
POST (fun (_:unit) => p ~> Array (L[i:=v])).
Proof using.
......@@ -730,7 +730,7 @@ Hint Extern 1 (Register_Spec val_array_set) => Provide Rule_array_set.
Lemma Rule_array_make : forall n v,
n >= 0 ->
Triple (val_array_make `n `v)
Triple (val_array_make ``n ``v)
PRE \[]
POST (fun p => Hexists L, \[L = make n v] \* p ~> Array L).
Proof using.
......
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