Coq中S-表达式打印函数sexpprint单射性证明求助

核心思路说明 #

你的分层归纳思路是完全可行的，问题在于缺少了两个前置引理的拆分：打印结果的唯一可拆分性、子S-表达式列表打印结果的单射性，不需要对双列表同时做归纳。

需要的归纳原理陈述 #

你可以直接使用自然数的强归纳原理配合你定义的深度函数，也可以使用专门针对嵌套递归类型的增强归纳原理，该原理可以通过Coq的Scheme命令自动生成，命题陈述如下：

Scheme sexp_ind2 := Induction for sexp Sort Prop
  with list_sexp_ind2 := Induction for list sexp Sort Prop.
Combined Scheme sexp_full_ind from sexp_ind2, list_sexp_ind2.

该归纳原理的作用是在证明S-表达式的性质时，可以直接递归使用所有子S-表达式的归纳假设，比Coq默认生成的弱归纳原理更适配嵌套定义的sexp类型。

关键前置引理证明 #

你首先需要证明如下唯一前缀拆分引理，这个引理可以直接解决列表归纳的问题：

Lemma sexpprint_prefix_cancel s1 s2 xs ys :
  sexpprint s1 ++ xs = sexpprint s2 ++ ys ->
  s1 = s2 /\ xs = ys.

该引理用深度强归纳证明即可：

1. 展开sexpprint的定义，首先可以从等式两边提取出构造器名n1 = n2
2. 再通过括号匹配的性质，将等式拆解为子列表打印拼接结果的相等：concat (map sexpprint l1) ++ [")"] ++ xs = concat (map sexpprint l2) ++ [")"] ++ ys
3. 递归应用前缀拆分引理逐元素匹配子列表的打印结果，即可得到l1 = l2，最终得到s1 = s2和剩余列表xs = ys的结论。

主定理证明步骤 #

1. 先补全你写的depth_decr引理的证明，直接调用Coq标准库中list_max的相关性质即可完成。
2. 用强归纳对深度做归纳，证明对任意深度小于m的S-表达式，sexpprint是单射的。
3. 证明深度为m的S-表达式的单射性时，展开sexpprint的定义得到构造器名相等后，将子列表的打印相等性代入刚才证明的前缀拆分引理，逐元素匹配即可得到两个子列表相等，从而得到顶层S-表达式相等的结论。
4. 将分层结论推广到所有深度的S-表达式，即可得到最终的sexpprint_inj定理。

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