From a953a68d9b9f30f8aa4e0e36811b9175f3f2ea58 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 13 Dec 2016 22:46:55 +0100 Subject: [PATCH] agree: prove non-step-indexed uninjection --- theories/algebra/agree.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v index 1d28662f..acf7bdd5 100644 --- a/theories/algebra/agree.v +++ b/theories/algebra/agree.v @@ -354,7 +354,7 @@ Proof. intros a b ?. apply equiv_dist=>n. apply to_agree_injN. by apply equiv_dist. Qed. -Lemma to_agree_uninj n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x. +Lemma to_agree_uninjN n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x. Proof. intros Hl. exists (agree_car x). rewrite /dist /agree_dist /=. split. @@ -362,6 +362,16 @@ Proof. - apply (list_agrees_iff_setincl _); first set_solver+. done. Qed. +Lemma to_agree_uninj (x : agree A) : ✓ x → ∃ y : A, to_agree y ≡ x. +Proof. + intros Hl. exists (agree_car x). rewrite /dist /agree_dist /=. + split. + - apply: list_setincl_singleton_in. set_solver+. + - apply (list_agrees_iff_setincl _); first set_solver+. + eapply list_agrees_subrel; last exact: Hl; [apply _..|]. + intros ???. by apply equiv_dist. +Qed. + Lemma to_agree_included (a b : A) : to_agree a ≼ to_agree b ↔ a ≡ b. Proof. split. -- GitLab