Условная Доказательство Тактика в Coq

Question

Я считаю, что название довольно само собой разумеющееся: https://en.wikipedia.org/wiki/Conditional_proof

Я хотел бы использовать тактику, в которой я принимаю предложение и продолжаю искать другое, в случае успеха, тогда я обнаружил, что первыйПредложение подразумевает второе, и это выдвигается в качестве гипотезы в контексте.

Так, например, Ltac cp P Q создает подцель Q и помещает P в контекст.Если я действительно смогу достичь подцели Q, тогда подцель сбрасывается и P->Q добавляется в контекст.Как мне этого добиться?

Редактировать: Понятно, что при доказательстве assert (P->Q). intro. делает работу, но я не могу объединить их в тактику Ltac, выдает ошибку No focused proof (No proof-editing in progress).

Answer 1

Уже существует такая тактика, она называется enough, так как «достаточно показать, что P».Предполагается, что P, и теперь вы можете закончить доказательство, используя P.Когда вы закончите, вы должны доказать P.

Если его легко закончить, вы можете использовать by (так же, как для assert).Я часто делаю enough (bla bla) by (subst; auto). или что-то подобное, что ставит меня перед целью bla bla.

Эта тактика также может оказаться полезной, т. Е. Если вы не хотите вводить весь сложный антецедент в enough заявление:

Ltac postpone_antecedent H :=
  match type of H with  ?A -> _ =>
    let Q := fresh in enough A as Q ; [specialize (H Q) | ]
  end.

Answer 2

Чтобы определить новые тактики, вам нужно составить их с помощью ;.

Ltac cp P Q := assert (P -> Q); [ intro | ].
  (* Use intro in the first subgoal of assert *)