The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> "FB" == Frédéric Besson 
>>>>> <frederic.besson AT inria.fr>
>>>>>  writes:

> 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).

Hi Frédéric,

The base case is actually quite easily shown:

  inversion Finite0.
    eapply Finite_downward_closed; eauto with sets.
    intros ? H0; inversion H0; inversion H1.

Here is the full example, so you can see what I'm trying to prove and why:

Attachment: Map.v
Description: Binary data

I'm trying to create a mapping function for ensembles, and to show that
mapping over a finite ensemble must always result in a finite ensemble.

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2