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

Cleanup SepLogic: move [hpure] in SepLogicSetup, define hand, hor hwand and...

Cleanup SepLogic: move [hpure] in SepLogicSetup, define hand, hor hwand and hforall in SepLogicSetup, and avoid exporting SepLogicSetup when SepLogicTactics is already exported.
parent 057e0274
......@@ -95,11 +95,6 @@ Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
(** Lifting of pure predicates: [ \[P] ] *)
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
(** The top heap predicate: [ \Top ], same as [Hexists H, H] *)
Definition htop :=
......@@ -112,9 +107,6 @@ Definition htop :=
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
......@@ -250,7 +242,6 @@ End SepBasicCore.
(** Here, we instantiate the functors to obtained derived definitions,
lemmas, notation, and tactics. *)
Module Export SepBasicSetup := SepLogicSetup SepBasicCore.
Module Export SepBasicTactics := SepLogicTactics SepBasicCore.
......
......@@ -171,9 +171,6 @@ Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Definition htop :=
hexists (fun (H:hprop) => H).
......@@ -183,8 +180,6 @@ Definition htop :=
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99) : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
......@@ -446,7 +441,6 @@ End SepCreditsCore.
(* ********************************************************************** *)
(* * Properties of the logic *)
Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore.
Module Export SepCreditsTactics := SepLogicTactics SepCreditsCore.
......
......@@ -121,9 +121,6 @@ Program Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Definition htop :=
hexists (fun (H:hprop) => H).
......@@ -133,8 +130,6 @@ Definition htop :=
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99) : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
......@@ -588,7 +583,6 @@ End SepROCore.
(* ********************************************************************** *)
(* * Properties of the logic *)
Module Export SepROSetup := SepLogicSetup SepROCore.
Module Export SepROTactics := SepLogicTactics SepROCore.
......
......@@ -183,18 +183,6 @@ Notation "Q \*+ H" := (fun x => hstar (Q x) H)
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
(** Pure propositions lifted to heap predicates,
written [ \[P] ].
Remark: the definition below is equivalent to
[fun h => (hempty h /\ P)]. *)
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** The "Top" predicate, written [\Top], which holds of any heap,
implemented as [Hexists H, H]. *)
......@@ -203,28 +191,6 @@ Definition htop : hprop :=
Notation "\Top" := (htop) : heap_scope.
(* Remark: disjunction on heap predicates is not needed in practice,
because we use pattern matching and conditional construct from the
logic. If we wanted, we could define it as follows:
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
*)
(* Remark: non-separating conjunction is not defined, because we
never need it. If we wanted, we could define it as follows:
Definition hand (H1 H2 : hprop) : hprop :=
fun h => H1 h /\ H2 h.
*)
(* Remark: magic wand construct is not defined here, because we
rarely need it. If we wanted, we could define it as follows:
Definition hwand (H1 H2 : hprop) : hprop :=
Hexists H, (H \* [H \* H1 ==> H2]).
*)
Open Scope heap_scope.
......@@ -286,6 +252,41 @@ Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types P : Prop.
(* ---------------------------------------------------------------------- *)
(* ** Additional connectives *)
(** Pure propositions lifted to heap predicates,
written [ \[P] ].
Remark: the definition below is equivalent to
[fun h => (hempty h /\ P)]. *)
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** Disjunction *)
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
(** Non-separating conjunction *)
Definition hand (H1 H2 : hprop) : hprop :=
fun h => H1 h /\ H2 h.
(** Magic wand *)
Definition hwand (H1 H2 : hprop) : hprop :=
hexists (fun (H:hprop) => H \* (hpure (H \* H1 ==> H2))).
(** Forall *)
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(* ---------------------------------------------------------------------- *)
(* ** Additional notation for entailment *)
......
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