在Coq中证明泵引理时卡在MApp分支求解决思路

我正在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.

我的MApp部分证明代码 #

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 *)
    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 *)
    simpl. intros contra. inversion contra.
  - (* MChar *)
    simpl. intros. inversion H. inversion H1.
  - (* MApp *)
    simpl. rewrite app_length. intros.
    apply add_le_cases in H.
    destruct H as [H|H].
    + (*case pumping_constant re1 <= length s1 ommitted*)
    + apply IH2 in H. destruct H as [ss1 [ss2 [ss3 [H1 [H2 [H3 H4]]]]]].
      exists (s1++ss1), ss2, ss3. split.
      * rewrite H1. rewrite <- app_assoc. reflexivity.
      * split. apply H2.
        split. rewrite app_length.
        assert (Hc: length s1 < pumping_constant re1 \/ length s1 >= pumping_constant re1).
        apply lt_ge_cases.
        destruct Hc as [Hc|Hc].
        apply le_S in Hc.
        apply Sn_le_Sm__n_le_m in Hc.
        rewrite <- add_assoc.
        apply (Plus.plus_le_compat _ _ _ _ Hc).
        apply H3.
        (* stuck *)

当前卡住的目标状态 #

当处理Hc: length s1 >= pumping_constant re1的情况时，当前目标如下：

Goal:
2 goals
T : Type
s1 : list T
re1 : reg_exp T
s2 : list T
re2 : reg_exp T
Hmatch1 : s1 =~ re1
Hmatch2 : s2 =~ re2
IH1 : pumping_constant re1 <= length s1 ->
      exists s2 s3 s4 : list T,
        s1 = s2 ++ s3 ++ s4 /\
        s3 <> [ ] /\
        length s2 + length s3 <= pumping_constant re1 /\
        (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re1)
IH2 : pumping_constant re2 <= length s2 ->
      exists s1 s3 s4 : list T,
        s2 = s1 ++ s3 ++ s4 /\
        s3 <> [ ] /\
        length s1 + length s3 <= pumping_constant re2 /\
        (forall m : nat, s1 ++ napp m s3 ++ s4 =~ re2)
ss1, ss2, ss3 : list T
H1 : s2 = ss1 ++ ss2 ++ ss3
H2 : ss2 <> [ ]
H3 : length ss1 + length ss2 <= pumping_constant re2
H4 : forall m : nat, ss1 ++ napp m ss2 ++ ss3 =~ re2
Hc : length s1 >= pumping_constant re1
______________________________________(1/2)
length s1 + length ss1 + length ss2 <=
pumping_constant re1 + pumping_constant re2

我尝试通过分情况length s1 = pumping_constant re1 \/ length s1 > pumping_constant re1来解决，但右侧分支仍难以推进，请问该如何突破？

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