The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

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