The Coq mailing list

[Jason Gross <jagro AT google.com>]

Take A := unit, B := nat, r x := (snd x = 0).  Then your hypotheses are (at least extensionally) true (r is singleton) but your conclusion is false (it is equivalent to saying that [nat] is finite), right?

On Wed, Jul 27, 2016 at 3:29 PM Frédéric Besson <frederic.besson AT inria.fr> wrote:

Hi,

My feeling is that this is not provable.
If you go by induction over Finite0, for the base case, you need to prove:
  Finite (A * B)
    (fun x : A * B =>
     exists b : B, In (A * B) (Empty_set (A * B)) (fst x, b))
This is morally an empty set — but unless you allow functional extensionality —
I doubt this is provably equal to Empty_set (A * B).

Good luck,
—
Frédéric

> On 27 Jul 2016, at 23:49, John Wiegley <johnw AT newartisans.com> wrote:
>
> Hello,
>
> Can anyone help me with the following goal:
>
>  A : Type
>  B : Type
>  f : A -> B -> B
>  r : Ensemble (A * B)
>  Finite0 : Finite (A * B) r
>  ============================
>   Finite (A * B) (fun x : A * B => exists b : B, In (A * B) r (fst x, b))
>
> It would seem that "finitude" must carry, since the goal does not add any
> elements, but I am having difficulties with the existential variable.  Is
> there any way to proceed?
>
> Thank you,
> --
> John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2