algebra/dec_agree.v

-From iris.algebra Require Export cmra.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
-
-(* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
-  | DecAgree : A → dec_agree A
-  | DecAgreeBot : dec_agree A.
-Arguments DecAgree {_} _.
-Arguments DecAgreeBot {_}.
-Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
-  match x with DecAgree a => Some a | _ => None end.
-
-Section dec_agree.
-Context `{EqDecision A}.
-Implicit Types a b : A.
-Implicit Types x y : dec_agree A.
-
-Instance dec_agree_valid : Valid (dec_agree A) := λ x,
-  if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
-
-Instance dec_agree_op : Op (dec_agree A) := λ x y,
-  match x, y with
-  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
-  | _, _ => DecAgreeBot
-  end.
-Instance dec_agree_pcore : PCore (dec_agree A) := Some.
-
-Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
-Proof.
-  apply ra_total_mixin; apply _ || eauto.
-  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - by intros [?|] [?|] ?.
-Qed.
-
-Canonical Structure dec_agreeR : cmraT :=
-  discreteR (dec_agree A) dec_agree_ra_mixin.
-
-Global Instance dec_agree_total : CMRATotal dec_agreeR.
-Proof. intros x. by exists x. Qed.
-
-(* Some properties of this CMRA *)
-Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
-Proof. by constructor. Qed.
-
-Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
-Proof. intros. by rewrite /= decide_False. Qed.
-
-Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x = x.
-Proof. destruct x; by rewrite /= ?decide_True. Qed.
-
-Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
-Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-
-Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b ↔ a = b.
-Proof.
-  split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
-Qed.
-End dec_agree.
-
-Arguments dec_agreeC : clear implicits.
-Arguments dec_agreeR _ {_}.

algebra/deprecated.v

-From iris.algebra Require Import ofe.
-
-(* Old notation for backwards compatibility. *)
-
-(* Deprecated 2016-11-22. Use ofeT instead. *)
-Notation cofeT := ofeT (only parsing).

algebra/frac.v

-From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export cmra.
-
-Notation frac := Qp (only parsing).
-
-Section frac.
-Canonical Structure fracC := leibnizC frac.
-
-Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
-Instance frac_pcore : PCore frac := λ _, None.
-Instance frac_op : Op frac := λ x y, (x + y)%Qp.
-
-Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc.
-Proof.
-  split.
-  - intros [z ->%leibniz_equiv]; simpl.
-    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
-    by rewrite (Qcplus_comm y) Qcplus_assoc Qcplus_opp_r Qcplus_0_l.
-Qed.
-Corollary frac_included_weak (x y : frac) : x ≼ y → (x ≤ y)%Qc.
-Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
-
-Definition frac_ra_mixin : RAMixin frac.
-Proof.
-  split; try apply _; try done.
-  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
-  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
-Qed.
-Canonical Structure fracR := discreteR frac frac_ra_mixin.
-End frac.
-
-(** Exclusive *)
-Global Instance frac_full_exclusive : Exclusive 1%Qp.
-Proof.
-  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
-Qed.
-
-Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
-Proof. done. Qed.

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 internal_eq_refl' : I.

base_logic/deprecated.v

-From iris.base_logic Require Import primitive.
-
-(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
-Notation "■ φ" := (uPred_pure φ%C%type)
-    (at level 20, right associativity, only parsing) : uPred_scope.
-
-(* Deprecated 2016-11-22. Use ⌜x = y⌝ instead. *)
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_scope.
-
-(* Deprecated 2016-11-22. Use ⌜x ⊥ y ⌝ instead. *)
-Notation "x ⊥ y" := (uPred_pure (x%C%type ⊥ y%C%type)) (only parsing) : uPred_scope.

base_logic/hlist.v

-From iris.prelude Require Export hlist.
-From iris.base_logic Require Export base_logic.
-Import uPred.
-
-Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∃ x, uPred_hexist (Φ x)
-  end%I.
-Fixpoint uPred_hforall {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∀ x, uPred_hforall (Φ x)
-  end%I.
-
-Section hlist.
-Context {M : ucmraT}.
-
-Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hexist (hcompose Φ f) ⊣⊢ ∃ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - induction As as [|A As IH]; simpl.
-    + by rewrite -(exist_intro hnil) .
-    + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
-      by rewrite -(exist_intro (hcons x xs)).
-  - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite -(exist_intro x) IH.
-Qed.
-
-Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hforall (hcompose Φ f) ⊣⊢ ∀ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite (forall_elim x) IH.
-  - induction As as [|A As IH]; simpl.
-    + by rewrite (forall_elim hnil) .
-    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
-      by rewrite (forall_elim (hcons x xs)).
-Qed.
-End hlist.