1 
Lemma re_not_empty_correct : forall T (re : @reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split.
  - admit. (* I proved it myself *)
  - intros. induction re.
    + simpl in H. discriminate H.
    + exists []. apply MEmpty.
    + exists [t]. apply MChar.
    + simpl in H. rewrite -> andb_true_iff in H. destruct H as [H1 H2].
      apply IHre1 in H1. apply IHre2 in H2.

到目前为止，这是我们所得到的：

1 subgoal (ID 505)

T : Type
re1, re2 : reg_exp
H1 : exists s : list T, s =~ re1
H2 : exists s : list T, s =~ re2
IHre1 : re_not_empty re1 = true -> exists s : list T, s =~ re1
IHre2 : re_not_empty re2 = true -> exists s : list T, s =~ re2
============================
exists s : list T, s =~ App re1 re2

现在我需要将 H1 和 H2 组合成exists s : list T, s =~ App re1 re2或将目标分解为 2 个子目标，并使用 H1 和 H2 分别证明它们。但我不知道，该怎么做。

4

1 回答 1

1

您可以将其exists视为包含值及其属性的对类型。就像普通的pair类型一样，你可以destruct。

例如，destruct H1 as [s1 H1].此时给出

s1 : list T
H1 : s1 =~ re1

鉴于此，考虑如何s在满足的目标中构造一个s =~ App re1 re2。然后使用策略exists (your answer).（这会将目标更改为(your answer) =~ App re1 re2）并填写证明的其余部分（如果您s是正确的，这应该是微不足道的）。

于 2019-06-22T08:04:59.677 回答