Software Foundations中weak_pumping引理MStarApp分支证明求助

问题场景 #

学习《Software Foundations》过程中完成了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，之后对两个分支分别调用对应的归纳假设IH1、IH2，再通过destruct和exists语句完成证明，但找不到对应的拆分引理。 #

可行证明方案 #

1. 第一步先调用pumping_constant对Star结构的定义：pumping_constant (Star re) = pumping_constant re，对假设H做重写。
2. 使用自然数序的可判定性引理Nat.le_ge_dec或者SF中介绍过的decide tactic，对命题pumping_constant re <= length s1做分支拆分：
   • 分支1：pumping_constant re <= length s1成立
     直接调用IH1得到s1的拆分s_a, s_b, s_c，满足s1 = s_a ++ s_b ++ s_c、s_b <> []、forall m, s_a ++ napp m s_b ++ s_c =~ re。
     你要构造的目标拆分就是s_a, s_b, s_c ++ s2：
     • 字符串相等性用列表append的结合律即可证明
     • s_b非空直接继承IH1的结论
     • 匹配性用MStarApp构造子拼接即可：前半段s_a ++ napp m s_b ++ s_c匹配re，后半段s2匹配Star re，自然能得到整体匹配Star re。
   • 分支2：pumping_constant re <= length s1不成立
     此时可得length s1 < pumping_constant re，结合重写后的Hpumping_constant re <= length s1 + length s2，可以推导出length s2 >= 1，同时满足pumping_constant (Star re) <= length s2，直接调用IH2得到s2的拆分s_a, s_b, s_c。
     你要构造的目标拆分就是s1 ++ s_a, s_b, s_c：
     • 字符串相等性用列表append的结合律即可证明
     • s_b非空直接继承IH2的结论
     • 匹配性用MStarApp构造子拼接即可：前半段s1匹配re，后半段s_a ++ napp m s_b ++ s_c匹配Star re，自然能得到整体匹配Star re。

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