Commit cb8e35b8 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/frac-combine' into 'master'

fix combining two q/2 fractions to a q

See merge request iris/iris!540
parents af0efbba 96455f78
......@@ -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
......
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.
......
......@@ -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.
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