IndProp：re_not_empty_correct

Question

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 分别证明它们。但是我不知道，怎么做。

Answer 1

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

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

s1 : list T
H1 : s1 =~ re1

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

IndProp：re_not_empty_correct

IndProp: re_not_empty_correct

coq

logical-foundations