Commit 35551d40 authored by Ralf Jung's avatar Ralf Jung

cancellable invariants are contractive

parent f987ca78
...@@ -28,10 +28,12 @@ Section proofs. ...@@ -28,10 +28,12 @@ Section proofs.
Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p). Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed. Proof. rewrite /cinv_own; apply _. Qed.
Global Instance cinv_contractive N γ : Contractive (cinv N γ).
Proof. solve_contractive. Qed.
Global Instance cinv_ne N γ : NonExpansive (cinv N γ). Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
Proof. solve_proper. Qed. Proof. exact: contractive_ne. Qed.
Global Instance cinv_proper N γ : Proper (() ==> ()) (cinv N γ). Global Instance cinv_proper N γ : Proper (() ==> ()) (cinv N γ).
Proof. apply (ne_proper _). Qed. Proof. exact: ne_proper. Qed.
Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P). Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
Proof. rewrite /cinv; apply _. Qed. Proof. rewrite /cinv; apply _. Qed.
......
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