Как разделить гипотезу неравенства по длине в лемме накачки? - PullRequest
Новая
       18

Как разделить гипотезу неравенства по длине в лемме накачки?

0 голосов
/ 06 мая 2019

Это 5-звездочное упражнение от Фондов программного обеспечения. 

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 <> [] /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.
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 ]; simpl; intros.
  - omega.
  - omega.
  -

1 subgoal
T : Type
s1 : list T
re1 : reg_exp
s2 : list T
re2 : reg_exp
Hmatch1 : s1 =~ re1
Hmatch2 : s2 =~ re2
IH1 : pumping_constant re1 <= length s1 ->
      exists s2 s3 s4 : list T,
        s1 = s2 ++ s3 ++ s4 /\
        s3 <> [ ] /\ (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 <> [ ] /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ re2)
H : pumping_constant re1 + pumping_constant re2 <= length (s1 ++ s2)
______________________________________(1/1)
exists s0 s3 s4 : list T,
  s1 ++ s2 = s0 ++ s3 ++ s4 /\
  s3 <> [ ] /\ (forall m : nat, s0 ++ napp m s3 ++ s4 =~ App re1 re2)

Я потратил слишком много времени, пытаясь разделить это H, только чтобы понять, что, несмотря на полтора дня работы над этим, многие из моих предположений о том, как работает неравенство, оказались неверными. Вчера вечером у меня были отличные идеи, которые теперь, когда они были отброшены, оставляют меня в замешательстве об этой проблеме, как никогда. Кажется, я только что выучил алгебру за последние два дня.

Я буду очень смущен, если ответ окажется, что мне нужно соответствовать на s с или length s с или pumping_constant re с, потому что я не могу найти способ протолкнуть туда .

Способ решения этой проблемы настоятельно предполагает, что H следует как-то разбить, чтобы сделать индукцию. Я до сих пор с подозрением отношусь к этому.

1 Ответ

1 голос
/ 07 мая 2019

Да, вам нужно разделить H, чтобы продолжить.

Неясный намек: Сделайте Search (_ + _ <= _ + _). и найдите теорему, которая бросается в глаза.

Подсказка:

...