coq - 坚持一个关于正则表达式的简单证明

Question

我正在尝试使用 Coq 对正则表达式 (RE) 的一些属性进行形式化。但是，我在证明一个相当简单的属性时遇到了一些麻烦:

For all strings s, if s is in the language of (epsilon)* RE, then s = "", where epsilon and * denotes the empty string RE and Kleene star operation.

这似乎是归纳/反转策略的明显应用，但我无法使其发挥作用。

带有问题引理的最小工作代码在以下 gist 中。
任何关于我应该如何进行的提示将不胜感激。

编辑 :

我的尝试之一是这样的:

Lemma star_lemma : forall s, s <<- (#1 ^*) -> s = "".
Proof.  
  intros s H.
  inverts* H.
  inverts* H2.
  inverts* H1.
  inverts* H1.
  inverts* H2.
  simpl in *.
  -- stuck here

这给我留下了以下目标:

s' : string
H4 : s' <<- (#1 ^*)
============================
s' = ""

至少对我来说，使用归纳法似乎可以完成证明，因为我可以在归纳假设中使用 H4 来完成证明，但是当我开始证明时使用

induction H

代替

inverts* H

我得到了一些(至少对我而言)毫无意义的目标。在 Idris/Agda 中，这样的证明只是通过对 s <<- (#1 ^*) 的结构进行模式匹配和递归。我的观点是如何在 Coq 中进行这种递归。

Answer 1

这是原始问题的一种可能解决方案:

Lemma star_lemma : forall s,
    s <<- (#1 ^*) -> s = "".
Proof.
  refine (fix star_lemma s prf {struct prf} : s = "" := _).
  inversion_clear prf; subst.
  inversion_clear H; subst.
  - now inversion H0.
  - inversion_clear H0; subst. inversion_clear H; subst.
    rewrite (star_lemma s' H1).
    reflexivity.
Qed.

主要思想是在上下文中引入一个术语，它类似于典型 Idris 证明中的递归调用。使用 remember 和 dependent induction 的方法效果不佳(没有修改 in_regex )，因为它们引入了不可能满足的方程作为归纳假设的前提。

注意:检查这个引理可能需要一段时间(在我的机器上在 Coq 8.5pl3 下大约 40 秒)。我认为这是因为 inversion 策略倾向于生成大量证明项。