Split [FromAssumption] into three, depending on wheter the parameters are...

Split [FromAssumption] into three, depending on wheter the parameters are evars. This is to avoid loops in TC search.

theories/proofmode/class_instances.v

@@ -27,34 +27,55 @@ Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
 Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
 
 Global Instance from_assumption_persistently_r P Q :
-  FromAssumption true P Q → FromAssumption true P (bi_persistently Q).
+  FromAssumption true P Q → KnownRFromAssumption true P (bi_persistently Q).
 Proof.
-  rewrite /FromAssumption /= =><-.
+  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
   by rewrite -{1}affinely_persistently_idemp affinely_elim.
 Qed.
 Global Instance from_assumption_affinely_r P Q :
-  FromAssumption true P Q → FromAssumption true P (bi_affinely Q).
-Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
+  FromAssumption true P Q → KnownRFromAssumption true P (bi_affinely Q).
+Proof.
+  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
+  by rewrite affinely_idemp.
+Qed.
 Global Instance from_assumption_absorbingly_r p P Q :
-  FromAssumption p P Q → FromAssumption p P (bi_absorbingly Q).
-Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (bi_absorbingly Q).
+Proof.
+  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
+  apply absorbingly_intro.
+Qed.
 
 Global Instance from_assumption_affinely_persistently_l p P Q :
-  FromAssumption true P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
+  FromAssumption true P Q → KnownLFromAssumption p (□ P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  by rewrite affinely_persistently_if_elim.
+Qed.
 Global Instance from_assumption_persistently_l_true P Q :
-  FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
+  FromAssumption true P Q → KnownLFromAssumption true (bi_persistently P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  by rewrite persistently_idemp.
+Qed.
 Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
-  FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
+  FromAssumption true P Q → KnownLFromAssumption false (bi_persistently P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  by rewrite affine_affinely.
+Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
-  FromAssumption p P Q → FromAssumption p (bi_affinely P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_elim. Qed.
+  FromAssumption p P Q → KnownLFromAssumption p (bi_affinely P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  by rewrite affinely_elim.
+Qed.
 
 Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
-  FromAssumption p (Φ x) Q → FromAssumption p (∀ x, Φ x) Q.
-Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
+  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀ x, Φ x) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption=> <-.
+  by rewrite forall_elim.
+Qed.
 
 (* IntoPure *)
 Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
@@ -999,32 +1020,32 @@ Implicit Types P Q R : PROP.
 
 (* FromAssumption *)
 Global Instance from_assumption_later p P Q :
-  FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
-Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (▷ Q)%I.
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply later_intro. Qed.
 Global Instance from_assumption_laterN n p P Q :
-  FromAssumption p P Q → FromAssumption p P (▷^n Q)%I.
-Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q)%I.
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply laterN_intro. Qed.
 Global Instance from_assumption_except_0 p P Q :
-  FromAssumption p P Q → FromAssumption p P (◇ Q)%I.
-Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (◇ Q)%I.
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply except_0_intro. Qed.
 
 Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
-  FromAssumption p P Q → FromAssumption p P (|==> Q).
-Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
 Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q :
-  FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
+  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)%I.
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
 
 Global Instance from_assumption_plainly_l_true `{BiPlainly PROP} P Q :
-  FromAssumption true P Q → FromAssumption true (■ P) Q.
+  FromAssumption true P Q → KnownLFromAssumption true (■ P) Q.
 Proof.
-  rewrite /FromAssumption /= =><-.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
   by rewrite persistently_elim plainly_elim_persistently.
 Qed.
 Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP} P Q :
-  FromAssumption true P Q → FromAssumption false (■ P) Q.
+  FromAssumption true P Q → KnownLFromAssumption false (■ P) Q.
 Proof.
-  rewrite /FromAssumption /= =><-.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
   by rewrite affine_affinely plainly_elim_persistently.
 Qed.
 

theories/proofmode/classes.v

@@ -8,10 +8,20 @@ Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   from_assumption : □?p P ⊢ Q.
 Arguments FromAssumption {_} _ _%I _%I : simpl never.
 Arguments from_assumption {_} _ _%I _%I {_}.
-(* No need to restrict Hint Mode, we have a default instance that will always
-be used in case of evars *)
 Hint Mode FromAssumption + + - - : typeclass_instances.
 
+Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
+  knownl_from_assumption :> FromAssumption p P Q.
+Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
+Arguments knownl_from_assumption {_} _ _%I _%I {_}.
+Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
+
+Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
+  knownr_from_assumption :> FromAssumption p P Q.
+Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
+Arguments knownr_from_assumption {_} _ _%I _%I {_}.
+Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
+
 Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
   into_pure : P ⊢ ⌜φ⌝.
 Arguments IntoPure {_} _%I _%type_scope : simpl never.

theories/proofmode/monpred.v

@@ -123,24 +123,30 @@ Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P 𝓟 :
 Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
 
 Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
-  MakeMonPredAt i P 𝓟 → IsBiIndexRel j i → FromAssumption p (P j) 𝓟.
+  MakeMonPredAt i P 𝓟 → IsBiIndexRel j i → KnownLFromAssumption p (P j) 𝓟.
 Proof.
-  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
+  rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
   apply  bi.affinely_persistently_if_elim.
 Qed.
 Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
-  MakeMonPredAt i P 𝓟 → IsBiIndexRel i j → FromAssumption p 𝓟 (P j).
+  MakeMonPredAt i P 𝓟 → IsBiIndexRel i j → KnownRFromAssumption p 𝓟 (P j).
 Proof.
-  rewrite /MakeMonPredAt /FromAssumption /IsBiIndexRel=><- ->.
+  rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
   apply  bi.affinely_persistently_if_elim.
 Qed.
 
 Global Instance from_assumption_make_monPred_absolutely P Q :
-  FromAssumption p P Q → FromAssumption p (∀ᵢ P) Q.
-Proof. intros ?. by rewrite /FromAssumption monPred_absolutely_elim. Qed.
+  FromAssumption p P Q → KnownLFromAssumption p (∀ᵢ P) Q.
+Proof.
+  intros ?.
+  by rewrite /KnownLFromAssumption /FromAssumption monPred_absolutely_elim.
+Qed.
 Global Instance from_assumption_make_monPred_relatively P Q :
-  FromAssumption p P Q → FromAssumption p P (∃ᵢ Q).
-Proof. intros ?. by rewrite /FromAssumption -monPred_relatively_intro. Qed.
+  FromAssumption p P Q → KnownRFromAssumption p P (∃ᵢ Q).
+Proof.
+  intros ?.
+  by rewrite /KnownRFromAssumption /FromAssumption -monPred_relatively_intro.
+Qed.
 
 Global Instance as_valid_monPred_at φ P (Φ : I → PROP) :
   AsValid0 φ P → (∀ i, MakeMonPredAt i P (Φ i)) → AsValid φ (∀ i, Φ i) | 100.

[Ralf Jung]

With MakeSep, I can understand what L and R mean -- left- and right-hand-side of the operator. But with FromAssumption, what's this supposed to mean?

Also, the more classes we convert to this, the more I am convinced that we want some more generic approach instead -- if we keep going this way, we'll end up having three times as many typeclasses as we used to. And we already had extremely many. Introducing equalities (like I suggested elsewhere) is not nice, but at least it's a per-Instance thing -- so, the "interface" (which typeclasses exist and what they do) is not affected. That's a significant advantage, IMHO.

[Jacques-Henri Jourdan]

With MakeSep, I can understand what L and R mean -- left- and right-hand-side of the operator. But with FromAssumption, what's this supposed to mean?

To me FromAssumption is essentially a type class trying to unify to assertions. L means we know the left assumption and R means we need the right. Perhaps that's not a good name.

Also, the more classes we convert to this, the more I am convinced that we want some more generic approach instead -- if we keep going this way, we'll end up having three times as many typeclasses as we used to. And we already had extremely many. Introducing equalities (like I suggested elsewhere) is not nice, but at least it's a per-Instance thing -- so, the "interface" (which typeclasses exist and what they do) is not affected. That's a significant advantage, IMHO.

Yeah, it seems like you are right. Although I am not that opposed to increase the number of TCs.

[Ralf Jung]

To me FromAssumption is essentially a type class trying to unify to assertions. L means we know the left assumption and R means we need the right. Perhaps that's not a good name.

Well, it's somewhat different from the usual "left/right-hand-side of operator". Also, FromAssumption is not symmetric. "known assumption" and "known conclusion" would be much more informative, can anyone think of some nice abbreviation for that?

[Robbert Krebbers]

Let's make an issue for the more generic approach. We can try that later.

[Robbert Krebbers]

I would also like to investigate performance impact of both approaches.

[Ralf Jung]

Done: https://gitlab.mpi-sws.org/FP/iris-coq/issues/165