Move base_logic stuff to its own folder: base_logic.

_CoqProject

@@ -51,10 +51,6 @@ algebra/agree.v
 algebra/dec_agree.v
 algebra/excl.v
 algebra/iprod.v
-algebra/upred.v
-algebra/upred_tactics.v
-algebra/upred_big_op.v
-algebra/upred_hlist.v
 algebra/frac.v
 algebra/csum.v
 algebra/list.v
@@ -62,7 +58,15 @@ algebra/updates.v
 algebra/local_updates.v
 algebra/gset.v
 algebra/coPset.v
-algebra/double_negation.v
+base_logic/upred.v
+base_logic/primitive.v
+base_logic/derived.v
+base_logic/base_logic.v
+base_logic/tactics.v
+base_logic/big_op.v
+base_logic/hlist.v
+base_logic/soundness.v
+base_logic/double_negation.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v

algebra/agree.v

 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {

algebra/auth.v

 From iris.algebra Require Export excl local_updates.
-From iris.algebra Require Import upred updates.
+From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import class_instances.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.

algebra/csum.v

 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred updates local_updates.
+From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import local_updates.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.

algebra/excl.v

 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 

algebra/gmap.v

 From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
-From iris.algebra Require Import upred updates local_updates.
+From iris.algebra Require Import updates local_updates.
+From iris.base_logic Require Import base_logic.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.

algebra/iprod.v

-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.base_logic Require Import base_logic.
 From iris.prelude Require Import finite.
 
 (** * Indexed product *)

algebra/list.v

 From iris.algebra Require Export cmra.
 From iris.prelude Require Export list.
-From iris.algebra Require Import upred updates local_updates.
+From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates local_updates.
 
 Section cofe.
 Context {A : cofeT}.

base_logic/base_logic.v

+From iris.base_logic Require Export derived.
+
+Module uPred.
+  Include uPred_entails.
+  Include uPred_primitive.
+  Include uPred_derived.
+End uPred.
+
+(* Hint DB for the logic *)
+Import uPred.
+Hint Resolve pure_intro.
+Hint Resolve or_elim or_intro_l' or_intro_r' : I.
+Hint Resolve and_intro and_elim_l' and_elim_r' : I.
+Hint Resolve always_mono : I.
+Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
+Hint Immediate True_intro False_elim : I.
+Hint Immediate iff_refl eq_refl' : I.

algebra/upred_big_op.v → base_logic/big_op.v

-From iris.algebra Require Export upred list cmra_big_op.
+From iris.algebra Require Export list cmra_big_op.
+From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import gmap fin_collections functions.
 Import uPred.
 
+(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
+CMRA structure on uPred. *)
+Section cmra.
+  Context {M : ucmraT}.
+
+  Instance uPred_valid : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x.
+  Instance uPred_validN : ValidN (uPred M) := λ n P,
+    ∀ n' x, n' ≤ n → ✓{n'} x → P n' x.
+  Instance uPred_op : Op (uPred M) := uPred_sep.
+  Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.
+
+  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
+  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
+
+  Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I.
+  Proof.
+    unseal=> HP; split=> n' x ??; split; [done|].
+    intros _. by apply HP.
+  Qed.
+
+  Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ★ Q)%I → ✓{n} P.
+  Proof.
+    unseal. intros HPQ n' x ??.
+    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
+    eapply uPred_mono with x1; eauto using cmra_includedN_l.
+  Qed.
+
+  Lemma uPred_included P Q : P ≼ Q → Q ⊢ P.
+  Proof. intros [P' ->]. apply sep_elim_l. Qed.
+
+  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
+  Proof.
+    apply cmra_total_mixin; try apply _ || by eauto.
+    - intros n P Q ??. by cofe_subst.
+    - intros P; split.
+      + intros HP n n' x ?. apply HP.
+      + intros HP n x. by apply (HP n).
+    - intros n P HP n' x ?. apply HP; auto.
+    - intros P. by rewrite left_id.
+    - intros P Q _. exists True%I. by rewrite left_id.
+    - intros n P Q. apply uPred_cmra_validN_op_l.
+    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
+      + by rewrite left_id.
+      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
+      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
+        by rewrite left_id.
+  Qed.
+
+  Canonical Structure uPredR :=
+    CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin.
+
+  Instance uPred_empty : Empty (uPred M) := True%I.
+
+  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
+  Proof.
+    split; last done.
+    - by rewrite /empty /uPred_empty uPred_pure_eq.
+    - intros P. by rewrite left_id.
+  Qed.
+
+  Canonical Structure uPredUR :=
+    UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
+
+  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
+  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
+  Global Instance uPred_always_if_homomorphism b :
+    UCMRAHomomorphism (uPred_always_if b).
+  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
+  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
+  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+  Global Instance uPred_except_0_homomorphism :
+    CMRAHomomorphism uPred_except_0.
+  Proof. split. apply _. apply except_0_sep. Qed.
+  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
+  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
+End cmra.
+
+Arguments uPredR : clear implicits.
+Arguments uPredUR : clear implicits.
+
+(* Notations *)
 Notation "'[★]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
 
 Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))

algebra/double_negation.v → base_logic/double_negation.v

-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Import upred.
 
 (* In this file we show that the bupd can be thought of a kind of

algebra/upred_hlist.v → base_logic/hlist.v

 From iris.prelude Require Export hlist.
-From iris.algebra Require Export upred.
+From iris.base_logic Require Export base_logic.
 Import uPred.
 
 Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=

base_logic/soundness.v

+From iris.base_logic Require Export primitive.
+Import uPred_entails uPred_primitive.
+
+Section adequacy.
+Context {M : ucmraT}.
+
+(** Consistency and adequancy statements *)
+Lemma soundness φ n : (True ⊢ Nat.iter n (λ P, |==> ▷ P) (@uPred_pure M φ)) → φ.
+Proof.
+  cut (∀ x, ✓{n} x → Nat.iter n (λ P, |==> ▷ P)%I (@uPred_pure M φ) n x → φ).
+  { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
+    eapply H; try unseal; by eauto using ucmra_unit_validN. }
+  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
+  destruct (Hupd (S n) ∅) as (x'&?&?); rewrite ?right_id; auto.
+  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
+Qed.
+
+Corollary consistency_modal n :
+  ¬ (True ⊢ Nat.iter n (λ P, |==> ▷ P) (False : uPred M)).
+Proof. exact (soundness False n). Qed.
+
+Corollary consistency : ¬ (True ⊢ False : uPred M).
+Proof. exact (consistency_modal 0). Qed.
+End adequacy.

algebra/upred_tactics.v → base_logic/tactics.v

 From iris.prelude Require Import gmap.
-From iris.algebra Require Export upred.
-From iris.algebra Require Export upred_big_op.
+From iris.base_logic Require Export base_logic big_op.
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.

base_logic/upred.v

+From iris.algebra Require Export cmra.
+
+Record uPred (M : ucmraT) : Type := IProp {
+  uPred_holds :> nat → M → Prop;
+  uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
+  uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
+}.
+Arguments uPred_holds {_} _ _ _ : simpl never.
+Add Printing Constructor uPred.
+Instance: Params (@uPred_holds) 3.
+
+Delimit Scope uPred_scope with I.
+Bind Scope uPred_scope with uPred.
+Arguments uPred_holds {_} _%I _ _.
+
+Section cofe.
+  Context {M : ucmraT}.
+
+  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
+    { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
+  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
+  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
+    { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
+  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
+  Program Instance uPred_compl : Compl (uPred M) := λ c,
+    {| uPred_holds n x := c n n x |}.
+  Next Obligation. naive_solver eauto using uPred_mono. Qed.
+  Next Obligation.
+    intros c n1 n2 x ???; simpl in *.
+    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
+  Qed.
+  Definition uPred_cofe_mixin : CofeMixin (uPred M).
+  Proof.
+    split.
+    - intros P Q; split.
+      + by intros HPQ n; split=> i x ??; apply HPQ.
+      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
+    - intros n; split.
+      + by intros P; split=> x i.
+      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+      + intros P Q Q' HP HQ; split=> i x ??.
+        by trans (Q i x);[apply HP|apply HQ].
+    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
+    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
+  Qed.
+  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
+End cofe.
+Arguments uPredC : clear implicits.
+
+Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Proof.
+  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
+Qed.
+Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
+Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
+
+Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
+  P ≡{n2}≡ Q → n2 ≤ n1 → ✓{n2} x → Q n1 x → P n2 x.
+Proof.
+  intros [Hne] ???. eapply Hne; try done.
+  eapply uPred_closed; eauto using cmra_validN_le.
+Qed.
+
+(** functor *)
+Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} (P : uPred M1) :
+  uPred M2 := {| uPred_holds n x := P n (f x) |}.
+Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
+Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
+
+Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
+Proof.
+  intros x1 x2 Hx; split=> n' y ??.
+  split; apply Hx; auto using cmra_monotone_validN.
+Qed.
+Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
+Proof. by split=> n x ?. Qed.
+Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
+  uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
+Proof. by split=> n x Hx. Qed.
+Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
+Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
+  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
+Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
+    `{!CMRAMonotone f, !CMRAMonotone g} n :
+  f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
+Proof.
+  by intros Hfg P; split=> n' y ??;
+    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
+Qed.
+
+Program Definition uPredCF (F : urFunctor) : cFunctor := {|
+  cFunctor_car A B := uPredC (urFunctor_car F B A);
+  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
+Qed.
+Next Obligation.
+  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
+  apply uPred_map_ext=>y. by rewrite urFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
+  apply uPred_map_ext=>y; apply urFunctor_compose.
+Qed.
+
+Instance uPredCF_contractive F :
+  urFunctorContractive F → cFunctorContractive (uPredCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
+Qed.
+
+(** logical entailement *)
+Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
+  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
+Hint Extern 0 (uPred_entails _ _) => reflexivity.
+Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
+
+Hint Resolve uPred_mono uPred_closed : uPred_def.
+
+(** Notations *)
+Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
+  (at level 99, Q at level 200, right associativity) : C_scope.
+Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
+  (at level 95, no associativity) : C_scope.
+Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
+
+Module uPred_entails.
+Section entails.
+Context {M : ucmraT}.
+Implicit Types P Q : uPred M.
+
+Global Instance: PreOrder (@uPred_entails M).
+Proof.
+  split.
+  - by intros P; split=> x i.
+  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+Qed.
+Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
+Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+
+Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+Proof.
+  split; [|by intros [??]; apply (anti_symm (⊢))].
+  intros HPQ; split; split=> x i; apply HPQ.
+Qed.
+Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
+Proof. apply equiv_spec. Qed.
+Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
+Proof. apply equiv_spec. Qed.
+Global Instance entails_proper :
+  Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation (uPred M)).
+Proof.
+  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
+  - by trans P1; [|trans Q1].
+  - by trans P2; [|trans Q2].
+Qed.
+Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
+Proof. by intros ->. Qed.
+Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
+Proof. by intros ? <-. Qed.
+End entails.
+End uPred_entails.

heap_lang/lib/barrier/proof.v

@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.prelude Require Import functions.
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import saved_prop sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.

program_logic/adequacy.v

 From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic Require Import big_op soundness.
 From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -144,12 +145,12 @@ Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
-    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(?&?&?&Hσ)".
     iUpdIntro. iNext. iApply wptp_result; eauto.
     iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
-    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
     iUpdIntro. iNext. iApply wptp_safe; eauto.
     iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
@@ -162,7 +163,7 @@ Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
   φ σ2.
 Proof.
   intros Hwp HI [n ?]%rtc_nsteps.
-  eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+  eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
   rewrite Nat_iter_S. iUpd (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
   rewrite fupd_eq in Hwp.
   iUpd (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.

program_logic/auth.v

 From iris.program_logic Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 Import uPred.