1

I believe the title is pretty self explanatory : https://en.wikipedia.org/wiki/Conditional_proof

I would like to have a tactic where I assume a proposition and proceed to find another one, if succeeded, then I have found that the first proposition implies the second one and this is put as an hypothesis in the context.

So for example Ltac cp P Q creates a subgoal Qand puts Pin the context. If I can indeed reach the subgoal Q, then the subgoal is discharged and P->Q is added to the context. How can I achieve this ?

Edit: It is clear that while proving assert (P->Q). intro. does the job, but I cannot combine them into a Ltac tactic, it gives an error of No focused proof (No proof-editing in progress).

4

2 回答 2

2

要定义新策略，您需要用;.

Ltac cp P Q := assert (P -> Q); [ intro | ].
  (* Use intro in the first subgoal of assert *)
于 2018-10-22T00:13:25.043 回答
2

已经有这样的策略，它被enough称为“足以表明 P”。它假设P并且您现在可以使用P. 完成后，您必须证明P.

如果很容易完成，您可以使用by（与 for 相同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.
于 2018-10-24T07:42:34.510 回答