Continuing my work on Software Foundations, I've reached the weak_pumping
lemma. I managed to get through almost everything, but I can't find a solution for MStarApp
case.
Here's the Lemma:
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 ].
I've managed to solve every case, except for the last one. Here's the current state:
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)
It looks to me that if I can find a way to split H
into pumping_constant re <= length s1 \/ pumping_constant (Star re) <= length s2
then I have a way forward (by splitting H
into H1
and H2
and applying the relevant IHk
to the matching Hk
then proceeding with a destruct
, three exists
, and so on).
But I can't find a lemma that allows me to split H
as suggested.
Is there anything else I can do here?
Thanks
Try to destruct s1 and look again on lemma napp_star in one of cases.