解决这个coq练习

我正在学习COQ，我被困在书练习之一。这本书没有给我一个解决方案，所以我不知道该怎么办。我已经完成了第一个。我必须将这些语句谓词逻辑翻译：解决这个coq练习

h0 : Everybody knows somebody 
    h1 : Nobody doesn't know anybody. 
    h2 : Everybody knows somebody 
    h3 : A footballer is known by everybody. 
    h4 : Footballers only know footballers. 
    h5 : There is somebody who only knows one person.

代码：

Section Stadium. 

Variable Fans : Set. 
Variable Knows : Fans -> Fans -> Prop. 
Variable Footballer : Fans -> Prop. 

Hypothesis h0 : forall x: Fans, exists y: Fans, Knows x y. 


End Stadium

。

你能帮忙吗？非常感谢！

来源

2012-10-21 Nayr

“The book”是[Coq'Art]（http://labri.fr/perso/casteran/CoqArt/index.html），我说得对吗？ – minopret

我认为这些定义是提供给你的，所以“所有人”都由Fans的成员代表。

你在坚持什么？

例如，h1说“没有人不认识任何人”。这可归结为一个事实，即“不是有人不认识任何人”。现在您有两种方法可以进行：

您手动编码“某人不认识任何人”，并且只是否定它。
（或者）您重复使用h0，注意其否定是“某人不认识任何人”。

谈谈足球，你只需验证一个变量x : Fans满足Footballer x ->。例如，H3将开始这样的：

forall x, Footballer x -> (* here, you encode "everybody knows x" *)

也许H5是有点困难。编码“只有一个人”的一种方法是说他知道一个人p0，并且如果他知道另一个人p1，则p1 = p0。

不上你发现了什么困难的进一步的细节，这是很难为你提供一个有用的答案是不是解决办法。

来源

2012-10-21 02:56:58 Ptival

解决这个coq练习

回答

相关问题