Commit 96cc63fc authored by charguer's avatar charguer

normally

parent 93d279ac
(* ---------------------------------------------------------------------- *)
Module Normally2.
Program Definition normally (H:hprop) :=
fun h => H (h^f,fmap_empty).
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfolds normal, normally.
intros h M. lets: (>> N M).
skip.
Qed.
(*
Lemma normal_normally : forall H,
normal (normally H).
Proof using.
intros H. unfolds normal, normally. intros h M.
Qed.
*)
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Proof using.
introv M. unfold normal, normally.
intros h N. hhsimpl~.
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normal, normally. intros h (h1&h2&M1&M2&M3&M4).
(* exists (h1^f \+ h2^f, (fmap_empty:state)).*)
skip.
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
Proof using.
intros. unfolds normal, normally. intros h M. simpl.
(* *)
skip.
Qed.
End Normally2.
(* ---------------------------------------------------------------------- *)
Module Normally3.
Definition normally H :=
Hexists H1 H2, \[normal H1] \* H1 \* \[H1 \* RO H2 ==> H].
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfold normally. hsimpl H \[].
{ rewrite RO_empty. hsimpl. }
{ auto. }
Qed.
Lemma normal_normally : forall H,
normal (normally H).
Proof using.
intros H. applys normal_hexists. intros H1.
applys normal_hexists. intros H2.
applys normal_pure_star_hprop. intros N1.
applys normal_star. auto.
applys normal_pure.
Qed.
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Proof using.
introv M. unfold normally. hpull ;=> H1a H1b N1 R1.
hsimpl~ H1a H1b. hchanges~ R1.
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normally. hpull ;=> H1a H1b N1 R1 H2a H2b N2 R2.
hsimpl (H1a \* H2a) (H1b \* H2b).
{ rew_heap. hchange (RO_star H1b H2b). hchange R1. hchanges R2. }
{ applys~ normal_star. }
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
Proof using.
intros. applys normally_intro. applys normal_normally.
Qed.
End Normally3.
Lemma normally_idempotent2 : forall H,
normally (normally H) ==> normally H.
Proof using.
......
......@@ -1258,109 +1258,72 @@ Qed.
(* ********************************************************************** *)
(* * Extension: [normally] modality (WORK IN PROGRESS) *)
(* * Extension: [normally] modality *)
Module Normally.
Module Normally1.
Definition normally H :=
fun h => H h /\ h^r = fmap_empty.
Program Definition normally (H:hprop) :=
fun h => H (h^f,fmap_empty).
Lemma normally_erase : forall H,
normally H ==> H.
Proof using. intros H h (N&E). auto. Qed.
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfolds normal, normally.
intros h M. lets: (>> N M).
skip.
Qed.
Proof using. introv N. intros h M. split~. Qed.
(*
Lemma normal_normally : forall H,
normal (normally H).
Lemma normally_idempotent : forall H,
normally H = normally (normally H).
Proof using.
intros H. unfolds normal, normally. intros h M.
intros. applys himpl_antisym.
{ intros h (N&E). split~. split~. }
{ intros h ((N&E1)&E2). split~. }
Qed.
*)
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Proof using.
introv M. unfold normal, normally.
intros h N. hhsimpl~.
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normal, normally. intros h (h1&h2&M1&M2&M3&M4).
(* exists (h1^f \+ h2^f, (fmap_empty:state)).*)
skip.
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
Proof using.
intros. unfolds normal, normally. intros h M. simpl.
(* *)
skip.
Qed.
End Normally1.
(* ---------------------------------------------------------------------- *)
Proof using. introv M. intros h (N&E). split~. Qed.
Module Normally2.
Definition normally H :=
Hexists H1 H2, \[normal H1] \* H1 \* \[H1 \* RO H2 ==> H].
Lemma normally_intro : forall H,
normal H ->
H ==> normally H.
Proof using.
introv N. unfold normally. hsimpl H \[].
{ rewrite RO_empty. hsimpl. }
{ auto. }
Lemma normally_hpure : forall (P:Prop),
normally \[P] = \[P].
Proof using.
intros. applys himpl_antisym.
{ intros h (N&E). auto. }
{ intros h N. lets (N1&N2): hpure_inv N. lets N3: hempty_inv N2.
split~. { subst h. auto. } }
Qed.
Lemma normal_normally : forall H,
normal (normally H).
Proof using.
intros H. applys normal_hexists. intros H1.
applys normal_hexists. intros H2.
applys normal_pure_star_hprop. intros N1.
applys normal_star. auto.
applys normal_pure.
Lemma normally_hempty :
normally \[] = \[].
Proof using.
intros. rewrite hempty_eq_hpure_true. rewrite~ normally_hpure.
Qed.
Lemma normally_himpl : forall H1 H2,
(H1 ==> H2) ->
normally H1 ==> normally H2.
Lemma normally_hexists : forall A (J:A->hprop),
normally (hexists J) = hexists (fun x => normally (J x)).
Proof using.
introv M. unfold normally. hpull ;=> H1a H1b N1 R1.
hsimpl~ H1a H1b. hchanges~ R1.
intros. applys himpl_antisym.
{ intros h ((x&N)&E). exists x. split~. }
{ intros h (x&(N&E)). split~. exists~ x. }
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 ==> normally (H1 \* H2).
Proof using.
intros. unfold normally. hpull ;=> H1a H1b N1 R1 H2a H2b N2 R2.
hsimpl (H1a \* H2a) (H1b \* H2b).
{ rew_heap. hchange (RO_star H1b H2b). hchange R1. hchanges R2. }
{ applys~ normal_star. }
Qed.
Lemma normally_idempotent1 : forall H,
normally H ==> normally (normally H).
normally H1 \* normally H2 = normally (H1 \* H2).
Proof using.
intros. applys normally_intro. applys normal_normally.
intros. applys himpl_antisym.
{ intros. intros h (h1&h2&(M1&E1)&(M2&E2)&M3&M4). split.
{ exists~ h1 h2. }
{ subst h. rew_heap~. rewrite E1,E2. rew_fmap~. } }
{ intros h ((h1&h2&M1&M2&M3&M4)&E). subst h. rew_heap~ in E.
exists h1 h2. splits~.
{ split~. applys* fmap_union_eq_empty_inv_l. }
{ split~. applys* fmap_union_eq_empty_inv_r. } }
Qed.
End Normally2.
End Normally.
(* ---------------------------------------------------------------------- *)
......
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