Commit 1d90abca authored by charguer's avatar charguer

tactics1

parent 1c8dabf6
......@@ -10,8 +10,196 @@ License: MIT.
*)
Require Import LibTactics Shared LibOperation LibStruct.
(********************************************************************)
(** * Structure *)
(*------------------------------------------------------------------*)
(* ** Operators of a Separation Logic *)
Module SepLogicOps.
Record SepLogicOps (heap : Type) :=
make_SepLogicOps {
(* let hprop := heap -> Prop in *)
pure : Prop -> (heap->Prop);
star : (heap->Prop) -> (heap->Prop) -> (heap->Prop);
exist : forall {A}, A -> (heap->Prop);
gc : (heap->Prop);
}.
Implicit Arguments pure [heap].
Implicit Arguments star [heap].
Implicit Arguments exist [heap A].
Implicit Arguments gc [heap].
End SepLogicOps.
(*------------------------------------------------------------------*)
(* ** Properties of a Separation Logic *)
Module SepLogicProp.
Export SepLogicOps.
Section Def.
Variables (heap : Type) (S : @SepLogicOps heap).
Local Notation "H1 '\*' H2" := (star S H1 H2)
(at level 41, right associativity).
Definition hprop := heap -> Prop.
Definition empty := pure S True.
Record SepLogicProp := make_SepLogicProp {
star_neutral_l : neutral_l (star S) empty;
star_comm : comm (star S);
star_assoc : assoc (star S);
star_exists : forall A (J:A->hprop) H,
H \* (exist S J) = exist S (fun x => H \* (J x));
extract_prop : forall H (P:Prop) H',
(P -> (H ==> H')) ->
H \* (pure S P) ==> H';
extract_exists : forall A (J:A->hprop) H',
(forall x, (J x ==> H')) ->
exist S J ==> H';
}.
End Def.
Implicit Arguments make_SepLogicProp [heap].
Implicit Arguments SepLogicProp [heap].
End SepLogicProp.
(*------------------------------------------------------------------*)
(* ** Package of a Separation Logic *)
Module SepLogic.
Export SepLogicProp.
Record SepLogic := make_SepLogic {
heap : Type;
ops :> SepLogicOps heap;
prop : SepLogicProp ops; }.
Implicit Arguments make_SepLogic [heap ops].
End SepLogic.
(********************************************************************)
(** * Derived definitions *)
Module Type SepLogicArg.
Import SepLogic.
Parameter S : SepLogic.
End SepLogicArg.
(*---*)
Module SepLogicSetup (SL:SepLogicArg).
Import SepLogic SL.
Hint Extern 1 (SepLogicProp (ops S)) => apply (prop SL.S).
(*------------------------------------------------------------------*)
(* ** Notation *)
Notation "'heap'" := (heap S).
Definition hprop := heap -> Prop.
Definition empty := pure S True.
Notation "\[ L ]" := (pure S L)
(at level 0, L at level 99) : heap_scope.
Notation "\[]" := (empty)
(at level 0) : heap_scope.
Notation "H1 '\*' H2" := (star S H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => star S (Q x) H)
(at level 40) : heap_scope.
Notation "'Hexists' x1 , H" := (exist S (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (exist S (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (exist S (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "\GC" := (gc S) : heap_scope.
(*
Notation "r '~~>' v" := (hprop_single r v)
(at level 32, no associativity) : heap_scope.
*)
Lemma star_neutral_r : neutral_r (star S) empty.
Proof using.
applys neutral_r_from_comm_neutral_l.
applys~ star_comm.
applys~ star_neutral_l.
Qed.
End SepLogicSetup.
(********************************************************************)
(** * Demo *)
Module MySepLogic : SepLogicArg.
Export SepLogic.
Parameter heap : Type.
Parameter ops : SepLogicOps heap.
Parameter prop : SepLogicProp ops.
Definition S := make_SepLogic prop.
End MySepLogic.
Module MySepLogicSetup.
Import SepLogic.
Module Import SLS := SepLogicSetup MySepLogic.
Open Scope heap_scope.
Lemma demo1 : \[] = \[] :> hprop.
Proof using. auto. Qed.
Lemma demo2 : forall (H:hprop), H \* \[] = H.
Proof using. applys star_neutral_r. Qed.
End MySepLogicSetup.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
(*------------------------------------------------------------------*)
(* ** Separation Logic monoid *)
......@@ -752,3 +940,6 @@ Tactic Notation "hchange" constr(E1) constr(E2) :=
hchange E1; hchange E2.
Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) :=
hchange E1; hchange E2 E3.
*)
\ No newline at end of file
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