coq – 坚持关于正则表达式的简单证明

发布时间：2020-12-14 06:03:38 所属栏目：百科来源：网络整理

导读：我正在尝试使用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 operatio

我正在尝试使用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中进行这样的递归.

解决方法

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

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证明中的递归调用的术语.具有记忆和依赖感应的方法不能很好地工作(没有修改in_regex),因为它们引入了不可能满足方程作为归纳假设的前提.

注意：检查此引理可能需要一段时间(在Coq 8.5pl3下我的机器上大约40秒).我认为这是因为反演策略往往会产生很大的证明条件.

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!