diff --git a/Makefile b/Makefile index fb2ff409f..f6ac22680 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/') # Check Coq version -COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 +COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1 or-else 9.0.0 or-else 9.0.1 or-else 9.1.0 COQV=$(shell $(COQC) -v) ifneq ($(IGNORECOQVERSION),true) diff --git a/builddep/coq-vst-on-iris-builddep.opam b/builddep/coq-vst-on-iris-builddep.opam index 10d1bd271..5224f135f 100644 --- a/builddep/coq-vst-on-iris-builddep.opam +++ b/builddep/coq-vst-on-iris-builddep.opam @@ -25,10 +25,10 @@ bug-reports: "https://github.com/PrincetonUniversity/VST/issues" license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE" depends: [ - "coq" {>= "8.19.1" & <= "8.20.0"} - "coq-compcert" {>= "3.11"} + "coq" { (>= "8.19" ) } + "coq-iris" { (>= "4.4.0") } + "coq-compcert" {= "3.15"} "coq-vst-zlist" {>= "2.11"} "coq-flocq" {>= "4.1.0"} - "coq-iris" {="4.3.0"} - "coq-vst-ora" {="1.1"} + "coq-iris-ora" {(= "1.3.0") | (= "~dev")} ] diff --git a/floyd/canon.v b/floyd/canon.v index 96547a4e5..7e38b589b 100644 --- a/floyd/canon.v +++ b/floyd/canon.v @@ -157,7 +157,7 @@ Proof. induction H; simpl; f_equiv; done. Qed. -#[global] Instance LOCALx_proper : Proper (equiv(Equiv := list.list_equiv(H := equivL)) ==> equiv ==> equiv) (LOCALx). +#[global] Instance LOCALx_proper : Proper (equiv(Equiv := list_relations.list_equiv(H := equivL)) ==> equiv ==> equiv) (LOCALx). Proof. intros ??????. rewrite /LOCALx; f_equiv; last done. diff --git a/floyd/closed_lemmas.v b/floyd/closed_lemmas.v index 90cb7e9fe..1a369a4df 100644 --- a/floyd/closed_lemmas.v +++ b/floyd/closed_lemmas.v @@ -126,7 +126,7 @@ Qed. Lemma closed_wrt_map_subst: forall id e `(Q: list (environ -d> A)), Forall (closed_wrt_vars (eq id)) Q -> - @equiv _ (list.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q. + @equiv _ (list_relations.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q. Proof. induction Q; intros. simpl; constructor. @@ -139,7 +139,7 @@ Qed. Lemma closed_wrt_map_subst' `{!heapGS Σ}: forall id e (Q: list (environ -d> mpred)), Forall (closed_wrt_vars (eq id)) Q -> - @equiv _ (list.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q. + @equiv _ (list_relations.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q. Proof. intros. apply closed_wrt_map_subst. done. diff --git a/ivst.md b/ivst.md index 1419bced5..fcb5d532c 100644 --- a/ivst.md +++ b/ivst.md @@ -6,7 +6,8 @@ Install opam: ```(bash) -opam switch create vst_on_iris ocaml-variants.4.14.1+options ocaml-option-flambda +opam switch create ccris ocaml-variants.4.14.2+options ocaml-option-flambda +eval $(opam env) ``` Install dependencies: @@ -14,7 +15,8 @@ Install dependencies: ```(bash) opam repo add coq-released https://coq.inria.fr/opam/released opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git -opam pin add builddep/ +opam update +opam pin add builddep/ -y ``` Download submodules: @@ -26,7 +28,7 @@ At this point, we use [`Makefile`](./Makefile) ```(bash) make ``` -Addtionally, to generate `_CoqProject`: +Additionally, to generate `_CoqProject`: ```(bash) make _CoqProject diff --git a/shared/dshare.v b/shared/dshare.v index b62127d5f..23d0ea33a 100644 --- a/shared/dshare.v +++ b/shared/dshare.v @@ -30,9 +30,9 @@ Notation "" := (DfracOwn (Share share_top)) (in custom dfrac). Section dfrac. -Context `{ST : ShareType}. +Context {SI : sidx} `{ST : ShareType}. Set Warnings "-redundant-canonical-projection". - Canonical Structure dfracO := leibnizO dfrac. + Canonical Structure dfracO := ofe.leibnizO dfrac. Set Warnings "redundant-canonical-projection". Implicit Types p q : share_car. @@ -84,15 +84,18 @@ Set Warnings "redundant-canonical-projection". Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p ⋅ q). Proof. done. Qed. + (* Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances. *) + Lemma dfrac_op_discarded : DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded. - Proof. rewrite /op /dfrac_op_instance /= left_id //. Qed. + Proof. rewrite /op /dfrac_op_instance /= + (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed. Lemma dfrac_op_own_discarded q : DfracOwn q ⋅ DfracDiscarded = DfracBoth q. - Proof. rewrite /op /= right_id //. Qed. + Proof. rewrite /op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed. Lemma dfrac_op_both_discarded q : DfracBoth q ⋅ DfracDiscarded = DfracBoth q. - Proof. rewrite /op /= right_id //. Qed. + Proof. rewrite /op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed. Lemma dfrac_included_eq dq dp : dq ≼ dp ↔ match dq, dp with | DfracOwn q, DfracOwn p | DfracOwn q, DfracBoth p | DfracBoth q, DfracBoth p => q ≼ p @@ -144,9 +147,9 @@ Set Warnings "redundant-canonical-projection". Proof. apply: discrete_cancelable. intros [q1|q1] [q2|q2] ? [=]; simplify_eq/=; try done. - - by apply (share_cancelable _ 0) in H1 as ->. + - by apply (share_cancelable _ 0ᵢ) in H1 as ->. - destruct H as (? & J & ?). - apply (share_cancelable _ 0) in H1 as ->; try done. + apply (share_cancelable _ 0ᵢ) in H1 as ->; try done. rewrite J; hnf; eauto. Qed. @@ -166,7 +169,7 @@ Set Warnings "redundant-canonical-projection". Proof. intros ??? ->%dfrac_full_exclusive H. destruct z; last done. - rewrite /op /cmra_op /= right_id in H; injection H as H. + rewrite /op /cmra_op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) in H; injection H as H. symmetry in H; apply share_op_join in H as (? & ? & [=] & ? & J); subst. rewrite share_op_comm in J; apply share_op_top' in J as (_ & ->); done. Qed. @@ -174,7 +177,7 @@ Set Warnings "redundant-canonical-projection". Definition dfrac_ucmra_mixin : UcmraMixin dfrac. Proof. split; try done. - intros [|]; rewrite /op /dfrac_op_instance /= left_id //. + intros [|]; rewrite /op /dfrac_op_instance /= (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed. Set Warnings "-redundant-canonical-projection". Canonical Structure dfracUC := Ucmra dfrac dfrac_ucmra_mixin. @@ -210,7 +213,7 @@ Set Warnings "redundant-canonical-projection". ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ ∃ sh, q = Share sh ∧ ~share_writable sh. Proof. rewrite /op /= /valid /=. - rewrite right_id //. + rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed. Definition readable_dfrac (dq : dfrac) := @@ -229,7 +232,7 @@ Set Warnings "redundant-canonical-projection". Qed. Global Instance dfrac_is_op q q1 q2 : - @IsOp shareR q q1 q2 → + @IsOp _ shareR q q1 q2 → IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2). Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed. @@ -262,7 +265,7 @@ Set Warnings "redundant-canonical-projection". - inversion 1; hnf; auto. - intros ?? [?|?]; subst. + by left. - + right; destruct x; rewrite /op /= left_id //. + + right; destruct x; rewrite /op /= (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. - intros ??? [?|?] [?|?]; subst; hnf; auto. right; destruct x; rewrite !dfrac_op_both_discarded //. - intros ??? [?|?]; subst; hnf; auto. diff --git a/shared/share_alg.v b/shared/share_alg.v index 7cdf0dde7..28ada30f7 100644 --- a/shared/share_alg.v +++ b/shared/share_alg.v @@ -36,7 +36,7 @@ Inductive share_car `{ShareType} := Section share. - Context `{ST : ShareType}. + Context {SI : sidx} `{ST : ShareType}. Lemma share_op_top' a b : share_op a share_top = Some b -> b = share_top /\ a = share_bot. Proof. diff --git a/shared/shared.v b/shared/shared.v index 35e089cfb..5e0a0cb5c 100644 --- a/shared/shared.v +++ b/shared/shared.v @@ -11,7 +11,7 @@ From iris.prelude Require Import options. Section shared. -Context `{ST : ShareType}. +Context {SI : sidx} `{ST : ShareType}. Definition readable_share' (s : shareO) := match s with Share sh => share_readable sh | _ => False end. @@ -50,9 +50,9 @@ Local Instance shared_equiv : Equiv shared := λ x y, Definition shared_ofe_mixin : OfeMixin shared. Proof. split. - - destruct x, y; intuition; try split; try pose proof (H 0) as H'; try destruct H; try destruct H'; try done. + - destruct x, y; intuition; try split; try pose proof (H 0ᵢ) as H'; try destruct H; try destruct H'; try done. + intros n; specialize (H n); destruct H; done. - + apply O. + + apply 0ᵢ. - intros n; split; rewrite /dist /shared_dist. + intros x; destruct x; done. + intros [|] [|]; try done. @@ -62,7 +62,7 @@ Proof. * by intros ->. - intros ?? [|] [|]; try done. intros [??]; split; first done. - eapply dist_lt; eauto. + eapply dist_le; eauto. Qed. Canonical Structure sharedO := Ofe shared shared_ofe_mixin. @@ -390,7 +390,7 @@ Proof. intros [|] ?; done. Qed. Lemma dfrac_error_discarded : forall x, dfrac_error (DfracDiscarded ⋅ x) = dfrac_error x. Proof. - destruct x; simpl; rewrite left_id //. + destruct x; simpl; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed. Lemma share_op_None : forall (s : shareO), s ⋅ ShareBot = ShareBot. @@ -401,9 +401,9 @@ Qed. Local Instance shared_unit_left_id : LeftId equiv (ε : shared) op. Proof. intros [|]; rewrite /op /=. - - rewrite right_id. + - rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)). destruct (readable_dfrac_dec _); done. - - hnf; rewrite left_id //. + - hnf; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed. Definition shared_cmra_mixin : CmraMixin shared. @@ -428,9 +428,9 @@ Proof. - intros [|]; intuition. + by destruct H. + split; apply cmra_valid_validN, H. - + apply (H 0). - - intros ? [|]; try done. - intros [??]; split; last apply cmra_validN_S; done. + + apply (H 0ᵢ). + - intros ?? [|]; try done. + intros [??]; split; last eapply cmra_validN_le; done. - intros ???. pose proof (shared_op_alt x (y ⋅ z)) as Hop1. pose proof (shared_op_alt (x ⋅ y) z) as Hop2. @@ -467,7 +467,7 @@ Proof. destruct shyz; last by rewrite share_op_None in H; destruct H. destruct Hop3 as (? & ? & ? & ? & -> & -> & [=] & ?); simpl in *; subst. rewrite /op /shared_op_instance; hnf. - apply (@cmra_assoc shareR). + apply (@cmra_assoc _ shareR). - intros ??. pose proof (shared_op_alt x y) as Hop1. pose proof (shared_op_alt y x) as Hop2. @@ -479,11 +479,11 @@ Proof. by inversion Hv; subst. + destruct (dfrac_error _) eqn: Herr; first by rewrite Hop1 Hop2. destruct Hop1 as (? & ? & ? & ? & -> & -> & -> & ?), Hop2 as (? & ? & ? & ? & [=] & [=] & -> & ?); subst. - hnf; by rewrite (@cmra_comm shareR). + hnf; by rewrite (@cmra_comm _ shareR). - intros [|]. + rewrite /op /shared_op_instance /core /pcore /shared_pcore_instance /=. destruct dq. - * rewrite /ε /shared_unit_instance right_id. + * rewrite /ε /shared_unit_instance (right_id _ _ (RightId:=ucmra_unit_right_id)). destruct (readable_dfrac_dec _); done. * rewrite comm dfrac_op_both_discarded. destruct (readable_dfrac_dec _); try done. @@ -507,7 +507,7 @@ Proof. { destruct z as [[|]|]; done. } exists (YES DfracDiscarded I v0). unshelve rewrite YES_op /=; last split; rewrite ?dfrac_op_both_discarded //. - rewrite -agree_included H -Some_included_total -Hval; eexists; done. + rewrite H -agree_included -Some_included_total -Hval; eexists; done. * destruct (dfrac_error _) eqn: Herr; last by destruct Hop as (? & ? & ? & ? & ? & ?). rewrite Hop in H; destruct y; inversion H; subst. exists err; done. @@ -682,13 +682,13 @@ Proof. rewrite dfrac_of_op' val_of_op'; simpl. destruct (dfrac_error _) eqn: Herr; [left | right]. - by apply dfrac_error_fail. - - rewrite !left_id //. + - rewrite !(left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed. Lemma readable_dfrac_order : forall dq dq', dq ≼ₒ dq' -> readable_dfrac dq -> readable_dfrac dq'. Proof. intros ?? [-> | <-]; try done. - destruct dq as [[|]|[|]]; try done; simpl; rewrite right_id //. + destruct dq as [[|]|[|]]; try done; simpl; rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed. Lemma dfrac_error_order : forall dq dq', dq ≼ₒ dq' -> dfrac_error dq = dfrac_error dq'. @@ -697,7 +697,7 @@ Proof. rewrite (comm _ dq) dfrac_error_discarded //. Qed. -Lemma shared_orderN_op : ∀ (n : nat) (x x' y : shared), x ≼ₒ{n} x' → x ⋅ y ≼ₒ{n} x' ⋅ y. +Lemma shared_orderN_op : ∀ (n : SI) (x x' y : shared), x ≼ₒ{n} x' → x ⋅ y ≼ₒ{n} x' ⋅ y. Proof. intros. destruct H as [H | [??]]. @@ -758,12 +758,12 @@ Proof. rewrite /core /=; destruct x, y; try done; simpl in *. + right; destruct Hd as [<- | <-], dq; rewrite ?dfrac_op_own_discarded ?dfrac_op_both_discarded // /=. split. - * right; rewrite left_id //. + * right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. * apply agree_increasing. + right; destruct Hd as [<- | <-]; try done. rewrite dfrac_op_own_discarded. destruct sh; split; try done. - right; rewrite left_id //. + right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. + destruct Hd as [[=] | ?]; subst; try done. destruct sh0; [right | left]; done. - intros ???? Hvalid [? | [Hd Hv]]. @@ -801,9 +801,9 @@ Proof. + eexists; split; first right; done. - intros ??? [Hd Hv]%shared_dist_implies. right; split; [hnf; auto | by apply ora_dist_orderN]. - - intros ??? [H | [? ?%ora_orderN_S]]. + - intros ???? [H | [? ?]]. + destruct y; inversion H; subst; by left. - + by right. + + intros. eapply ora_orderN_le in H0; eauto. by right. - intros ???? Hord [H | [Hd Hv]]. { destruct z; inversion H; subst; by left. } destruct Hord as [Hy | [??]]. @@ -820,7 +820,7 @@ Proof. - split. + intros [? | [??]] ?; first by left. right; split; last apply ora_order_orderN; done. - + intros H; pose proof (H 0) as H0; destruct H0 as [? | [??]]; first by left. + + intros H; pose proof (H 0ᵢ) as H0; destruct H0 as [? | [??]]; first by left. right; split; try done. apply ora_order_orderN; intros n1. destruct (H n1) as [? | [??]]; first destruct y; done. @@ -832,12 +832,12 @@ Proof. destruct x; simpl in *. * right; destruct dq, cx; inversion Heq; subst; simpl. -- destruct (_ ⋅ _); try done. - split; first by right; rewrite left_id. + split; first by right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)). apply agree_increasing. -- destruct (dfrac_of y); split; simpl; try done; rewrite -H0 -Hv Some_op_opM Some_order; destruct (val_of y); try done; rewrite /= comm; apply agree_increasing. * destruct sh, cx; inversion Heq; subst; simpl. -- right; destruct (_ ⋅ _); try done; simpl. - split; first by right; rewrite left_id. + split; first by right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)). apply agree_increasing. -- destruct (dfrac_of y); done. + destruct (dfrac_error _) eqn: Herr; first by destruct (x ⋅ y); inversion Hop; subst; left. @@ -887,7 +887,7 @@ Qed. End shared. -Arguments YES {_ _ _} _ _ _. -Arguments NO {_ _ _} _ _. -Arguments dfrac_of {_ _ _} _. -Arguments val_of {_ _ _} _. +Arguments YES {_ _ _ _} _ _ _. +Arguments NO {_ _ _ _} _ _. +Arguments dfrac_of {_ _ _ _} _. +Arguments val_of {_ _ _ _} _. diff --git a/veric/external_state.v b/veric/external_state.v index 5e7a37ac3..29a6dd248 100644 --- a/veric/external_state.v +++ b/veric/external_state.v @@ -11,15 +11,15 @@ Class externalGS (Z : Type) (Σ : gFunctors) := ExternalGS { }. Definition has_ext {Z : Type} `{!externalGS Z Σ} (z : Z) : iProp Σ := - own(inG0 := external_inG) external_name (auth_frag(A := optionUR (@exclR (leibnizO Z))) (Excl' z)). + own(inG0 := external_inG) external_name (auth_frag(A := optionUR (@exclR _(leibnizO Z))) (Excl' z)). Definition ext_auth {Z : Type} `{!externalGS Z Σ} (z : Z) : iProp Σ := - own(inG0 := external_inG) external_name (auth_auth(A := optionUR (@exclR (leibnizO Z))) (DfracOwn 1) (Excl' z)). + own(inG0 := external_inG) external_name (auth_auth(A := optionUR (@exclR _(leibnizO Z))) (DfracOwn 1) (Excl' z)). Lemma ext_alloc {Z : Type} `{!inG Σ (excl_authR (leibnizO Z))} (z : Z) : ⊢ |==> ∃ _ : externalGS Z Σ, ext_auth z ∗ has_ext z. Proof. rewrite /ext_auth /has_ext. - iMod (own_alloc (●E (z : leibnizO Z) ⋅ ◯E (z : leibnizO Z) : excl_authR (leibnizO Z))) as (γ) "?". + iMod (own_alloc (●E (z : leibnizO Z) ⋅ ◯E (z : leibnizO Z) : @excl_authR natSI (leibnizO Z))) as (γ) "?". { apply excl_auth_valid. } iExists (ExternalGS _ _ _ γ). rewrite own_op //. diff --git a/veric/juicy_mem.v b/veric/juicy_mem.v index 40d1fa4f8..940ae2643 100644 --- a/veric/juicy_mem.v +++ b/veric/juicy_mem.v @@ -1015,7 +1015,7 @@ Section mpred. apply shared_valid in Hv as (_ & Hv). apply option_included_total in H as [-> | (? & ? & -> & Heq & H)]; auto. rewrite Heq /= in Hv |- *. - assert (✓{0} x2) by (by apply cmra_valid_validN). + assert (✓{0ᵢ} x2) by (by apply cmra_valid_validN). right; f_equal; symmetry; apply (elem_of_agree_ne' O); first done. symmetry; apply agree_valid_includedN; first done. by apply @cmra_included_includedN. diff --git a/veric/juicy_mem_lemmas.v b/veric/juicy_mem_lemmas.v index 2dd04ec9e..f4cbbe10f 100644 --- a/veric/juicy_mem_lemmas.v +++ b/veric/juicy_mem_lemmas.v @@ -390,7 +390,7 @@ Proof. iExists lx; iFrame; done. Qed. -Lemma big_opL_seq_index : forall {M : ofe} (o : M -> M -> M) `{Monoid _ o} n (f : nat -> nat -> M), (([^o list] k↦v ∈ seq 0 n, f k v) ≡ [^o list] v ∈ seq 0 n, f v v)%stdpp. +Lemma big_opL_seq_index : forall {M : ofe} (o : M -> M -> M) `{!Monoid o} n (f : nat -> nat -> M), (([^o list] k↦v ∈ seq 0 n, f k v) ≡ [^o list] v ∈ seq 0 n, f v v)%stdpp. Proof. intros. apply big_opL_proper. diff --git a/veric/lifting.v b/veric/lifting.v index 430126bbe..26bb09b05 100644 --- a/veric/lifting.v +++ b/veric/lifting.v @@ -2211,6 +2211,12 @@ Qed. Definition exit_ret_assert R : assert := ((RA_break R -∗ False) ∧ (RA_continue R -∗ False) ∧ (∀ v, (RA_normal R ∨ RA_return R v) -∗ ∀ m z, ⎡state_interp m z⎤ -∗ ⌜∃ i, ext_spec_exit OK_spec (Some (Vint i)) z m⌝)). + +Hint Extern 2 (Increasing _) => +match goal with +| |- @Increasing ?A _ _ _ => apply (@ext_order.incl_increasing _ A) +end : typeclass_instances. + Lemma guarded_stop : forall E f R, f.(fn_vars) = [] → exit_ret_assert R ⊢ guarded E f Kstop R. diff --git a/veric/mpred.v b/veric/mpred.v index 03b19ab3e..ea45e1319 100644 --- a/veric/mpred.v +++ b/veric/mpred.v @@ -206,7 +206,7 @@ Definition MaskTT A := ArrowType A (ConstType coPset). Section ofe. -Context `{Cofe PROP1} `{Cofe PROP2}. +Context `{!Cofe PROP1} `{!Cofe PROP2}. Inductive funspec_ := mk_funspec (sig : typesig) (cc : calling_convention) (A: TypeTree) @@ -266,7 +266,7 @@ Proof. + intros [] [] [] (-> & -> & -> & ? & ? & ?) (-> & -> & -> & ? & ? & ?); repeat (split; auto). exists eq_refl; split3; etrans; eauto. - intros ?? [] [] (-> & -> & -> & ? & ? & ?) ?; repeat (split; auto). - exists eq_refl; split3; eapply dist_lt; eauto. + exists eq_refl; split3; eapply dist_le; eauto. Qed. Canonical Structure funspecO := Ofe funspec_ funspec_ofe_mixin. @@ -360,13 +360,13 @@ Definition funspecO' := (laterO (funspecO (iPropO Σ) (iPropO Σ))). Definition funspecOF' := (laterOF (funspecOF idOF)). Definition dtfr A := (oFunctor_car (dependent_type_functor_rec A) (iProp Σ) (iProp Σ)). -Lemma OfeMor_eq : forall {A B : ofe} (f1 f2 : A -> B) {H1 H2}, f1 = f2 -> @OfeMor A B f1 H1 = @OfeMor A B f2 H2. +Lemma OfeMor_eq : forall {A B : ofe} (f1 f2 : A -> B) {H1 H2}, f1 = f2 -> @OfeMor _ A B f1 H1 = @OfeMor _ A B f2 H2. Proof. intros; subst. f_equal. apply proof_irr. Qed. -Lemma funspec_equivI PROP1 `{Cofe PROP1} PROP2 `{Cofe PROP2} (f1 f2 : funspec_ PROP1 PROP2) : (f1 ≡ f2 : iProp Σ) ⊣⊢ ∃ sig cc A E P1 P2 Q1 Q2, +Lemma funspec_equivI PROP1 `{!Cofe PROP1} PROP2 `{!Cofe PROP2} (f1 f2 : funspec_ PROP1 PROP2) : (f1 ≡ f2 : iProp Σ) ⊣⊢ ∃ sig cc A E P1 P2 Q1 Q2, ⌜f1 = mk_funspec sig cc A E P1 Q1 ∧ f2 = mk_funspec sig cc A E P2 Q2⌝ ∧ P1 ≡ P2 ∧ Q1 ≡ Q2. Proof. ouPred.unseal; split=> n x ?.