Replace separation logic base library with references to coqutil.

bedrock2/src/bedrock2/HeapletwiseHyps.v

@@ -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
@@ -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.
 

bedrock2/src/bedrock2/Lift1Prop.v

@@ -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.

bedrock2/src/bedrock2/Map/Separation.v

@@ -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.