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
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 holds by the assumption
H, so you can finish the proof with
exact H. or
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