From f01839f757fc9a67dfb982f1c64cc42961a605ea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Apr 2017 11:56:42 +0200
Subject: [PATCH] =?UTF-8?q?add=20Ale=C5=A1's=20proof=20that=20agree=20is?=
=?UTF-8?q?=20not=20complete?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/algebra/agree.v | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 5f699ec7d..13f87dbf6 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -6,6 +6,27 @@ Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
+(** Define an agreement construction such that Agree A is discrete when A is discrete.
+ Notice that this construction is NOT complete. The fullowing is due to Aleš:
+
+
+Proposition: Ag(T) is not necessarily complete.
+Proof.
+ Let T be the set of binary streams (infinite sequences) with the usual
+ ultrametric, measuring how far they agree.
+
+ Let Aâ‚™ be the set of all binary strings of length n. Thus for Aâ‚™ to be a
+ subset of T we have them continue as a stream of zeroes.
+
+ Now Aâ‚™ is a finite non-empty subset of T. Moreover {Aâ‚™} is a Cauchy sequence
+ in the defined (Hausdorff) metric.
+
+ However the limit (if it were to exist as an element of Ag(T)) would have to
+ be the set of all binary streams, which is not exactly finite.
+
+ Thus Ag(T) is not necessarily complete.
+*)
+
Record agree (A : Type) : Type := Agree {
agree_car : A;
agree_with : list A;
--
GitLab