如何解决Coq中的证明模式定义?
任何人都可以给我一些有关如何阅读证明模式定义的好资料(给出一个例子:)
Definition A (ss: FSS) (n:nat)
(s: {s:S | state_is_wf s
/\ RESS.get_element n (proj1_sig ss) = Some s})
: FS.
destruct s. destruct a.
refine (exist _ x _).
apply H.
Defined.
其中“ FSS”,“ FS”和“ S”是先前定义的信号类型。我知道独特的策略“破坏”,“完善”和“应用”是做什么的,但在证明意义上 一个定义,我可能无法编译就无法阅读该证明(我无法编译这些文件,只能读取其源代码。)有人可以帮助我阅读此类定义,还是可以指向某些源代码?
解决方法
如果不编译定义(并且不查看FS
和FSS
的定义),这是不可能的,但是我们仍然可以猜测。 destruct
策略在match with
上创建s
类型的sig
构造,该构造具有唯一的构造函数exist
。函数的参数中没有a
,因此a
是全局符号,或者是由第一个destruct
创建的变量。让我们假设是后者。 x
也是如此。
策略refine
创建了一个可能带有漏洞的术语。术语exist _ x _
包含两个孔。第一个_
由Coq填充,但最后一个{大概必须由用户填充,因此apply H
就是这个目的。对于H
,让我们假设它来自先前的destruct
之一。
请注意,apply
可能首先仅使用一个构造函数分解归纳值。因此,如果H
的类型恰好是A /\ B
(如果它来自第一个destruct
,则实际上是apply H
或apply (proj1 H)
或apply (proj2 H)
。无论如何,由于证明现已完成,因此此apply
可能是exact
。
因此,有很多可能性。这是一个示例:
Definition A ss n s :=
match s with
| exist _ a H =>
match a with
| ... x ... => (* H could come from there too *)
exist _ x (proj1 H) (* or (proj2 H),or plain H *)
end
end.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。