Commit 3f66477c authored by Robbert Krebbers's avatar Robbert Krebbers

Propers for fixpoints.

parent c8578f92
...@@ -26,6 +26,10 @@ Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n : ...@@ -26,6 +26,10 @@ Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n :
Proper (pointwise_relation (A PROP) (pointwise_relation A (dist n)) ==> Proper (pointwise_relation (A PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_least_fixpoint. dist n ==> dist n) bi_least_fixpoint.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance least_fixpoint_proper {PROP : bi} {A : ofeT} :
Proper (pointwise_relation (A PROP) (pointwise_relation A ()) ==>
() ==> ()) bi_least_fixpoint.
Proof. solve_proper. Qed.
Section least. Section least.
Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}. Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}.
...@@ -85,6 +89,10 @@ Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n : ...@@ -85,6 +89,10 @@ Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n :
Proper (pointwise_relation (A PROP) (pointwise_relation A (dist n)) ==> Proper (pointwise_relation (A PROP) (pointwise_relation A (dist n)) ==>
dist n ==> dist n) bi_greatest_fixpoint. dist n ==> dist n) bi_greatest_fixpoint.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance greatest_fixpoint_proper {PROP : bi} {A : ofeT} :
Proper (pointwise_relation (A PROP) (pointwise_relation A ()) ==>
() ==> ()) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
Section greatest. Section greatest.
Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}. Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}.
......
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