如何在Coq中定义带重叠产生式的递归迁移序列符号？

方法一：直接展开为合取式 #

利用Coq记号（Notation）的左结合特性，无需额外定义归纳类型，就能让链式写法直接展开为多个迁移谓词的合取。

首先保留你已定义的单个迁移记号（假设你已提前定义Label和State类型）：

Inductive Label : Type :=
| L : nat -> Label.

Inductive State : Type :=
| S : nat -> State.

Inductive Trans : Label -> State -> State -> Prop :=
| T : forall l s1 s2, Trans l s1 s2.

Notation "S1 -{ a }-> S2" := (Trans a S1 S2) (at level 70).

然后定义左结合的链式记号，级别与单个迁移一致：

Notation "S1 -{ a }-> S2 -{ b }-> S3" := ((S1 -{ a }-> S2) /\ (S2 -{ b }-> S3)) (at level 70, left associativity).

当你写S1 -{a1}-> S2 -{a2}-> S3 -{a3}-> S4时，Coq会自动按左结合解析为：

((S1 -{a1}-> S2) /\ (S2 -{a2}-> S3)) /\ (S3 -{a3}-> S4)

这与你期望的多合取逻辑完全等价，因为命题合取满足结合律。

方法二：定义归纳序列谓词（更符合Coq风格） #

如果需要灵活处理整个迁移序列的标签列表（比如量化、遍历序列），可以先定义归纳的迁移序列谓词，再将链式写法映射到该谓词：

1. 定义迁移序列的归纳类型：

Inductive TransSeq : list Label -> State -> State -> Prop :=
| SeqNil : forall s, TransSeq [] s s  (* 空序列：状态保持不变 *)
| SeqCons : forall a l s1 s2 s3,
    Trans a s1 s2 -> TransSeq l s2 s3 -> TransSeq (a :: l) s1 s3.

2. 扩展链式记号以支持序列：

(* 单个迁移仍对应Trans *)
Notation "S1 -{ a }-> S2" := (Trans a S1 S2) (at level 70).
(* 链式写法自动累积标签列表，对应TransSeq *)
Notation "S1 -{ a }-> S2 -{ l }-> S3" := (TransSeq (a :: l) S1 S3) 
  (at level 70, left associativity, l at level 0).

3. 可通过归纳法证明该序列谓词与合取式等价：

Lemma TransSeq_equiv_conj : forall s1 s2 l,
  TransSeq l s1 s2 <->
  match l with
  | [] => s1 = s2
  | [a] => Trans a s1 s2
  | a :: (b :: ls) => exists s', (Trans a s1 s') /\ TransSeq (b :: ls) s' s2
  end.
Proof.
(* 通过对l的归纳完成证明 *)
Admitted.

语法妥协（可选） #

如果原分隔符-{a}->导致解析冲突，可简化为更简洁的形式，比如-[a]->，定义逻辑完全一致：

Notation "S1 -[ a ]-> S2" := (Trans a S1 S2) (at level 70).
Notation "S1 -[ a ]-> S2 -[ b ]-> S3" := ((S1 -[ a ]-> S2) /\ (S2 -[ b ]-> S3)) (at level 70, left associativity).

内容的提问来源于stack exchange，提问作者radrow