Commit 1b0cd6b0 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/no-eta' into 'master'

do not eta-expand when sealing

Closes #285

See merge request iris/iris!490
parents 7f690d29 45c14ba9
......@@ -315,7 +315,8 @@ Qed.
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
Definition fixpoint := fixpoint_aux.(unseal).
Arguments fixpoint {A _ _} f {_}.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Section fixpoint.
......
......@@ -9,10 +9,11 @@ Import uPred.
Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
wsat ownE E1 == (wsat ownE E2 P).
Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. Proof. by eexists. Qed.
Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
uPred_fupd_aux.(seal_eq).
Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
Arguments uPred_fupd {Σ _}.
Lemma uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
......
......@@ -75,8 +75,8 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_name : gname;
gen_meta_name : gname
}.
Arguments gen_heap_name {_ _ _ _ _} _ : assert.
Arguments gen_meta_name {_ _ _ _ _} _ : assert.
Arguments gen_heap_name {L V Σ _ _} _ : assert.
Arguments gen_meta_name {L V Σ _ _} _ : assert.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
......@@ -121,9 +121,10 @@ Section definitions.
γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]})
own γm (namespace_map_data N (to_agree (encode x))).
Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
Definition meta := meta_aux.(unseal).
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
Arguments meta {L _ _ V Σ _ A _ _} l N x.
Local Notation "l ↦{ q } v" := (mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
......
......@@ -10,10 +10,10 @@ Import uPred.
Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
E, ⌜↑N E |={E,E N}=> P ( P ={E N,E}= True).
Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv := inv_aux.(unseal).
Arguments inv {Σ _} N P.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
Instance: Params (@inv) 3 := {}.
Typeclasses Opaque inv.
(** * Invariants *)
Section inv.
......
......@@ -58,10 +58,10 @@ Instance: Params (@iRes_singleton) 4 := {}.
Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
Definition own := own_aux.(unseal).
Arguments own {Σ A _} γ a.
Definition own_eq : @own = @own_def := own_aux.(seal_eq).
Instance: Params (@own) 4 := {}.
Typeclasses Opaque own.
(** * Properties about ghost ownership *)
Section global.
......
......@@ -193,7 +193,8 @@ Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
{| uPred_holds n x := φ |}.
Solve Obligations with done.
Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Definition uPred_pure := uPred_pure_aux.(unseal).
Arguments uPred_pure {M}.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
......@@ -201,14 +202,16 @@ Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
Definition uPred_and {M} := uPred_and_aux.(unseal) M.
Definition uPred_and := uPred_and_aux.(unseal).
Arguments uPred_and {M}.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
Definition uPred_or {M} := uPred_or_aux.(unseal) M.
Definition uPred_or := uPred_or_aux.(unseal).
Arguments uPred_or {M}.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
......@@ -220,7 +223,8 @@ Next Obligation.
eapply HPQ; auto. exists (x2 x4); by rewrite assoc.
Qed.
Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
Definition uPred_impl := uPred_impl_aux.(unseal).
Arguments uPred_impl {M}.
Definition uPred_impl_eq :
@uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
......@@ -228,7 +232,8 @@ Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
Definition uPred_forall := uPred_forall_aux.(unseal).
Arguments uPred_forall {M A}.
Definition uPred_forall_eq :
@uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
......@@ -236,14 +241,16 @@ Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
Definition uPred_exist {M A} := uPred_exist_aux.(unseal) M A.
Definition uPred_exist := uPred_exist_aux.(unseal).
Arguments uPred_exist {M A}.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 {n} a2 |}.
Solve Obligations with naive_solver eauto 2 using dist_le.
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
Arguments uPred_internal_eq {M A}.
Definition uPred_internal_eq_eq:
@uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
......@@ -255,7 +262,8 @@ Next Obligation.
eapply dist_le, Hn. by rewrite Hy Hx assoc.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
Definition uPred_sep {M} := uPred_sep_aux.(unseal) M.
Definition uPred_sep := uPred_sep_aux.(unseal).
Arguments uPred_sep {M}.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
......@@ -267,7 +275,8 @@ Next Obligation.
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
Definition uPred_wand := uPred_wand_aux.(unseal).
Arguments uPred_wand {M}.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
......@@ -278,7 +287,8 @@ Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
Definition uPred_plainly := uPred_plainly_aux.(unseal).
Arguments uPred_plainly {M}.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
......@@ -286,7 +296,8 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
Definition uPred_persistently := uPred_persistently_aux.(unseal).
Arguments uPred_persistently {M}.
Definition uPred_persistently_eq :
@uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
......@@ -296,7 +307,8 @@ Next Obligation.
intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Qed.
Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
Definition uPred_later {M} := uPred_later_aux.(unseal) M.
Definition uPred_later := uPred_later_aux.(unseal).
Arguments uPred_later {M}.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
......@@ -307,7 +319,8 @@ Next Obligation.
exists (a' x2). by rewrite Hx(assoc op) Hx1.
Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
Definition uPred_ownM := uPred_ownM_aux.(unseal).
Arguments uPred_ownM {M}.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
......@@ -315,7 +328,8 @@ Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := {n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
Arguments uPred_cmra_valid {M A}.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
......@@ -330,7 +344,8 @@ Next Obligation.
eauto using uPred_mono, cmra_includedN_l.
Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
Definition uPred_bupd := uPred_bupd_aux.(unseal).
Arguments uPred_bupd {M}.
Definition uPred_bupd_eq :
@uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
......
......@@ -57,7 +57,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
Definition big_sepM2 := big_sepM2_aux.(unseal).
Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
Definition big_sepM2_eq : @big_sepM2 = @big_sepM2_def := big_sepM2_aux.(seal_eq).
Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
(big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
......
......@@ -88,9 +88,9 @@ End definition.
(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
Definition atomic_update_eq :
@atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
Definition atomic_update := atomic_update_aux.(unseal).
Arguments atomic_update {PROP _ TA TB}.
Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
......
From stdpp Require Import coPset.
From iris.bi Require Import bi.
Set Default Proof Using "Type".
(** Definitions. *)
Structure biIndex :=
......@@ -126,9 +127,9 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
MonPred (λ i, ( j, i j Φ j)%I) _.
Next Obligation. solve_proper. Qed.
Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP), MonPred (λ _, P) _.
Definition monPred_embed_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
Definition monPred_embed : Embed PROP monPred := monPred_embed_aux.(unseal).
Definition monPred_embed := monPred_embed_aux.(unseal).
Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
......@@ -743,10 +744,11 @@ Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objectiv
Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_bupd_aux `{BiBUpd PROP} : seal monPred_bupd_def. Proof. by eexists. Qed.
Definition monPred_bupd `{BiBUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = _ :=
monPred_bupd_aux.(seal_eq).
Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
Definition monPred_bupd := monPred_bupd_aux.(unseal).
Arguments monPred_bupd {_}.
Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
Proof.
......@@ -807,11 +809,13 @@ Proof. rewrite /bi_except_0. apply _. Qed.
(** Internal equality *)
Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
MonPred (λ _, a b)%I _.
Definition monPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@monPred_internal_eq_def _).
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
Proof. by eexists. Qed.
Definition monPred_internal_eq `{!BiInternalEq PROP} := monPred_internal_eq_aux.(unseal).
Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
@internal_eq _ (@monPred_internal_eq _) = _ := monPred_internal_eq_aux.(seal_eq).
Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
Arguments monPred_internal_eq {_}.
Lemma monPred_internal_eq_eq `{!BiInternalEq PROP} :
@internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
BiInternalEqMixin monPredI (@monPred_internal_eq _).
......@@ -861,10 +865,11 @@ Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
(P : monPred) : monPred :=
MonPred (λ i, |={E1,E2}=> P i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_fupd_aux `{BiFUpd PROP} : seal monPred_fupd_def. Proof. by eexists. Qed.
Definition monPred_fupd `{BiFUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = _ :=
monPred_fupd_aux.(seal_eq).
Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
Definition monPred_fupd := monPred_fupd_aux.(unseal).
Arguments monPred_fupd {_}.
Lemma monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
Proof.
......@@ -898,9 +903,11 @@ Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(** Plainly *)
Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
MonPred (λ _, i, (P i))%I _.
Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. Proof. by eexists. Qed.
Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
Definition monPred_plainly := monPred_plainly_aux.(unseal).
Arguments monPred_plainly {_}.
Lemma monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
Proof.
......
......@@ -57,12 +57,14 @@ Proof.
rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
Qed.
Definition twp_def `{!irisG Λ Σ} (s : stuckness) (E : coPset)
(e : expr Λ) (Φ : val Λ iProp Σ) :
iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
Definition twp_aux `{!irisG Λ Σ} : seal (@twp_def Λ Σ _). Proof. by eexists. Qed.
Instance twp' `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
:= λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
Definition twp' := twp_aux.(unseal).
Arguments twp' {Λ Σ _}.
Existing Instance twp'.
Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
Proof. rewrite -twp_aux.(seal_eq) //. Qed.
Section twp.
Context `{!irisG Λ Σ}.
......
......@@ -44,11 +44,14 @@ Proof.
repeat (f_contractive || f_equiv); apply Hwp.
Qed.
Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre s).
Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). Proof. by eexists. Qed.
Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
λ s : stuckness, fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
Definition wp' := wp_aux.(unseal).
Arguments wp' {Λ Σ _}.
Existing Instance wp'.
Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
Section wp.
Context `{!irisG Λ Σ}.
......
......@@ -237,9 +237,9 @@ way, [iFresh] can simply be implemented by changing the goal from
using the tactic [change_no_check]. This way, the generated proof term
contains no additional steps for changing the counter.
For all definitions below, we first define a version that take the two contexts
[env_intuitionistic] and [env_spatial] as its arguments, and then lift these
definitions that take the whole proof mode context [Δ : envs PROP]. This is
We first define a version [pre_envs_entails] that takes the two contexts
[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
crucial to make sure that the counter [env_counter] is not part of the seal. *)
Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
env_intuitionistic_valid : env_wf Γp;
......@@ -257,15 +257,19 @@ Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
Instance: Params (@of_envs) 1 := {}.
Arguments of_envs : simpl never.
Definition envs_entails_aux :
seal (λ (PROP : bi) (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs Q).
Proof. by eexists. Qed.
Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
of_envs' Γp Γs Q.
Definition pre_envs_entails_aux : seal (@pre_envs_entails_def). Proof. by eexists. Qed.
Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
Definition pre_envs_entails_eq : @pre_envs_entails = @pre_envs_entails_def :=
pre_envs_entails_aux.(seal_eq).
Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
envs_entails_aux.(unseal) PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
pre_envs_entails PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
Definition envs_entails_eq :
@envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ Q).
Proof. by rewrite /envs_entails envs_entails_aux.(seal_eq). Qed.
Arguments envs_entails {PROP} Δ Q%I : rename.
Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
Arguments envs_entails {PROP} Δ Q%I.
Instance: Params (@envs_entails) 1 := {}.
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
......
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