Commit e8de79e4 authored by charguer's avatar charguer

vars

parent 274c256e
......@@ -36,9 +36,9 @@ Definition Formula := forall `{Enc A}, hprop -> (A -> hprop) -> Prop.
Global Instance Inhab_Formula : Inhab Formula.
Proof using. apply (Inhab_of_val (fun _ _ _ _ => True)). Qed.
Notation "' F H Q" := ((F:Formula) _ _ H Q)
Notation "^ F H Q" := ((F:Formula) _ _ H Q)
(at level 65, F at level 0, H at level 0, Q at level 0,
format "' F H Q") : charac.
format "^ F H Q") : charac.
(** Constructor to force the return type of a Formula *)
Definition Formula_typed `{Enc A1} (F : hprop->(A1->hprop)->Prop) : Formula :=
......@@ -85,23 +85,23 @@ Definition Cf_val (v:val) : Formula :=
Definition Cf_if_val (v:val) (F1 F2 : Formula) : Formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (b:bool), v = enc b /\
(b = true -> 'F1 H Q) /\ (b = false -> 'F2 H Q).
(b = true -> ^F1 H Q) /\ (b = false -> ^F2 H Q).
Definition Cf_seq (F1 : Formula) (F2 : Formula) : Formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (Q1:unit->hprop), 'F1 H Q1 /\ 'F2 (Q1 tt) Q.
exists (Q1:unit->hprop), ^F1 H Q1 /\ ^F2 (Q1 tt) Q.
Definition Cf_let (F1 : Formula) (F2of : forall `{EA1:Enc A1}, A1 -> Formula) : Formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (A1:Type) (EA1:Enc A1) (Q1:A1->hprop),
'F1 H Q1
/\ (forall (X:A1), '(F2of X) (Q1 X) Q).
^F1 H Q1
/\ (forall (X:A1), ^(F2of X) (Q1 X) Q).
Definition Cf_let_typed `{EA1:Enc A1} (F1 : Formula) (F2of : A1 -> Formula) : Formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (Q1:A1->hprop),
'F1 H Q1
/\ (forall (X:A1), '(F2of X) (Q1 X) Q).
^F1 H Q1
/\ (forall (X:A1), ^(F2of X) (Q1 X) Q).
Definition Cf_if (F0 F1 F2 : Formula) : Formula :=
Cf_let_typed F0 (fun (X:bool) => Local (Cf_if_val (enc X) F1 F2)).
......@@ -114,18 +114,18 @@ Definition Cf_while (F1 F2 : Formula) : Formula :=
fun `{Enc A} H (Q:A->hprop) =>
forall (F:Formula), is_local (@F unit _) ->
(forall H' (Q':unit->hprop),
'(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
'(F:Formula) H' Q') ->
'(F:Formula) H Q.
^(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
^(F:Formula) H' Q') ->
^(F:Formula) H Q.
*)
Definition Cf_while (F1 F2 : Formula) : Formula :=
Formula_typed (fun H (Q:unit->hprop) =>
forall (F:Formula), is_local (@F unit _) ->
(forall H' (Q':unit->hprop),
'(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
'(F:Formula) H' Q') ->
'(F:Formula) H Q).
^(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
^(F:Formula) H' Q') ->
^(F:Formula) H Q).
Definition Cf_for (n1 n2 : int) (F1 : int->Formula) : Formula :=
(* Formula_typed (fun H (Q:unit->hprop) => *)
......@@ -133,8 +133,8 @@ Definition Cf_for (n1 n2 : int) (F1 : int->Formula) : Formula :=
forall (S:int->Formula), (forall i, is_local (@S i unit _)) ->
let F i := Local (If (i <= n2) then (Local (Cf_seq (F1 i) (S (i+1))))
else (Local (Cf_val val_unit))) in
(forall i H' Q', '(F i) H' Q' -> '(S i) H' Q') ->
'(S n1) H Q.
(forall i H' Q', ^(F i) H' Q' -> ^(S i) H' Q') ->
^(S n1) H Q.
(* ---------------------------------------------------------------------- *)
......@@ -195,7 +195,7 @@ Proof.
Qed.
Definition Sound_for (t:trm) (F:Formula) :=
forall `{EA:Enc A} H (Q:A->hprop), 'F H Q -> Triple t H Q.
forall `{EA:Enc A} H (Q:A->hprop), ^F H Q -> Triple t H Q.
Lemma Sound_for_Local : forall t (F:Formula),
Sound_for t F ->
......@@ -269,7 +269,7 @@ Proof using.
Qed.
Theorem Triple_of_Cf : forall (t:trm) A `{EA:Enc A} H (Q:A->hprop),
'(Cf t) H Q ->
^(Cf t) H Q ->
Triple t H Q.
Proof using. intros. applys* Sound_for_Cf. Qed.
......@@ -383,14 +383,14 @@ Definition Cf_while_inv (F1 F2 : Formula) := fun (H:hprop) (Q:unit->hprop) =>
wf R
/\ (H ==> Hexists b X, I b X \* H')
/\ (forall (F:Formula), is_local (@F unit _) -> forall b X,
(forall b' X', R X' X -> 'F (I b' X') (fun (_:unit) => Hexists Y, I false Y)) ->
'(Local (Cf_if F1 (Local (Cf_seq F2 F)) (Local (Cf_val val_unit))))
(forall b' X', R X' X -> ^F (I b' X') (fun (_:unit) => Hexists Y, I false Y)) ->
^(Local (Cf_if F1 (Local (Cf_seq F2 F)) (Local (Cf_val val_unit))))
(I b X) (fun (_:unit) => Hexists Y, I false Y))
/\ ((fun (_:unit) => Hexists X, I false X \* H') ===> Q).
Lemma Cf_while_of_Cf_while_inv : forall (F1 F2 : Formula) (H:hprop) (Q:unit->hprop),
(Cf_while_inv F1 F2) H Q ->
'(Cf_while F1 F2) H Q.
^(Cf_while F1 F2) H Q.
Proof using.
introv (A&I&R&H'&MR&MH&MB&MQ). exists Q; split; [|applys @PostChange_refl].
intros F LF HF. xchange MH. xpull ;=> b X.
......@@ -709,9 +709,9 @@ Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
Lemma Cf_let_intro : forall A1 (EA1:Enc A1) (Q1:A1->hprop) (F1 : Formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> Formula),
forall A (EA:Enc A) H (Q:A->hprop),
'F1 H Q1 ->
(forall (X:A1), '(F2of A1 X) (Q1 X) Q) ->
'(Cf_let F1 F2of) H Q.
^F1 H Q1 ->
(forall (X:A1), ^(F2of A1 X) (Q1 X) Q) ->
^(Cf_let F1 F2of) H Q.
Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
Ltac xlet_untyped_core tt :=
......
......@@ -248,6 +248,69 @@ End Red.
(* ********************************************************************** *)
(* * Notation for terms *)
(* ---------------------------------------------------------------------- *)
(** Notation for program variables *)
Notation "''a'" := ("a":var) : var_scope.
Notation "''b'" := ("b":var) : var_scope.
Notation "''c'" := ("c":var) : var_scope.
Notation "''d'" := ("d":var) : var_scope.
Notation "''e'" := ("e":var) : var_scope.
Notation "''f'" := ("f":var) : var_scope.
Notation "''g'" := ("g":var) : var_scope.
Notation "''h'" := ("h":var) : var_scope.
Notation "''i'" := ("i":var) : var_scope.
Notation "''j'" := ("j":var) : var_scope.
Notation "''k'" := ("k":var) : var_scope.
Notation "''l'" := ("l":var) : var_scope.
Notation "''m'" := ("m":var) : var_scope.
Notation "''n'" := ("n":var) : var_scope.
Notation "''o'" := ("o":var) : var_scope.
Notation "''p'" := ("p":var) : var_scope.
Notation "''q'" := ("q":var) : var_scope.
Notation "''r'" := ("r":var) : var_scope.
Notation "''s'" := ("s":var) : var_scope.
Notation "''t'" := ("t":var) : var_scope.
Notation "''u'" := ("u":var) : var_scope.
Notation "''v'" := ("v":var) : var_scope.
Notation "''w'" := ("w":var) : var_scope.
Notation "''x'" := ("x":var) : var_scope.
Notation "''y'" := ("y":var) : var_scope.
Notation "''z'" := ("z":var) : var_scope.
Notation "''A'" := ("A":var) : var_scope.
Notation "''B'" := ("B":var) : var_scope.
Notation "''C'" := ("C":var) : var_scope.
Notation "''D'" := ("D":var) : var_scope.
Notation "''E'" := ("E":var) : var_scope.
Notation "''F'" := ("F":var) : var_scope.
Notation "''G'" := ("G":var) : var_scope.
Notation "''H'" := ("H":var) : var_scope.
Notation "''I'" := ("I":var) : var_scope.
Notation "''J'" := ("J":var) : var_scope.
Notation "''K'" := ("K":var) : var_scope.
Notation "''L'" := ("L":var) : var_scope.
Notation "''M'" := ("M":var) : var_scope.
Notation "''N'" := ("N":var) : var_scope.
Notation "''O'" := ("O":var) : var_scope.
Notation "''P'" := ("P":var) : var_scope.
Notation "''Q'" := ("Q":var) : var_scope.
Notation "''R'" := ("R":var) : var_scope.
Notation "''S'" := ("S":var) : var_scope.
Notation "''T'" := ("T":var) : var_scope.
Notation "''U'" := ("U":var) : var_scope.
Notation "''V'" := ("V":var) : var_scope.
Notation "''W'" := ("W":var) : var_scope.
Notation "''X'" := ("X":var) : var_scope.
Notation "''Y'" := ("Y":var) : var_scope.
Notation "''Z'" := ("Z":var) : var_scope.
Open Scope var_scope.
(* Note: for variable names with several letters, add your own definition *)
(* ---------------------------------------------------------------------- *)
(** Notation for concrete programs *)
......
......@@ -27,16 +27,6 @@ Implicit Types k : field.
Implicit Type l p q : loc.
Implicit Types n : int.
Notation "'B'" := ("B":var) : var_scope.
Notation "'I'" := ("I":var) : var_scope.
Notation "'N'" := ("N":var) : var_scope.
Notation "'M'" := ("M":var) : var_scope.
Notation "'P'" := ("P":var) : var_scope.
Notation "'Q'" := ("Q":var) : var_scope.
Notation "'V'" := ("V":var) : var_scope.
Notation "'X'" := ("X":var) : var_scope.
Local Open Scope var_scope.
(* ********************************************************************** *)
(* * Derived basic functions *)
......@@ -46,10 +36,10 @@ Local Open Scope var_scope.
(** Increment function *)
Definition val_incr :=
ValFun P :=
Let N := val_get P in
Let M := val_add N 1 in
val_set P M.
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_add 'n 1 in
val_set 'p 'm.
(** Same proof using characteristic formulae with advanced tactics *)
......@@ -68,7 +58,7 @@ Hint Extern 1 (Register_spec val_incr) => Provide rule_incr.
(** Negation *)
Definition val_not :=
ValFun N := If_ val_eq N true Then false Else true.
ValFun 'n := If_ val_eq 'n true Then false Else true.
Lemma rule_not : forall (b:bool),
triple (val_not b)
......@@ -87,9 +77,9 @@ Hint Extern 1 (Register_spec val_not) => Provide rule_not.
(** Disequality test *)
Definition val_neq :=
ValFun M N :=
Let X := val_eq M N in
val_not X.
ValFun 'm 'n :=
Let 'x := val_eq 'm 'n in
val_not 'x.
Lemma rule_neq : forall v1 v2,
triple (val_neq v1 v2)
......@@ -109,9 +99,9 @@ Hint Extern 1 (Register_spec val_neq) => Provide rule_neq.
(** Read to a record field *)
Definition val_get_field (k:field) :=
ValFun P :=
Let Q := val_ptr_add P (nat_to_Z k) in
val_get Q.
ValFun 'p :=
Let 'q := val_ptr_add 'p (nat_to_Z k) in
val_get 'q.
Lemma rule_get_field : forall l k v,
triple ((val_get_field k) l)
......@@ -122,7 +112,7 @@ Proof using.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> HN. xapplys~ rule_get.
xpull ;=> N. xapplys~ rule_get.
Qed.
......@@ -130,9 +120,9 @@ Qed.
(** Write to a record field *)
Definition val_set_field (k:field) :=
ValFun P V :=
Let Q := val_ptr_add P (nat_to_Z k) in
val_set Q V.
ValFun 'p 'v :=
Let 'q := val_ptr_add 'p (nat_to_Z k) in
val_set 'q 'v.
Lemma rule_set_field : forall v' l k v,
triple ((val_set_field k) l v)
......@@ -143,7 +133,7 @@ Proof using.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> HN. xapplys~ rule_set.
xpull ;=> N. xapplys~ rule_set.
Qed.
Arguments rule_set_field : clear implicits.
......@@ -193,7 +183,7 @@ Lemma Array_middle_eq : forall n p L,
Array L1 p \* (abs(p+n) ~~~> x) \* Array L2 (p + length L1 + 1)%nat.
Proof using.
(* TODO: simplify the Z/nat math, by using a result from LibListZ directly *)
introv HN. applys himpl_antisym.
introv N. applys himpl_antisym.
{ forwards (L1&x&L2&E&HM): list_middle_inv (abs n) L.
asserts (N1&N2): (0 <= abs n /\ (abs n < length L)%Z).
{ split; rewrite abs_nonneg; math. } math.
......@@ -231,7 +221,7 @@ Lemma rule_alloc_array : forall n,
(fun r => Hexists (p:loc) (L:list val), \[r = val_loc p] \*
\[length L = n :> int] \* Array L p).
Proof using.
introv HN. xapp. math.
introv N. xapp. math.
intros r. hpull ;=> l (E&Nl). subst r.
hchange Array_of_Alloc. hpull ;=> L HL.
hsimpl~. rewrite HL. rewrite~ abs_nonneg.
......@@ -249,9 +239,9 @@ Implicit Types i ofs len : int.
(** Array get *)
Definition val_array_get : val :=
ValFun P I :=
Let N := val_ptr_add P I in
val_get N.
ValFun 'p 'i :=
Let 'n := val_ptr_add 'p 'i in
val_get 'n.
Lemma rule_array_get : forall p i L,
index L i ->
......@@ -259,7 +249,7 @@ Lemma rule_array_get : forall p i L,
(Array L p)
(fun r => \[r = L[i]] \* Array L p).
Proof using.
introv HN. rewrite index_eq_inbound in HN.
introv N. rewrite index_eq_inbound in N.
xcf. xapps. { math. }
rewrites (>> Array_middle_eq i). { math. }
xpull ;=> L1 x L2 EL HL.
......@@ -278,9 +268,9 @@ Notation "'Array'' p `[ i ]" := (trm_app (trm_app (trm_val val_array_get) p) i)
(** Array set *)
Definition val_array_set : val :=
ValFun P I X :=
Let N := val_ptr_add P I in
val_set N X.
ValFun 'p 'i 'x :=
Let 'n := val_ptr_add 'p 'i in
val_set 'n 'x.
Lemma rule_array_set : forall p i v L,
index L i ->
......@@ -288,7 +278,7 @@ Lemma rule_array_set : forall p i v L,
(Array L p)
(fun r => \[r = val_unit] \* Array (L[i:=v]) p).
Proof using.
introv HN. rewrite index_eq_inbound in HN.
introv N. rewrite index_eq_inbound in N.
xcf. xapps. { math. }
rewrites (>> Array_middle_eq i). { math. }
xpull ;=> L1 x L2 EL HL.
......@@ -309,13 +299,13 @@ Notation "'Array'' p `[ i ] `<- x" := (trm_app (trm_app (trm_app (trm_val val_ar
(** Array make *)
Definition val_array_make : val :=
ValFun N V :=
Let P := val_alloc N in
Let B := val_sub N 1 in
For I := 0 To B Do (* todo: allow inlining of B *)
Array' P`[I] `<- V
ValFun 'n 'v :=
Let 'p := val_alloc 'n in
Let 'b := val_sub 'n 1 in
For 'i := 0 To 'b Do (* todo: allow inlining of B *)
Array' 'p`['i] `<- 'v
Done;;
P.
'p.
Lemma rule_array_make : forall n v,
n >= 0 ->
......@@ -323,16 +313,16 @@ Lemma rule_array_make : forall n v,
\[]
(fun r => Hexists p L, \[r = val_loc p] \* \[L = make n v] \* Array L p).
Proof using.
introv HN. xcf. xapp~ rule_alloc_array ;=> r p L Er EL. subst r.
introv N. xcf. xapp~ rule_alloc_array ;=> r p L Er EL. subst r.
xapps. xseq.
{ (* todo: xfor tactic *)
applys local_erase. esplit; esplit; splits; [reflexivity|reflexivity|].
intros S LS EF HM. subst EF. simpl in HM.
intros S LS EF M. subst EF. simpl in M.
cuts G: (forall i L', i >= 0 -> length L' = n-i ->
S i (Array ((make i v)++L') p) (fun r => \[r = '()] \* (Array (make n v) p))).
{ applys_eq (>> G L) 2. math. math. rewrite make_zero. rew_list~. }
intros i. induction_wf IH: (upto n) i. intros L' Ei EL'.
applys (rm HM). case_if.
applys (rm M). case_if.
{ xapp~. { rewrite index_eq_inbound. rew_list. rewrite length_make; math. }
destruct L' as [|x L']. { false. rew_list in EL'. math. }
rewrite~ update_middle; [| rewrite length_make; math ].
......
......@@ -430,12 +430,11 @@ End Alloc_to_Record.
See below for the generalization to arbitrary arities. *)
Definition val_new_record_2 :=
Vars X1, X2, P in
ValFun X1 X2 :=
Let P := val_alloc 2 in
val_set_field 0%nat P X1;;
val_set_field 1%nat P X2;;
P.
ValFun 'x 'y :=
Let 'p := val_alloc 2 in
val_set_field 0%nat 'p 'x;;
val_set_field 1%nat 'p 'y;;
'p.
Lemma Rule_new_record_2 : forall `{EA1:Enc A1} `{EA2:Enc A2} (v1:A1) (v2:A2),
Triple (val_new_record_2 `v1 `v2)
......
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