Commit 59b3ac80 authored by charguer's avatar charguer

model_hpull

parent 20a819cd
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
(*------------------------------------------------------------------*)
(* ** Separation Logic monoid *)
Require Import LibStruct.
Definition sep_monoid := monoid_ heap_is_star heap_is_empty.
Global Instance sep_Monoid : Monoid sep_monoid.
Proof using.
constructor; simpl.
apply star_assoc.
apply star_neutral_l.
apply star_neutral_r.
Qed.
Global Instance sep_Monoid_commutative : Monoid_commutative sep_monoid.
Proof using.
constructor; simpl.
applys sep_Monoid.
apply star_comm.
Qed.
(********************************************************************)
(* ** Shared tactics *)
Ltac on_formula_pre cont :=
match goal with
| |- _ ?H ?Q => cont H
| |- _ _ ?H ?Q => cont H
| |- _ _ _ ?H ?Q => cont H
| |- _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ _ _ _ _ ?H ?Q => cont H
| |- _ _ _ _ _ _ _ _ _ _ ?H ?Q => cont H
end.
Ltac on_formula_post cont :=
match goal with
| |- _ ?H ?Q => cont Q
| |- _ _ ?H ?Q => cont Q
| |- _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ _ _ _ _ ?H ?Q => cont Q
| |- _ _ _ _ _ _ _ _ _ _ ?H ?Q => cont Q
end.
Ltac remove_empty_heaps_formula tt :=
repeat (on_formula_pre ltac:(remove_empty_heaps_from)).
(********************************************************************)
(* ** Other stuff *)
Lemma heap_weaken_star : forall H1' H1 H2 H3,
(H1 ==> H1') -> (H1' \* H2 ==> H3) -> (H1 \* H2 ==> H3).
Proof using.
introv W M (h1&h2&N). unpack N. apply M. exists~ h1 h2.
Qed. (* todo: move *)
Lemma hsimpl_to_qunit : forall (H:hprop) (Q:unit->hprop),
Q = (fun _ => H) ->
H ==> Q tt.
Proof using. intros. subst. auto. Qed. (* todo: needed? *)
Hint Resolve hsimpl_to_qunit.
Lemma hprop_empty_core_eq_empty :
hprop_empty_core = \[].
Proof using.
unfold hprop_empty, hprop_pure. applys hprop_eq; intros h; autos*.
Qed.
Lemma hprop_star_empty_l : neutral_l hprop_star hprop_empty.
Proof using.
intros H. rewrite <- hprop_empty_core_eq_empty.
applys hprop_star_empty_core_l.
Qed.
========================
(**
This file provides tactics for automatically simplifying heap
......
This diff is collapsed.
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