Commit 15ce289f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `derived_laws_bi` → `derived_laws` and `derived_laws_sbi` → `derived_laws_later`.

parent 76bec8b7
......@@ -44,8 +44,8 @@ theories/si_logic/bi.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws_bi.v
theories/bi/derived_laws_sbi.v
theories/bi/derived_laws.v
theories/bi/derived_laws_later.v
theories/bi/plainly.v
theories/bi/internal_eq.v
theories/bi/big_op.v
......
From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op.
From iris.bi Require Export derived_laws derived_laws_later big_op.
From iris.bi Require Export updates internal_eq plainly embedding.
Set Default Proof Using "Type".
Module Import bi.
Export bi.interface.bi.
Export bi.derived_laws_bi.bi.
Export bi.derived_laws_sbi.bi.
Export bi.derived_laws.bi.
Export bi.derived_laws_later.bi.
End bi.
From stdpp Require Import countable fin_sets functions.
From iris.bi Require Import derived_laws_sbi.
From iris.bi Require Import derived_laws_later.
From iris.algebra Require Export big_op.
Set Default Proof Using "Type".
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(** Notations for unary variants *)
Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
......
......@@ -119,7 +119,7 @@ Notation "mP -∗? Q" := (bi_wandM mP Q)
(** This class is required for the [iLöb] tactic. For most logics this class
should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
in [derived_laws_sbi] should be used. A direct instance of the class is useful
in [derived_laws_later] should be used. A direct instance of the class is useful
when considering a BI logic with a discrete OFE, instead of a OFE that takes
step-indexing of the logic in account.*)
Class BiLöb (PROP : bi) :=
......
......@@ -10,7 +10,7 @@ From iris.algebra Require Import monoid.
Module bi.
Import interface.bi.
Section bi_derived.
Section derived.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
......@@ -1551,5 +1551,5 @@ Qed.
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A PROP) :
NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
End bi_derived.
End derived.
End bi.
From iris.bi Require Export derived_laws_bi.
From iris.bi Require Export derived_laws.
From iris.algebra Require Import monoid.
Module bi.
Import interface.bi.
Import derived_laws_bi.bi.
Section sbi_derived.
Import derived_laws.bi.
Section later_derived.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
......@@ -398,5 +399,5 @@ Proof. split; try apply _. apply laterN_intro. Qed.
Global Instance bi_except_0_sep_entails_homomorphism :
MonoidHomomorphism bi_sep bi_sep (flip ()) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_intro. Qed.
End sbi_derived.
End later_derived.
End bi.
From iris.bi Require Import interface derived_laws_sbi big_op.
From iris.bi Require Import interface derived_laws_later big_op.
From iris.bi Require Import plainly updates internal_eq.
From iris.algebra Require Import monoid.
......
......@@ -121,7 +121,7 @@ Section bi_mixin.
identity function, as the Löb axiom or contractiveness of later is not part of
[BiLaterMixin]. For step-indexed BIs one should separately prove an instance
of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
instance [Contractive (▷) → BiLöb PROP] in [derived_laws_later].)
For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
the smart constructor [bi_later_mixin_id] below. *)
......
From iris.bi Require Import derived_laws_sbi big_op.
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
From iris.bi Require Import derived_laws_later big_op.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(** This file defines a type class for BIs with a notion of internal equality.
Internal equality is not part of the [bi] canonical structure as [internal_eq]
......
From iris.bi Require Import derived_laws_sbi big_op internal_eq.
From iris.bi Require Import derived_laws_later big_op internal_eq.
From iris.algebra Require Import monoid.
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
Import interface.bi derived_laws.bi derived_laws_later.bi.
Class Plainly (A : Type) := plainly : A A.
Hint Mode Plainly ! : typeclass_instances.
......
From stdpp Require Import coPset.
From iris.bi Require Import interface derived_laws_sbi big_op plainly.
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
From iris.bi Require Import interface derived_laws_later big_op plainly.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
......
Supports Markdown
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