The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 8 Nov 2012 14:03:08 -0800,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> On Thu, Nov 8, 2012 at 1:15 PM, Jonas Oberhauser 
> <s9joober AT gmail.com>
> wrote:
> > One thing that has opened my eyes a little bit was this provable
> > proposition that Smolka and CE Brown showed to me:
> >
> > Goal forall X, forall f : X -> (X -> Prop),  exists g, forall x, f
> > x <> g.
> >
> > What does this mean? Does it mean that there are more "sets of X"
> > than there are "elements of X"? Or does it just mean that there is
> > no procedure (in the Coq-World) that gives every procedure in (X ->
> > Prop) a unique object of X? Certainly you can only write down
> > countably many procedures (or "sets") in Coq, but the number of
> > sets of e.g. natural numbers is much larger.
> 
> I'm not sure exactly what you're trying to get at with this example.
> Of course it's easy to prove this without axioms:
> 
> Definition same_set {X} (A B:X->Prop) : Prop :=
> forall x:X, A x <-> B x.
> 
> Lemma Cantor_diag: forall {X} (f:X -> (X->Prop)),
>   exists B:X->Prop, forall x:X, ~ same_set (f x) B.
> 
> But this is just a refinement of the statement that every
> undergraduate math major learns.  And since it's also easy to prove
> A=B -> same_set A B, so ~ same_set A B -> A <> B, your statement is an
> easy corollary.

You can do it direcly without using intermediate definitions.

Goal forall X, forall f : X -> (X -> Prop),  exists g, forall x, f x <>
g. (* introductions of hypothesis *)
refine (fun (X : Type) (f : X -> X -> Prop) => _).
(* g witness *)
exists (fun x => f x x -> False).
(* introductions *)
refine (fun (x : X) (H : f x = (fun y => f y y -> False)) => _).
(* the fun stuff *)
refine ((fun (K : f x x -> False) => K (_(*proof 1*) : f x x))
        (fun (K : f x x) => (_(*proof 2*) : f x x -> False) K)).
(*proof 1*) rewrite H; exact K.
(*proof 2*) rewrite H in K; exact K.


> 
> The way I tend to look at functional extensionality is: x=y is
> equivalent to Leibniz equality, i.e. forall P, P x <-> P y or
> equivalently forall P, P x -> P y.  The statement that functional
> extensionality is consistent, to me, means that for propositions you
> can build within Coq, there's no proposition which distinguishes f
> from g if all their values are equal.  And adding functional
> extensionality as an axiom is essentially a promise that you won't add
> any other axioms or parameters, like a "function introspection on the
> reduction" operation, which would allow you to distinguish for example
> between fun n => n and fun n => n+0.

For this reason, I was also wondering, about a family of axioms which
looks weaker than functionnal extensionnality but stronger than
eta-expansion. More precisely, for any inductive type, we can define a
representation of its function space to any type using a coinductive:

Inductive bool : Set := True | False.
CoInductive boolfun (X : bool -> Type) : Type :=
 BoolVals : X true -> X false -> boolfun X.

Inductive nat : Set := O | S : nat -> nat.
CoInductive natfun (X:nat -> Type) : Type :=
 NatVals : X O -> natfun (fun n => X (S n)) -> natfun X.
-or without dependant types-
CoInductive natfun (X : Type) : Type :=
 NatVals : X -> natfun X -> natfun X.
(also know as stream)

and so on.

Here we could "split" the extensionnality in two.
For instance, in the nat case,

CoFixpoint rep (T : nat -> Type) (f : forall n, T n) : natfun T :=
  NatVals (f O) (rep (fun n => T (S n)) (fun n => f (S n)) end.

Fixpoint eval (T : nat -> Type) (nf : natfun T) (n : nat) : T n :=
  match nf with NatVals vO vS => match n with
                                 | O => vO
                                 | S n => eval (fun n => T (S n)) vS n
                                 end
  end.

Then here, two axioms could be considered:
(1) ∀ T (f g : ∀ n, T n), (∀ x, f x = g x) → (rep T f) = (rep T g)
(2) ∀ T (f g : ∀ n, T n), (rep T f) = (rep T g) → f = g.

In the case where the inductive has a finite domain (like in bool), (1)
is easy to prove, so (2) is equivalent to extensionnality.

In the case where the inductive has non finite domain (like in nat),
(1)+(2) imply extensionnality
extensionnality implies (1)
but extensionnality does not imply (2) [at least I do not see how].
Another axiom,
(3) ∀ T (f : ∀ n, T n), (eval (rep T f)) = f
could be combined with extensionnality to get (2)
and we could also add some symmetric one:
(4) ∀ T (fn : natfun T), rep (eval T fn) = fn

If we replace '=' with
CoInductive sim (T : nat → Type) : natfun T → natfun T → Prop :=
Sim : ∀ (x : T O) (u v : natfun (fun n => T (S n))), sim T u v →
         sim T (NatVals T x u) (NatVals T x v).
Then (1) and (4) become provable.