Résoudre cet exercice de coq

Question

J'apprends le COQ et je suis bloqué sur l'un des exercices du livre. Le livre ne me donne pas de solution donc je ne sais pas quoi faire. J'ai fait le premier cependant. Je dois traduire ces déclarations à la logique sous-jacente:

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 

.

Pourriez-vous m'aider s'il vous plaît? Merci beaucoup!

Answer 1

Je suppose que ces définitions vous ont été fournies, donc "tout le monde" est représenté par les membres de Fans.

Avec quoi êtes-vous coincé? Par exemple, h1 dit que "personne ne connaît personne". Cela se résume au fait que «ce n'est pas le cas que quelqu'un ne connaisse personne». Maintenant, vous avez deux façons de procéder:

1. Vous codez "quelqu'un ne connaît personne" manuellement, et annulez simplement. (Ou) Vous réutilisez h0, en notant que sa négation est "quelqu'un ne connaît personne".

---

Pour parler de joueurs de football, vous vérifiez simplement qu'une x : Fans variables Footballer x -> satisfait. Par exemple, h3 commencerais comme:

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

---

h5 Peut-être est un peu plus difficile. Une façon d'encoder "une seule personne" est de dire qu'il connaît une personne p0, et que s'il connaît une autre personne p1, alors p1 = p0.

---

Sans plus de détails sur ce que vous trouvez difficile, il est difficile de vous fournir une réponse utile qui n'est pas la solution.