Stream: Coq users

Topic: ✔ [Newbie] How to prove a -> (b -> a)

Julin S (Apr 21 2021 at 03:00):

Hi. I'm just getting started with Coq and was trying to prove

a -> (b -> a)

How can this be done?

I reached only here:

Theorem Hello: forall (a b : Prop), a -> (b->a).
Proof.
  intros a b H.  (* I guess this isn't the way to go about it.. *)
Qed.

Jasper Hugunin (Apr 21 2021 at 03:05):

At that point in your proof, you have an assumption called H saying that a holds, and your goal is to prove b -> a, that b implies a. The way to prove an implication is to introduce the antecedent as an assumption with intros H2. (where H2 now becomes an assumption saying that b holds), leaving you with the goal to prove a. But a holds by the assumption H, so you can finish the proof with exact H. or assumption..

Julin S (Apr 21 2021 at 03:14):

Thanks!

I did as you said with

Theorem Hello: forall (a b : Prop), a -> (b->a).
Proof.
  intros a b H.
  intros H2.
  exact H.
Qed.

And the proof finished.

Notification Bot (Jul 16 2021 at 07:36):

Ju-sh has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC