Commit 50520536 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan Committed by Ralf Jung

Fractional typeclass.

parent b81fb420
......@@ -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
......
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.
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.
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 :
......
......@@ -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
......
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