我正在尝试找出如何解决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.
我的想法是引入第一个正则表达式,因为它将使我们满足第一个析取项,
我不理解这种推理(也许这不是您真正的意思)。如果您只能证明第一个析取物,那么将析取物放在第一位是没有意义的。
而所有其他正则表达式形式将允许一个证明存在的权利析取关系。
“其他”不是什么?
((iii)是否有任何方法可以接受证明的单个部分,然后再返回证明(因为这个简单的案例使我失望,并且我想研究其他一些案例。)]
有admit.
策略可以跳过当前目标,Admitted.
命令可以跳过整个证明。
此问题的提示:第一个假设是什么意思:a :: s =~ (App re0 re1)
(即,看看=~
的定义对App
的看法是什么?]