卡在逻辑基金会的Mapp案件中

Question

我正在教自己通过逻辑基础课程使用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.

到目前为止，我的方法是在假设pupping_constant re1 + pumping_constant re2＆lt; =长度S1 +长度S2的假设上应用add_le_case ＆lt; =长度S1 \/ pumping_constant re2＆lt; =长度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＆lt; =长度S1导致了一个简单的目标。情况pumping_constant re2＆lt; =长度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 *)

我必须证明长度（S1 ++ S1'） +长度S3'＆lt; = pupping_constant（App Re1 re2）（或长度S1 +长度S1' +长度S1' +长度S3'＆lt; = pupping_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' <> [ ]

我在正确的轨道上选择（s1 ++ s1'），s3'，s4'。还是死胡同？如果不是死胡同，我该如何更接近证明我当前的目标？