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

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

.

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.

Ju-sh has marked this topic as resolved.

Last updated: Feb 06 2023 at 13:03 UTC