Stream: Coq users

Topic: ✔ Construct a function from a point

Yu Zhang (Dec 14 2021 at 15:41):

I have no idea how to prove the following lemma. Can anyone help me with it? I wouldn't mind using classical logic. Thanks!

  Lemma foo {I : Type} {J : I -> Type} (ix: I) (jx: J ix):
      exists f : forall i : I, J i, f ix = jx.
  Proof.
  Admitted.

Gaëtan Gilbert (Dec 14 2021 at 15:48):

you can't, it's absurd

Lemma bad : (forall {I : Type} {J : I -> Type} (ix: I) (jx: J ix),
                exists f : forall i : I, J i, f ix = jx)
            -> False.
Proof.
  intros F.
  destruct (F bool (fun b => if b then True else False) true I) as [f _].
  exact (f false).
Qed.

Théo Winterhalter (Dec 14 2021 at 15:49):

If you take I to be bool and J true = True and J false = False and ix = true then jx is just a proof of True but you also need to provide a proof of False because f false : False?

Yu Zhang (Dec 14 2021 at 15:50):

I see. Thank you both!

Notification Bot (Dec 14 2021 at 15:50):

Yu Zhang has marked this topic as resolved.

Last updated: Oct 01 2023 at 19:01 UTC