0

给定 Coq 中的任意归纳命题定义，在对归纳命题调用归纳策略时，是否有一个通用公式可以推导出合理的 disj_conj_intro_pattern 使用？

通常，对于任何一个归纳定义的构造函数，完整的 intro_pattern 可能需要（命名）多个假设和多个归纳假设，在这种情况下，模式中提供的名称顺序可能包括所有参数，然后一个假设和一个相应的归纳假设，然后是一个或多个由假设和归纳假设组成的附加对。例如，软件基础包括以下内容：

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar : forall x, exp_match [x] (Char x)
| MApp : forall s1 re1 s2 re2,
           exp_match s1 re1 ->
           exp_match s2 re2 ->
           exp_match (s1 ++ s2) (App re1 re2)
| MUnionL : forall s1 re1 re2,
              exp_match s1 re1 ->
              exp_match s1 (Union re1 re2)
| MUnionR : forall re1 s2 re2,
              exp_match s2 re2 ->
              exp_match s2 (Union re1 re2)
| MStar0 : forall re, exp_match [] (Star re)
| MStarApp : forall s1 s2 re,
               exp_match s1 re ->
               exp_match s2 (Star re) ->
               exp_match (s1 ++ s2) (Star re).

Notation "s =~ re" := (exp_match s re) (at level 80).

Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T),
  s =~ re ->
  In x s ->
  In x (re_chars re).
Proof.
  intros T s re x Hmatch Hin.
  induction Hmatch
    as [
        |x'
        |s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
        |s1 re1 re2 Hmatch IH|re1 s2 re2 Hmatch IH
        |re|s1 s2 re Hmatch1 IH1 Hmatch2 IH2].

在这个例子中，MApp 和 MStarApp 的 intro_patterns 各有两对假设和归纳假设——大​​概是因为这两个构造函数都包含以下形式的表达式

x -> y -> z

关于这一点，当前的参考手册似乎只说

归纳术语为 disj_conj_intro_pattern

这表现为归纳术语，但使用 disj_conj_intro_pattern 中的名称来命名上下文中引入的变量。disj_conj_intro_pattern 通常必须是 [ p11 … p1n1 | … | pm1 ... pmnm ] 其中 m 是术语类型的构造函数的数量。在第 i 个目标的上下文中通过归纳引入的每个变量都从列表 pi1 ... pini 中按顺序获取其名称。如果没有足够的名称，则归纳为要引入的剩余变量发明名称。更一般地说，pij 可以是任何分离式/连接式引入模式（参见第 8.3.2 节）。例如，对于具有一个构造函数的归纳类型，可以使用模式表示法 (p1 , ... , pn) 代替 [ p1 ... pn ]。

这似乎没有指定如何为给定的归纳定义确定完整的 disj_conj_intro_pattern 的正确形式。

我上面的经验观察是1）每个构造函数的形式参数首先出现，然后是构造函数的假设与相应的归纳假设配对；2）假设和归纳假设对的数量来自构造函数中假设的数量，事情的总和？或者还有更多吗？

除了参考手册的战术章节和第 1 章中关于 Gallina 语法模式的一般性讨论之外，还有其他相关文档吗？

4

1 回答 1

0

如果我正确理解您的问题，那么答案是“是”。您可以为归纳导出一个介绍模式。

Coq 会自动为任何归纳定义生成一个归纳原理，并将其命名_ind为后缀，因此该归纳原理就exp_match变成了exp_match_ind。如果您探索exp_match_ind使用Check命令的类型，您将能够生成所需的介绍模式。

Check exp_match_ind.

(* output:
exp_match_ind
     : forall (T : Type) (P : list T -> reg_exp T -> Prop),
       P [] EmptyStr ->
       (forall x : T, P [x] (Char x)) ->
       (forall (s1 : list T) (re1 : reg_exp T) 
          (s2 : list T) (re2 : reg_exp T),
        s1 =~ re1 ->
        P s1 re1 ->
        s2 =~ re2 -> P s2 re2 -> P (s1 ++ s2) (App re1 re2)) ->
       (forall (s1 : list T) (re1 re2 : reg_exp T),
        s1 =~ re1 -> P s1 re1 -> P s1 (Union re1 re2)) ->
       (forall (re1 : reg_exp T) (s2 : list T) (re2 : reg_exp T),
        s2 =~ re2 -> P s2 re2 -> P s2 (Union re1 re2)) ->
       (forall re : reg_exp T, P [] (Star re)) ->
       (forall (s1 s2 : list T) (re : reg_exp T),
        s1 =~ re ->
        P s1 re ->
        s2 =~ Star re -> P s2 (Star re) -> P (s1 ++ s2) (Star re)) ->
       forall (l : list T) (r : reg_exp T), l =~ r ->
       P l r
*)

这种类型表示（如果您跳过最初的forall“标题”）您需要证明一堆子目标来证明目标P l r。->顶层的every分隔子目标：

1）MEmpty案例：

P [] EmptyStr

没有假设，这就是我们开始的原因 induction Hmatch as [ | ——注意 . 的左侧没有任何内容|。

2）MChar案例：

(forall x : T, P [x] (Char x))

这种情况下的介绍模式很简单：对于一些x'我们需要证明P [x'] (Char x'). 此时我们的模式变为：[ | x'...

3）MApp案例：

(forall (s1 : list T) (re1 : reg_exp T) 
        (s2 : list T) (re2 : reg_exp T),  (* s1 re1 s2 re2 *)
        s1 =~ re1 ->                      (* Hmatch1 *)
        P s1 re1 ->                       (* IH1 *)
        s2 =~ re2 ->                      (* Hmatch2 *)
        P s2 re2 ->                       (* IH2 *)
        P (s1 ++ s2) (App re1 re2))       (* the current subgoal *)

我根据定理中使用的变量和假设在上面的评论中标记了变量和假设in_re_match。此时我们的模式变为：[ | x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2...

其余的子目标可以类似地完成，从而产生定理中使用的模式。

于 2016-08-31T07:19:37.750 回答