Skip to content
Snippets Groups Projects
Commit 14a67809 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Prove pure_ne to make f_equiv work better.

parent 9b6de3dd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/primitive.v
+ 4
− 1
View file @ 14a67809
...@@ -211,8 +211,11 @@ Arguments uPred_holds {_} !_ _ _ /. ...@@ -211,8 +211,11 @@ Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails. Hint Immediate uPred_in_entails.
(** Non-expansiveness and setoid morphisms *) (** Non-expansiveness and setoid morphisms *)
Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M). Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M) | 0.
Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed. Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
Global Instance pure_ne n : Proper (iff ==> dist n) (@uPred_pure M) | 1.
Proof. by intros φ1 φ2 ->. Qed.
Global Instance and_ne : NonExpansive2 (@uPred_and M). Global Instance and_ne : NonExpansive2 (@uPred_and M).
Proof. Proof.
intros n P P' HP Q Q' HQ; unseal; split=> x n' ??. intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
......
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