如何在coq证明中(和其他一般的coq要求中处理EmptySet regex构造函数?

问题描述 投票:0回答:1

我正在尝试找出如何解决SF中的app_ne问题。我的想法是对第一个正则表达式进行归纳,因为它将使我们满足第一个析取关系,而所有其他正则表达式形式将使我们能够证明存在的权利析取。

(i)这是解决问题的正确方法吗?(ii)如果是这样,如何处理空案?这让我马上。(iii)是否有任何方法可以接受证明的单个部分,然后再返回证明(因为这个简单的案例使我失望,并且我想解决其他一些案例。)

Lemma app_ne : forall (a : ascii) s re0 re1,
    a :: s =~ (App re0 re1) <->
    ([ ] =~ re0 /\ a :: s =~ re1) \/
    exists s0 s1, s = s0 ++ s1 /\ a :: s0 =~ re0 /\ s1 =~ re1.
Proof.
  intros.
  split.
  - intros. induction re0.
    * right. inversion H.
      (* + apply re_not_empty_correct. *)
      (* + apply MEmpty. *)
Abort.
regex coq theorem-proving
1个回答
0
投票

我的想法是引入第一个正则表达式,因为它将使我们满足第一个析取项,

我不理解这种推理(也许这不是您真正的意思)。如果您只能证明第一个析取物,那么将析取物放在第一位是没有意义的。

而所有其他正则表达式形式将允许一个证明存在的权利析取关系。

“其他”不是什么?

((iii)是否有任何方法可以接受证明的单个部分,然后再返回证明(因为这个简单的案例使我失望,并且我想研究其他一些案例。)]

admit.策略可以跳过当前目标,Admitted.命令可以跳过整个证明。


此问题的提示:第一个假设是什么意思:a :: s =~ (App re0 re1)(即,看看=~的定义对App的看法是什么?]

© www.soinside.com 2019 - 2024. All rights reserved.