The Coq mailing list

[Jason Gross <jagro AT google.com>]

You are already lost when you [apply Exists_preserves_finite_conj]:

Lemma Map_Finite_subgoal_False (A := unit) (B := nat) : (forall r : Ensemble (A * B),

   Finite (A * B) r -> Finite (A * B) (fun x : A * B => exists b : B, In (A * B) r (fst x, b))) -> Finite (unit * nat) (Full_set _).

Proof.

  intro H.

  unfold Map, Lookup, In, A, B in *.

  specialize (H (Add _ (Empty_set _) (tt, 0))). 

  let T := match type of H with ?T -> _ => T end in

  assert (H' : T).

  { constructor; [ constructor | intro H' ].

    hnf in H'.

    destruct H'. }

  specialize (H H'); clear H'.

  eapply Finite_downward_closed; [ eassumption | ].

  intros [ [] ?] ?; hnf.

  eexists; right; constructor.

Qed.

You need to use the fact that there is a surjection from [r] onto your conclusion ensemble: map [p] to [(fst p, f (fst p) (snd p))].  Then prove that if you have a surjection [X ↠ Y], then [Finite X -> Finite Y].

-Jason

On Mon, Aug 1, 2016 at 9:22 AM John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "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:


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