Commit 92eaf4f9 by Robbert Krebbers

### Prove that `is_lock` is contractive.

parent ae0b5798
 ... ... @@ -13,7 +13,7 @@ Structure lock Σ `{!heapG Σ} := Lock { is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ; locked (γ: name) : iProp Σ; (* -- general properties -- *) is_lock_ne N γ lk : NonExpansive (is_lock N γ lk); is_lock_ne N γ lk : Contractive (is_lock N γ lk); is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R); locked_timeless γ : Timeless (locked γ); locked_exclusive γ : locked γ -∗ locked γ -∗ False; ... ...
 ... ... @@ -36,8 +36,8 @@ Section proof. Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l). Proof. solve_proper. Qed. Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l). Proof. solve_proper. Qed. Global Instance is_lock_contractive γ l : Contractive (is_lock γ l). Proof. solve_contractive. Qed. (** The main proofs. *) Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R). ... ...
 ... ... @@ -54,11 +54,10 @@ Section proof. Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I. Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln). Proof. solve_proper. Qed. Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk). Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln). Proof. solve_proper. Qed. Global Instance is_lock_contractive γ lk : Contractive (is_lock γ lk). Proof. solve_contractive. Qed. Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R). Proof. apply _. Qed. Global Instance locked_timeless γ : Timeless (locked γ). ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!