Commit 7177cd8d authored by Robbert Krebbers's avatar Robbert Krebbers

Remove `bi_hforall` and `bi_hexist`, these are superseded by the telescoped versions.

parent 220e7379
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
......
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.
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.
......
Markdown is supported
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