Commit d9498942 by Ralf Jung

### uPred entailment commutes over limits

parent 9c55bc2c
 ... @@ -68,7 +68,7 @@ End ofe_mixin. ... @@ -68,7 +68,7 @@ End ofe_mixin. Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption. Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption. (** Discrete COFEs and Timeless elements *) (** Discrete OFEs and Timeless elements *) (* TODO: On paper, We called these "discrete elements". I think that makes (* TODO: On paper, We called these "discrete elements". I think that makes more sense. *) more sense. *) Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. ... ...
 ... @@ -172,5 +172,13 @@ Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ ... @@ -172,5 +172,13 @@ Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ Proof. by intros ->. Qed. Proof. by intros ->. Qed. Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R). Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R). Proof. by intros ? <-. Qed. Proof. by intros ? <-. Qed. Lemma entails_lim (P Q : chain (uPredC M)) : (∀ n, P n ⊢ Q n) → compl P ⊢ compl Q. Proof. intros Hlim. split. intros n m Hval HP. eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl. Qed. End entails. End entails. End uPred. End uPred.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!