Skip to content
Snippets Groups Projects
Commit 025885e6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/make' into 'master' 

Move `Make` classes/instances to their own file, and improve documentation

See merge request iris/iris!836
parents abefed6c abcd6b85
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 260 additions and 225 deletions
_CoqProject
+ 3
− 1
View file @ 025885e6
......@@ -134,13 +134,15 @@ iris/proofmode/sel_patterns.v
iris/proofmode/tactics.v
iris/proofmode/notation.v
iris/proofmode/classes.v
iris/proofmode/classes_make.v
iris/proofmode/class_instances.v
iris/proofmode/class_instances_later.v
iris/proofmode/class_instances_updates.v
iris/proofmode/class_instances_embedding.v
iris/proofmode/class_instances_plainly.v
iris/proofmode/class_instances_internal_eq.v
iris/proofmode/frame_instances.v
iris/proofmode/class_instances_frame.v
iris/proofmode/class_instances_make.v
iris/proofmode/monpred.v
iris/proofmode/modalities.v
iris/proofmode/modality_instances.v
......
iris/bi/lib/fractional.v
+ 1
− 1
View file @ 025885e6
From iris.bi Require Export bi.
From iris.proofmode Require Import classes class_instances.
From iris.proofmode Require Import classes classes_make.
From iris.prelude Require Import options.
Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
......
iris/proofmode/class_instances.v
+ 1
− 2
View file @ 025885e6
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi telescopes.
From iris.bi Require Import telescopes.
From iris.proofmode Require Import base modality_instances classes.
From iris.proofmode Require Import ltac_tactics.
From iris.prelude Require Import options.
......
iris/proofmode/frame_instances.v → iris/proofmode/class_instances_frame.v
+ 9
− 108
View file @ 025885e6
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import classes.
From iris.bi Require Import telescopes.
From iris.proofmode Require Import classes classes_make.
From iris.prelude Require Import options.
Import bi.
(** This file defines the instances that make up the framing machinery. *)
(** When framing below logical connectives/modalities, framing will perform
some "clean up" to remove connectives/modalities if the result of framing is
[True] or [emp]. For example, framing [P] in [P ∗ Q] or [<affine> P] will
result in [Q] and [emp], respectively, instead of [emp ∗ Q] and [<affine> emp],
respectively. One could imagine a smarter way of cleaning up, as implemented in
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
but that makes framing less predictable and might have some performance impact.
Hence, we only perform such cleanup for [True] and [emp]. *)
Section bi.
Section class_instances_frame.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
(* Frame *)
(**
When framing [R] against itself, we leave [True] if possible (via
(** When framing [R] against itself, we leave [True] if possible (via
[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
goal. Otherwise we leave [emp] via [frame_here].
Only if all those options fail, we start decomposing [R], via instances like
......@@ -57,16 +46,6 @@ Proof.
- by rewrite right_id -affinely_affinely_if affine_affinely.
Qed.
Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
Frame p R P Q → MakeEmbed Q Q' →
Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same cost as default. *)
......@@ -79,17 +58,6 @@ Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
Frame p ⌜φ⌝ ⎡P⎤ Q' | 2. (* Same cost as default. *)
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.
Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.
Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
Proof. intros. apply True_sep, _. Qed.
Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
Frame true R (P1 ∗ P2) Q' | 9.
......@@ -138,17 +106,6 @@ Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
Global Instance make_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
MaybeFrame p R P1 Q1 progress1 →
MaybeFrame p R P2 Q2 progress2 →
......@@ -160,19 +117,8 @@ Proof.
apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
Qed.
Global Instance make_or_true_l P : KnownLMakeOr True P True.
Proof. apply left_absorb, _. Qed.
Global Instance make_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
(* We could in principle write the instance [frame_or_spatial] by a bunch of
instances, i.e. (omitting the parameter [p = false]):
(** We could in principle write the instance [frame_or_spatial] by a bunch of
instances (omitting the parameter [p = false]):
Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
Frame R P1 True → Frame R (P1 ∨ P2) P2
......@@ -184,6 +130,7 @@ appears at most once.
If Coq would memorize the results of type class resolution, the solution with
multiple instances would be preferred (and more Prolog-like). *)
Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
TCOr (TCEq (progress1 && progress2) true) (TCOr
......@@ -206,13 +153,6 @@ Proof.
by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.
Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
Global Instance frame_affinely p R P Q Q' :
TCOr (TCEq p true) (Affine R) →
Frame p R P Q → MakeAffinely Q Q' →
......@@ -222,22 +162,6 @@ Proof.
by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
Qed.
Global Instance make_intuitionistically_emp :
@KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_emp.
Qed.
Global Instance make_intuitionistically_True :
@KnownMakeIntuitionistically PROP True emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp.
Qed.
Global Instance make_intuitionistically_default P :
MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.
Global Instance frame_intuitionistically R P Q Q' :
Frame true R P Q → MakeIntuitionistically Q Q' →
Frame true R (□ P) Q' | 2. (* Same cost as default. *)
......@@ -246,16 +170,6 @@ Proof.
rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
Qed.
Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
Proof.
by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-absorbingly_emp_True.
Qed.
Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed.
Global Instance frame_absorbingly p R P Q Q' :
Frame p R P Q → MakeAbsorbingly Q Q' →
Frame p R (<absorb> P) Q' | 2. (* Same cost as default. *)
......@@ -321,14 +235,6 @@ Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
Frame p (a ≡ b) ⎡P⎤ Q'. (* Default cost > 1 *)
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_emp `{!BiAffine PROP} n :
@KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
Global Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
Frame p R P Q → MakeLaterN 1 Q Q' →
......@@ -353,11 +259,6 @@ Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
Global Instance frame_except_0 p R P Q Q' :
Frame p R P Q → MakeExcept0 Q Q' →
Frame p R (◇ P) Q' | 2. (* Same cost as default *)
......@@ -365,4 +266,4 @@ Proof.
rewrite /Frame /MakeExcept0=><- <-.
by rewrite except_0_sep -(except_0_intro (□?p R)).
Qed.
End bi.
End class_instances_frame.
iris/proofmode/class_instances_internal_eq.v
+ 1
− 2
View file @ 025885e6
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
From iris.prelude Require Import options.
Import bi.
......@@ -25,7 +24,7 @@ Global Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
NatCancel n 1 n' 0 →
IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
rewrite /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
Qed.
......
iris/proofmode/class_instances_later.v
+ 5
− 2
View file @ 025885e6
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
From iris.proofmode Require Import classes classes_make modality_instances.
From iris.prelude Require Import options.
Import bi.
......@@ -283,6 +282,10 @@ Global Instance into_laterN_later only_head n n' m' P Q lQ :
progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
into [P], as such, we continue with [MaybeIntoLaterN]. *)
TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) →
(* Similar to [iFrame], the [iNext] tactic also performs a traversal through a
term (a hypothesis) to find laters to strip. And like [iFrame] we don't want
this to be excessively smart. So we use the same typeclass as [iFrame] here.
*)
MakeLaterN m' Q lQ →
IntoLaterN only_head n (▷ P) lQ | 2.
Proof.
......
iris/proofmode/class_instances_make.v 0 → 100644
+ 99
− 0
View file @ 025885e6
(** IMPORTANT: Read the comment in [classes_make] about the "constant time"
requirements of these instances. *)
From iris.proofmode Require Export classes_make.
From iris.prelude Require Import options.
Import bi.
Section class_instances_make.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.
Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.
Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
Proof. intros. apply True_sep, _. Qed.
Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
Global Instance make_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
Global Instance make_or_true_l P : KnownLMakeOr True P True.
Proof. apply left_absorb, _. Qed.
Global Instance make_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
Global Instance make_intuitionistically_emp :
@KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_emp.
Qed.
Global Instance make_intuitionistically_True :
@KnownMakeIntuitionistically PROP True emp | 0.
Proof.
by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
intuitionistically_True_emp.
Qed.
Global Instance make_intuitionistically_default P :
MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.
Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
Proof.
by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-absorbingly_emp_True.
Qed.
Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed.
Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_emp `{!BiAffine PROP} n :
@KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
Global Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
End class_instances_make.
iris/proofmode/classes.v
+ 0
− 107
View file @ 025885e6
......@@ -321,113 +321,6 @@ Global Instance maybe_frame_default {PROP : bi} (R P : PROP) :
TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
variant, that only succeeds if the parameter(s) is not an evar. In
the case the parameter(s) is an evar, then [MakeXxxx] will not
instantiate it arbitrarily.
The reason for this is that if given an evar, these typeclasses
would typically try to instantiate this evar with some arbitrary
logical constructs such as emp or True. Therefore, we use a Hint
Mode to disable all the instances that would have this behavior. *)
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
Global Arguments MakeEmbed {_ _ _} _%I _%I.
Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
known_make_embed :> MakeEmbed P Q.
Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
Global Arguments MakeSep {_} _%I _%I _%I.
Global Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownl_make_sep :> MakeSep P Q PQ.
Global Arguments KnownLMakeSep {_} _%I _%I _%I.
Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownr_make_sep :> MakeSep P Q PQ.
Global Arguments KnownRMakeSep {_} _%I _%I _%I.
Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
Class MakeAnd {PROP : bi} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
Global Arguments MakeAnd {_} _%I _%I _%I.
Global Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownl_make_and :> MakeAnd P Q PQ.
Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownr_make_and :> MakeAnd P Q PQ.
Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
Global Arguments MakeOr {_} _%I _%I _%I.
Global Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
knownl_make_or :> MakeOr P Q PQ.
Global Arguments KnownLMakeOr {_} _%I _%I _%I.
Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
Global Arguments KnownRMakeOr {_} _%I _%I _%I.
Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
Global Arguments MakeAffinely {_} _%I _%I.
Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
known_make_affinely :> MakeAffinely P Q.
Global Arguments KnownMakeAffinely {_} _%I _%I.
Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
Global Arguments MakeIntuitionistically {_} _%I _%I.
Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
known_make_intuitionistically :> MakeIntuitionistically P Q.
Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
Global Arguments MakeAbsorbingly {_} _%I _%I.
Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
known_make_absorbingly :> MakeAbsorbingly P Q.
Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
Global Arguments MakePersistently {_} _%I _%I.
Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
known_make_persistently :> MakePersistently P Q.
Global Arguments KnownMakePersistently {_} _%I _%I.
Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Global Arguments MakeLaterN {_} _%nat _%I _%I.
Global Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
known_make_laterN :> MakeLaterN n P lP.
Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
Global Arguments MakeExcept0 {_} _%I _%I.
Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
Global Arguments KnownMakeExcept0 {_} _%I _%I.
Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
Global Arguments into_except_0 {_} _%I _%I {_}.
......
iris/proofmode/classes_make.v 0 → 100644
+ 138
− 0
View file @ 025885e6
(** The [MakeX] classes are "smart constructors" for the logical connectives
and modalities that perform some trivial logical simplifications to give "clean"
results.
For example, when framing below logical connectives/modalities, framing should
remove connectives/modalities if the result of framing is [emp]. For example,
when framing [P] (using [iFrame]) in goal [P ∗ Q], the result should be [Q]. The
result should not be [emp ∗ Q], where [emp] would be the result of (recursively)
framing [P] in [P]. Hence, in the recursive calls, the framing machinery uses
the class [MakeSep P Q PQ]. If either [P] or [Q] is [emp] (or [True] in case of
appropriate assumptions w.r.t. affinity), the result [PQ] is [Q] or [P],
respectively. In other cases, the result is [PQ] is simply [P ∗ Q].
The [MakeX] classes are used in each recursive step of the framing machinery.
Hence, they should be "constant time", which means that the number of steps in
the inference search for [MakeX] should not depend on the size of the inputs.
This implies that [MakeX] instances should not be recursive, and [MakeX]
instances should not have premises of other classes with recursive instances. In
particular, [MakeX] instances should not have [Affine] or [Absorbing] premises
(because these could invoke a recursive search). Instances for [MakeX] instances
typically look only at the top-level symbol of the input, or check if the whole
BI is affine (via the [BiAffine] class) -- the latter can be linear in
the size of `PROP` itself, but is still independent of the size of the term.
One could imagine a smarter way of "cleaning up", as implemented in
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
but that makes framing less predictable and might have some performance impact
(i.e., not be constant time). Hence, we only perform such cleanup for [True]
and [emp].
For each of the [MakeX] class, there is a [KnownMakeX] variant, which only
succeeds if the parameter(s) is not an evar. In the case the parameter(s) is an
evar, then [MakeX] will not instantiate it arbitrarily.
The reason for this is that if given an evar, these classes would typically
try to instantiate this evar with some arbitrary logical constructs such as
[emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances
that would have this behavior. *)
From iris.bi Require Export bi.
From iris.prelude Require Import options.
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
Global Arguments MakeEmbed {_ _ _} _%I _%I.
Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
known_make_embed :> MakeEmbed P Q.
Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
Global Arguments MakeSep {_} _%I _%I _%I.
Global Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownl_make_sep :> MakeSep P Q PQ.
Global Arguments KnownLMakeSep {_} _%I _%I _%I.
Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
knownr_make_sep :> MakeSep P Q PQ.
Global Arguments KnownRMakeSep {_} _%I _%I _%I.
Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
Class MakeAnd {PROP : bi} (P Q PQ : PROP) := make_and_l : P ∧ Q ⊣⊢ PQ.
Global Arguments MakeAnd {_} _%I _%I _%I.
Global Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownl_make_and :> MakeAnd P Q PQ.
Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
knownr_make_and :> MakeAnd P Q PQ.
Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
Global Arguments MakeOr {_} _%I _%I _%I.
Global Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
knownl_make_or :> MakeOr P Q PQ.
Global Arguments KnownLMakeOr {_} _%I _%I _%I.
Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
Global Arguments KnownRMakeOr {_} _%I _%I _%I.
Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely : <affine> P ⊣⊢ Q.
Global Arguments MakeAffinely {_} _%I _%I.
Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
known_make_affinely :> MakeAffinely P Q.
Global Arguments KnownMakeAffinely {_} _%I _%I.
Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
make_intuitionistically : □ P ⊣⊢ Q.
Global Arguments MakeIntuitionistically {_} _%I _%I.
Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
known_make_intuitionistically :> MakeIntuitionistically P Q.
Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : <absorb> P ⊣⊢ Q.
Global Arguments MakeAbsorbingly {_} _%I _%I.
Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
known_make_absorbingly :> MakeAbsorbingly P Q.
Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : <pers> P ⊣⊢ Q.
Global Arguments MakePersistently {_} _%I _%I.
Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
known_make_persistently :> MakePersistently P Q.
Global Arguments KnownMakePersistently {_} _%I _%I.
Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
make_laterN : ▷^n P ⊣⊢ lP.
Global Arguments MakeLaterN {_} _%nat _%I _%I.
Global Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
known_make_laterN :> MakeLaterN n P lP.
Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
make_except_0 : ◇ P ⊣⊢ Q.
Global Arguments MakeExcept0 {_} _%I _%I.
Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
known_make_except_0 :> MakeExcept0 P Q.
Global Arguments KnownMakeExcept0 {_} _%I _%I.
Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
iris/proofmode/monpred.v
+ 1
− 1
View file @ 025885e6
From iris.bi Require Export monpred.
From iris.bi Require Import plainly.
From iris.proofmode Require Import proofmode modality_instances.
From iris.proofmode Require Import proofmode classes_make modality_instances.
From iris.prelude Require Import options.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
......
iris/proofmode/proofmode.v
+ 2
− 1
View file @ 025885e6
......@@ -7,5 +7,6 @@ these files. *)
From iris.proofmode Require Import class_instances class_instances_later
class_instances_updates class_instances_embedding
class_instances_plainly class_instances_internal_eq.
From iris.proofmode Require Import frame_instances modality_instances.
From iris.proofmode Require Import class_instances_frame class_instances_make.
From iris.proofmode Require Import modality_instances.
From iris.prelude Require Import options.
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