All geek questions in one place

The solution to this exercise

I am learning COQ and I am stuck in one of the exercises. The book does not give me a solution, so I do not know what to do. I did the first one though. I have to translate these statements into predicate logic:

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.

code:

 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

.

You can help? Thank you very much!

+4
source share
1 answer

I assume that these definitions were provided to you, so "all" are submitted by Fans members.

What are you stuck with?

For example, h1 says that "no one knows anyone." It comes down to the fact that "this is not the case when someone does not know anyone." You now have two ways:

  • You encode "someone knows no one" manually and simply deny it.

  • (or) You reuse h0, noting that his denial of "someone knows no one."

To talk about footballers, you just make sure that the x : Fans variable satisfies Footballer x -> . For example, h3 will start as follows:

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

Maybe h5 is a bit more complicated. One way to encode “only one person” is that he knows one person p0 and that if he knows another person p1, then p1 = p0.

Without further details about what is difficult for you, it is difficult to give you a useful answer that is not a solution.

+3
source

Source: https://habr.com/ru/post/1441028/

More articles:


All Articles