Coq Logical Foundations泵引理MApp分支证明受阻求解

我正在通过《Logical Foundations》课程自学Coq证明助手。
我在证明泵引理的MApp分支时遇到了阻碍，待证明的引理如下：

Lemma pumping : forall T (re : reg_exp T) s,
  s =~ re ->
  pumping_constant re <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    s2 <> [] /\
    length s1 + length s2 <= pumping_constant re /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.

现有证明思路 #

我目前的证明思路为：针对前提pumping_constant re1 + pumping_constant re2 <= length s1 + length s2应用add_le_cases，推导得出pumping_constant re1 <= length s1 \/ pumping_constant re2 <= length s2，已编写的证明代码如下：

Proof.
  intros T re s Hmatch.
  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 ].
  - (* MEmpty -- omitted *)
  - (* MChar -- omitted *)
  - (* MApp *)
    intro Hlength. simpl in Hlength. 
    rewrite app_length in Hlength. 
    pose proof (add_le_cases (pumping_constant re1) 
                             (pumping_constant re2) 
                             (length s1) 
                             (length s2) 
                             Hlength) as [Hre1ineq | Hre2ineq].

其中pumping_constant re1 <= length s1的分支可以轻松完成证明，但pumping_constant re2 <= length s2的分支推进困难，该分支当前编写的代码如下：

-- (* pumping_constant re1 <= length s1 -- omitted *)
    -- (* pumping_constant re2 <= length s2. *)
      pose proof (IH2 Hre2ineq) as [s1' [s3' [s4' [
      Hs2eq [Hs3'len [Hlens1's3' Hnapp]]]]]].
      exists (s1++s1'), s3', s4'. repeat split.
      --- rewrite Hs2eq. repeat rewrite <- app_assoc.
          reflexivity.
      --- assumption.
      --- (* stuck *)

当前卡壳的子目标 #

当前需要证明的子目标为length (s1 ++ s1') + length s3' <= pumping_constant (App re1 re2)，化简后等价于length s1 + length s1' + length s3' <= pumping_constant re1 + pumping_constant re2，现有可用前提如下：

Hre2ineq: pumping_constant re2 <= length s2
Hlength: pumping_constant re1 + pumping_constant re2 <= length s1 + length s2
Hlens1's3': length s1' + length s3' <= pumping_constant re2
Hs2eq: s2 = s1' ++ s3' ++ s4'
Hs3'len: s3' <> [ ]

解答 #

你选择的存在量词实例化方向本身是对的，卡壳的核心原因是分支拆分逻辑有问题：
你直接用add_le_cases拆分得到的两个分支不是互斥的，在pumping_constant re2 <= length s2成立的同时，pumping_constant re1 <= length s1也可能成立，这种情况下你没有length s1 < pumping_constant re1的约束，自然无法证明长度不等式——毕竟s1本身的长度就已经大于等于pumping_constant re1，加上s1'和s3'的长度后很容易超过总泵常数。
修正分支拆分方式即可：

1. 不要直接用add_le_cases的结果做析取拆分，首先对pumping_constant re1 <= length s1做判定：
   • 第一种情况：pumping_constant re1 <= length s1，走你原来已经证完的第一个分支即可，用IH1拆分s1，构造的拆分前缀不需要包含s2部分。
   • 第二种情况：~ (pumping_constant re1 <= length s1)，也就是length s1 < pumping_constant re1，这个前提下结合Hlength可以直接推导出pumping_constant re2 <= length s2，此时再调用IH2拆分s2。
2. 第二种情况下去证明长度目标非常直接：
   已知Hlens1's3': length s1' + length s3' <= pumping_constant re2，加上当前分支的前提length s1 < pumping_constant re1，可以直接推出：

   length s1 + length s1' + length s3' < pumping_constant re1 + pumping_constant re2
   

   自然满足小于等于的要求。
3. 最后一个关于任意m次重复后仍匹配的目标不需要修改，你原来的证明逻辑成立：拆分后s1' ++ napp m s3' ++ s4'匹配re2，前面拼接s1后整体自然匹配App re1 re2。

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