Commit 73711bd5 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'add-missing-proof' into 'master'

Add missing `Proof.` to sealing proofs to help async proof checking

See merge request iris/iris!406
parents 6eb52a82 8b5f7383
......@@ -37,7 +37,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). by eexists. Qed.
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
......@@ -51,7 +51,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
Definition big_opS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). by eexists. Qed.
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
......@@ -62,7 +62,7 @@ Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). by eexists. Qed.
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
......
......@@ -303,7 +303,7 @@ 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). by eexists. Qed.
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_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
......
......@@ -9,7 +9,7 @@ Import uPred.
Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I.
Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. by eexists. Qed.
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).
......
......@@ -106,21 +106,21 @@ Section definitions.
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own (gen_heap_name hG) ( {[ l := (q, to_agree (v : leibnizO V)) ]}).
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]})
own γm (namespace_map_token E))%I.
Definition meta_token_aux : seal (@meta_token_def). by eexists. Qed.
Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]})
own γm (namespace_map_data N (to_agree (encode x))))%I.
Definition meta_aux : seal (@meta_def). by eexists. Qed.
Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
......
......@@ -9,7 +9,7 @@ Import uPred.
(** Semantic Invariants *)
Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( E, ⌜↑N E |={E,E N}=> P ( P ={E N,E}= True))%I.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
Instance: Params (@inv) 3 := {}.
......
......@@ -56,7 +56,7 @@ 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). by eexists. Qed.
Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
Definition own_eq : @own = @own_def := own_aux.(seal_eq).
Instance: Params (@own) 4 := {}.
......
......@@ -55,7 +55,7 @@ Section definitions.
Definition proph_def (p : P) (vs : list V) : iProp Σ :=
own (proph_map_name pG) ( {[p := Excl vs]}).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
Definition proph := proph_aux.(unseal).
Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
End definitions.
......
......@@ -192,7 +192,7 @@ Hint Resolve uPred_mono : uPred_def.
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). by eexists. Qed.
Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
......@@ -200,14 +200,14 @@ Definition uPred_pure_eq :
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). by eexists. Qed.
Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
Definition uPred_and {M} := uPred_and_aux.(unseal) 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). by eexists. Qed.
Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
Definition uPred_or {M} := uPred_or_aux.(unseal) M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
......@@ -219,7 +219,7 @@ Next Obligation.
rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
eapply HPQ; auto. exists (x2 x4); by rewrite assoc.
Qed.
Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. 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_eq :
@uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
......@@ -227,7 +227,7 @@ Definition uPred_impl_eq :
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). by eexists. Qed.
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_eq :
@uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
......@@ -235,14 +235,14 @@ Definition uPred_forall_eq :
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). by eexists. Qed.
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_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 (A:=A)).
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed.
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_eq:
@uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
......@@ -254,7 +254,7 @@ Next Obligation.
exists x1, (x2 z); split_and?; eauto using uPred_mono, cmra_includedN_l.
eapply dist_le, Hn. by rewrite Hy Hx assoc.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. 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_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
......@@ -266,7 +266,7 @@ Next Obligation.
eapply uPred_mono with n3 (x1 x3);
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. 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_eq :
@uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
......@@ -277,7 +277,7 @@ Definition uPred_wand_eq :
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). by eexists. Qed.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
......@@ -287,7 +287,7 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
Definition uPred_persistently_eq :
@uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
......@@ -297,7 +297,7 @@ Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
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). by eexists. 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_eq :
@uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
......@@ -308,7 +308,7 @@ Next Obligation.
intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn. eapply cmra_includedN_le=>//.
exists (a' x2). by rewrite Hx(assoc op) Hx1.
Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. 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_eq :
@uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
......@@ -316,7 +316,7 @@ Definition uPred_ownM_eq :
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). by eexists. Qed.
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_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
......@@ -331,7 +331,7 @@ Next Obligation.
exists (x' x3); split; first by rewrite -assoc.
eauto using uPred_mono, cmra_includedN_l.
Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. 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_eq :
@uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
......
......@@ -54,7 +54,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
(Φ : K A B PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
( k, is_Some (m1 !! k) is_Some (m2 !! k)
[ map] k xy map_zip m1 m2, Φ k xy.1 xy.2)%I.
Definition big_sepM2_aux : seal (@big_sepM2_def). by eexists. Qed.
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).
......
......@@ -87,7 +87,7 @@ Section definition.
End definition.
(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
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).
......
......@@ -126,88 +126,88 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
Next Obligation. solve_proper. Qed.
Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
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_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
Definition monPred_emp_aux : seal (@monPred_emp_def). by eexists. Qed.
Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
Definition monPred_emp := monPred_emp_aux.(unseal).
Definition monPred_emp_eq : @monPred_emp = _ := monPred_emp_aux.(seal_eq).
Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
Definition monPred_pure_aux : seal (@monPred_pure_def). Proof. by eexists. Qed.
Definition monPred_pure := monPred_pure_aux.(unseal).
Definition monPred_pure_eq : @monPred_pure = _ := monPred_pure_aux.(seal_eq).
Definition monPred_objectively_def P : monPred := MonPred (λ _, i, P i)%I _.
Definition monPred_objectively_aux : seal (@monPred_objectively_def). by eexists. Qed.
Definition monPred_objectively_aux : seal (@monPred_objectively_def). Proof. by eexists. Qed.
Definition monPred_objectively := monPred_objectively_aux.(unseal).
Definition monPred_objectively_eq : @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
Definition monPred_subjectively_def P : monPred := MonPred (λ _, i, P i)%I _.
Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). by eexists. Qed.
Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). Proof. by eexists. Qed.
Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
Definition monPred_subjectively_eq : @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
Program Definition monPred_and_def P Q : monPred :=
MonPred (λ i, P i Q i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_and_aux : seal (@monPred_and_def). by eexists. Qed.
Definition monPred_and_aux : seal (@monPred_and_def). Proof. by eexists. Qed.
Definition monPred_and := monPred_and_aux.(unseal).
Definition monPred_and_eq : @monPred_and = _ := monPred_and_aux.(seal_eq).
Program Definition monPred_or_def P Q : monPred :=
MonPred (λ i, P i Q i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_or_aux : seal (@monPred_or_def). by eexists. Qed.
Definition monPred_or_aux : seal (@monPred_or_def). Proof. by eexists. Qed.
Definition monPred_or := monPred_or_aux.(unseal).
Definition monPred_or_eq : @monPred_or = _ := monPred_or_aux.(seal_eq).
Definition monPred_impl_def P Q : monPred :=
monPred_upclosed (λ i, P i Q i)%I.
Definition monPred_impl_aux : seal (@monPred_impl_def). by eexists. Qed.
Definition monPred_impl_aux : seal (@monPred_impl_def). Proof. by eexists. Qed.
Definition monPred_impl := monPred_impl_aux.(unseal).
Definition monPred_impl_eq : @monPred_impl = _ := monPred_impl_aux.(seal_eq).
Program Definition monPred_forall_def A (Φ : A monPred) : monPred :=
MonPred (λ i, x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_forall_aux : seal (@monPred_forall_def). by eexists. Qed.
Definition monPred_forall_aux : seal (@monPred_forall_def). Proof. by eexists. Qed.
Definition monPred_forall := monPred_forall_aux.(unseal).
Definition monPred_forall_eq : @monPred_forall = _ := monPred_forall_aux.(seal_eq).
Program Definition monPred_exist_def A (Φ : A monPred) : monPred :=
MonPred (λ i, x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_exist_aux : seal (@monPred_exist_def). by eexists. Qed.
Definition monPred_exist_aux : seal (@monPred_exist_def). Proof. by eexists. Qed.
Definition monPred_exist := monPred_exist_aux.(unseal).
Definition monPred_exist_eq : @monPred_exist = _ := monPred_exist_aux.(seal_eq).
Program Definition monPred_sep_def P Q : monPred :=
MonPred (λ i, P i Q i)%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_sep_aux : seal (@monPred_sep_def). by eexists. Qed.
Definition monPred_sep_aux : seal (@monPred_sep_def). Proof. by eexists. Qed.
Definition monPred_sep := monPred_sep_aux.(unseal).
Definition monPred_sep_eq : @monPred_sep = _ := monPred_sep_aux.(seal_eq).
Definition monPred_wand_def P Q : monPred :=
monPred_upclosed (λ i, P i - Q i)%I.
Definition monPred_wand_aux : seal (@monPred_wand_def). by eexists. Qed.
Definition monPred_wand_aux : seal (@monPred_wand_def). Proof. by eexists. Qed.
Definition monPred_wand := monPred_wand_aux.(unseal).
Definition monPred_wand_eq : @monPred_wand = _ := monPred_wand_aux.(seal_eq).
Program Definition monPred_persistently_def P : monPred :=
MonPred (λ i, <pers> (P i))%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
Definition monPred_persistently_aux : seal (@monPred_persistently_def). Proof. by eexists. Qed.
Definition monPred_persistently := monPred_persistently_aux.(unseal).
Definition monPred_persistently_eq : @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
Program Definition monPred_in_def (i0 : I) : monPred :=
MonPred (λ i : I, i0 i%I) _.
Next Obligation. solve_proper. Qed.
Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
Definition monPred_in := monPred_in_aux.(unseal).
Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
End Bi.
......@@ -225,14 +225,14 @@ Implicit Types P Q : monPred.
Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred :=
MonPred (λ _, a b)%I _.
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). Proof. by eexists. Qed.
Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
Definition monPred_internal_eq_eq : @monPred_internal_eq = _ :=
monPred_internal_eq_aux.(seal_eq).
Program Definition monPred_later_def P : monPred := MonPred (λ i, (P i))%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_later_aux : seal monPred_later_def. by eexists. Qed.
Definition monPred_later_aux : seal monPred_later_def. Proof. by eexists. Qed.
Definition monPred_later := monPred_later_aux.(unseal).
Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
End Sbi.
......@@ -768,7 +768,7 @@ 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. by eexists. 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).
......@@ -865,7 +865,7 @@ 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. by eexists. 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).
......@@ -902,7 +902,7 @@ 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. by eexists. Qed.
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).
......
......@@ -60,7 +60,7 @@ 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 Λ Σ _). by eexists. Qed.
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).
......
......@@ -46,7 +46,7 @@ Qed.
Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre s).
Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
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).
......
......@@ -56,7 +56,7 @@ Hint Resolve siProp_closed : siProp_def.
Program Definition siProp_pure_def (φ : Prop) : siProp :=
{| siProp_holds n := φ |}.
Solve Obligations with done.
Definition siProp_pure_aux : seal (@siProp_pure_def). by eexists. Qed.
Definition siProp_pure_aux : seal (@siProp_pure_def). Proof. by eexists. Qed.
Definition siProp_pure := unseal siProp_pure_aux.
Definition siProp_pure_eq :
@siProp_pure = @siProp_pure_def := seal_eq siProp_pure_aux.
......@@ -64,21 +64,21 @@ Definition siProp_pure_eq :
Program Definition siProp_and_def (P Q : siProp) : siProp :=
{| siProp_holds n := P n Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
Definition siProp_and_aux : seal (@siProp_and_def). by eexists. Qed.
Definition siProp_and_aux : seal (@siProp_and_def). Proof. by eexists. Qed.
Definition siProp_and := unseal siProp_and_aux.
Definition siProp_and_eq: @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.
Program Definition siProp_or_def (P Q : siProp) : siProp :=
{| siProp_holds n := P n Q n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
Definition siProp_or_aux : seal (@siProp_or_def). by eexists. Qed.
Definition siProp_or_aux : seal (@siProp_or_def). Proof. by eexists. Qed.
Definition siProp_or := unseal siProp_or_aux.
Definition siProp_or_eq: @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.
Program Definition siProp_impl_def (P Q : siProp) : siProp :=
{| siProp_holds n := n', n' n P n' Q n' |}.
Next Obligation. intros P Q [|n1] [|n2]; auto with lia. Qed.
Definition siProp_impl_aux : seal (@siProp_impl_def). by eexists. Qed.
Definition siProp_impl_aux : seal (@siProp_impl_def). Proof. by eexists. Qed.
Definition siProp_impl := unseal siProp_impl_aux.
Definition siProp_impl_eq :
@siProp_impl = @siProp_impl_def := seal_eq siProp_impl_aux.
......@@ -86,7 +86,7 @@ Definition siProp_impl_eq :
Program Definition siProp_forall_def {A} (Ψ : A siProp) : siProp :=
{| siProp_holds n := a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
Definition siProp_forall_aux : seal (@siProp_forall_def). by eexists. Qed.
Definition siProp_forall_aux : seal (@siProp_forall_def). Proof. by eexists. Qed.
Definition siProp_forall {A} := unseal siProp_forall_aux A.
Definition siProp_forall_eq :
@siProp_forall = @siProp_forall_def := seal_eq siProp_forall_aux.
......@@ -94,14 +94,14 @@ Definition siProp_forall_eq :
Program Definition siProp_exist_def {A} (Ψ : A siProp) : siProp :=
{| siProp_holds n := a, Ψ a n |}.
Solve Obligations with naive_solver eauto 2 with siProp_def.
Definition siProp_exist_aux : seal (@siProp_exist_def). by eexists. Qed.
Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
Definition siProp_exist {A} := unseal siProp_exist_aux A.
Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
{| siProp_holds n := a1 {n} a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). by eexists. Qed.
Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
Definition siProp_internal_eq_eq:
@siProp_internal_eq = @siProp_internal_eq_def := seal_eq siProp_internal_eq_aux.
......@@ -109,7 +109,7 @@ Definition siProp_internal_eq_eq:
Program Definition siProp_later_def (P : siProp) : siProp :=
{| siProp_holds n := match n return _ with 0 => True | S n' => P n' end |}.
Next Obligation. intros P [|n1] [|n2]; eauto using siProp_closed with lia. Qed.
Definition siProp_later_aux : seal (@siProp_later_def). by eexists. Qed.
Definition siProp_later_aux : seal (@siProp_later_def). Proof. by eexists. Qed.
Definition siProp_later := unseal siProp_later_aux.
Definition siProp_later_eq :
@siProp_later = @siProp_later_def := seal_eq siProp_later_aux.
......
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