diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v index b6128cb5a1a52c783be801496f9065b13855dcd9..ec27778846a13e362e0de1df5ad3108be36d690b 100644 --- a/theories/bi/derived_connectives.v +++ b/theories/bi/derived_connectives.v @@ -1,6 +1,5 @@ From iris.bi Require Export interface. From iris.algebra Require Import monoid. -From stdpp Require Import hlist. Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I. Arguments bi_iff {_} _%I _%I : simpl never. @@ -77,17 +76,6 @@ Instance: Params (@bi_intuitionistically_if) 2. Typeclasses Opaque bi_intuitionistically_if. Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope. -Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP := - match As return himpl As PROP → PROP with - | tnil => id - | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x) - end%I. -Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP := - match As return himpl As PROP → PROP with - | tnil => id - | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x) - end%I. - Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP := match n with | O => P diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v index b78d0fe7e99f1ee9e76a822b2a7e5452a7ab893d..f924a6f9b4a9b059759b34027b51d3b0038fbe9f 100644 --- a/theories/bi/derived_laws_bi.v +++ b/theories/bi/derived_laws_bi.v @@ -1,6 +1,5 @@ From iris.bi Require Export derived_connectives. From iris.algebra Require Import monoid. -From stdpp Require Import hlist. (** Naming schema for lemmas about modalities: M1_into_M2: M1 P ⊢ M2 P @@ -1449,31 +1448,6 @@ Global Instance bi_persistently_sep_entails_homomorphism : MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP). Proof. split. apply _. simpl. apply persistently_emp_intro. Qed. -(* Heterogeneous lists *) -Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → PROP) : - bi_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 → PROP) : - bi_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. - (* Limits *) Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) : NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x). @@ -1492,5 +1466,4 @@ 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 bi. diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v index 4201349f1703af21d348286ce1acc84704fd1a5a..89036d8abc4788a29b016b59e84bd6656667cc30 100644 --- a/theories/bi/embedding.v +++ b/theories/bi/embedding.v @@ -1,6 +1,5 @@ From iris.algebra Require Import monoid. From iris.bi Require Import interface derived_laws_sbi big_op plainly updates. -From stdpp Require Import hlist. Class Embed (A B : Type) := embed : A → B. Arguments embed {_ _ _} _%I : simpl never. @@ -189,13 +188,6 @@ Section embed. ⎡□?b P⎤ ⊣⊢ □?b ⎡P⎤. Proof. destruct b; simpl; auto using embed_intuitionistically. Qed. - Lemma embed_hforall {As} (Φ : himpl As PROP1): - ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ). - Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed. - Lemma embed_hexist {As} (Φ : himpl As PROP1): - ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose embed Φ). - Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed. - Global Instance embed_persistent P : Persistent P → Persistent ⎡P⎤. Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed. Global Instance embed_affine `{!BiEmbedEmp PROP1 PROP2} P : Affine P → Affine ⎡P⎤.