Commit 7be4642f by charguer

### record_set

parent ee61420a
 ... ... @@ -127,9 +127,9 @@ Hint Resolve app_basic_local. (********************************************************************) (* ** Generic notation for list of dyns *) (* DEPRECATED Notation "'Dyn' x" := (@dyn _ x) (at level 0). *) (* useful for reading goals *) Local Notation "'Dyn' x" := (@dyn _ x) (at level 0). Notation "[ x1 ]" := ((dyn x1)::nil) (at level 0, x1 at level 0) : dynlist. ... ... @@ -618,17 +618,21 @@ Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x (* Axiomatic access in record fields *) Axiom record_get : func. Axiom record_set : func. Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A), app_keep record_get [r f] (r ~> record_repr_one f v) \[= v]. Axiom record_set_spec : forall (r:loc) (f:nat) A (v w:A), app record_get [r f w] (r ~> record_repr_one f v) (# r ~> record_repr_one f w). Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B), app record_set [r f w] (r ~> record_repr_one f v) (# r ~> record_repr_one f w). Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic := match L with | nil => None | (f',d')::L' => if Nat.eq_dec f f' then Some d' else record_get_compute_dyn f L' | (f',d')::T' => if Nat.eq_dec f f' then Some d' else record_get_compute_dyn f T' end. Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop := ... ... @@ -644,7 +648,7 @@ Proof using. introv M. unfolds record_get_compute_spec. sets_eq <- do E: (record_get_compute_dyn f L). destruct do as [[T v]|]; inverts M. induction L as [|[f' [T' d']] L']; [false|]. induction L as [|[f' [D' d']] T']; [false|]. simpl in E. intros r. do 2 Xunfold record_repr at 1. simpl. case_if. { inverts E. ... ... @@ -653,14 +657,60 @@ Proof using. { apply record_get_spec. } { hsimpl. } { hsimpl~. } } { specializes IHL' (rm E). { specializes IHT' (rm E). eapply local_frame. { apply app_local. auto_false. } { apply IHL'. } { apply IHT'. } { hsimpl. } { hsimpl~. } } Qed. (* todo: could use xapply in this proof *) Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option record_descr := match L with | nil => None | (f',d')::T' => if Nat.eq_dec f f' then Some ((f,d)::T') else match record_set_compute_dyn f d T' with | None => None | Some L' => Some ((f',d')::L') end end. Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Prop := match record_set_compute_dyn f (dyn w) L with | None => None | Some L' => Some (forall r, app record_set [r f w] (r ~> record_repr L) (# r ~> record_repr L')) end. Lemma record_set_compute_spec_correct : forall f A (w:A) L (P:Prop), record_set_compute_spec f w L = Some P -> P. Proof using. introv M. unfolds record_set_compute_spec. sets_eq <- do E: (record_set_compute_dyn f (dyn w) L). destruct do as [L'|]; inverts M. gen L'. induction L as [|[f' [T' v']] T]; intros; [false|]. simpl in E. Xunfold record_repr at 1. simpl. case_if. { inverts E. eapply local_frame. { apply app_local. auto_false. } { apply record_set_spec. } { hsimpl. } { Xunfold record_repr at 2. simpl. hsimpl~. } } { cases (record_set_compute_dyn f Dyn (w) T) as C; [|false]. inverts E. specializes~ IHT r. eapply local_frame. { apply app_local. auto_false. } { apply IHT. } { hsimpl. } { Xunfold record_repr at 2. simpl. hsimpl~. } } Qed. (* todo: could use xapply in this proof *) (* DEPRECATED Lemma record_get_compute_spec_correct' : forall f L, match record_get_compute_spec f L with | None => True ... ... @@ -670,6 +720,7 @@ Proof using. intros. cases (record_get_compute_spec f L). applys* record_get_compute_spec_correct. auto. Qed. *) Module RecordDemo. ... ... @@ -690,19 +741,16 @@ Ltac xspec_record_get_compute tt := xspec_record_get_compute_for f L end. Lemma demo_get_3 : forall r, app_keep record_get [r g] (r ~> `{ g := 1 }) \[= 1]. Proof using. intros. xspec_record_get_compute tt. intros G. apply G. Qed. Ltac xspec_record_set_compute_for f w L := let G := fresh in forwards G: (record_set_compute_spec_correct f w L); [ reflexivity | revert G ]. Ltac xspec_record_set_compute tt := match goal with |- app record_set [?r ?f ?w] (?r ~> record_repr ?L) _ => xspec_record_set_compute_for f w L end. Lemma demo_get_2 : forall r, app_keep record_get [r g] (r ~> `{ f := 1+1 ; g := 1 }) \[= 1]. Proof using. intros. xspec_record_get_compute tt. intros G. apply G. Qed. Lemma demo_get_1 : forall r, app_keep record_get [r f] (r ~> `{ f := 1+1 ; g := 1 }) \[= 2]. ... ... @@ -731,6 +779,28 @@ Qed. apply G. *) Lemma demo_get_2 : forall r, app_keep record_get [r g] (r ~> `{ f := 1+1 ; g := 1 }) \[= 1]. Proof using. intros. xspec_record_get_compute tt. intros G. apply G. Qed. Lemma demo_get_3 : forall r, app_keep record_get [r g] (r ~> `{ g := 1 }) \[= 1]. Proof using. intros. xspec_record_get_compute tt. intros G. apply G. Qed. Lemma demo_set_1 : forall r, (forall H', app record_set [r f 4] (r ~> `{ f := 1+1 ; g := 1 }) (#H') -> True) -> True. Proof using. introv M. applys (rm M). xspec_record_set_compute tt. intros G. apply G. Qed. End RecordDemo. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!