Apply a lemma to a conjunction branch without splitting in coq

Question

I have a conjunction, let's abstract it as: A /\ B and I have a Lemma proven that C -> A and I wish to get as a result the goal C /\ B. Is this possible?

If yes, I'd be interested in how to do it. If I use split and then apply the lemma to the first subgoal, I can't reassemble the two resulting subgoals C and B to C /\ B - or can I? Also apply does not seem to be applyable to only one branch of a conjunction.

If no, please explain to me why this is not possible :-)

Answer 1

You could introduce a lemma like :

Theorem cut: forall (A B C: Prop), C /\ B -> (C -> A) -> A /\ B.
Proof.
  intros; destruct H; split; try apply H0; assumption.
Qed.

And then define a tactic like :

Ltac apply_left lemma := eapply cut; [ | apply lemma].

As an example, you could do stuff like :

Theorem test: forall (m n:nat),  n <= m -> max n m = m /\ min n m = n.
Proof.
  intros.
  apply_left max_r.
  ...
Qed.

In this case, the context goes from :

Nat.max n m = m /\ Nat.min n m = n

to

n <= m /\ Nat.min n m = n

I assume that's what you are looking for. Hope this will help you !