Применим лемму к ветви конъюнкции без разбиения на coq

Question

У меня есть конъюнкция, давайте абстрагируем ее как: A /\ B, и у меня есть лемма, доказывающая, что C -> A и я sh получаем в результате цель C /\ B. Возможно ли это?

Если да, мне было бы интересно, как это сделать. Если я использую разделение, а затем применяю лемму к первой подцели, я не могу повторно собрать две результирующие подцели C и B в C /\ B - или могу? Также apply кажется неприменимым только к одной ветви соединения.

Если нет, пожалуйста, объясните мне, почему это невозможно: -)

Answer 1

Вы можете ввести лемму, например:

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

А затем определить тактильные c как:

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

В качестве примера вы можете сделать что-то вроде:

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

В этом случае контекст меняется от:

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

до

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

Я предполагаю, что это то, что вы ищете. Надеюсь, это вам поможет!