coq - 软件基础:weak_pumping 引理证明
问题描述
继续我在软件基础上的工作,我已经达到了weak_pumping
引理。我设法通过了几乎所有事情,但我找不到MStarApp
案例的解决方案。
这是引理:
s =~ re ->
pumping_constant re <= length s ->
exists s1 s2 s3,
s = s1 ++ s2 ++ s3 /\
s2 <> [] /\
forall m, s1 ++ napp m s2 ++ s3 =~ re.
(** You are to fill in the proof. Several of the lemmas about
[le] that were in an optional exercise earlier in this chapter
may be useful. *)
Proof.
intros T re s Hmatch.
induction Hmatch
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
我设法解决了所有情况,除了最后一个。这是当前状态:
1 subgoal (ID 918)
T : Type
s1, s2 : list T
re : reg_exp T
Hmatch1 : s1 =~ re
Hmatch2 : s2 =~ Star re
IH1 : pumping_constant re <= length s1 ->
exists s2 s3 s4 : list T,
s1 = s2 ++ s3 ++ s4 /\
s3 <> [ ] /\ (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re)
IH2 : pumping_constant (Star re) <= length s2 ->
exists s1 s3 s4 : list T,
s2 = s1 ++ s3 ++ s4 /\
s3 <> [ ] /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ Star re)
H : pumping_constant (Star re) <= length s1 + length s2
============================
exists s0 s4 s5 : list T,
s1 ++ s2 = s0 ++ s4 ++ s5 /\
s4 <> [ ] /\ (forall m : nat, s0 ++ napp m s4 ++ s5 =~ Star re)
在我看来,如果我能找到一种方法来拆分H
,pumping_constant re <= length s1 \/ pumping_constant (Star re) <= length s2
那么我就有了前进的道路(通过拆分H
并H1
应用H2
相关IHk
的匹配,Hk
然后继续进行 a destruct
, threeexists
等等)。
但是我找不到允许我H
按照建议进行拆分的引理。
还有什么我可以在这里做的吗?
谢谢
解决方案
在其中一种情况下,尝试破坏 s1 并再次查看引理 napp_star。
推荐阅读
- angular - 以角度提交表单时出现mat-select问题
- java - Hibernate 代码在提交 txn 之前检查会话是否已关闭,但随后会抱怨会话已关闭
- azure - 监控外部 IP 的日志分析查询
- sql - SQL server : Replace the value using like operator
- typescript - 如何控制 Angular 6 上的内存泄漏和节点
- sql - 如何在 Spark Scala 中将 Hive 表的表统计信息导入 Dataframe
- spacy - 基于 POS 标签的 N-gram:Spacy
- python - pd.DataFrame.agg(np.var) 与 pd.Series.np.var
- php - Laravel 和 Postgresql 带有消息“找不到驱动程序”错误的 PDOException
- excel - 在 Mac osx 上添加图像注释 Excel 16