Merge branch 'jh/fractional' into 'master'

Fractional typeclass.

A typeclass for fractional assertions, that is assertions that depend on a fraction and that can be split.

This is used to derive generically a few other instances for framing , destructing, combining and spliting assertions of sums of fractions. I found it usefull when doing fraction-heavy proofs in LambdaRust.

The Right Way  To Do It would be to use a typeclass over the *predicate* itself. Unfortunately, the unification algorithm of typeclasses is not powerful enough to do the right beta-expansion that would expose the predicate applied to some fraction. Instead, the `Fractional` type class has as parameters both the predicate and the applied form that can be directly unified with the fractured assertion. Not very pretty.

I wonder whether I should split this into two type classes: the first one would depend only on the predicate and would actually state the fractionality of it, and the second would do the beta-expansion job. What do you think?

See merge request !23

_CoqProject

@@ -83,6 +83,7 @@ base_logic/lib/boxes.v
 base_logic/lib/thread_local.v
 base_logic/lib/cancelable_invariants.v
 base_logic/lib/counter_examples.v
+base_logic/lib/fractional.v
 program_logic/adequacy.v
 program_logic/lifting.v
 program_logic/weakestpre.v

base_logic/lib/cancelable_invariants.v

-From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Export invariants fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -31,12 +31,11 @@ Section proofs.
   Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
-  Lemma cinv_own_op γ q1 q2 :
-    cinv_own γ q1 ∗ cinv_own γ q2 ⊣⊢ cinv_own γ (q1 + q2).
-  Proof. by rewrite /cinv_own own_op. Qed.
-
-  Lemma cinv_own_half γ q : cinv_own γ (q/2) ∗ cinv_own γ (q/2) ⊣⊢ cinv_own γ q.
-  Proof. by rewrite cinv_own_op Qp_div_2. Qed.
+  Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
+  Proof. intros ??. by rewrite -own_op. Qed.
+  Global Instance cinv_own_as_fractionnal γ q :
+    AsFractional (cinv_own γ q) (cinv_own γ) q.
+  Proof. done. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp.
   Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed.
@@ -56,7 +55,7 @@ Section proofs.
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
-    iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
+    iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
   Qed.
 
   Lemma cinv_open E N γ p P :
@@ -66,6 +65,6 @@ Section proofs.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose".
     - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
-    - iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
+    - iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
   Qed.
 End proofs.

base_logic/lib/fractional.v

+From iris.base_logic Require Export derived.
+From iris.proofmode Require Import classes class_instances.
+
+Class Fractional {M} (Φ : Qp → uPred M) :=
+  fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
+Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) :=
+  as_fractional : P ⊣⊢ Φ q.
+
+Arguments fractional {_ _ _} _ _.
+
+Hint Mode AsFractional - + - - : typeclass_instances.
+Hint Mode AsFractional - - + + : typeclass_instances.
+
+Section fractional.
+  Context {M : ucmraT}.
+  Implicit Types P Q : uPred M.
+  Implicit Types Φ : Qp → uPred M.
+  Implicit Types p q : Qp.
+
+  Lemma fractional_sep `{Fractional _ Φ} p q :
+    Φ (p + q)%Qp ⊢ Φ p ∗ Φ q.
+  Proof. by rewrite fractional. Qed.
+  Lemma sep_fractional `{Fractional _ Φ} p q :
+    Φ p ∗ Φ q ⊢ Φ (p + q)%Qp.
+  Proof. by rewrite fractional. Qed.
+  Lemma fractional_half_equiv `{Fractional _ Φ} p :
+    Φ p ⊣⊢ Φ (p/2)%Qp ∗ Φ (p/2)%Qp.
+  Proof. by rewrite -(fractional (p/2) (p/2)) Qp_div_2. Qed.
+  Lemma fractional_half `{Fractional _ Φ} p :
+    Φ p ⊢ Φ (p/2)%Qp ∗ Φ (p/2)%Qp.
+  Proof. by rewrite fractional_half_equiv. Qed.
+  Lemma half_fractional `{Fractional _ Φ} p q :
+    Φ (p/2)%Qp ∗ Φ (p/2)%Qp ⊢ Φ p.
+  Proof. by rewrite -fractional_half_equiv. Qed.
+
+  (** Mult instances *)
+
+  Global Instance mult_fractional_l Φ Ψ p :
+    (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Ψ → Fractional Φ.
+  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_l F. Qed.
+  Global Instance mult_fractional_r Φ Ψ p :
+    (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Ψ → Fractional Φ.
+  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_r F. Qed.
+
+  (* REMARK: These two instances do not work in either direction of the
+     search:
+       - In the forward direction, they make the search not terminate
+       - In the backward direction, the higher order unification of Φ
+         with the goal does not work. *)
+  Instance mult_as_fractional_l P Φ p q :
+    AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
+  Proof. done. Qed.
+  Instance mult_as_fractional_r P Φ p q :
+    AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
+  Proof. done. Qed.
+
+  (** Proof mode instances *)
+
+  Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → Fractional Φ →
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    FromSep P P1 P2.
+  Proof. by rewrite /FromSep=> -> -> -> ->. Qed.
+  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → Fractional Φ →
+    AsFractional P Φ (q1 + q2) →
+    FromSep P P1 P2 | 10.
+  Proof. by rewrite /FromSep=> -> -> <- ->. Qed.
+
+  Global Instance from_sep_fractional_half_fwd P Q Φ q :
+    AsFractional P Φ q → Fractional Φ →
+    AsFractional Q Φ (q/2) →
+    FromSep P Q Q | 10.
+  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=> -> -> ->. Qed.
+  Global Instance from_sep_fractional_half_bwd P Q Φ q :
+    AsFractional P Φ (q/2) → Fractional Φ →
+    AsFractional Q Φ q →
+    FromSep Q P P.
+  Proof. rewrite /FromSep=> -> <- ->. by rewrite Qp_div_2. Qed.
+
+  Global Instance into_and_fractional P P1 P2 Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → Fractional Φ →
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    IntoAnd false P P1 P2.
+  Proof. by rewrite /AsFractional /IntoAnd=>->->->->. Qed.
+  Global Instance into_and_fractional_half P Q Φ q :
+    AsFractional P Φ q → Fractional Φ →
+    AsFractional Q Φ (q/2) →
+    IntoAnd false P Q Q | 100.
+  Proof. by rewrite /AsFractional /IntoAnd -{1}(Qp_div_2 q)=>->->->. Qed.
+
+  Global Instance frame_fractional_l R Q PP' QP' Φ r p p' :
+    AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
+    Frame R (Φ p) Q → MakeSep Q (Φ p') QP' → Frame R PP' QP'.
+  Proof. rewrite /Frame=>->->-><-<-. by rewrite assoc. Qed.
+  Global Instance frame_fractional_r R Q PP' PQ Φ r p p' :
+    AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
+    Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ.
+  Proof.
+    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. done.
+  Qed.
+  Global Instance frame_fractional_half P Q R Φ p:
+    AsFractional R Φ (p/2) → AsFractional P Φ p → Fractional Φ →
+    AsFractional Q Φ (p/2)%Qp →
+    Frame R P Q.
+  Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed.
+
+End fractional.

heap_lang/heap.v

 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
 From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import wsat auth.
+From iris.base_logic.lib Require Import wsat auth fractional.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
@@ -78,46 +78,34 @@ Section heap.
   Proof. rewrite /heap_ctx. apply _. Qed.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
-
-  Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
+  Global Instance heap_mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
+    unfold Fractional; intros.
     by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
   Qed.
+  Global Instance heap_mapsto_as_fractional l q v :
+    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+  Proof. done. Qed.
 
-  Lemma heap_mapsto_op l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ ⌜v1 = v2⌝ ∧ l ↦{q1+q2} v1.
+  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
+    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    destruct (decide (v1 = v2)) as [->|].
-    { by rewrite heap_mapsto_op_eq pure_True // left_id. }
-    apply (anti_symm (⊢)); last by apply pure_elim_l.
-    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
-    eapply pure_elim; [done|] =>  /=.
-    rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
+    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid
+            op_singleton singleton_valid.
+    f_equiv. move=>[_ ] /=.
+    destruct (decide (v1 = v2)) as [->|?]; first done. by rewrite dec_agree_ne.
   Qed.
 
-  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝ ∧ l ↦{q1+q2} v1.
-  Proof. by rewrite heap_mapsto_op. Qed.
-
-  Lemma heap_mapsto_op_half l q v1 v2 :
-    l ↦{q/2} v1 ∗ l ↦{q/2} v2 ⊣⊢ ⌜v1 = v2⌝ ∧ l ↦{q} v1.
-  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
-
-  Lemma heap_mapsto_op_half_1 l q v1 v2 :
-    l ↦{q/2} v1 ∗ l ↦{q/2} v2 ⊢ ⌜v1 = v2⌝ ∧ l ↦{q} v1.
-  Proof. by rewrite heap_mapsto_op_half. Qed.
-
-  Lemma heap_ex_mapsto_op l q1 q2 : l ↦{q1} - ∗ l ↦{q2} - ⊣⊢ l ↦{q1+q2} -.
+  Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
   Proof.
-    iSplit.
+    intros p q. iSplit.
+    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
     - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
-      iDestruct (heap_mapsto_op_1 with "[$H1 $H2]") as "[% ?]"; subst; eauto.
-    - iDestruct 1 as (v) "H". rewrite -heap_mapsto_op_eq.
-      iDestruct "H" as "[H1 H2]"; iSplitL "H1"; eauto.
+      iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
   Qed.
-
-  Lemma heap_ex_mapsto_op_half l q : l ↦{q/2} - ∗ l ↦{q/2} - ⊣⊢ l ↦{q} -.
-  Proof. by rewrite heap_ex_mapsto_op Qp_div_2. Qed.
+  Global Instance heap_ex_mapsto_as_fractional l q :
+    AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
+  Proof. done. Qed.
 
   Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
   Proof.
@@ -126,7 +114,10 @@ Section heap.
   Qed.
   Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
     l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof. rewrite heap_mapsto_op heap_mapsto_valid. auto with I. Qed.
+  Proof.
+    iIntros "[H1 H2]". iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->.
+    iApply (heap_mapsto_valid l _ v2). by iFrame.
+  Qed.
 
   (** Weakest precondition *)
   Lemma wp_alloc E e v :

heap_lang/proofmode.v

@@ -12,10 +12,6 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Global Instance into_and_mapsto l q v :
-  IntoAnd false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoAnd heap_mapsto_op_eq Qp_div_2. Qed.
-
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E →