给定 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 语法模式的一般性讨论之外,还有其他相关文档吗?