Commit ffc2f17f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make Normal a type class, and prove [normally_hwand_or_hwand_false].

parent 0eb80e14
...@@ -641,49 +641,45 @@ Implicit Types Q : val -> hprop. ...@@ -641,49 +641,45 @@ Implicit Types Q : val -> hprop.
Definition duplicatable (H:hprop) : Prop := Definition duplicatable (H:hprop) : Prop :=
H ==> H \* H. H ==> H \* H.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Definitions and properties of [normal] *) (* ** Definitions and properties of [normal] *)
Program Definition normal (H:hprop) : Prop := Class Normal (H:hprop) : Prop :=
forall h, H h -> h^r = fmap_empty. normal_emp h : H h -> h^r = fmap_empty.
Definition normal_post A (Q:A->hprop) :=
forall x, normal (Q x).
Arguments normal_post [A]. Notation Normal_post Q := (forall x, Normal (Q x)).
Lemma normal_hempty : Instance Normal_hempty :
normal \[]. Normal \[].
Proof using. Proof using.
Transparent hempty hpure. Transparent hempty hpure.
introv M. unfolds hempty, hpure. subst. autos*. introv M. unfolds hempty, hpure. subst. autos*.
Qed. Qed.
Lemma normal_hpure : forall P, Instance Normal_hpure : forall P,
normal \[P]. Normal \[P].
Proof using. Proof using.
Transparent hpure. Transparent hpure.
introv (p&M). unfolds hempty. subst. auto. introv (p&M). unfolds hempty. subst. auto.
Qed. Qed.
Lemma normal_hempty' : (* simpler proof *) Lemma Normal_hempty' : (* simpler proof *)
normal \[]. Normal \[].
Proof using. Proof using.
intros. rewrite hempty_eq_hpure_true. applys~ normal_hpure. intros. rewrite hempty_eq_hpure_true. applys~ Normal_hpure.
Qed. Qed.
Lemma normal_hsingle : forall l v, Instance Normal_hsingle : forall l v,
normal (hsingle l v). Normal (hsingle l v).
Proof using. Proof using.
Transparent hsingle. Transparent hsingle.
introv M. unfolds hsingle. autos*. introv M. unfolds hsingle. autos*.
Qed. Qed.
Lemma normal_hstar : forall H1 H2, Instance Normal_hstar : forall H1 H2,
normal H1 -> Normal H1 ->
normal H2 -> Normal H2 ->
normal (H1 \* H2). Normal (H1 \* H2).
Proof using. Proof using.
introv N1 N2 (h1&h2&P1&P2&M1&EQ). introv N1 N2 (h1&h2&P1&P2&M1&EQ).
lets (_&E): heap_eq_forward EQ. simpls. rewrite E. lets (_&E): heap_eq_forward EQ. simpls. rewrite E.
...@@ -692,42 +688,42 @@ Proof using. ...@@ -692,42 +688,42 @@ Proof using.
rewrite~ fmap_union_empty_r. rewrite~ fmap_union_empty_r.
Qed. Qed.
Lemma normal_hexists : forall A (J:A->hprop), Instance Normal_hexists : forall A (J:A->hprop),
normal_post J -> Normal_post J ->
normal (hexists J). Normal (hexists J).
Proof using. introv M (x&N). rewrites~ (>> M N). Qed. Proof using. introv M (x&N). rewrites~ (>> M N). Qed.
Lemma normal_hor : forall H1 H2, Instance Normal_hor : forall H1 H2,
normal H1 -> Normal H1 ->
normal H2 -> Normal H2 ->
normal (hor H1 H2). Normal (hor H1 H2).
Proof using. Proof using.
introv M1 M2 [N|N]. introv M1 M2 [N|N].
{ rewrites~ (>> M1 N). } { rewrites~ (>> M1 N). }
{ rewrites~ (>> M2 N). } { rewrites~ (>> M2 N). }
Qed. Qed.
Lemma normal_hand_l : forall H1 H2, Instance Normal_hand_l : forall H1 H2,
normal H1 -> Normal H1 ->
normal (hand H1 H2). Normal (hand H1 H2).
Proof using. introv M (N1&N2). forwards*: M N1. Qed. Proof using. introv M (N1&N2). forwards*: M N1. Qed.
Lemma normal_hand_r : forall H1 H2, Instance Normal_hand_r : forall H1 H2,
normal H2 -> Normal H2 ->
normal (hand H1 H2). Normal (hand H1 H2).
Proof using. introv M (N1&N2). forwards*: M N2. Qed. Proof using. introv M (N1&N2). forwards*: M N2. Qed.
Lemma normal_himpl : forall H1 H2, Lemma Normal_himpl : forall H1 H2,
normal H2 -> Normal H2 ->
(H1 ==> H2) -> (H1 ==> H2) ->
normal H1. Normal H1.
Proof using. introv HS HI M. lets: HI M. applys* HS. Qed. Proof using. introv HS HI M. lets: HI M. applys* HS. Qed.
(* Note: normal_hwand is not true *) (* Note: Normal_hwand is not true *)
Lemma normal_hpure_star_hprop : forall (P:Prop) H, Lemma Normal_hpure_star_hprop : forall (P:Prop) H,
(P -> normal H) -> (P -> Normal H) ->
normal (\[P] \* H). Normal (\[P] \* H).
Proof using. Proof using.
introv N (h1&h2&P1&P2&M1&EQ). introv N (h1&h2&P1&P2&M1&EQ).
lets (_&E): heap_eq_forward EQ. simpls. rewrite E. lets (_&E): heap_eq_forward EQ. simpls. rewrite E.
...@@ -736,7 +732,6 @@ Proof using. ...@@ -736,7 +732,6 @@ Proof using.
rewrites~ (>> N P2). rew_fmap~. rewrites~ (>> N P2). rew_fmap~.
Qed. Qed.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Definitions and properties of [ROl] *) (* ** Definitions and properties of [ROl] *)
...@@ -881,7 +876,7 @@ Qed. ...@@ -881,7 +876,7 @@ Qed.
Lemma on_rw_sub_htop' : forall H h, Lemma on_rw_sub_htop' : forall H h,
(H \* \Top) h -> (H \* \Top) h ->
normal H -> Normal H ->
on_rw_sub H h. on_rw_sub H h.
Proof using. Proof using.
introv (h1&h2&N1&N2&N3&N4) N. exists h1 h2. splits~. introv (h1&h2&N1&N2&N3&N4) N. exists h1 h2. splits~.
...@@ -1006,7 +1001,7 @@ Qed. ...@@ -1006,7 +1001,7 @@ Qed.
Lemma rule_frame_read_only : forall t H1 Q1 H2, Lemma rule_frame_read_only : forall t H1 Q1 H2,
triple t (H1 \* RO H2) Q1 -> triple t (H1 \* RO H2) Q1 ->
normal H2 -> Normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2). triple t (H1 \* H2) (Q1 \*+ H2).
Proof using. Proof using.
introv M N. intros h1 h2 D (h11&h12&P11&P12&R1&R2). introv M N. intros h1 h2 D (h11&h12&P11&P12&R1&R2).
...@@ -1084,10 +1079,10 @@ Qed. ...@@ -1084,10 +1079,10 @@ Qed.
Lemma rule_frame : forall t H1 Q1 H2, Lemma rule_frame : forall t H1 Q1 H2,
triple t H1 Q1 -> triple t H1 Q1 ->
normal H2 -> Normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2). triple t (H1 \* H2) (Q1 \*+ H2).
Proof using. Proof using.
introv M N. applys~ rule_frame_read_only. introv M N. applys~ rule_frame_read_only.
applys rule_consequence (H1 \* \Top). hsimpl. applys rule_consequence (H1 \* \Top). hsimpl.
applys* rule_htop_pre. auto. applys* rule_htop_pre. auto.
Qed. Qed.
...@@ -1108,7 +1103,7 @@ Qed. ...@@ -1108,7 +1103,7 @@ Qed.
Lemma rule_val : forall v H Q, Lemma rule_val : forall v H Q,
H ==> Q v -> H ==> Q v ->
normal H -> Normal H ->
triple (trm_val v) H Q. triple (trm_val v) H Q.
Proof using. Proof using.
introv M HS. intros h1 h2 D P1. specializes HS P1. introv M HS. intros h1 h2 D P1. specializes HS P1.
...@@ -1119,7 +1114,7 @@ Qed. ...@@ -1119,7 +1114,7 @@ Qed.
Lemma rule_fix : forall f x t1 H Q, Lemma rule_fix : forall f x t1 H Q,
H ==> Q (val_fix f x t1) -> H ==> Q (val_fix f x t1) ->
normal H -> Normal H ->
triple (trm_fix f x t1) H Q. triple (trm_fix f x t1) H Q.
Proof using. Proof using.
introv M HS. intros h1 h2 D P1. exists___. splits*. introv M HS. intros h1 h2 D P1. exists___. splits*.
...@@ -1186,7 +1181,7 @@ Proof using. ...@@ -1186,7 +1181,7 @@ Proof using.
introv M. forwards~ M': M. introv M. forwards~ M': M.
applys_eq (>> rule_let \[] (fun x => \[x = v1])) 2. applys_eq (>> rule_let \[] (fun x => \[x = v1])) 2.
{ applys rule_val. rewrite <- (@hstar_hempty_r \[v1=v1]). { applys rule_val. rewrite <- (@hstar_hempty_r \[v1=v1]).
applys~ himpl_hprop_r. applys normal_hempty. } applys~ himpl_hprop_r. applys Normal_hempty. }
{ intros X. applys rule_extract_hprop. applys M. } { intros X. applys rule_extract_hprop. applys M. }
{ rewrite~ hstar_hempty_l. } { rewrite~ hstar_hempty_l. }
Qed. Qed.
...@@ -1205,7 +1200,7 @@ Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) := ...@@ -1205,7 +1200,7 @@ Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
Lemma rule_let_fix : forall f x t1 t2 H Q, Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val), spec_fix f x t1 F -> triple (subst f F t2) H Q) -> (forall (F:val), spec_fix f x t1 F -> triple (subst f F t2) H Q) ->
normal H -> Normal H ->
triple (trm_let f (trm_fix f x t1) t2) H Q. triple (trm_let f (trm_fix f x t1) t2) H Q.
Proof using. Proof using.
introv M HS. applys rule_let_simple (fun F => \[spec_fix f x t1 F] \* H). introv M HS. applys rule_let_simple (fun F => \[spec_fix f x t1 F] \* H).
...@@ -1296,8 +1291,8 @@ Qed. ...@@ -1296,8 +1291,8 @@ Qed.
Definition normally H := Definition normally H :=
fun h => H h /\ h^r = fmap_empty. fun h => H h /\ h^r = fmap_empty.
Lemma normal_normally : forall H, Instance Normal_normally : forall H,
normal (normally H). Normal (normally H).
Proof using. introv (M&E). auto. Qed. Proof using. introv (M&E). auto. Qed.
Lemma normally_erase : forall H, Lemma normally_erase : forall H,
...@@ -1305,16 +1300,14 @@ Lemma normally_erase : forall H, ...@@ -1305,16 +1300,14 @@ Lemma normally_erase : forall H,
Proof using. intros H h (N&E). auto. Qed. Proof using. intros H h (N&E). auto. Qed.
Lemma normally_intro : forall H, Lemma normally_intro : forall H,
normal H -> Normal H ->
H ==> normally H. H ==> normally H.
Proof using. introv N. intros h M. split~. Qed. Proof using. introv N. intros h M. split~. Qed.
Lemma normally_idempotent : forall H, Lemma normally_Normal_eq : forall H,
normally H = normally (normally H). Normal H -> normally H = H.
Proof using. Proof using. introv N.
intros. applys himpl_antisym. applys himpl_antisym; [apply normally_erase|apply normally_intro, _].
{ intros h (N&E). split~. split~. }
{ intros h ((N&E1)&E2). split~. }
Qed. Qed.
Lemma normally_himpl : forall H1 H2, Lemma normally_himpl : forall H1 H2,
...@@ -1322,20 +1315,17 @@ Lemma normally_himpl : forall H1 H2, ...@@ -1322,20 +1315,17 @@ Lemma normally_himpl : forall H1 H2,
normally H1 ==> normally H2. normally H1 ==> normally H2.
Proof using. introv M. intros h (N&E). split~. Qed. Proof using. introv M. intros h (N&E). split~. Qed.
Lemma normally_idempotent : forall H,
normally (normally H) = normally H.
Proof using. intros. apply normally_Normal_eq, _. Qed.
Lemma normally_hpure : forall (P:Prop), Lemma normally_hpure : forall (P:Prop),
normally \[P] = \[P]. normally \[P] = \[P].
Proof using. Proof using. intros. apply normally_Normal_eq, _. Qed.
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 normally_hempty : Lemma normally_hempty :
normally \[] = \[]. normally \[] = \[].
Proof using. Proof using. intros. apply normally_Normal_eq, _. Qed.
intros. rewrite hempty_eq_hpure_true. rewrite~ normally_hpure.
Qed.
Lemma normally_hexists : forall A (J:A->hprop), Lemma normally_hexists : forall A (J:A->hprop),
normally (hexists J) = hexists (fun x => normally (J x)). normally (hexists J) = hexists (fun x => normally (J x)).
...@@ -1376,20 +1366,42 @@ Proof using. ...@@ -1376,20 +1366,42 @@ Proof using.
intros M. rewrite <- normally_hstar. applys~ normally_himpl. intros M. rewrite <- normally_hstar. applys~ normally_himpl.
Qed. Qed.
(** Alternative definition of [normal] in terms of [normally] *) Lemma normally_hwand_normal : forall H1 H2,
Normal H1 ->
normally (H1 \--* H2) ==> H1 \--* normally H2.
Proof.
intros. hchanges normally_hwand. rewrite normally_Normal_eq; auto.
Qed.
Definition normal' H := Lemma normally_hwand_or_hwand_false : forall H1 H2,
H1 \--* normally H2 ==> hor (normally (H1 \--* H2)) (H1 \--* \[False]).
Proof.
intros H1 H2 h Hh. tests Hhr : (h^r = fmap_empty).
- left. split; [|auto]. destruct Hh as [H0 Hh]. exists H0.
revert Hh. rewrite hstar_comm, hstar_pure. intros [??].
rewrite hstar_comm, hstar_pure. split; [|auto]. hchanges H.
apply normally_erase.
- right. eexists (eq h). rewrite hstar_comm, hstar_pure. split; [|auto].
destruct Hh as [H0 Hh]. rewrite hstar_comm, hstar_pure in Hh.
destruct Hh as [IMPL Hh]. intros h' (h1 & h2 & ? & Hh2 & Hh12 & ?).
destruct Hhr. subst. destruct (IMPL (h1 \u h2)) as (_ & EMP); last first.
{ eapply fmap_union_eq_empty_inv_l. rewrite <- heap_union_r; eauto. }
eexists _, _. eauto.
Qed.
(** Alternative definition of [Normal] in terms of [normally] *)
Definition Normal' H :=
(H ==> normally H). (H ==> normally H).
Lemma normal_eq_normal' : Lemma Normal_eq_Normal' :
normal = normal'. Normal = Normal'.
Proof using. Proof using.
applys pred_ext_1. intros H. unfold normal, normal', normally. iff N. applys pred_ext_1. intros H. unfold Normal, Normal', normally. iff N.
{ intros h M. split~. } { intros h M. split~. }
{ intros h M. forwards~ (R&E): N h. } { intros h M. forwards~ (R&E): N h. }
Qed. Qed.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Read-only frame rule reformulated using normally *) (* ** Read-only frame rule reformulated using 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