From 96455f78404f95a284ce490e9e5c38e03a0b0985 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 10 Oct 2020 12:05:23 +0200
Subject: [PATCH] fix combining two q/2 fractions to a q

---
 tests/proofmode_iris.ref | 29 +++++++++++++++++++++++++++++
 tests/proofmode_iris.v   | 11 +++++++++++
 theories/algebra/frac.v  |  2 +-
 3 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 9cbbce1b7..100a162b6 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -115,6 +115,35 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
+"test_frac_split_combine"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  inG0 : inG Σ fracR
+  γ : gname
+  ============================
+  "H1" : own γ (1 / 2)%Qp
+  "H2" : own γ (1 / 2)%Qp
+  --------------------------------------∗
+  own γ 1%Qp
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  inG0 : inG Σ fracR
+  γ : gname
+  ============================
+  "H" : own γ 1%Qp
+  --------------------------------------∗
+  own γ 1%Qp
+  
 "test_iInv"
      : string
 1 subgoal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 416707464..e3e510200 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics monpred.
+From iris.algebra Require Import frac.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
@@ -236,6 +237,16 @@ Section iris_tests.
     x' ≼ x →
     own γ x -∗ own γ x'.
   Proof. intros. by iApply own_mono. Qed.
+
+  Check "test_frac_split_combine".
+  Lemma test_frac_split_combine `{!inG Σ fracR} γ :
+    own γ 1%Qp -∗ own γ 1%Qp.
+  Proof.
+    iIntros "[H1 H2]". Show.
+    iCombine "H1 H2" as "H". Show.
+    iExact "H".
+  Qed.
+
 End iris_tests.
 
 Section monpred_tests.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 4fea0470c..017254200 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -60,5 +60,5 @@ Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
 
 (* This one has a higher precendence than [is_op_op] so we get a [+] instead
    of an [â‹…]. *)
-Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2.
+Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
 Proof. done. Qed.
-- 
GitLab