The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

>However, such a function requires a strong form of decidability
>(booleans in my example or forall x, {P x}+{~P x}) and there may not
>be a workaround such that forall x, P x \/ ~P x suffices."

I had replaced the disjunction with the sumbool, yeah, but i thought that since the end result is in Prop, when it came time to tie everything up together, there'd be a way to bring back the regular disjunction.

>"However, to my greatest frustration, I don’t know how to
>prove it. Specifically

CoInductive eq__cn : CN -> CN -> Prop :=
| eqz : eq__cn cz cz
| eqs : forall n1 n2, eq__cn n1 n2 -> eq__cn (cs n1) (cs n2).

Goal forall (p:CN->bool), (forall n1 n2, eq__cn n1 n2 -> p n1 = p n2)
-> (forall n:nat, p (finite n) = false) -> forall n, p n = false

>Let someone better at co-inductives than I am solve this one, maybe.

I think the issue here is just that there aren't enough premisses; namely, "p inf = false". Escardó proves a lemma very similar to the one you were trying to (except it includes the premiss i mentioned), called ℕ∞-density (this should also be a link to it: http://www.cs.bham.ac.uk/~mhe/agda/GenericConvergentSequence.html#5592 ).

2016-07-14 18:13 GMT-03:00 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>:

Mmm… you’re right… There are a few things which may make this impossible to
actually prove.

The standard way to prove such a result would be to exhibit a witness
with a selection function:

Require Import Coq.Bool.Bool.
Require Coq.Setoids.Setoid.

Notation " f ∘ g " := (Basics.compose f g) (at level 10).

CoInductive CN :=
| cs (n:CN)
| cz.

CoFixpoint ε (p:CN->bool) : CN :=
  match p cz with
  | true => cz
  | false => cs (ε (p∘cs))
  end.

However, such a function requires a strong form of decidability
(booleans in my example or forall x, {P x}+{~P x}) and there may not
be a workaround such that forall x, P x \/ ~P x suffices.

As per extensionality: as you’ve discovered co-inductives are not much
better than functions with respect to extensionality issues (you can
prove that the function type given by Escardó and the co-natural
numbers are equivalent, but you will need extensional equality on both
side).

At any rate, the trickiest part of the proof is to start the proof of

p (ε p) = false -> forall n, p n = false

Since you have no inductive to eliminate or co-inductive to
generate. I haven’t been able to complete the proof, but you need a
topological principle like the following:

Fixpoint finite (n:nat) : CN :=
  match n with
  | 0 => cz
  | S n => cs (finite n)
  end.

Goal (forall n:nat, p (finite n) = false) -> forall n, p n = false

To introduce something to destruct. As it happens, this is a
meta-theorem (every closed term CN->bool in Coq has this
property). And this sort of meta-theorem is usually proved by
parametricity. So I’d expect it to be true of every parametric
function, and unless I’m mistaken, these are exactly the extensional
functions. However, to my greatest frustration, I don’t know how to
prove it. Specifically

CoInductive eq__cn : CN -> CN -> Prop :=
| eqz : eq__cn cz cz
| eqs : forall n1 n2, eq__cn n1 n2 -> eq__cn (cs n1) (cs n2).

Goal forall (p:CN->bool), (forall n1 n2, eq__cn n1 n2 -> p n1 = p n2)
-> (forall n:nat, p (finite n) = false) -> forall n, p n = false

Let someone better at co-inductives than I am solve this one, maybe.

​

On 14 July 2016 at 19:45, Hugo Carvalho <hugoccomp AT gmail.com> wrote:

Hi Arnaud! Just checking, is the theorem

forall P, (forall a:CN, P n \/ ~P n) -> (forall a:CN, P a) \/ exists a:CN, ~P a

really true? I've spent an afternoon on this, to no luck.

Martin Escardó's Agda developments impose an additional constraint on P: it must be "extensional", that is, if a is extensionally equal to b, then "P a <-> P b". He uses elements from a function type, instead of CN, so i was hoping to avoid the usage of extensionality, but it seems that there's an analogous condition in CN, namely requiring that if a is bisimilar to b, then "P a <-> P b".

2016-07-03 17:16 GMT-03:00 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>:

This is emphatically not true of the natural numbers.

It is true of the “one-point compacification” of the natural numbers (sometimes called co-natural numbers):

CoInductive CN : Type :=
| O : CN
| S : CN -> CN

In fact, for this one-point compacification of the natural number we get a slightly stronger (and, frankly, more useful):

forall P, (forall a:CN, P n \/ ~P n) -> (forall a:CN, P a) \/ exists a:CN, ~P a

Martin Escardó & Paulo Oliva have spend quite some energy studying this latter property.

This [ http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf ], I believe, may be a good, rather programming-oriented, starting point.

​

On 3 July 2016 at 21:56, Jonathan Leivent <jonikelee AT gmail.com> wrote:

I hit another constructive goal that is messing with my classical logic encumbered brain - a form of excluded middle at a point vs. overall:

  A : Type
  P : A -> Prop
  emp : forall a : A, P a \/ ~ P a
  ============================
  (forall a : A, P a) \/ ~ (forall a : A, P a)

I would think this is not provable in Coq in general, but it is certainly true for many A and P.  What properties of A and/or P make this true?  I would think it is true for example on any type A such that one can enumerate the elements somehow - such as nat, or maybe any inductive type.  But, I don't even see how to prove it if A is nat for arbitrary P.  It's trivial to prove if A is bool for arbitrary P, and probably so for any other finite type.

How does one go about such proofs when A is not finite - what other hypotheses about A and/or P are needed to make headway?

-- Jonathan