Coq中蕴含传递性引理证明及应用问题求助

Part 1: Proving if_trans #

You’re already off to a solid start splitting the conjunction with intros P Q R [E1 E2]—that gives you E1 : P → Q and E2 : Q → R. Now, your goal is to prove P → R. To tackle an implication like this, you need to assume the premise (P) and then derive the conclusion (R). Here’s a step-by-step breakdown using only the tactics you mentioned:

Lemma if_trans : forall (P Q R: Prop), (P -> Q) /\ (Q -> R) -> (P ->R).
Proof.
intros P Q R [E1 E2].
% Assume the premise of the implication we need to prove
intros H. % Now H : P
% Use E1 to turn P into Q
apply E1 in H. % Now H : Q
% Use E2 to turn Q into R
apply E2 in H. % Now H : R
% Our goal is R, so we can directly use the hypothesis
exact H.
Qed.

If you prefer a more concise version (still using allowed tactics):

Lemma if_trans : forall (P Q R: Prop), (P -> Q) /\ (Q -> R) -> (P ->R).
Proof.
intros P Q R [E1 E2] H.
% To get R, we first need Q (via E2), then P (via E1)
apply E2.
apply E1.
exact H.
Qed.

Note: The confusion you had with apply E2 in E1 comes from E1 being an implication (P→Q), not a concrete proposition like P or Q. The apply ... in tactic works best when you’re modifying a hypothesis that’s a specific statement, not an implication rule. That’s why that approach led to unexpected subgoals.

Part 2: Using if_trans with Separate Hypotheses #

If you have H1 : P → Q and H2 : Q → R, and your goal is P → R, you first need to combine H1 and H2 into a single conjunction hypothesis. Here’s how to do it explicitly with basic tactics:

Theorem example : forall P Q R, (P→Q) → (Q→R) → (P→R).
Proof.
intros P Q R H1 H2.
% Create a new hypothesis that combines H1 and H2 into a conjunction
assert (H : (P→Q) ∧ (Q→R)) by (split; [exact H1 | exact H2]).
% Apply our if_trans lemma to this conjunction to get the desired implication
apply if_trans H.
Qed.

Alternatively, you can skip the assert step by directly using the conj constructor (which builds conjunctions in Coq):

Theorem example : forall P Q R, (P→Q) → (Q→R) → (P→R).
Proof.
intros P Q R H1 H2.
apply if_trans (conj H1 H2).
Qed.

The split; [exact H1 | exact H2] line in the first method uses split to break the conjunction into two subgoals (proving P→Q and Q→R), then closes each subgoal with the existing hypotheses.

内容的提问来源于stack exchange，提问作者Anon