Commit b212b3fa by Ralf Jung

### Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 35a17feb ef5af56a
 ... @@ -35,7 +35,7 @@ Section proofs. ... @@ -35,7 +35,7 @@ Section proofs. Proof. intros ??. by rewrite -own_op. Qed. Proof. intros ??. by rewrite -own_op. Qed. Global Instance cinv_own_as_fractionnal γ q : Global Instance cinv_own_as_fractionnal γ q : AsFractional (cinv_own γ q) (cinv_own γ) 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. Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp. Proof. apply (own_valid_2 γ q1 q2). Qed. Proof. apply (own_valid_2 γ q1 q2). Qed. ... ...
 ... @@ -5,8 +5,10 @@ From iris.proofmode Require Import classes class_instances. ... @@ -5,8 +5,10 @@ From iris.proofmode Require Import classes class_instances. Class Fractional {M} (Φ : Qp → uPred M) := Class Fractional {M} (Φ : Qp → uPred M) := fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q. fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q. Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) := Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) := { as_fractional : P ⊣⊢ Φ q. as_fractional : P ⊣⊢ Φ q; as_fractional_fractional :> Fractional Φ }. Arguments fractional {_ _ _} _ _. Arguments fractional {_ _ _} _ _. ... @@ -78,11 +80,15 @@ Section fractional. ... @@ -78,11 +80,15 @@ Section fractional. (** Mult instances *) (** Mult instances *) Global Instance mult_fractional_l Φ Ψ p : Global Instance mult_fractional_l Φ Ψ p : (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Ψ → Fractional Φ. (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ. Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_l F. Qed. Proof. intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_l. by apply H. Qed. Global Instance mult_fractional_r Φ Ψ p : Global Instance mult_fractional_r Φ Ψ p : (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Ψ → Fractional Φ. (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ. Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_r F. Qed. 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 (* REMARK: These two instances do not work in either direction of the search: search: ... @@ -91,58 +97,71 @@ Section fractional. ... @@ -91,58 +97,71 @@ Section fractional. with the goal does not work. *) with the goal does not work. *) Instance mult_as_fractional_l P Φ p q : Instance mult_as_fractional_l P Φ p q : AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) 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 : Instance mult_as_fractional_r P Φ p q : AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) 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 *) (** Proof mode instances *) Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 : Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → Fractional Φ → AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → FromSep P P1 P2. 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 : Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 : AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → Fractional Φ → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) → AsFractional P Φ (q1 + q2) → FromSep P P1 P2 | 10. 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 : Global Instance from_sep_fractional_half_fwd P Q Φ q : AsFractional P Φ q → Fractional Φ → AsFractional P Φ q → AsFractional Q Φ (q/2) → AsFractional Q Φ (q/2) → FromSep P Q Q | 10. 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 : Global Instance from_sep_fractional_half_bwd P Q Φ q : AsFractional P Φ (q/2) → Fractional Φ → AsFractional P Φ (q/2) → AsFractional Q Φ q → AsFractional Q Φ q → FromSep Q P P. 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 : Global Instance into_and_fractional P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → Fractional Φ → AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → IntoAnd false P P1 P2. 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 : Global Instance into_and_fractional_half P Q Φ q : AsFractional P Φ q → Fractional Φ → AsFractional P Φ q → AsFractional Q Φ (q/2) → AsFractional Q Φ (q/2) → IntoAnd false P Q Q | 100. IntoAnd false P Q Q | 100. Proof. by rewrite /AsFractional /IntoAnd -{1}(Qp_div_2 q)=>->->->. Qed. Proof. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed. Global Instance frame_fractional_l R Q PP' QP' Φ r p p' : (* The instance [frame_fractional] can be tried at all the nodes of AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ → the proof search. The proof search then fails almost always on Frame R (Φ p) Q → MakeSep Q (Φ p') QP' → Frame R PP' QP'. [AsFractional R Φ r], but the slowdown is still noticeable. For Proof. rewrite /Frame=>->->-><-<-. by rewrite assoc. Qed. that reason, we factorize the three instances that could ave been Global Instance frame_fractional_r R Q PP' PQ Φ r p p' : defined for that purpose into one. *) AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ → Inductive FrameFractionalHyps R Φ RES : Qp → Qp → Prop := Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ. | 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. 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. 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. End fractional.
 ... @@ -78,10 +78,12 @@ Qed. ... @@ -78,10 +78,12 @@ Qed. Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n. Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n. Proof. induction i; simpl; lia. Qed. Proof. induction i; simpl; lia. Qed. Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (Fin.of_nat_lt H) = n. Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (fin_of_nat H) = n. Proof. Proof. revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia. revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia. Qed. Qed. Lemma fin_of_to_nat {n} (i : fin n) H : @fin_of_nat (fin_to_nat i) n H = i. Proof. apply (inj fin_to_nat), fin_to_of_nat. Qed. Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type) Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type) (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1)) (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1)) ... @@ -258,16 +260,28 @@ Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) : ... @@ -258,16 +260,28 @@ Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) : vec_to_list v = take i v ++ v !!! i :: drop (S i) v. vec_to_list v = take i v ++ v !!! i :: drop (S i) v. Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed. Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed. Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x : v !!! i = x ↔ (v : list A) !! (i : nat) = Some x. Proof. induction v as [|? ? v IH]; inv_fin i. simpl; split; congruence. done. Qed. Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x : (∃ H : i < n, v !!! (fin_of_nat H) = x) ↔ (v : list A) !! i = Some x. Proof. split. - intros [Hlt ?]. rewrite <-(fin_to_of_nat i n Hlt). by apply vlookup_lookup. - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix). rewrite vec_to_list_length in Hlt. exists Hlt. apply vlookup_lookup. by rewrite fin_to_of_nat. Qed. Lemma elem_of_vlookup {A n} (v : vec A n) x : Lemma elem_of_vlookup {A n} (v : vec A n) x : x ∈ vec_to_list v ↔ ∃ i, v !!! i = x. x ∈ vec_to_list v ↔ ∃ i, v !!! i = x. Proof. Proof. split. rewrite elem_of_list_lookup. setoid_rewrite <-vlookup_lookup'. - induction v; simpl; [by rewrite elem_of_nil |]. split; [by intros (?&?&?); eauto|]. intros [i Hx]. inversion 1; subst; [by eexists 0%fin|]. exists i, (fin_to_nat_lt _). by rewrite fin_of_to_nat. destruct IHv as [i ?]; trivial. by exists (FS i). - intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|]. right; apply IH. Qed. Qed. Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) : Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) : Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i). Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i). Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed. Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed. ... ...
 ... @@ -82,7 +82,7 @@ Section gen_heap. ... @@ -82,7 +82,7 @@ Section gen_heap. Qed. Qed. Global Instance mapsto_as_fractional l q v : Global Instance mapsto_as_fractional l q v : AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q. 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⌝. Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝. Proof. Proof. ... @@ -100,7 +100,7 @@ Section gen_heap. ... @@ -100,7 +100,7 @@ Section gen_heap. Qed. Qed. Global Instance heap_ex_mapsto_as_fractional l q : Global Instance heap_ex_mapsto_as_fractional l q : AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I 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. Lemma mapsto_valid l q v : l ↦{q} v ⊢ ✓ q. Proof. Proof. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!