Commit a9d41b63 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Split the MakeXXX typeclasses into two, and add Hint Modes for them.

They are split into:
1- KnownMakeXXX , which only works if the parameter is not an evar. Hence, it will never force this evar to becomes e.g., emp or True.
2- MakeXXX, which works even if this is an evar, but it only has instances that will not instanciate arbitrarilly this evar.
parent db4424f2
Pipeline #7076 passed with stage
in 10 minutes and 49 seconds
......@@ -871,16 +871,13 @@ Proof.
rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
Qed.
Class MakeEmbed `{BiEmbedding PROP PROP'} P (Q : PROP') :=
make_embed : P Q.
Arguments MakeEmbed {_ _ _} _%I _%I.
Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ :
MakeEmbed ⌜φ⌝ ⌜φ⌝.
Proof. by rewrite /MakeEmbed bi_embed_pure. Qed.
KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
Proof. apply bi_embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
MakeEmbed emp emp.
Proof. by rewrite /MakeEmbed bi_embed_emp. Qed.
Global Instance make_embed_default `{BiEmbedding PROP PROP'} :
KnownMakeEmbed emp emp.
Proof. apply bi_embed_emp. Qed.
Global Instance make_embed_default `{BiEmbedding PROP PROP'} P :
MakeEmbed P P | 100.
Proof. by rewrite /MakeEmbed. Qed.
......@@ -894,20 +891,18 @@ Global Instance frame_pure_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') φ
Frame p ⌜φ⌝ P Q MakeEmbed Q Q' Frame p ⌜φ⌝ P Q'.
Proof. rewrite /Frame /MakeEmbed -bi_embed_pure. apply (frame_embed p P Q). Qed.
Class MakeSep (P Q PQ : PROP) := make_sep : P Q PQ.
Arguments MakeSep _%I _%I _%I.
Global Instance make_sep_emp_l P : MakeSep emp P P.
Proof. by rewrite /MakeSep left_id. Qed.
Global Instance make_sep_emp_r P : MakeSep P emp P.
Proof. by rewrite /MakeSep right_id. Qed.
Global Instance make_sep_true_l P : Absorbing P MakeSep True P P.
Proof. intros. by rewrite /MakeSep True_sep. Qed.
Global Instance make_and_emp_l_absorbingly P : MakeSep True P (bi_absorbingly P) | 10.
Proof. intros. by rewrite /MakeSep. Qed.
Global Instance make_sep_true_r P : Absorbing P MakeSep P True P.
Proof. intros. by rewrite /MakeSep sep_True. Qed.
Global Instance make_and_emp_r_absorbingly P : MakeSep P True (bi_absorbingly P) | 10.
Proof. intros. by rewrite /MakeSep comm. 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_and_emp_l_absorbingly P : KnownLMakeSep True P (bi_absorbingly P) | 10.
Proof. intros. by rewrite /KnownLMakeSep /MakeSep. 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_and_emp_r_absorbingly P : KnownRMakeSep P True (bi_absorbingly P) | 10.
Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P Q) | 100.
Proof. by rewrite /MakeSep. Qed.
......@@ -937,20 +932,18 @@ Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
Frame p R ([ list] k y l, Φ k y) Q.
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
Class MakeAnd (P Q PQ : PROP) := make_and : P Q PQ.
Arguments MakeAnd _%I _%I _%I.
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_emp_l P : Affine P MakeAnd emp P P.
Proof. intros. by rewrite /MakeAnd emp_and. Qed.
Global Instance make_and_emp_l_affinely P : MakeAnd emp P (bi_affinely P) | 10.
Proof. intros. by rewrite /MakeAnd. Qed.
Global Instance make_and_emp_r P : Affine P MakeAnd P emp P.
Proof. intros. by rewrite /MakeAnd and_emp. Qed.
Global Instance make_and_emp_r_affinely P : MakeAnd P emp (bi_affinely P) | 10.
Proof. intros. by rewrite /MakeAnd comm. 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_l_affinely P : KnownLMakeAnd emp P (bi_affinely P) | 10.
Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. 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_emp_r_affinely P : KnownRMakeAnd P emp (bi_affinely P) | 10.
Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
......@@ -965,16 +958,14 @@ Proof.
[rewrite and_elim_l|rewrite and_elim_r]; done.
Qed.
Class MakeOr (P Q PQ : PROP) := make_or : P Q PQ.
Arguments MakeOr _%I _%I _%I.
Global Instance make_or_true_l P : MakeOr True P True.
Proof. by rewrite /MakeOr left_absorb. Qed.
Global Instance make_or_true_r P : MakeOr P True True.
Proof. by rewrite /MakeOr right_absorb. Qed.
Global Instance make_or_emp_l P : Affine P MakeOr emp P emp.
Proof. intros. by rewrite /MakeOr emp_or. Qed.
Global Instance make_or_emp_r P : Affine P MakeOr P emp emp.
Proof. intros. by rewrite /MakeOr or_emp. 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.
......@@ -1013,12 +1004,10 @@ Proof.
by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.
Class MakeAffinely (P Q : PROP) := make_affinely : bi_affinely P Q.
Arguments MakeAffinely _%I _%I.
Global Instance make_affinely_True : MakeAffinely True emp | 0.
Proof. by rewrite /MakeAffinely affinely_True_emp affinely_emp. Qed.
Global Instance make_affinely_affine P : Affine P MakeAffinely P P | 1.
Proof. intros. by rewrite /MakeAffinely affine_affinely. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
Global Instance make_affinely_affine P : Affine P KnownMakeAffinely P P | 1.
Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed.
Global Instance make_affinely_default P : MakeAffinely P (bi_affinely P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
......@@ -1029,10 +1018,11 @@ Proof.
by rewrite -{1}affinely_idemp affinely_sep_2.
Qed.
Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : bi_absorbingly P Q.
Arguments MakeAbsorbingly _%I _%I.
Global Instance make_absorbingly_emp : MakeAbsorbingly emp True | 0.
Proof. by rewrite /MakeAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
Proof.
by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-absorbingly_True_emp absorbingly_pure.
Qed.
(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
because framing will never turn a proposition that is not absorbing into
something that is absorbing. *)
......@@ -1043,12 +1033,13 @@ Global Instance frame_absorbingly p R P Q Q' :
Frame p R P Q MakeAbsorbingly Q Q' Frame p R (bi_absorbingly P) Q'.
Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed.
Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P Q.
Arguments MakePersistently _%I _%I.
Global Instance make_persistently_true : MakePersistently True True.
Proof. by rewrite /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_emp : MakePersistently emp True.
Proof. by rewrite /MakePersistently -persistently_True_emp persistently_pure. Qed.
Global Instance make_persistently_true : @KnownMakePersistently PROP True True.
Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
Proof.
by rewrite /KnownMakePersistently /MakePersistently
-persistently_True_emp persistently_pure.
Qed.
Global Instance make_persistently_default P :
MakePersistently P (bi_persistently P) | 100.
Proof. by rewrite /MakePersistently. Qed.
......@@ -1536,10 +1527,8 @@ Global Instance frame_eq_embed `{SbiEmbedding PROP PROP'} p P Q (Q' : PROP')
Frame p (a b) P Q MakeEmbed Q Q' Frame p (a b) P Q'.
Proof. rewrite /Frame /MakeEmbed -sbi_embed_internal_eq. apply (frame_embed p P Q). Qed.
Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ^n P lP.
Arguments MakeLaterN _%nat _%I _%I.
Global Instance make_laterN_true n : MakeLaterN n True True | 0.
Proof. by rewrite /MakeLaterN laterN_True. 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_0 P : MakeLaterN 0 P P | 0.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance make_laterN_1 P : MakeLaterN 1 P ( P) | 2.
......@@ -1569,11 +1558,8 @@ Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q :
Frame p R P Q Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
Class MakeExcept0 (P Q : PROP) := make_except_0 : P Q.
Arguments MakeExcept0 _%I _%I.
Global Instance make_except_0_True : MakeExcept0 True True.
Proof. by rewrite /MakeExcept0 except_0_True. 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.
......
......@@ -389,6 +389,94 @@ 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,
  • Could you somewhere describe the motivation for this. Why do we need these different classes?

    (The commit message does not say so either).

  • I added a bit more comment. Tell me if you want me to expand.

  • I think I get it now. Cannot we directly use KnownRMakeSep in frame_sep_l (and similarly at other places)?

  • No: In frame_sep_l, it is very possible that P2 be an evar. Moreover, make_sep_default does not apply to KnownRMakeSep.

  • Isn't there a way to do this more generally, have typeclass instances only apply if some argument doesn't contain evars? I imagine a class like

    Class EvarFree {T : Type} (t1 t2: T) := evar_free : t1 = t2.
    Hint Mode EvarFree + + !.
    Global Instance {T : Type} (t: T) : EvarFree t t := eq_refl.

    and then instances like

    Global Instance make_except_0_True P : @EvarFree PROP True P -> @MakeExcept0 PROP P True.

    okay this is very unreadable...

    Edited by Ralf Jung
  • Also, these class were in class_instances before, now they are defined here. Why the move? Was there a good reason they were defined elsewhere before?

  • Isn't there a way to do this more generally, have typeclass instances only apply if some argument doesn't contain evars? I imagine a class like

    I already thought about this, but this actually does not work. Think about make_sep_emp: Here, the thing that needs to not be an evar is emp. There is no way of using EvarFree for it.

    Edited by Jacques-Henri Jourdan
  • Also, these class were in class_instances before, now they are defined here. Why the move? Was there a good reason they were defined elsewhere before?

    First, these are classes, so they should be put in classes.v. Second, most of class_instances is in sections, and the declaration of classes has to be done outside of sections, because Hint Mode is not exported from sections.

  • I already thought about this, but this actually does not work. Think about make_sep_emp: Here, the thing that need to not be an evar is emp. There is no way of using EvarFree for it.

    Global Instance make_sep_emp_l P Q : EvarFree emp Q -> MakeSep Q P P.
    Edited by Ralf Jung
  • First, these are classes, so they should be put in classes.v.

    @robbertkrebbers why are some classes here and some there? My interpretation was that classes.v is for "externally visible" classes only that users are supposed to implement for their extensions.

  • That was indeed the idea. Now sure if that principle is still preserved.

  • I already thought about this, but this actually does not work. Think about make_sep_emp: Here, > the thing that need to not be an evar is emp. There is no way of using EvarFree for it.

    Global Instance make_sep_emp_l P Q : EvarFree emp Q -> MakeSep Q P P.

    Oh, sorry, I did not see EvarFree had two parameters (you edited it, didn't you?). Your EvarFree type class is essentially some form of TCEq. The issue using this is that you essentially change the statement of all these instances into something that is less readable. So it is arguable what is the best.

  • @robbertkrebbers why are some classes here and some there? My interpretation was that classes.v is for "externally visible" classes only that users are supposed to implement for their extensions.

    I was not aware of this distinction. In any case, MakeSep is also used in fractional...

  • Oh, sorry, I did not see EvarFree had two parameters (you edited it, didn't you?).

    Yes I did, after realizing that my first proposal doesn't work. Sorry for that.

  • The issue using this is that you essentially change the statement of all these instances into something that is less readable. So it is arguable what is the best.

    True. OTOH, adding a dozen new typeclasses doesn't make this much more readable either. The general proposal is at least uniform.

    Also, doesn't this change resolution behavior? Now typeclass search has to first apply the coercions that turn the Make goals into KnownMake to apply those, seems like that could affect backtracking? We have to be careful not to descend on both of them, for example, or we'll get exponential blowup.

  • Also, doesn't this change resolution behavior? Now typeclass search has to first apply the coercions that turn the Make goals into KnownMake to apply those, seems like that could affect backtracking? We have to be careful not to descend on both of them, for example, or we'll get exponential blowup.

    I do not see why this would create any exponential blowup. All the backtracking that is now possible was previously possible.

    Frankly, I think this is really a detail. If you want to change this to a version using something like EvarFree, then please do. Otherwise, I really do not think we now have time to lose on discussing this kind of details.

  • Frankly, I think this is really a detail.

    Agreed, let's focus on interesting issues like #161 (closed), #126 (closed), !121 (merged)

  • Sure. I was just trying to understand better what is going on.

Please register or sign in to reply
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. *)
Class MakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : P Q.
Arguments MakeEmbed {_ _ _ _} _%I _%I.
Hint Mode MakeEmbed + + + + - - : typeclass_instances.
Class KnownMakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
go_make_embed :> MakeEmbed P Q.
Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P Q PQ .
Arguments MakeSep {_} _%I _%I _%I.
Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) := gol_make_sep :> MakeSep P Q PQ.
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) := gor_make_sep :> MakeSep P Q PQ.
Arguments KnownRMakeSep {_} _%I _%I _%I.
Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
Class MakeAnd {PROP : bi} (P Q PQ : PROP) := make_and_l : P Q PQ.
Arguments MakeAnd {_} _%I _%I _%I.
Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) := gol_make_and :> MakeAnd P Q PQ.
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) := gor_make_and :> MakeAnd P Q PQ.
Arguments KnownRMakeAnd {_} _%I _%I _%I.
Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P Q PQ.
Arguments MakeOr {_} _%I _%I _%I.
Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) := gol_make_or :> MakeOr P Q PQ.
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := gor_make_or :> MakeOr P Q PQ.
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
Class MakeAffinely {PROP : bi} (P Q : PROP) :=
make_affinely :> bi_affinely P Q.
Arguments MakeAffinely {_} _%I _%I.
Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
go_make_affinely : MakeAffinely P Q.
Arguments KnownMakeAffinely {_} _%I _%I.
Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
make_absorbingly : bi_absorbingly P Q.
Arguments MakeAbsorbingly {_} _%I _%I.
Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
go_make_absorbingly :> MakeAbsorbingly P Q.
Arguments KnownMakeAbsorbingly {_} _%I _%I.
Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
Class MakePersistently {PROP : bi} (P Q : PROP) :=
make_persistently : bi_persistently P Q.
Arguments MakePersistently {_} _%I _%I.
Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
go_make_persistently :> MakePersistently P Q.
Arguments KnownMakePersistently {_} _%I _%I.
Hint Mode KnownMakePersistently + ! - : typeclass_instances.
Class MakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
make_laterN : ^n P lP.
Arguments MakeLaterN {_} _%nat _%I _%I.
Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
go_make_laterN :> MakeLaterN n P lP.
Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
Class MakeExcept0 {PROP : sbi} (P Q : PROP) :=
make_except_0 : sbi_except_0 P Q.
Arguments MakeExcept0 {_} _%I _%I.
Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : sbi} (P Q : PROP) :=
go_make_except_0 :> MakeExcept0 P Q.
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P Q.
Arguments IntoExcept0 {_} _%I _%I : simpl never.
Arguments into_except_0 {_} _%I _%I {_}.
......
......@@ -369,4 +369,15 @@ Proof.
iMatchHyp (fun H _ =>
iApply ("H" with [spec_patterns.SIdent H; spec_patterns.SIdent "HQ"])).
Qed.
Lemma iFrame_with_evar_r P Q :
P - Q - R, P R.
Proof.
iIntros "HP HQ". iExists _. iFrame. iApply "HQ".
Qed.
Lemma iFrame_with_evar_l P Q :
P - Q - R, R P.
Proof.
iIntros "HP HQ". iExists _. iFrame. iApply "HQ".
Qed.
  • These tests succeeded before, right? The point of this commit is to make iFrame fail in certain situations where it worked before. Could you add tests with Fail for that?

    Edited by Ralf Jung
  • No, the first test (or the second, I do not remember) failed before. iFrame instantiated the evar with emp, because the wrong MakeSep instance was used.

Please register or sign in to reply
End tests.
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