diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v index 468990508e39148a52f07b3b2fe0d4c2c306baa7..08a3e348bdc8a99280edfa0e7f7bbe21d290b181 100644 --- a/theories/base_logic/lib/cancelable_invariants.v +++ b/theories/base_logic/lib/cancelable_invariants.v @@ -35,7 +35,7 @@ Section proofs. Proof. intros ??. by rewrite -own_op. Qed. Global Instance cinv_own_as_fractionnal γ q : AsFractional (cinv_own γ q) (cinv_own γ) q. - Proof. done. Qed. + Proof. split. done. apply _. Qed. Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp. Proof. apply (own_valid_2 γ q1 q2). Qed. diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v index 98c4a03dfad61ca3873681e9b0775057c5e78c49..cce3c8057cab7271dfe4d73f59ecfda721086cf5 100644 --- a/theories/base_logic/lib/fractional.v +++ b/theories/base_logic/lib/fractional.v @@ -5,8 +5,10 @@ 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. +Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) := { + as_fractional : P ⊣⊢ Φ q; + as_fractional_fractional :> Fractional Φ +}. Arguments fractional {_ _ _} _ _. @@ -78,11 +80,15 @@ Section fractional. (** 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. + (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ. + Proof. + intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_l. by apply H. + 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. + (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ. + Proof. + intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_r. by apply H. + Qed. (* REMARK: These two instances do not work in either direction of the search: @@ -91,58 +97,71 @@ Section fractional. 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. + Proof. + intros H. split. apply H. eapply (mult_fractional_l _ Φ p). + split. done. apply H. + Qed. Instance mult_as_fractional_r P Φ p q : AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q. - Proof. done. Qed. + Proof. + intros H. split. apply H. eapply (mult_fractional_r _ Φ p). + split. done. apply H. + 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 → + AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → FromSep P P1 P2. - Proof. by rewrite /FromSep=> -> -> -> ->. Qed. + 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) → + AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) → FromSep P P1 P2 | 10. - Proof. by rewrite /FromSep=> -> -> <- ->. Qed. + Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed. Global Instance from_sep_fractional_half_fwd P Q Φ q : - AsFractional P Φ q → Fractional Φ → - AsFractional Q Φ (q/2) → + AsFractional P Φ q → AsFractional Q Φ (q/2) → FromSep P Q Q | 10. - Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=> -> -> ->. Qed. + 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 → + AsFractional P Φ (q/2) → AsFractional Q Φ q → FromSep Q P P. - Proof. rewrite /FromSep=> -> <- ->. by rewrite Qp_div_2. Qed. + 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 → + AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → IntoAnd false P P1 P2. - Proof. by rewrite /AsFractional /IntoAnd=>->->->->. Qed. + Proof. by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. Qed. Global Instance into_and_fractional_half P Q Φ q : - AsFractional P Φ q → Fractional Φ → - AsFractional Q Φ (q/2) → + AsFractional P Φ q → 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. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed. + + (* The instance [frame_fractional] can be tried at all the nodes of + the proof search. The proof search then fails almost always on + [AsFractional R Φ r], but the slowdown is still noticeable. For + that reason, we factorize the three instances that could ave been + defined for that purpose into one. *) + Inductive FrameFractionalHyps R Φ RES : Qp → Qp → Prop := + | frame_fractional_hyps_l Q p p' r: + Frame R (Φ p) Q → MakeSep Q (Φ p') RES → + FrameFractionalHyps R Φ RES r (p + p') + | frame_fractional_hyps_r Q p p' r: + Frame R (Φ p') Q → MakeSep Q (Φ p) RES → + FrameFractionalHyps R Φ RES r (p + p') + | frame_fractional_hyps_half p: + AsFractional RES Φ (p/2)%Qp → FrameFractionalHyps R Φ RES (p/2)%Qp p. + Existing Class FrameFractionalHyps. + Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r + frame_fractional_hyps_half. + Global Instance frame_fractional R r Φ P p RES: + AsFractional R Φ r → AsFractional P Φ p → FrameFractionalHyps R Φ RES r p → + Frame R P RES. Proof. - rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. + rewrite /Frame=>-[HR _][->?]H. + revert H HR=>-[Q p0 p0' r0|Q p0 p0' r0|p0]. + - rewrite fractional=><-<-. by rewrite assoc. + - rewrite fractional=><-<-=>_. + rewrite (comm _ Q (Φ p0)) !assoc. f_equiv. by rewrite comm. + - move=>-[-> _]->. by rewrite -fractional Qp_div_2. 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. diff --git a/theories/program_logic/gen_heap.v b/theories/program_logic/gen_heap.v index 826a62ddf11807d96af8f8d3f5748e366f8a5c78..a19923ef3b567dddbae688266c8562b18db2ebbd 100644 --- a/theories/program_logic/gen_heap.v +++ b/theories/program_logic/gen_heap.v @@ -82,7 +82,7 @@ Section gen_heap. Qed. Global Instance mapsto_as_fractional l q v : AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q. - Proof. done. Qed. + Proof. split. done. apply _. Qed. Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝. Proof. @@ -100,7 +100,7 @@ Section gen_heap. Qed. Global Instance heap_ex_mapsto_as_fractional l q : AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q. - Proof. done. Qed. + Proof. split. done. apply _. Qed. Lemma mapsto_valid l q v : l ↦{q} v ⊢ ✓ q. Proof.