Commit dcfe93aa by Robbert Krebbers

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

parents dcc164e3 b00233e4
 ... ... @@ -131,10 +131,24 @@ Proof. intuition eauto 10 using dra_disjoint_minus, dra_op_minus. Qed. Definition validityRA : cmraT := discreteRA validity_ra. Definition validity_update (x y : validityRA) : Lemma validity_update (x y : validityRA) : (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y. Proof. intros Hxy. apply discrete_update. intros z (?&?&?); split_ands'; try eapply Hxy; eauto. Qed. Lemma to_validity_valid (x : A) : ✓ to_validity x → ✓ x. Proof. intros. done. Qed. Lemma to_validity_op (x y : A) : ✓ x → ✓ y → (✓ (x ⋅ y) → x ⊥ y) → to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y. Proof. intros Hvalx Hvaly Hdisj. split; [split | done]. - simpl. auto. - simpl. intros (_ & _ & ?). auto using dra_op_valid, to_validity_valid. Qed. End dra.
 ... ... @@ -333,22 +333,13 @@ Lemma sts_op_auth_frag_up s T : Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed. Lemma sts_op_frag S1 S2 T1 T2 : T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2. Proof. (* Somehow I feel like a very similar proof muts have happened above, when proving the DRA axioms. After all, we are just reflecting the operation here. *) intros HT HS1 HS2; split; [split|constructor; solve_elem_of]; simpl. - intros; split_ands; try done; []. constructor; last solve_elem_of. by eapply closed_ne. - intros (_ & _ & H). inversion_clear H. constructor; first done. + move=>s /elem_of_intersection [/(closed_disjoint _ _ HS1) Hs1 /(closed_disjoint _ _ HS2) Hs2]. solve_elem_of +Hs1 Hs2. + move=> s1 s2 /elem_of_intersection [Hs1 Hs2] Hstep. apply elem_of_intersection. split; eapply closed_step; eauto; [|]; eapply framestep_mono, Hstep; done || solve_elem_of. intros HT HS1 HS2. rewrite /sts_frag. (* FIXME why does rewrite not work?? *) etransitivity; last eapply to_validity_op; try done; []. intros Hval. constructor; last solve_elem_of. eapply closed_ne, Hval. Qed. (** Frame preserving updates *) ... ...
 ... ... @@ -53,18 +53,19 @@ Section sts. (* The same rule as implication does *not* hold, as could be shown using sts_frag_included. *) Lemma sts_ownS_weaken E γ S1 S2 T : S1 ⊆ S2 → sts.closed S2 T → sts_ownS γ S1 T ⊑ pvs E E (sts_ownS γ S2 T). Proof. intros. by apply own_update, sts_update_frag. Qed. Lemma sts_ownS_weaken E γ S1 S2 T1 T2 : T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 ⊑ pvs E E (sts_ownS γ S2 T2). Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed. Lemma sts_own_weaken E γ s S T : s ∈ S → sts.closed S T → sts_own γ s T ⊑ pvs E E (sts_ownS γ S T). Proof. intros. by apply own_update, sts_update_frag_up. Qed. Lemma sts_own_weaken E γ s S T1 T2 : T1 ≡ T2 → s ∈ S → sts.closed S T2 → sts_own γ s T1 ⊑ pvs E E (sts_ownS γ S T2). (* FIXME for some reason, using "->" instead of "<-" does not work? *) Proof. intros <- ? ?. by apply own_update, sts_update_frag_up. Qed. Lemma sts_ownS_op γ S1 S2 T1 T2 : T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I. Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!