Commit ab569279 authored by charguer's avatar charguer

himpl_prop

parent 99a3d3fe
......@@ -301,6 +301,7 @@ Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Implicit Types H : hprop.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc heap_union.
Lemma hprop_empty_prove :
......@@ -372,10 +373,6 @@ Proof using.
{ rewrite~ <- heap_union_assoc. } }
Qed.
Lemma hprop_star_cancel : forall H1 H2 H2',
H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
(hprop_single l v1) \* (hprop_single l v2) ==> \[False].
Proof using.
......@@ -390,23 +387,38 @@ Proof using.
introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_empty_l.
Qed.
Lemma hprop_star_prop_extract_prop : forall (P:Prop) H H',
Lemma himpl_refl : forall H,
H ==> H.
Proof using. intros h. auto. Qed.
Lemma himpl_trans : forall H1 H2 H3,
(H1 ==> H2) -> (H2 ==> H3) -> (H1 ==> H3).
Proof using. introv M1 M2. intros h H1h. eauto. Qed.
Lemma himpl_antisym : forall H1 H2,
(H1 ==> H2) -> (H2 ==> H1) -> (H1 = H2).
Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed.
Lemma himpl_cancel : forall H1 H2 H2',
H2 ==> H2' -> (H1 \* H2) ==> (H1 \* H2').
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma himpl_extract_prop : forall (P:Prop) H H',
(P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using. introv W Hh. lets (?&?): hprop_star_prop_elim Hh. applys* W. Qed.
Lemma hprop_exists_witness : forall A (x:A) H J,
Lemma himpl_extract_exists : forall A (x:A) H J,
(H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma hprop_gc_remove : forall H H',
Lemma himpl_remove_gc : forall H H',
H ==> H' ->
H ==> H' \* \GC.
Proof using.
introv M. intros h Hh. exists h heap_empty. splits*.
exists \[]. auto.
exists \[]. applys hprop_empty_prove.
Qed.
End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
......@@ -539,8 +551,8 @@ Lemma rule_consequence : forall H' Q' t H Q,
triple t H Q'.
Proof using.
introv WH M WQ. applys rule_consequence_gc M.
{ applys~ hprop_gc_remove. }
{ intros r. applys~ hprop_gc_remove. }
{ applys~ himpl_remove_gc. }
{ intros r. applys~ himpl_remove_gc. }
Qed.
Lemma rule_frame : forall t H Q H',
......
......@@ -213,13 +213,14 @@ Qed.
(*------------------------------------------------------------------*)
(* ** Properties of [hprop] *)
(* ** Properties of [hprop] and [==>] *)
Global Instance hprop_inhab : Inhab hprop.
Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Implicit Types H : hprop.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc heap_union.
Lemma hprop_empty_prove :
......@@ -287,10 +288,6 @@ Proof using.
{ rewrite~ heap_union_assoc. } }
Qed. (* later: exploit symmetry in the proof *)
Lemma hprop_star_cancel : forall H1 H2 H2',
H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
(hprop_single l v1) \* (hprop_single l v2) ==> \[False].
Proof using.
......@@ -304,20 +301,36 @@ Proof using.
introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_empty_l.
Qed.
Lemma hprop_star_prop_extract_prop : forall (P:Prop) H H',
Lemma himpl_refl : forall H,
H ==> H.
Proof using. intros h. auto. Qed.
Lemma himpl_trans : forall H1 H2 H3,
(H1 ==> H2) -> (H2 ==> H3) -> (H1 ==> H3).
Proof using. introv M1 M2. intros h H1h. eauto. Qed.
Lemma himpl_antisym : forall H1 H2,
(H1 ==> H2) -> (H2 ==> H1) -> (H1 = H2).
Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed.
Lemma himpl_cancel : forall H1 H2 H2',
H2 ==> H2' -> (H1 \* H2) ==> (H1 \* H2').
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma himpl_extract_prop : forall (P:Prop) H H',
(P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using. introv W Hh. lets (?&?): hprop_star_prop_elim Hh. applys* W. Qed.
Lemma hprop_exists_witness : forall A (x:A) H J,
Lemma himpl_extract_exists : forall A (x:A) H J,
(H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma hprop_gc_remove : forall H H',
Lemma himpl_remove_gc : forall H H',
H ==> H' ->
H ==> H' \* \GC.
Proof using.
introv M. intros h Hh. exists h heap_empty. splits*.
exists \[]. auto.
exists \[]. applys hprop_empty_prove.
Qed.
End HeapProp.
......@@ -325,6 +338,7 @@ End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
(********************************************************************)
(* ** Rules *)
......@@ -401,8 +415,8 @@ Lemma rule_consequence : forall H' Q' t H Q,
triple t H Q'.
Proof using.
introv WH M WQ. applys rule_consequence_gc M.
{ applys~ hprop_gc_remove. }
{ intros r. applys~ hprop_gc_remove. }
{ applys~ himpl_remove_gc. }
{ intros r. applys~ himpl_remove_gc. }
Qed.
Lemma rule_frame : forall t H Q H',
......
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