Merge branch 'robbert/lc_proofmode_fix' into 'master'

Tweak priority of proof mode instances for £.

Closes #470

See merge request iris/iris!818

iris/base_logic/lib/later_credits.v

@@ -105,24 +105,26 @@ Section later_credit_theory.
     rewrite lc_unseal /lc_def. apply _.
   Qed.
 
+  (** Make sure that the rule for [+] is used before [S], otherwise Coq's
+  unification applies the [S] hint too eagerly. See Iris issue #470. *)
   Global Instance from_sep_lc_add n m :
-    FromSep (£ (n + m)) (£ n) (£ m).
+    FromSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /FromSep lc_split.
   Qed.
   Global Instance from_sep_lc_S n :
-    FromSep (£ (S n)) (£ 1) (£ n).
+    FromSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /FromSep (lc_succ n).
   Qed.
 
   Global Instance into_sep_lc_add n m :
-    IntoSep (£ (n + m)) (£ n) (£ m).
+    IntoSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /IntoSep lc_split.
   Qed.
   Global Instance into_sep_lc_S n :
-    IntoSep (£ (S n)) (£ 1) (£ n).
+    IntoSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /IntoSep (lc_succ n).
   Qed.

tests/proofmode_iris.ref

@@ -172,6 +172,38 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 The command has indeed failed with message:
 Tactic failure: iMod: "H" not fresh.
+"test_iIntros_lc"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  "Hlc2" : £ m
+  --------------------------------------∗
+  £ (S n)
+"lc_iSplit_lc"
+     : string
+2 goals
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  --------------------------------------∗
+  £ (S n)
+
+goal 2 is:
+ "Hlc2" : £ m
+ --------------------------------------∗
+ £ m
 "test_iInv"
      : string
 1 goal

tests/proofmode_iris.v

@@ -250,6 +250,15 @@ Section iris_tests.
     iIntros "H H'". Fail iDestruct "H'" as ">H".
   Abort.
 
+  (** Make sure that the splitting rule for [+] gets priority over the one for
+  [S]. See issue #470. *)
+  Check "test_iIntros_lc".
+  Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).
+  Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
+
+  Check "lc_iSplit_lc".
+  Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
+  Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
 End iris_tests.
 
 Section monpred_tests.