coq - {assumption, apply, intro} 足以满足最小 prop 逻辑

Question

我读到 Ltac 中的策略集 {assumption, apply, intro} 足以证明最小构造命题逻辑中的任何重言式。

我想纸笔证明是通过对重言式的语法进行归纳来证明这 3 种策略可以逐步构建代表重言式的术语。

我很想知道是否可以使用 Ltac 或其他元语言在 inside Coq 中提供替代证明。

这意味着 Ltac 或替代元语言可以反射(reflect)这些策略的实际作用，并可以将它们作为变量进行操纵。

我对这个方向的肯定答案很感兴趣，即使它有点做作。

Answer 1

实际上，只需apply 就足够了。只需应用正确类型的证明项。或者为了真正精简，根本不使用任何 Ltac，只需将证明项分配给

定义 name : <proposition> := <proof term>.

例子:

Lemma has_next :  forall n, exists n', S n = n'.
Proof. 
  intro n. 
  exists (S n). 
  reflexivity. 
Qed.

可以通过直接给出证明项来“证明”。

Definition has_next : forall n, exists n', S n = n' := fun n => ex_intro  _ (S n) eq_refl.

您知道，Ltac 命令没有什么神奇之处。它们只是使创建证明项变得更容易的工具，但如果您想使用尽可能少的策略，您可以一次性提供整个证明项。

“证明”来自这样一个事实，即您已经证明确实存在具有所需类型(命题)的证明项。 Coq 会为您对术语进行类型检查，以确保该术语确实具有该类型。

Coq 甚至不关心术语是如何构建的——通过神圣的洞察力或来自部分错误的程序，只要术语类型检查。