Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode

theories/proofmode/class_instances_bi.v

@@ -386,23 +386,73 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
+Global Instance into_wand_affine p q R P Q :
+  IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
+Proof.
+  rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
+  - rewrite (affinely_elim R) -(affine_affinely (□ R)%I) HR. destruct q; simpl in *.
+    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)%I).
+      by rewrite affinely_sep_2 wand_elim_l.
+    + by rewrite affinely_sep_2 wand_elim_l.
+  - rewrite HR. destruct q; simpl in *.
+    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)%I).
+      by rewrite affinely_sep_2 wand_elim_l.
+    + by rewrite affinely_sep_2 wand_elim_l.
+Qed.
+(* In case the argument is affine, but the wand resides in the spatial context,
+we can only eliminate the affine modality in the argument. This would lead to
+the following instance:
+
+  IntoWand false q R P Q → IntoWand' false q R (<affine> P) Q.
+
+This instance is redundant, however, since the elimination of the affine
+modality is already covered by the [IntoAssumption] instances that are used at
+the leaves of the instance search for [IntoWand]. *)
+Global Instance into_wand_affine_args q R P Q :
+  IntoWand true q R P Q → IntoWand' true q R (<affine> P) (<affine> Q).
+Proof.
+  rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
+  rewrite -(affine_affinely (□ R)%I) HR. destruct q; simpl.
+  - rewrite (affinely_elim P) -{2}(affine_affinely (□ P)%I).
+    by rewrite affinely_sep_2 wand_elim_l.
+  - by rewrite affinely_sep_2 wand_elim_l.
+Qed.
+
 Global Instance into_wand_intuitionistically p q R P Q :
-  IntoWand p q R P Q → IntoWand p q (□ R) P Q.
-Proof. by rewrite /IntoWand intuitionistically_elim. Qed.
+  IntoWand true q R P Q → IntoWand p q (□ R) P Q.
+Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
 Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
 Global Instance into_wand_persistently_false q R P Q :
   Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
-Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q (PP QQ RR : PROP) (P : PROP') :
-  IntoWand p q RR PP QQ →
-  IntoEmbed P PP →
-  IntoWand p q ⎡RR⎤ P ⎡QQ⎤.
-Proof.
-  rewrite /IntoEmbed /IntoWand !embed_intuitionistically_if_2=> -> ->.
-  apply bi.wand_intro_l.
-  by rewrite embed_intuitionistically_if_2 -embed_sep bi.wand_elim_r.
+
+Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
+  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
+
+(* There are two versions for [IntoWand ⎡RR⎤ ...] with the argument being
+[<affine> ⎡PP⎤]. When the wand [⎡RR⎤] resides in the intuitionistic context
+the result of wand elimination will have the affine modality. Otherwise, it
+won't. Note that when the wand [⎡RR⎤] is under an affine modality, the instance
+[into_wand_affine] would already have been used. *)
+Global Instance into_wand_affine_embed_true `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
+  IntoWand true q RR PP QQ → IntoWand true q ⎡RR⎤ (<affine> ⎡PP⎤) (<affine> ⎡QQ⎤) | 100.
+Proof.
+  rewrite /IntoWand /=.
+  rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
+  apply bi.wand_intro_l. destruct q; simpl.
+  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤%I).
+    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
+    by rewrite wand_elim_r intuitionistically_affinely.
+  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
+Qed.
+Global Instance into_wand_affine_embed_false `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
+  IntoWand false q RR (<affine> PP) QQ → IntoWand false q ⎡RR⎤ (<affine> ⎡PP⎤) ⎡QQ⎤ | 100.
+Proof.
+  rewrite /IntoWand /= => ->.
+  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
 Qed.
 
 (* FromWand *)

theories/proofmode/classes.v

@@ -482,14 +482,12 @@ Proof. apply _. Qed.
 (** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
 embeddings using [iModIntro].
 
-Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤].
-Also used backwards, i.e. Input [Q] and output [P]. *)
+Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
 Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
   into_embed : P ⊢ ⎡Q⎤.
 Arguments IntoEmbed {_ _ _} _%I _%I.
 Arguments into_embed {_ _ _} _%I _%I {_}.
 Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
-Hint Mode IntoEmbed + + + - !  : typeclass_instances.
 
 (* We use two type classes for [AsEmpValid], in order to avoid loops in
    typeclass search. Indeed, the [as_emp_valid_embed] instance would try