Commit 3083aaa2 authored by charguer's avatar charguer

fonctor_all_simplified

parent 2f75a379
......@@ -54,7 +54,7 @@ Proof using.
{ hsimpl. }
{ applys rule_set. }
{ intros r. applys himpl_hpure_l. intros E. subst.
applys himpl_hprop_r. { auto. } { auto. } }
applys himpl_hpure_r. { auto. } { auto. } }
Qed.
(** Same proof using [xapply], [xapplys] and [xpull] *)
......
......@@ -25,7 +25,7 @@ Tactic Notation "xdef" :=
(*
Definition is_extractible F :=
forall A (J:A->hprop) Q,
forall A (J:A->hprop) Q,
(forall x, F (J x) Q) ->
F (hexists J) Q.
*)
......@@ -3593,7 +3593,7 @@ Qed.
(* todo: already exist under different names
(* todo: already exist under different names
Lemma hexists_weaken : forall A (J J' : A -> hprop),
J ===> J' ->
......@@ -3616,7 +3616,7 @@ Arguments hwand_extend : clear implicits.
(* false if H1 is not habited
Lemma hwand_same_part : forall H1 H2 H3,
(H1 \* H2 \--* H1 \* H3) ==> (H2 \--* H3).
Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl.
Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl.
Lemma regular_regular_transformer : forall F,
......@@ -3627,22 +3627,22 @@ Proof using.
do 2 hchange hstar_hforall. rew_heap.
unfolds hforall. simpl. intros h Hh H'.
specializes Hh (H \* H'). hhsimpl.
hchanges (hwand_cancel_part H (H' \* \Top) (F (Q \*+ (H \* H')))).
hchanges (hwand_cancel_part H (H' \* \Top) (F (Q \*+ (H \* H')))).
rewrite (hstar_comm H' \Top).
apply hwand_move_part_r.
rewrite <- hstar_assoc. rewrite htop_hstar_htop.
rewrite <- hstar_assoc. rewrite htop_hstar_htop.
asserts_rewrite (Q \*+ (H \* H') = (fun x : val => (Q x \* H) \* H')).
{ apply fun_ext_1. intros x. rewrite~ hstar_assoc. }
pattern \Top at 3; rewrite <-
pattern \Top at 3; rewrite <-
applys himpl_trans. Focus 2. applys hwand_move_part_l.
applys himpl_trans. Focus 2. applys hwand_move_part_l.
hchanges (hwand_cancel_part \Top (H' \* \Top) (F (Q \*+ (H \* H')))).
hchanges (hwand_cancel_part \Top (H' \* \Top) (F (Q \*+ (H \* H')))).
hchange (hwand_extend \Top (H' \* \Top) (F (Q \*+ (H \* H')))). rew_heap.
hchanges (hwand_extend (H \* \Top) (H \* H' \* \Top) (F (Q \*+ (H \* H')))).
hchanges (
......@@ -3684,7 +3684,7 @@ Lemma regular_frame : forall H1 H2 F H Q,
H1 ==> F (fun x => H2 \--* Q x) ->
H ==> F Q.
Proof using.
introv R W M. applys~ regular_frame_top H1 H2. { hchanges W. }
introv R W M. applys~ regular_frame_top H1 H2. { hchanges W. }
Qed.
*)
......@@ -3695,14 +3695,14 @@ Lemma hpull_hforall : forall A H1 H2 H' (J:A->hprop),
(exists x, H1 \* J x \* H2 ==> H') ->
H1 \* (hforall J \* H2) ==> H'.
Proof using.
introv (x&M). rewrite hstar_comm_assoc.
introv (x&M). rewrite hstar_comm_assoc.
applys himpl_trans. applys hstar_hforall.
applys himpl_hforall_l. exists x.
rewrite~ <- hstar_comm_assoc.
Qed.
*)
(* partial support for hforall
(* partial support for hforall
Ltac hpull_step tt ::=
match goal with |- _ \* ?HN ==> _ =>
match HN with
......@@ -3735,7 +3735,7 @@ Qed.
Lemma weaken_formula_trans : forall (F1 F2:formula),
(forall H' Q', (H' ==> F1 Q') -> (H' ==> F2 Q')) ->
F1 ===> F2.
Proof using. introv M. intros Q. applys~ M (F1 Q). Qed.
Proof using. introv M. intros Q. applys~ M (F1 Q). Qed.
......@@ -3759,7 +3759,7 @@ Qed.
Definition sound_for' (t:trm) (F:formula) :=
forall Q, triple t (F Q) Q.
Lemma sound_for_eq_sound_for' :
Lemma sound_for_eq_sound_for' :
sound_for = sound_for'.
Proof using.
applys pred_ext_2. intros t f.
......@@ -3774,3 +3774,46 @@ Lemma sound_for'_local : forall t (F:formula),
Proof using. introv. rewrite <- sound_for_eq_sound_for'. applys sound_for_local. Qed.
(** Empty heap predicate, written [ \[] ]. *)
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
(** Separation Logic star, written [H1 \* H2]. *)
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
(** Notation for applying star to a post-condition,
written [Q \*+ H], short for [fun x => (Q x \* H)]. *)
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
(** Existential lifted to heap predicates,
written [Hexists x, H] *)
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
Notation "'Hexists' x1 , H" := (hexists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
(** Universal lifted to heap predicates
(currently, no notation provided) *)
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
Notation "'Hforall' x1 , H" := (hforall (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Parameter hforall : forall (A : Type) (J : A -> hprop), hprop.
Parameter hexists : forall A (J:A->hprop), hprop.
......@@ -29,40 +29,27 @@ Implicit Types k : field.
(* ********************************************************************** *)
(* * Construction of the logic *)
(* * Core of the logic *)
Module SepBasicCore.
(** All the definitions from this section are explained in the
[Module Type SepLogicCore], from file [SepFunctor.v]. *)
Module Export SepBasicCore <: SepCore.
(* ---------------------------------------------------------------------- *)
(* ** Types *)
(** Heaps *)
(** A heap is a state (a finite map from location to values)
as defined in [LambdaSemantics.v]. *)
Definition heap : Type := (state)%type.
(** A heap predicate, type [hprop] is a predicate over such heaps. *)
Definition hprop := heap -> Prop.
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
(* ---------------------------------------------------------------------- *)
(* ** Operations on heaps *)
(** For uniformity with other instantiations of the Separation Logic
functor, we introduce local names for operations and lemmas on heaps. *)
Definition heap_empty : heap := fmap_empty.
Notation "h1 \u h2" := (fmap_union h1 h2)
(at level 37, right associativity) : heap_scope.
(at level 37, right associativity) : heap_scope.
(* LATER: could try to introduce [heap_union := fmap_union] *)
Definition heap_union_empty_l := fmap_union_empty_l.
......@@ -70,11 +57,13 @@ Definition heap_union_empty_r := fmap_union_empty_r.
Definition heap_union_comm := fmap_union_comm_of_disjoint.
Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Operators *)
(** Hprop *)
(** A heap predicate, type [hprop] is a predicate over such heaps. *)
Definition hprop := heap -> Prop.
(** Empty heap predicate: [ \[] ] *)
......@@ -89,24 +78,15 @@ Definition hstar (H1 H2 : hprop) : hprop :=
/\ (\# h1 h2)
/\ h = h1 \+ h2.
(** Lifting of existentials: [Hexists x, H] *)
(** Quantifiers *)
Definition hexists A (J : A -> hprop) : hprop :=
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
(** Lifting of univerals *)
Definition hforall A (J : A -> hprop) : hprop :=
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(** The top heap predicate: [ \Top ], same as [Hexists H, H] *)
Definition htop :=
hexists (fun (H:hprop) => H).
(* ---------------------------------------------------------------------- *)
(* ** Notation *)
(** Notation *)
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
......@@ -117,9 +97,12 @@ Notation "H1 '\*' H2" := (hstar H1 H2)
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
Notation "\Top" := (htop) : heap_scope.
Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Types *)
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
(* ---------------------------------------------------------------------- *)
......@@ -131,7 +114,6 @@ Tactic Notation "fmap_disjoint_pre" :=
subst; rew_disjoint; jauto_set.
Hint Extern 1 (\# _ _) => fmap_disjoint_pre.
Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre.
(* ---------------------------------------------------------------------- *)
......@@ -148,19 +130,12 @@ Proof using. auto. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Properties of star *)
(* ** Core properties *)
Section Properties.
Hint Resolve hempty_intro.
Lemma hstar_intro : forall H1 H2 h1 h2,
H1 h1 ->
H2 h2 ->
\# h1 h2 ->
(H1 \* H2) (h1 \+ h2).
Proof using. intros. exists~ h1 h2. Qed.
Lemma hstar_hempty_l : forall H,
hempty \* H = H.
Proof using.
......@@ -188,10 +163,6 @@ Proof using.
exists (h1 \+ h2) h3. splits~. { exists* h1 h2. } }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Interaction of star with other operators *)
Lemma hstar_hexists : forall A (J:A->hprop) H,
(hexists J) \* H = hexists (fun x => (J x) \* H).
Proof using.
......@@ -200,7 +171,7 @@ Proof using.
{ destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
......@@ -217,15 +188,31 @@ End SepBasicCore.
(* ********************************************************************** *)
(* * Properties of the logic *)
(* ---------------------------------------------------------------------- *)
(* ** Functor instantiations *)
(* * Derived properties of the logic *)
(** Here, we instantiate the functors to obtained derived definitions,
lemmas, notation, and tactics. *)
Module Export SepBasicSetup := SepLogicSetup SepBasicCore.
Module Export SepBasicSetup := SepSetup SepBasicCore.
Export SepBasicCore.
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
(* ********************************************************************** *)
(* * Specific properties of the logic *)
(* ---------------------------------------------------------------------- *)
(* ** Auxiliary lemma for hstar *)
Lemma hstar_intro : forall H1 H2 h1 h2,
H1 h1 ->
H2 h2 ->
\# h1 h2 ->
(H1 \* H2) (h1 \+ h2).
Proof using. intros. exists~ h1 h2. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Singleton heap *)
......@@ -496,7 +483,7 @@ Lemma rule_extract_hwand_hpure_l : forall t (P:Prop) H Q,
triple t H Q ->
triple t (\[P] \--* H) Q.
Proof using.
introv HP M. intros HF h N.
introv HP M. intros HF h N.
lets N': hstar_hwand (rm N).
lets U: (conj (rm HP) (rm N')). rewrite <- hstar_pure in U.
lets U': hwand_cancel (rm U).
......@@ -780,8 +767,8 @@ Qed.
Lemma rule_for_trm : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v1, exists Q2,
triple t2 (Q1 v1) Q2
(forall v1, exists Q2,
triple t2 (Q1 v1) Q2
/\ (forall v2, triple (trm_for x v1 v2 t3) (Q2 v2) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using.
......@@ -802,9 +789,9 @@ Definition is_val_int (v:val) :=
Lemma rule_for_trm_int : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v, ~ is_val_int v -> (Q1 v) ==> \[False]) ->
(forall (n1:int), exists Q2,
triple t2 (Q1 (val_int n1)) Q2
/\ (forall v, ~ is_val_int v -> (Q2 v) ==> \[False])
(forall (n1:int), exists Q2,
triple t2 (Q1 (val_int n1)) Q2
/\ (forall v, ~ is_val_int v -> (Q2 v) ==> \[False])
/\ (forall (n2:int), triple (trm_for x n1 n2 t3) (Q2 (val_int n2)) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using. (* might be simplified using rule_for_trm *)
......@@ -977,6 +964,10 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Alternative, low-level definition of triples *)
Section TripleAlternative.
Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre.
Definition triple' t H Q :=
forall h1 h2,
\# h1 h2 ->
......@@ -1006,6 +997,8 @@ Proof using.
exists h3' h2. splits~. } }
Qed.
End TripleAlternative.
(* ---------------------------------------------------------------------- *)
(* ** Practical additional rules *)
......
......@@ -88,10 +88,12 @@ Qed.
End Redn.
(* ********************************************************************** *)
(* * Construction of core of the logic *)
(* * Core of the logic *)
Module Export SepCreditsCore <: SepCore.
Module SepCreditsCore.
(* ---------------------------------------------------------------------- *)
(* ** Representation of credits *)
......@@ -103,19 +105,16 @@ Definition credits : Type := nat.
(** Zero and one credits *)
Definition credits_zero : credits := 0%nat.
Definition credits_one : credits := 1%nat.
(* ---------------------------------------------------------------------- *)
(* ** Types *)
(** Heaps *)
Definition heap : Type := (state * credits)%type.
(** Type of heaps *)
Definition hprop := heap -> Prop.
(* ---------------------------------------------------------------------- *)
(* ** Operations on heaps *)
Definition heap : Type := (state * credits)%type.
(** Empty heap *)
......@@ -156,7 +155,13 @@ Notation "h1 \u h2" := (heap_union h1 h2)
(* ---------------------------------------------------------------------- *)
(* ** Operators *)
(** Hprop *)
(** Type of heap predicates *)
Definition hprop := heap -> Prop.
(** Heap predicates *)
Definition hempty : hprop :=
fun h => h = heap_empty.
......@@ -174,21 +179,23 @@ Definition hexists A (J : A -> hprop) : hprop :=
Definition hforall A (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
Definition htop :=
hexists (fun (H:hprop) => H).
(* ---------------------------------------------------------------------- *)
(* ** Notation *)
(** Notation *)
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
Notation "\Top" := (htop) : heap_scope.
Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Types *)
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
(* ---------------------------------------------------------------------- *)
......@@ -357,7 +364,7 @@ Proof using. auto. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Properties of star *)
(* ** Core properties *)
Section Properties.
......@@ -394,10 +401,6 @@ Proof using.
{ subst. applys heap_eq. split. { fmap_eq. } { simpl; math. } } }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Interaction of star with other operators *)
Lemma hstar_hexists : forall A (J:A->hprop) H,
(hexists J) \* H = hexists (fun x => (J x) \* H).
Proof using.
......@@ -406,7 +409,7 @@ Proof using.
{ destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
......@@ -422,11 +425,22 @@ End Properties.
End SepCreditsCore.
(* ********************************************************************** *)
(* * Properties of the logic *)
(* * Derived properties of the logic *)
Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore.
(** Here, we instantiate the functors to obtained derived definitions,
lemmas, notation, and tactics. *)
Module Export SepCreditsSetup := SepSetup SepCreditsCore.
Export SepCreditsCore.
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
(* ********************************************************************** *)
(* * Specific properties of the logic *)
(* ---------------------------------------------------------------------- *)
(* ** Singleton heap *)
......@@ -525,8 +539,6 @@ Ltac fmap_red_base tt ::=
Implicit Types t : trm.
Implicit Types v w : val.
Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
(* ---------------------------------------------------------------------- *)
......@@ -714,7 +726,7 @@ Proof using.
exists 0%nat ((m1' \+ h^s),h^c) (val_loc l). splits~.
{ applys~ red_ref. }
{ exists (m1',0%nat) h. split.
{ exists l. applys~ himpl_hprop_r. unfold m1'. hnfs~. }
{ exists l. applys~ himpl_hpure_r. unfold m1'. hnfs~. }
{ splits~. hhsimpl~. } }
Qed.
......
......@@ -2,12 +2,27 @@
Set Implicit Arguments.
From Sep Require Import LambdaSep SepGPM.
(* ---------------------------------------------------------------------- *)
(** Proof mode definitions for LambdaSep *)
Module ProofMode.
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicSetup.
(* ********************************************************************** *)
(* * Exposing [heap_empty] to GPM *)
Module SepBasicCoreHempty <: SepCoreHemptySig SepBasicCore.
Definition heap_empty := heap_empty.
Lemma hempty_eq : hempty = (fun h => h = heap_empty).
Proof using. auto. Qed.
End SepBasicCoreHempty.
(* ********************************************************************** *)
(* * Subset of the interface of SepLogicSetup that needs to be exposed to GPM *)
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicCoreHempty SepBasicSetup.
Export SepBasicGPM.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop :=
......@@ -38,5 +53,10 @@ Proof.
apply rule_htop_pre. iIntros "$".
Qed.
(* ********************************************************************** *)
End ProofMode.
......@@ -22,28 +22,19 @@ Arguments exist [A] [P].
(* ********************************************************************** *)
(* * Construction of core of the logic *)
(* * Core of the logic *)
Module SepROCore.
Module Export SepROCore <: SepCore.
(* ---------------------------------------------------------------------- *)
(* ** Types *)
(** Heaps *)
(** Representation of heaps as pairs *)
Definition heap : Type :=
{ h : (state*state)%type | let '(f,r) := h in fmap_disjoint f r }.
Definition hprop := heap -> Prop.
(* ---------------------------------------------------------------------- *)
(* ** Operations on heaps *)
(** Empty heap *)
Program Definition heap_empty : heap :=
(fmap_empty, fmap_empty).
(** Projections *)
Definition heap_f (h:heap) : state :=
......@@ -58,7 +49,18 @@ Notation "h '^f'" := (heap_f h)
Notation "h '^r'" := (heap_r h)
(at level 9, format "h '^r'") : heap_scope.
Open Scope heap_scope.
(** State of heap *)
Coercion heap_state (h : heap) : state :=
(h^f \+ h^r).
(** Empty *)
Program Definition heap_empty : heap :=
(fmap_empty, fmap_empty).
Global Instance heap_inhab : Inhab heap.
Proof using. applys Inhab_of_val heap_empty. Qed.
(** Starable heaps: disjoint owned heaps, agreeible read-only heaps *)
......@@ -72,9 +74,6 @@ Definition heap_compat (h1 h2 : heap) : Prop :=
We implement it using a classical logic test, so as to avoid
dependently-typed programming. *)
Global Instance heap_inhab : Inhab heap.
Proof using. applys Inhab_of_val heap_empty. Qed.
Program Definition heap_union (h1 h2 : heap) : heap :=
If (heap_compat h1 h2) then (h1^f \+ h2^f, h1^r \+ h2^r) else arbitrary.
Next Obligation.
......@@ -84,14 +83,15 @@ Qed.
Notation "h1 \u h2" := (heap_union h1 h2)
(at level 37, right associativity) : heap_scope.
(** State of heap *)
Coercion heap_state (h : heap) : state :=
(h^f \+ h^r).
(* ---------------------------------------------------------------------- *)
(** Hprop *)
(** Type of heap predicates *)
(* ---------------------------------------------------------------------- *)
(* ** Operators *)
Definition hprop := heap -> Prop.
(** Heap predicates *)
Definition hempty : hprop :=
fun h => h = heap_empty.
......@@ -103,27 +103,22 @@ Program Definition hstar (H1 H2 : hprop) : hprop :=
/\ heap_compat h1 h2
/\ h = h1 \u h2.
Definition hexists A (J : A -> hprop) : hprop :=
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
Definition hforall A (J : A -> hprop) : hprop :=
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
Definition htop :=
hexists (fun (H:hprop) => H).
(* ---------------------------------------------------------------------- *)
(* ** Notation *)
(** Notation *)
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
Notation "\Top" := (htop) : heap_scope.
Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
......@@ -151,6 +146,8 @@ Ltac fequal_base ::=
| |- _ => f_equal_fixed
end.
(* ---------------------------------------------------------------------- *)
(* ** Equalities on [heap] *)
......@@ -484,7 +481,7 @@ Proof using. introv M. auto. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Properties of star *)
(* ** Core properties *)
Section Properties.
......@@ -532,10 +529,6 @@ Proof using.
{ subst. symmetry. applys~ heap_union_assoc. } }
Qed.