软件基础:弱泵引理证明

Question

继续我在软件基础方面的工作，我已经达到了weak_pumping引理。我设法解决了几乎所有的问题，但我找不到MStarApp案例的解决方案。

这是引理：

s =~ re ->
pumping_constant re <= length s ->
exists s1 s2 s3,
s = s1 ++ s2 ++ s3 /
s2 <> [] /
forall m, s1 ++ napp m s2 ++ s3 =~ re.
(** You are to fill in the proof. Several of the lemmas about
[le] that were in an optional exercise earlier in this chapter
may be useful. *)
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 ].

除了最后一个案子，我成功地解决了每一个案子。以下是当前状态：

1 subgoal (ID 918)

T : Type
s1, s2 : list T
re : reg_exp T
Hmatch1 : s1 =~ re
Hmatch2 : s2 =~ Star re
IH1 : pumping_constant re <= length s1 ->
exists s2 s3 s4 : list T,
s1 = s2 ++ s3 ++ s4 /
s3 <> [ ] / (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re)
IH2 : pumping_constant (Star re) <= length s2 ->
exists s1 s3 s4 : list T,
s2 = s1 ++ s3 ++ s4 /
s3 <> [ ] / (forall m : nat, s1 ++ napp m s3 ++ s4 =~ Star re)
H : pumping_constant (Star re) <= length s1 + length s2
============================
exists s0 s4 s5 : list T,
s1 ++ s2 = s0 ++ s4 ++ s5 /
s4 <> [ ] / (forall m : nat, s0 ++ napp m s4 ++ s5 =~ Star re)

在我看来，如果我能找到将H拆分为pumping_constant re <= length s1 / pumping_constant (Star re) <= length s2的方法，那么我就有了前进的道路(通过将H拆分为H1和H2，并将相关的IHk应用于匹配的Hk，然后继续进行一个destruct、三个exists，等等)。

但我找不到一个引理可以让我按照建议分裂H。

我还能在这里做什么吗？

感谢

Answer 1

在其中一种情况下，尝试破坏s1并再次查找引理napp_star。