Si j'ai E => (F =>G), par E je prouve que F => G et par F je prouve GCitation:
Envoyé par SpiceGuid
Dit autrement, E => (F =>G) est une autre façon d'écrire (E & F) => G
Je bloque un peu sur la question 11, mais je cherche en tâche de fond.
Version imprimable
Si j'ai E => (F =>G), par E je prouve que F => G et par F je prouve GCitation:
Envoyé par SpiceGuid
Dit autrement, E => (F =>G) est une autre façon d'écrire (E & F) => G
Je bloque un peu sur la question 11, mais je cherche en tâche de fond.
we:W(E) |->Citation:
Envoyé par DrTopos
weg: (W(E) -> W(G)) |->
wfg : (W(F) -> W(G)) |->
weg we
et
wf:W(F) |->
weg: (W(E) -> W(G)) |->
wfg : (W(F) -> W(G)) |->
wfg wf
C'est presque bon. Il n'empêche que si j'étais un compilateur j'enverrais un message d'erreur, disant qu'à la ligne 2 le symbole G est inconnu. La solution correcte est:Citation:
Envoyé par alex_pi
we:W(E) |->
G:O |->
weg: (W(E) -> W(G)) |->
wfg : (W(F) -> W(G)) |->
weg we
Allo ? Allo ?
Il n'y a plus personne sur ce fil ? Rien depuis deux jours. Où êtes vous tous passés ?
Vous devriez prendre le temps de continuer à vous amuser. C'est bon pour la santé. :D
Désolé mais je tourne à beaucoup d'heure de cours d'info théorique (entre autre) par jours, et quand je rentre le soir, je n'ai pas trop le courage d'en rajouter.Citation:
Envoyé par DrTopos
Bon. Je vais faire avancer un peu les choses.
La réponse d'alex_pi, confirmée par SpiceGuid pour la question 9 (définition de la disjonction) est bonne. On définit donc la disjonction de deux énoncés E et F comme suit:
E | F := ?q:O (E => q) => ((F => q) => q)
J'ai mis toutes les parenthèses pour éviter les confusions. Toutefois, on pourrait écrire cet énoncé comme ceci:
?q:O (E => q) => (F => q) => q
étant entendu que le signe binaire infix => s'associe à droite (comme la flèche des types fonctionnels).
Comme l'a dit alex_pi, cette définition ne fait que formaliser un principe de raisonnement bien connu et utilisé instinctivement par tout le monde (même non mathématicien) qui est la preuve par disjonction des cas. Autrement-dit, si on veut utiliser une hypothèse de la forme E | F pour démontrer un énoncé quelconque q, on produit deux démonstrations de q, l'une utilisant l'hypothèse E, l'autre utilisant l'hypothèse F, de façon à couvrir tous les cas possibles. En résumé, cette définition se lit:
?q:O (quel que soit l'énoncé à démontrer)
(E => q) (si je sais le démontrer en utilisant E)
=> (F => q) (et si je sais aussi le démontrer en utilisant F)
=> q (alors, je l'ai démontré)
Vous voyez que cette définition de la disjonction est une définition opérationnelle. Elle n'essaye pas de définir une sémantique pour la disjonction autrement qu'en disant comment on s'en sert. On conçoit aisément qu'une telle définition est d'une portée plus générale qu'une table de vérité booléenne. Je dirai qu'elle est ``béhavioriste'', car elle définit la disjonction par son comportement dans les démonstrations.
Ce qui apparaît donc clairement est que la propriété exprimée par cette définition est une propriété obligatoire (requise) de la disjonction. Ce qui est moins évident est que cette propriété suffise à caractériser la disjonction. Je ne vais pas m'étendre sur cette question, qui a une réponse affirmative très simple en théorie des catégories, consistant à utiliser le fait qu'un foncteur ne peut pas avoir plus d'un adjoint à gauche à isomorphisme canonique près. Malheureusement, ce fil ne permet pas développer de tels arguments. Les personnes intéressées pourront consulter un ouvrage de Théorie des Topos.
Une confirmation du fait que la disjonction est bien caractérisée est l'exercice que j'avais proposé dans le post #60, à savoir de trouver deux fonctions de types respectifs:
W(E) -> W(E | F) et W(F) -> W(E | F)
montrant que pour prouver E | F il suffit de prouver soit E, soit F. L'exercice a été résolu par alex_pi dans le post #62 (voir également la petite correction apportée dans le post ).
En ce qui concerne la question 10 (conjonction), alex_pi a proposé deux solutions, dont j'ai affirmé qu'elles sont équivalentes. C'est vrai si F ne dépend pas d'un témoin de E, sinon ce n'est pas équivalent et c'est la deuxième définition (celle qui autorise la dépendance) qui est la bonne. Je vais y revenir plus loin pour les détails.
La question 11 (quantificateur existentiel) a une solution similaire à la question 9. Je vous laisse chercher.
Je vais revenir dans un prochain post sur la question de la dépendance en donnant la solution de la question 8.
Donc voici une solution pour la question 8, qui était de nature moins formelle, donc peut-être plus troublante. Je commence par la langue naturelle.
Imaginons que nous soyons dans un contexte (lors d'une conversation) où on parle d'une personne bien définie. Cette personne sera représentée par le pronom personnel ``il''. Que pensez-vous de phrase suivante ?
Il doit en prendre soin.
Elle n'est pas claire n'est-ce pas ? Cela est dû au fait qu'on ne sait pas ce que représente le pronom adverbial ``en''.
En français, l'implication peut s'exprimer par la formule ``si ..., alors ...''. Q'en est-il de la phrase suivante ?
S'il a un chien, alors il doit en prendre soin.
Cette phrase est parfaitement claire, sachant qu'on sait qui est ``il''. En fait, le pronom adverbial ``en'' devient un terme bien formé (correct aussi bien du point de vue de la syntaxe que du point de vue de la sémantique) dans la portée de l'affirmation ``il a un chien'', puisqu'alors ``en'' désigne le chien. Autrement-dit, la deuxième partie de la phrase n'a de sens que si la première partie est vraie, autrement-dit si elle a un témoin (au sens de notre langage formel). Le pronom adverbial ``en'' contient donc une occurrence libre implicite d'une variable représentant un témoin de la première affirmation.
Voici maintenant un exemple similaire en mathématiques élémentaires. Nous sommes dans un contexte où on parle d'une partie A de l'ensemble des nombres réels, qui est supposée non vide. Par ailleurs, la borne supérieure d'une telle partie (si elle existe) est notée sup(A). Que pensez-vous de l'énoncé suivant ?
sup(A) > 0
Il est mal formé, n'est-ce pas ? C'est dû au fait qu'on a aucune garantie que la borne supérieure existe. Par contre, l'énoncé suivant est bien formé (je ne dis pas qu'il est vrai):
(A majoré) => sup(A) > 0
C'est dû au fait que d'après l'axiome de la borme supérieure (qui fait partie d'une définition possible de l'ensemble des réels) toute partie non vide et majorée de R a une borne supérieure.
Autrement-dit, le terme sup(A) contient quand il est bien formé, une occurrence libre implicite d'une variable représentant un témoin de l'énoncé A majoré (de même d'ailleurs qu'une occurrence libre implicite d'une variable représentant un témoin de A non vide).
Une question est de savoir pourquoi les occurrences des variables de témoins sont implicites dans la langue naturelle et dans les mathématiques. C'est une conséquence immédiate du fait (que j'ai déjà signalé) qu'un type de témoin ne peut pas avoir plus d'un seul élément. On peut exprimer cela par le slogan Si vous êtes tout seul sur une île déserte, avoir un nom ne vous sert à rien. Ce principe est appelé ``indiscernabilité des preuves'' ou ``proof-irrelevance'', mais pour ma part, je préfère l'appeler ``unicité du témoin''.
Les systèmes formels ne respectent pas tous ce principe, mais les quelques arguments ci--dessus devraient vous convaincre facilement qu'il est patent dans la langue naturelle et dans les mathématiques. En matière de démonstration, l'important est de prouver, peu importe comment.
Je ne me sens pas vraiment en mesure de combler la désaffection d'alex_pi.
Néanmoins, pour la question 11 je risque la proposition suivante:
?F:O ?w:W(?x:T E=>F) F
Qui dit qu'une preuve de F peut se construire par le fait que E implique F pour toutes les valeurs x de T.
Excellent. C'est exactement la bonne réponse. L'explication est un peu succincte, mais l'idée est bonne.Citation:
Envoyé par SpiceGuid
On peut réécrire cette formule comme suit (c'est la même au noms des variables près):
?q:O ((?x:T (E => q)) => q)
Elle s'analyse de la façon suivante (à rapprocher de la même analyse concernant la disjonction):
?q:O (quelque soit l'énoncé à démontrer)
(?x:T (E => q) (si je sais le prouver en déclarant x dans T et en supposant E)
=> q (alors je l'ai démontré)
C'est effectivement comme cela qu'on utilise une hypothèse d'existence de la forme !x:T E: on déclare x tel que E, et on prouve ce qu'on a à prouver.
On peut démontrer l'analogue de ce qui a été fait pour la disjonction (à savoir l'existence de deux fonctions de types W(E) -> W(E | F) et W(F) -> W(E | F)), en exhibant, étant donné un terme a de type T, et un témoin t de E[ a/x ], un terme de type W(!x:T E), ce qui confirmera que pour prouver !x:T E, il suffit d'exhiber un a dans T qui satisfait E. Je vous laisse le vérifier vous même.
Petit résumé des questions (ou parties de questions) qui ne sont pas résolues jusqu'ici:
- La question 9 demandait si la disjonction pouvait être dépendante. En fait, il s'agit d'expliquer pourquoi elle ne peut pas l'être.
- La question 10 demandait si la conjonction pouvait être dépendante. Comme je l'ai laissé entendre, la réponse est oui. Il s'agit seulement d'expliquer pourquoi c'est la deuxième proposition d'alex_pi (W(?q:O (E => (F => q)) => q)) qui est la bonne et non pas la première (W(?q:O ((E => q) | (F => q)) => q)).
- Dans le post précédent (quantificateur existentiel) j'ai demandé de produire un terme de type W(!x:T E), pour tout terme a de type T, et tout témoin t de E[ a/x ]. Le terme en question sera noté <a,t> et appelé une ``paire de Heyting''.
Vous savez que les quantificateurs universels et existentiels ne peuvent pas être permutés sans précautions. Le seul résultat général est le suivant:
Question 12. Soient T et U deux types. Soit E un énoncé pouvant contenir des occurrences libres de x (de type T) et y (de type U). Ecrivez un terme de type:
W((!x:T ?y:U E) => (?y:U !x:T E))
De même qu'on a introduit dans le post #16 la notion de type fonctionnel dépendant, on aurait pu introduire celle de produit dépendant. Etant donné un type T et un type U dépendant de T, on noterait leur produit dépendant comme ceci:
(x:T)*U
Bien entendu, il faudrait aussi préciser le constructeur, le destructeur et les règles de calcul beta et eta. Dans ces conditions, on aurait pu définir le quantificateur existentiel en imposant la règle:
W(!x:T E) = (x:T)*W(E)
qu'on pourrait qualifier de ``sémantique de Heyting pour le quantificateur existentiel''.
Question 13. La définition proposée ci-dessus pour le quantificateur existentiel ne peut pas être retenue dans ce système, car elle est incompatible avec l'un de ses principes fondamentaux. Voyez-vous lequel et pourquoi ?
Pour G c'est clair, c'est une variable de type O.Citation:
Envoyé par DrTopos
Quant à E et F ils n'appartiennent pas au type O mais à un type termes de type O qui est un type syntaxique, il fait partie de votre discours mais pas de votre 'langage imaginaire'.
Ensuite vous demandez => ~ et d'autres, d'autres quoi ?
D'autres macros des termes de type O vers les termes de type O, votre 'langage imaginaire' n'est pas le sujet, il est l'objet. Ou alors votre langage possède des propriétés réflexives que vous nous avez cachées.
Il n'est pas nécessaire de parler de ``type syntaxique'' (qui serait une sorte de méta-type). J'ai défini ce que sont les expressions du langage et j'ai bien pris soin de faire la distinction entre l'expression (le ``signifiant'') et ce qu'elle représente (le ``signifié''). Bien entendu tout signifiant a un type, qui est dailleurs le même que celui du signifié qu'elle représente. Je rappelle le vocabulaire de cette correspondance signifiant ---> signifié:Citation:
Envoyé par SpiceGuid
- terme ---> donnée
- énoncé ---> valeur de vérité
- preuve ---> témoin
la paire terme ---> donnée étant le cas générique, les autres des cas particuliers.
Pour en revenir à l'exemple que tu cites, G, E et F sont de même nature, ce sont des énoncés et ils représentent donc des valeurs de vérité. Je te fais remarquer qu'une variable n'est pas une donnée mais un terme. En l'occurrence, G n'est pas une valeur de vérité, mais un énoncé. Ce qui fait la différence est seulement que E et F étaient déclarés dans le texte de la question, et n'avaient donc pas besoin d'être redéclarés, alors que G ne l'était pas et avait donc besoin d'être déclaré dans la formule proposée. Evidemment on aurait pu se contenter d'écrire G |-> au lieu de (G:O) |->, puisque le type de G pouvait être déterminé par le contexte. Mais cela est une autre question.
On pourrait éventuellement parler de méta-type et faire la distinction entre le ``méta-type des énoncés'' et le ``type des valeurs de vérité''. Mais en l'occurrence cela ne sert à rien dans les questions posées. Cela serait par contre utile si on voulait enrichir le système avec un système des macros à la Lisp, de façon à pouvoir considérer les expressions comme des données et les manipuler comme telles, puis passer du signifiant au signifié par ``eval''. C'est ce qu'il convient de faire dans un langage réel, mais pas dans ce jeu qui doit rester simple.
D'ailleurs, le jeu lui-même n'est qu'une manipulation au niveau des termes (donc purement syntaxique). Tout le discours sur le sens (intuitif ou non) de ces termes n'est là que pour aider l'intuition. Il ne joue aucun rôle dans le jeu lui-même. En principe, on aurait pu omettre complètement les questions de sens, mais alors les motivations des participants auraient été totalement inexistantes.
Je ne vois pas cela comme des macros, mais comme des définitions (globales en l'occurrence), ce qui n'est pas la même chose.Citation:
Envoyé par SpiceGuid
J'aurai pu donner d'emblée des définitions pour tous les connecteurs logiques et ensuite demander de prouver formellement quelques unes de leurs propriétés. Toutefois, comme ces notions sont familières, j'ai trouvé plus pédagogique et plus progressif de demander d'en donner une ``définition raisonnable'', même s'il ne s'agit pas là d'une question très précise. D'ailleurs, alex_pi et toi avez trouvé la plupart des réponses à ce genre de question, ce qui vous a clairement obligé à réfléchir sur la façon dont on se sert des connecteurs dans les démonstrations plutôt que sur leur sens intuitif en termes de ``vrai'' et ``faux''. Jai donc atteint le but que je recherchais. Avec le quantificateur existentiel, on est au bout de ce genre de question.
Non, il n'y a pas de propriétés reflexives cachées (c'est à dire si je comprends bien ce que tu entends par là, pas de système de macros). Je ne vois pas ce que tu veux dire par la phrase ``votre 'langage imaginaire' n'est pas le sujet, il est l'objet''. Encore une fois, ceci n'est qu'un jeu (ou une théorie axiomatique, ce qui est la même chose). Je donne les règles du jeu, et chaque question consiste à faire une sorte de réussite dans le cadre de ce jeu, sauf bien sûr les quelques questions qui demandaient de proposer des définitions de connecteurs logiques, qu'on peut considérer comme des demandes de propositions pour de nouvelles règles à ajouter au jeu.Citation:
Envoyé par SpiceGuid
Les programmeurs sont habitués à des types qui ont toujours au moins un élément, et même en général beaucoup (la plupart des types usuels ont même une valeur par défaut). Avec les types W(E), on est dans une situation différente. Beaucoup d'entre eux ne contiennent rien, et il n'y a aucun terme de ces types là. C'est le cas chaque fois que E n'est pas démontrable. On est donc dans une situation en quelque sorte ``duale'' de la situation usuelle, où les types ont au moins un élément. Ici, ils en ont au plus un. D'ailleurs, il y a une chose qui etonnera peut-être les programmeurs, qui est que le type O, qui contient une infinité de données distinctes (tant qu'on n'introduit pas l'axiome du choix) s'implémente sur zero bits, alors que les types de témoins qui ne peuvent pas contenir plus d'une donnée, s'implémentent en utilisant des fermetures, comme les types fonctionnels (c'est une conséquence de l'existence d'un destructeur pour les types de témoin, que j'ai déjà évoqué, mais pas encore introduit). Tout cela indique bien qu'il y a une différence entre signifiants et signifiés, et qu'on ne pourrait pas concevoir un tel système sans une vision sémantique. Cette vision est fournie bien sûr par l'interprétation dans un topos, sujet trop technique pour que je l'aborde ici (du moins dans toute sa généralité).
Le fait qu'il n'y ait souvent aucun terme d'un type donné W(E) est déroutant sans doute, mais cela justifie les questions du genre ``trouvez un terme de type W(E)'', pour un certain E (qui serait triviale pour un type usuel). Je pourrais poser une telle question sous la forme ``prouvez E''. Si je prends la précaution de dire ``trouvez un terme...'' c'est pour faire sentir aux programmeurs que démontrer un énoncé mathématique n'est rien d'autre que de la programmation, et est donc une activité qui leur est familière. En fait, j'essaye depuis le début de ce quizz de faire comprendre aux programmeurs que les mathématiques sont une activité qui fait partie de leur domaine. Il y a beaucoup de programmeurs qui disent ne rien comprendre aux démonstrations (ou plus simplement en ont peur), mais qui comprennent très bien comment programmer en style fonctionnel. Je dis qu'il y a là une contradiction, puisque prouver c'est programmer. J'essaye de les réconcilier avec les maths en les présentant d'une façon qui devrait leur plaire (tous n'en ont pas besoin, évidemment).
----------------------------------------------
Je refais une petite mise au point sur la façon dont il faut voir ce quizz:
- C'est avant tout un jeu, et il est destiné à vous faire plaisir (tout en étant éventuellement instructif). Prenez-le comme tel.
- Ce n'est pas précisément le langage pour lequel je suis en train de réaliser un compilateur, mais seulement une présentation de quelques-uns des mécanismes internes de ce compilateur. Dans le langage réel, on se contente d'écrire des ``preuves informelles'' à l'aide d'une dizaine de sortes de phrases en langue naturelle, et c'est un algorithme de recherche de preuves qui trouve les termes des types W(E) (en demandant des compléments de preuves quand il ne trouve pas).
J'ai dans ma besace encore plusieurs dizaines de questions (et même plus éventuellement). Je suis évidemment un peu déçu (et aussi etonné) par le fait que certains programmeurs fonctionnels dont j'ai eu l'occasion d'apprécier la sagacité dans d'autres fils ne participent pas. Pour ma part, j'aime beaucoup m'occuper de ce quizz, la pédagogie étant chez moi une vocation, mais bien sûr, je ne vais pas le continuer tout seul.
Enfin, on a tout le temps. Il suffit peut être de faire une petite pose. Encore une fois, ce n'est qu'un jeu. Faites vous plaisir.
Question 11.
La paire de Heyting <a,t> :
Code:
2
3
4
5
Non. Cela ne va pas pour plusieurs raisons.Citation:
Envoyé par SpiceGuid
- La paire de Heyting <a,t> doit être de type W(!x:T E). Les deux premières déclarations a:T et t:W(E) sont donc de trop.
- t est donné de type W(E[ a/x ]), ce qui n'est pas la même chose que d'être de type W(E).
- Après avoir été déclaré, a n'est pas utilisé. C'est sans doute dû au fait que le terme qui commence à la déclaration q:O ne suit pas la définition du quantificateur existentiel. Il manque la déclaration correspondant au ?x:T.
Paire de Heyting. Etant donné a de type T et t de type W(E[ a/x ]). Si j'ai bien compris les types dépendant :
q:O |-> pq:W(?x:T (E => q)) |-> pq a t
devrait fonctionner
Question 12. Les types T et U sont supposés non dépendants (ça ne voudrait rien dire de permuter x et y
[B]p:W(!x:T ?y:U E) |-> y:U |-> q:O |-> p':(x:T -> pE:W(E) -> W(q))
|-> p q (x1 |-> p1 |-> p' x1 (p1 y))
Les notation deviennent un brin pénibles en fait...
Et je crois qu'en fait il faudrait développer un peu plus ce que sont les types dépendants.
C'est exact. Il suffit bien sûr de vérifier que c'est bien typé. La paire de Heyting <a,t> doit être de type W(!x:T E), c'est à dire de type (q:O) -> (p:W(?x:T (E => q)) -> W(q). On peut donc commencer en déclarant q et p:Citation:
Envoyé par alex_pi
(q:0) |-> (p:W(?x:T (E => q)) |-> s
et s devra être de type W(q). Pour produire s, on remaque que p est de type (x:T) -> (r:W(E)) -> W(q). Par conséquent p(a) est de type (r:W(E[ a/x ]) -> W(q), car, ne l'oublions pas, la 3ème règle (post ) pour les types fonctionnels dépendants est la suivante:
(et non pas de type U)Citation:
Si f est un terme de type (x:T) -> U, et a un terme de type T, le terme f(a) est de type U[ a/x ].
Dès lors, la fonction p(a) peut être appliquée à t qui est de type W(E[ a/x ]), ce qui fait que p(a)(t) est de type W(q). On peut donc poser la définition suivante:
<a,t> := (q:0) |-> (p:W(?x:T (E => q)) |-> p(a)(t)
Rappelons que le sens intuitif de la paire de Heyting <a,t> est qu'elle est une preuve d'existence par exhibition. Si on a un a dans T et qu'il satisfait E (c'est à dire qu'on sait prouver E[ a/x ]), alors on a prouvé l'énoncé d'existence !x:T E.
Précisément, les types T et U ne peuvent pas dépendre de x ni de y, mais ils peuvent dépendre d'autres variables.Citation:
Envoyé par alex_pi
La première partie de ce que tu proposes ne pose pas de problème, puisqu'elle ne fait que suivre les définitions des quantificateurs. Je me contente donc d'analyser le terme p q (x1 |-> p1 |-> p' x1 (p1 y)).
p étant de type W(!x:T ?y:U E), c'est à dire de type (q:0) -> (r:W(?x:T ((?y:U E) => q))) -> W(q), et q étant de type O, on voit que p q est de type (r:W(?x:T ((?y:U E) => q))) -> W(q). Il suffit donc pour obtenir un terme de type W(q) d'appliquer la fonction p q à un terme de type:
(x:T) -> (v:(y:U) -> W(E)) -> W(q)
Tu déclares donc x1 dans T, et p1 dans (y:U) -> W(E), ce qui fait que p1 y est de type W(E) et que p' x1 est de type W(E) -> W(q). Il en résulte que p' x1 (p1 y) est de type W(q), et donc que ta réponse est bonne.
Ceci dit, tu aurais dû mettre toi même toutes ces explications. Tu auras aussi remarqué que le fait de ne pas typer explicitement les arguments formels des fonctions (x1 et p1 par exemple) rend l'analyse du typage d'une formule extrêmement difficile.
C'est normal, car nous sommes ici dans un jeu qui ne peut pas être le langage utilisateur d'un système raisonnablement ergonomique. Tous ces termes pleins de flèches sont à construire par le compilateur lui-même à partir des indications (preuves informelles) données par l'utilisateur. On en reparlera plus loin. Toutefois, il faut utiliser autant que possible les abbréviations (définitions) introduites dans les posts précédents. Elles sont là pour simplifier l'écriture.Citation:
Envoyé par alex_pi
Je crois qu'il faut surtout bien relire les cinq règles du post #16, qui disent tout ce qu'il y a à savoir.Citation:
Envoyé par alex_pi
Une remarque: A cause des notations utilisées, on découvre parfois des smileys dans les formules. Quand vous écrivez un message, vous avez la possibilité de désactiver les smileys (coche en dessous de la zone de saisie).
Rappel pratique (pour ceux qui ne le savent pas): Pour mettre une formule en gras, marquez la (avec les touches flèchées par exemple) et cliquez sur le bouton G en haut à gauche de la zone de saisie.
Question 14. Soient T et U deux types ne dépendant pas des variables x et y, et E un énoncé pouvant dépendre de x et y. Le terme suivant est-il bien typé, et quel est son type ?
(p:W(!x:T ?y:U E)) |-> (y:U) |-> p(!x:T E)((x:T) |-> (r:(y:U) -> W(E)) |-> <x,r(y)>)
S'il y a besoin de développer alors je dirais quelque chose comme:Citation:
Envoyé par DrTopos
Quels termes sont dépendants ? (des énoncés et des témoins)
De quoi sont-ils dépendants ? (d'une variable x de type énoncé ou de type témoin)
Que représente (x:T) |-> E ? (une classe d'énoncés ou une classe de témoins, on peut produire un nouvel énoncé ou un nouveau témoin en instanciant cette classe, c'est-à-dire en appliquant a à ce terme, le résultat est un énoncé O[a/x] ou un témoin W[a/x] dans lequel x est une constante qui vaut a)
Au passage, dans cette interprétation "orientée objet", la béta-équivalence est devenue la béta-réduction, mais cela ne dérange personne (si l'égalité n'est pas orientée alors pourquoi devrais-je alimenter mon ordinateur portable?).
Juste pour info, je me suis ammusé, pour jouer un peu avec Coq, à montrer ce qu'on a fait ici en Coq (j'en suis à la question 12, je modifierai ce post quand j'avancerai)
J'avais tenté de faire quelque chose de plus haut niveau (higher-order abstract syntax), mais disons le clairement, je n'ai pas encore le niveau en Coq (donnez moi 2 ou 3 mois :-p). Donc le pour tout est codé par "forall" directement (qui est un produit dépendant, ce qui pose sans doute problème pour la question 13), il n'y pas pas de W (en Coq, une proposition et le type de ses preuves, c'est exactement la même chose.), et je ne suis pas très satisfait par mon encodage de l'existentiel.Code:
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134(* Faux ! *) Definition Faux := forall q : Prop, q. (* Vrai *) Definition Vrai := forall q : Prop, forall x : q, q. (* une preuve de Vrai *) Lemma Vrai_est_vrai : Vrai. Proof. unfold Vrai. intros. apply x. Qed. (* définition de la négation *) Definition Neg (E : Prop) := forall q : Prop, forall x : E, q. (* équivalence entre la négation Neg et celle de Coq *) Lemma neg_equiv_not : forall E : Prop, Neg E <-> ~E. Proof. intros. unfold not. unfold Neg. split. intros. apply H. apply H0. intros. assert False. apply H. apply x. contradiction. Qed. (* définition de l'implication *) Definition Impl (E F : Prop) := forall x : E, F. (* preuve de son équivalence avec l'implication de Coq *) Lemma Impl_equiv_fleche : forall E F : Prop, Impl E F <-> (E -> F). Proof. intros. unfold Impl. split; auto. Qed. (* commutation des quantificateurs universels *) Lemma commut_pour_tout : forall E : Prop, (forall x : E, forall q : Prop, q) <-> (forall q : Prop, forall x : E, q). Proof. intros. split;intros; apply H; apply x. Qed. (* définition de la disjonction *) Definition Disj (E F : Prop) := forall G : Prop, Impl (Impl E G) (Impl (Impl F G) G). (* preuve de son équivalence avec la disjonction de Coq *) Lemma or_equiv_disjonct : forall E F : Prop, E\/ F <-> Disj E F. Proof. intros. unfold Disj; unfold Impl. intros. split;intros. destruct H. apply x; apply H. apply x0; apply H. apply (H (E \/ F)); auto. Qed. (* définition de la conjonction *) Definition Conj (E F : Prop) := forall G : Prop, Impl (Impl E (Impl F G)) G. Lemma and_equiv_conjonc : forall E F : Prop, E /\F <-> Conj E F. Proof. intros. unfold Conj. unfold Impl. split. intros. destruct H. auto. intros. split. apply (H E). intros. auto. apply (H F). intros. auto. Qed. (* définition alternative de la conjontion *) Definition Autre_conj (E F : Prop) := forall G : Prop, Impl (Disj (Impl E G) (Impl F G)) G. (* preuve d'équivalence des deux versions *) Lemma equiv_def_conj : forall E F : Prop, Conj E F <-> Autre_conj E F. Proof. intros. unfold Conj. unfold Autre_conj. unfold Disj. unfold Impl. split. intros. apply (H G). intros. apply (x G); intro Hp; auto. intros. apply x. apply (H E). intros. apply x0. auto. apply (H F). intros. apply x1. auto. Qed. (* définition de l'existance. * Pour encoder le fait que E puisse contenir des occurences libres * de x, on en fait une fonction de x *) Definition Existe (T:Type) (E : T -> Prop) : Prop := forall q : Prop, Impl (forall x : T, Impl (E x) q) q. (* classiquement, preuve de l'équivalence avec la version Coq *) Lemma existe_equiv_exists : forall (T : Type) (E : T -> Prop), Existe T E <-> exists x : T, E x. Proof. intros. unfold Existe. unfold Impl. split. intros. apply (H (exists x : T, E x)). intros. exists x. apply x0. intros. destruct H. apply (x x0). apply H. Qed. (* prouvons la permutation du quantificateur existentiel et universel (dans un sens seulement, évidement !!) *) Lemma swap_existe_pourtout : forall (T U : Type) (E : T -> U -> Prop), (Existe T (fun x => forall y : U, E x y)) -> (forall y : U, Existe T (fun x => E x y)). Proof. unfold Existe. unfold Impl. intros. apply (H q). intros. apply (x x0). apply (x1 y). Qed.
Bravo.
Tout cela est quand même très difficile, quand tu rencontreras une grosse difficulté tu ne pourras pas vraiment savoir si ce qui fait obstacle c'est ton niveau en COQ ou bien le fait que les deux systèmes sont différents.
Merci :-)Citation:
Envoyé par SpiceGuid
Je te rassure, je pratique suffisement les maths pour savoir que si je n'arrive pas à démontrer quelque chose, je ne dois pas en déduire que c'est faux :-)Citation:
Envoyé par SpiceGuid
Mais j'aimerais voir à quel moment je commence à vraiment coincer dans l'encodage de cette théorie dans le calcul inductif des constructions.