如何解决Coq - 为“forall-exists”语句选择见证人的函数
在 Coq 证明中,假设我有一个形式的假设
forall a:A,P a -> exists b:B,Q a b
哪里
A B:Type
P : A -> Prop
Q : A -> B -> Prop
我想定义一个满足f : A -> B
的函数
forall a:A,P a -> Q a (f a)
所以这里有几个问题:
- 是否可以建设性地定义
f
? - 如果是,Coq 是否具有允许我定义
f
的内置机制? - 如果没有,我可以添加哪些公理/参数来定义
f
?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。