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

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

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

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


logic coq coq-tactic formal-verification
person Marius Melzer    schedule 09.07.2020    source источник
comment
Вы пытаетесь доказать C /\ B, зная только A /\ B и C -> A? Это невозможно, так как утверждение A /\ B -> (C -> A) -> C /\ B вообще неверно (возьмем A = B = True и C = False).   -  person Sven Williamson    schedule 09.07.2020
comment
@SvenWilliamson Нет, они пытаются доказать A /\ B из C /\ B и C -> A. У них нет A /\ B, у них есть цель A /\ B, и они хотят получить цель C /\ B с помощью леммы C -> A.   -  person HTNW    schedule 09.07.2020

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете ввести лемму вроде:

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

А затем определите тактику, например:

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

to

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

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

person Lucien David    schedule 09.07.2020