不能专注于COQ中剩余的未关注目标

Question

我试图证明抽水引理（这是逻辑基础书的练习之一）。我以为我已经完成了mstarapp案例，但解释器告诉我，仍然存在未加注的目标。只有我不能将剩余的目标带到前面。我尝试了每个子弹级级别，但是每次我得到[focus]错误的子弹：不再是目标。我不知道我的证明是否有问题，还是解释器中的错误。任何帮助都将不胜感激。

- (* MStarApp *)
    intros.
    destruct s1.
    -- replace ([ ] ++ s2) with s2 in *. apply (IH2 H).
       reflexivity.
    -- pose proof (lt_ge_cases (length (x::s1)) (pumping_constant re)) as [
    Hs1lt | Hs1ge].
      --- exists [ ], (x::s1), s2. repeat split.
        + unfold not. intro. inversion H0.
        + simpl. simpl in Hs1lt. 
          apply n_lt_m__n_le_m in Hs1lt.
          apply Hs1lt.
        + simpl. intro m. 
          apply (napp_star T m (x::s1) s2 re Hmatch1 Hmatch2).
      --- unfold ge in Hs1ge. pose proof (IH1 Hs1ge) as [
        s2' [s3' [s4' [Hxs1Eq [Hs3notEmpty [
        Hlens2's3' Hnapp]]]]]].
        exists s2', s3', (s4' ++ s2). repeat split.
        + rewrite Hxs1Eq. repeat rewrite <- app_assoc.
          reflexivity.
        + assumption.
        + simpl. assumption.
        + intro m. pose proof Hnapp m.
          replace (s2' ++ napp m s3' ++ s4' ++ s2) with 
          ((s2' ++ napp m s3' ++ s4') ++ s2).
          constructor.
          ++ assumption.
          ++ assumption.
          ++ repeat rewrite <- app_assoc. reflexivity.
(* 'There are unfocused goals.' *)

edit ：我不知道这是否相关，但在我的证明中更高（在mapp案例中）我有一个servert其关闭卷曲支架以不寻常的方式突出显示（以黄色而不是绿色 - 我正在使用VSCODE中的COQ语言支持扩展）。

Answer 1

您在一些早期的证明分支机构中没有完成业务。您提供的一个目标没有任何未完成的目标。您已经将未完成或录取 提出了一些较早的目标。或者可能您没有正确完成断言。如果您需要帮助，则需要显示证明的一部分。

这是您的证明开始的证明状态，并由您的解决方案解决
证明脚本。

Lemma foo   
(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 <> [ ] /\
        length s2 + length s3 <= pumping_constant re /\
        (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 <> [ ] /\
        length s1 + length s3 <= pumping_constant (Star re) /\
        (forall m : nat, s1 ++ napp m s3 ++ s4 =~ Star re))
:
pumping_constant (Star re) <= length (s1 ++ s2) ->
exists s0 s3 s4 : list T,
  s1 ++ s2 = s0 ++ s3 ++ s4 /\
  s3 <> [ ] /\
  length s0 + length s3 <= pumping_constant (Star re) /\
  (forall m : nat, s0 ++ napp m s3 ++ s4 =~ Star re)
.