Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move separation-logic basics into coqutil. #441

Merged
merged 2 commits into from
Jan 5, 2025
Merged

Move separation-logic basics into coqutil. #441

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
43a4a87
Bump coqutil
jadephilipoom Jan 4, 2025
21043ce
Replace separation logic base library with references to coqutil.
jadephilipoom Dec 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions bedrock2/src/bedrock2/HeapletwiseHyps.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1024,7 +1024,7 @@ Ltac start_canceling :=
let clausetree := reify (sep P Q) in change (Tree.to_sep clausetree m);
eapply (canceling_start_noand D)
end;
cbn [Tree.flatten Tree.interp bedrock2.Map.SeparationLogic.app].
cbn [Tree.flatten Tree.interp coqutil.Map.SeparationLogic.app].

Ltac path_in_mem_tree om m :=
lazymatch om with
Expand Down Expand Up @@ -1253,7 +1253,7 @@ Ltac start_canceling_in_hyp H :=
clear D;
cbn [SeparationLogic.Tree.flatten
SeparationLogic.Tree.interp
bedrock2.Map.SeparationLogic.app] in H
coqutil.Map.SeparationLogic.app] in H
end
end.

Expand Down
29 changes: 1 addition & 28 deletions bedrock2/src/bedrock2/Lift1Prop.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,28 +1 @@
Require Import Coq.Classes.Morphisms.

Section Binary.
Context {T: Type} (P Q: T -> Prop).
Definition impl1 := forall x, P x -> Q x.
Definition iff1 := forall x, P x <-> Q x.
Definition and1 := fun x => P x /\ Q x.
Definition or1 := fun x => P x \/ Q x.
End Binary.

Definition ex1 {A B} (P : A -> B -> Prop) := fun (b:B) => exists a:A, P a b.

Global Instance Transitive_impl1 T : Transitive (@impl1 T). firstorder idtac. Qed.
Global Instance Reflexive_impl1 T : Reflexive (@impl1 T). firstorder idtac. Qed.
Global Instance Proper_impl1_impl1 T : Proper (Basics.flip impl1 ==> impl1 ==> Basics.impl) (@impl1 T). firstorder idtac. Qed.
Global Instance subrelation_iff1_impl1 T : subrelation (@iff1 T) (@impl1 T). firstorder idtac. Qed.
Global Instance Equivalence_iff1 T : Equivalence (@iff1 T). firstorder idtac. Qed.
Global Instance Proper_iff1_iff1 T : Proper (iff1 ==> iff1 ==> iff) (@iff1 T). firstorder idtac. Qed.
Global Instance Proper_iff1_impl1 T : Proper (Basics.flip impl1 ==> impl1 ==> Basics.impl) (@impl1 T). firstorder idtac. Qed.
Global Instance Proper_impl1_iff1 T : Proper (iff1 ==> iff1 ==> iff) (@impl1 T). firstorder idtac. Qed.
Global Instance Proper_ex1_iff1 A B : Proper (pointwise_relation _ iff1 ==> iff1) (@ex1 A B). firstorder idtac. Qed.
Global Instance Proper_ex1_impl1 A B : Proper (pointwise_relation _ impl1 ==> impl1) (@ex1 A B). firstorder idtac. Qed.
Global Instance iff1_rewrite_relation T : RewriteRelation (@iff1 T) := {}.

Lemma impl1_ex1_l {A B} p q : impl1 (@ex1 A B p) q <-> (forall x, impl1 (p x) q).
Proof. firstorder idtac. Qed.
Lemma impl1_ex1_r {A B} p q x : impl1 p (q x) -> impl1 p (@ex1 A B q).
Proof. firstorder idtac. Qed.
Require Export coqutil.Lift1Prop.
25 changes: 1 addition & 24 deletions bedrock2/src/bedrock2/Map/Separation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,24 +1 @@
Require Import coqutil.Map.Interface bedrock2.Lift1Prop. Import map.

Section Sep.
Context {key value} {map : map key value}.
Definition emp (P : Prop) := fun m : map => m = empty /\ P.
Definition sep (p q : map -> Prop) m :=
exists mp mq, split m mp mq /\ p mp /\ q mq.
Definition ptsto k v := fun m : map => m = put empty k v.
Definition read k (P : value -> rep -> Prop) := (ex1 (fun v => sep (ptsto k v) (P v))).

Fixpoint seps (xs : list (rep -> Prop)) : rep -> Prop :=
match xs with
| cons x nil => x
| cons x xs => sep x (seps xs)
| nil => emp True
end.
End Sep.

Declare Scope sep_scope.
Delimit Scope sep_scope with sep.
Infix "*" := sep (at level 40, left associativity) : sep_scope.
Infix "⋆" := sep (at level 40, left associativity) : sep_scope.
Notation "m =* P" := ((P%sep) m) (at level 70, only parsing).
Notation "m =*> P" := (exists R, (sep P R) m) (at level 70, only parsing).
Require Export coqutil.Map.Separation.
Loading
Loading