Commit 00d2fb63 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Ensure that different `Cofe` proofs of `iProp` are convertible.

parent 8fa39f7c
Pipeline #64440 passed with stage
in 13 minutes and 49 seconds
......@@ -181,7 +181,7 @@ Structure bi := Bi {
bi_persistently : bi_car bi_car;
bi_later : bi_car bi_car;
bi_ofe_mixin : OfeMixin bi_car;
bi_cofe : Cofe (Ofe bi_car bi_ofe_mixin);
bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently;
bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
......@@ -191,8 +191,12 @@ Bind Scope bi_scope with bi_car.
Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
Global Instance bi_cofe' (PROP : bi) : Cofe PROP.
Proof. apply bi_cofe. Qed.
(** The projection [bi_cofe_aux] is not registered as an instance because it has
the wrong type. Its result type is unfolded, i.e., [Cofe (Ofe PROP ...)], and
thus should never be used. The instance [bi_cofe] has the proper result type
[Cofe (bi_ofeO PROP)]. *)
Global Instance bi_cofe (PROP : bi) : Cofe PROP := bi_cofe_aux PROP.
Global Instance: Params (@bi_entails) 1 := {}.
Global Instance: Params (@bi_emp) 1 := {}.
......@@ -17,3 +17,8 @@ Definition foo :=
(sigT (A:=Type -> Type)).
From iris.base_logic Require Import iprop.
Lemma bi_ofeO_iProp Σ : bi_ofeO (iPropI Σ) = iPropO Σ.
Proof. reflexivity. Qed.
Lemma bi_cofe_iProp Σ : bi_cofe (iPropI Σ) = @uPred_cofe (iResUR Σ).
Proof. reflexivity. Qed.
\ No newline at end of file
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