Coq 中的证明模式定义？

Question

谁能给我一些关于如何阅读证明模式定义的好资料（给出了一个例子:)

Definition A (ss: FSS) (n:nat)
             (s: {s:S | state_is_wf s
                            /\ RESS.get_element n (proj1_sig ss) = Some s})
    : FS.
    destruct s. destruct a.
    refine (exist _ x _).
    apply H.
  Defined.

其中 'FSS'、'FS' 和 'S' 是之前定义的 sig 类型。我知道个人策略 'destruct'、'refine' 和 'apply' 的作用，但在证明术语中一个定义，我可能不编译就无法阅读这个证明（我无法编译这些文件，只能阅读它们的源代码。）任何人都可以帮助我如何阅读这些定义或指出一些来源吗？

Answer 1

没有编译定义（也没有看到FS和FSS的定义），这是不可能的，但我们还是可以猜到一点。 destruct 策略在 s 上创建了一个 match with 构造，其类型为 sig，它具有唯一的构造函数 exist。函数的参数中没有a，所以a要么是全局符号，要么是第一个destruct创建的变量。让我们假设是后者。 x.

同样的事情

策略refine 创建一个术语，可能有漏洞。术语 exist _ x _ 包含两个漏洞。第一个 _ 由 Coq 填充，但最后一个可能必须由用户填充，所以这就是 apply H 的用途。至于 H，让我们假设它来自之前的 destruct.

之一

注意 apply 可能首先只用一个构造函数分解归纳值。因此，如果 H 恰好是 A /\ B 类型（如果它来自第一个 destruct，那么 apply H 实际上可能是 apply (proj1 H) 或apply (proj2 H)。反正现在证明完了，这个apply大概就是exact.

所以，有无数的可能性。这是一个例子：

Definition A ss n s :=
  match s with
  | exist _ a H =>
    match a with
    | ... x ... =>         (* H could come from there too *)
      exist _ x (proj1 H)  (* or (proj2 H), or plain H *)
    end
  end.

Coq 中的证明模式定义？

Proof mode definitions in Coq?

coq

coq-tactic