[Quizz] Fonctions et démonstrations.

[DrTopos]

Merci pour ta réponse. En cherchant dans le manuel de référence Coq, j'ai fini par trouver la réponse à ma question:

Envoyé par Manuel de Référence Coq

Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

C'est surtout la dernière ligne: because proofs can be eliminated only to build proofs évidemment qui indique clairement qu'on n'a pas de première projection pour les paires de Heyting. Dans ces conditions évidemment, proof-irrelevance ne pose pas de problème.

J'ai regardé la FAQ Coq section 5.2 (Axiomes). Les axiomes énumérés ne créent effectivement aucune contradiction en présence des seuls principes intuitionnistes. Tous ces axiomes seront d'ailleurs imposés dans le système que j'ai en tête, sauf le tiers exclu et l'axiome du choix (functional axiom of choice dans la FAQ Coq), lequel entraine le tiers exclu par Diaconescu, ce qui fait que le tiers exclu ne sera pas primitif. Donc en fait, la seule option sera de savoir si on utilise l'axiome du choix ou non, c'est à dire si on fait des mathématiques classiques ou intuitionnistes. L'axiome du choix peut éventuellement s'éliminer lors de l'optimisation des preuves. On pourra donc faire des mathématiques intuitionnistes en utilisant l'axiome du choix. Il suffira de vérifier que le compilateur parvient à en élimliner toutes les instances.

Coq a donc abandonné la philosophie Martin-Löf (à quelle époque ?), puisque dans le système de Martin-Löf on a la première projection des paires de Heyting. C'est d'ailleurs cela qui fait que l'axiome du choix peut être prouvé (constructivement) en Martin-Löf, mais que bien sûr Diaconescu ne peut pas l'être. En effet, s'il l'était, le tiers exclu serait constructif.

Mon approche est évidemment différente des gens qui font de la théorie des types, puisque l'interprétation dans les topos sur laquelle je me base impose d'office proof-irrelevance. C'est une approche plus sémantique. Mais évidemment, elle ne donne aucune information sur la façon de calculer. Pour cela, il faut revenir à la théorie de la démonstration (normalisation forte).

[DrTopos]

Je viens de taper une première mouture du résumé du quizz. Les suggestions et corrections sont bienvenues.

[Steki-kun]

Au départ le CoC (Calcul des Constructions) c'est en gros du lambda-calcul typé d'ordre supérieur où les types sont des valeurs de première classe. Par rapport à MartinLöf la différence c'est en particulier l'imprédicativité de Prop, non ? Il me semble que dans la théorie de Per Martin-Löf, un truc quantifié sur un type Uo sera dnas un type plus gros U1, etc.
En tout cas, en CoC, avant l'ajout des inductifs, il fallait donc définir les définir par leur schéma d'induction directement, ce qui est exactement le codage que l'on a suivi sur ce Quizz pour l'instant (et c'est la raison pour laquelle il me paraît si familier ).

[kaukau]

Je viens de taper une première mouture du résumé du quizz. Les suggestions et corrections sont bienvenues.

Superbe!

[Ekinoks]

Envoyé par DrTopos

Je viens de taper une première mouture du résumé du quizz. Les suggestions et corrections sont bienvenues.

Salut,

L'idée d'avoir un résumé du quizz est une très bonne idée =)

Mais j'aimerais savoir, quel niveau en maths il est nécessaire d'avoir pour comprend tout ca ?
Car j'ai beau passer 20minute par page, je comprend pas grand chose :'(

[DrTopos]

Envoyé par Ekinoks

Mais j'aimerais savoir, quel niveau en maths il est nécessaire d'avoir pour comprend tout ca ?
Car j'ai beau passer 20minute par page, je comprend pas grand chose :'(

Ca c'est embêtant. J'avais l'impression que ce serait assez facile à lire, même pour quelqu'un qui n'est pas habitué. Pourrais-tu me dire ce qui coince pour que j'essaye d'améliorer le texte.

[Ekinoks]

Envoyé par DrTopos

Ca c'est embêtant. J'avais l'impression que ce serait assez facile à lire, même pour quelqu'un qui n'est pas habitué. Pourrais-tu me dire ce qui coince pour que j'essaye d'améliorer le texte.

Ha... j'aurais normalement du été capable de comprendre ces notions ? Ca viens peu être de moi...

Comme tu me le demande, je vais essayer d'expliquer pour quoi j'ai du mal a assimiler ce document, mais ça viens peu être de mon mode de fonctionnement qui est différant de la moyenne


Donc mes remarques sont faite par rapport a mes méthodes d'apprentissage.


Donc, pour moi, le documents est trop "parfait", tout est définie de manière trop formelle sans aucune vulgarisation.
Je sais que les professeurs de maths n'aiment pas la vulgarisation, mais c'est en commençant par une première approche approximative et intuitive que cela me permet de mieux cerner le problème.

La deuxième remarque que je peu faire, c'est que tout les notions sont données trop vite. Bon, encore une foi c'est un mode de fonctionnement personnel, mais pour que j'arrive a comprendre "réellement" des choses, il faut que je me les appropries. Et pour me les approprier il faut que les notions soit donnée sur des exemples pour que je sache le "pourquoi" elles existent, et le pour quoi on a choisis cette notion et pas une autre.



J'ai bien insisté sur le fait que ces remarques sont faite par rapport a mon mode de fonctionnement. Donc si pour moi, ce genre de présentation ne me correspond pas, elle va corresponde je suis sur a beaucoup d'autre personne.
(La preuve c'est que la plus par des cours de maths de la fac sont fait de cette manière et cela semble gêner personne a part moi, qui suis obligé de chercher d'autre source d'information )

[DrTopos]

Envoyé par Ekinoks

tout est définie de manière trop formelle sans aucune vulgarisation.

C'est vrai, mais c'était d'une certaine façon voulu. Après tout ce n'est qu'un résumé et je voulais qu'il reste court. Donc, je n'y ai mis que le strict nécessaire.

Envoyé par Ekinoks

J'ai bien insisté sur le fait que ces remarques sont faite par rapport a mon mode de fonctionnement. Donc si pour moi, ce genre de présentation ne me correspond pas, elle va corresponde je suis sur a beaucoup d'autre personne.

En fait, presque tout le monde fonctionne comme toi (y compris moi-même). Encore une fois, ce n'est qu'un résumé, un ``quick reference card'' si on veut. Mais plus tard, je l'étofferai peut-être pour en faire un document plus pédagogique.

En théorie, c'est très simple. Il y a un ensemble de règles, et tout le jeu consiste à les appliquer sans se tromper. Mais bien sûr, notre cerveau est fait de telle façon, qu'il a du mal à appliquer les règles si elles ne correspondent pas à une intuition. On est tout le contraire d'un ordinateur. Peut-être faut-il revenir un peu à la lecture du fil lui-même, où sont données pas mal d'indications de nature intuitive.

[Ekinoks]

Envoyé par DrTopos

C'est vrai, mais c'était d'une certaine façon voulu. Après tout ce n'est qu'un résumé et je voulais qu'il reste court. Donc, je n'y ai mis que le strict nécessaire.

Ha ok, ce document s'adressent plus a des personnes qui on déjà suivit un peu le fils de la discutions et qui veule se remémorer ce qui a déjà été dit durant ces 8 pages alors...

Envoyé par DrTopos

En fait, presque tout le monde fonctionne comme toi (y compris moi-même).

Ha, ca fait plaisir a savoir ca, j'ai toujours crue que j'était un cas particulié ^^

Envoyé par DrTopos

Peut-être faut-il revenir un peu à la lecture du fil lui-même, où sont données pas mal d'indications de nature intuitive.

Ok, c'est ce que je vais essayer de faire, merci.

[Steki-kun]

Bon je vais reprendre mes réponses des questions 15 à 19 en détaillant le pourquoi du comment, histoire que ceux d'entre vous qui essayent de suivre puissent comprendre de quoi il retourne

Question 15:
La question 15 était de trouver une preuve de ?q:O.q => ~~q. Voilà le terme que je propose :

Envoyé par Steki-kun

(q:O) |-> ((urd : W(q)) |-> (abs : W(~q)) |-> abs urd).

Comme expliqué dans le post #94, il s'agit en fait de trouver une preuve de ?q:O.q => ~q => Faux. Ce terme prend donc d'abord une proposition q, une preuve de q et une preuve de ~q (appelés resp. urd et abs). Puisqu'une preuve de ~q n'est autre qu'une preuve de q=>Faux, on peut obtenir la preuve de Faux désirée en appliquant simplement notre preuve de q=>Faux à celle de q, en d'autres termes en écrivant abs urd.

Question 16:
La question 16 était de trouver une preuve de ?q:O.~~~q => ~q. Voilà le terme que je propose :

Envoyé par Steki-kun

(q:O) |-> (abs : W(~~~q)) |-> (urd : W(q)) |-> abs (Q15 q urd).
où Q15 correspond au terme de la question précédente.

Ici, pour toute proposition q, c'est une preuve de ~~~q => ~q que l'on cherche, autrement dit, une preuve de ~~~q => q => Faux, ou encore de façon plus détaillée, une preuve de (~~q => Faux) => q => Faux.
On suppose donc une preuve de (~~q => Faux), appelée abs, ainsi qu'une preuve de q, appelée urd. Il nous reste à obtenir une preuve de Faux. Pour faire ça, on a bien envie d'appliquer abs à une preuve de ~~q puisque abs prend une preuve de ~~q et retourne une preuve de Faux. Or, on vient de montrer dans la question 15, que dès qu'on a q, on sait prouver ~~q ! On peut donc trouver une preuve de ~~q en appliquant le terme de la question 15 : (Q15 q urd).
En appliquant à son tour abs à ce terme, on obtient bien une preuve de Faux.

Les autres questions suivront tout bientôt.

[DrTopos]

Je vais laisser Steki-kun détailler son post #92 afin que tous puissent vérifier les solutions données pour les questions 15 à 19. Je me contente de quelques commentaires.

L'énoncé ?q:O (q | ~q) est le ``principe du tiers exclu'' énoncé par Aristote (pas exactement sous cette forme) il y a de nombreux siècles. Il dit en gros qu'un énoncé ne peut être que vrai ou faux. Le fait qu'il pose un problème de constructivité n'est pas évident pour tout le monde (y compris parmi les matheux). Ce principe n'a été remis en question que vers 1912 par Brouwer qui l'a appelé par dérision le ``principe de l'omniscience''. L'argument de Brouwer est en gros (à une époque où Andrew Wiles n'était pas né): ``Je peux démontrer Fermat | ~Fermat par le tiers exclu, mais je n'arrive pas à démontrer Fermat ni à démontrer ~Fermat''. On comprend aisément sa conclusion ironique.

Un autre axiome ``classique'' est celui de la double négation: ?q:O (~~q => q). Il permet de raisonner par l'absurde. En effet, raisonner par l'absurde consiste à démontrer ~~E quand on doit démontrer E. Comme ~~E n'est autre que ~E => faux, on suppose ~E et on démontre faux, c'est à dire qu'on cherche une contradiction. On ne peut bien sûr en déduire E qu'à l'aide de l'axiome de la double négation. Par contraste, démontrer ~E en supposant E et en démontrant faux n'est pas (contrairement à ce que croient beaucoup de gens) un raisonnement par l'absurde, mais juste une utilisation de la définition de la négation.

L'objet de la question 17 était de montrer que le deux principes ci-dessus, tiers exclu et double négation, sont constructivement équivalents. Autrement-dit, admettre l'un revient à admettre l'autre. Quand on le fait, on fait des mathématiques dites ``classiques''. J'ai expliqué dans le post #56 pourquoi, en présence d'ensembles ou de types infinis, le tiers exclu est incompatible avec le constructivisme. Il est possible de démontrer (par plusieurs méthodes différentes) que ces deux énoncés sont indécidables dans les systèmes constructifs (dont bien sûr, celui qui est présenté ici).

La question 18 montrait qu'en mathématiques constructives on conserve des versions faibles des règles de de Morgan. En fait, j'ai commis un oubli avec cette question qui aurait pu être posée comme suit:

Question 18. Trouver un terme de type W(?p:O ? q:O ~(p | q) <=> (~p & ~q)).

avec une équivalence à la place d'une implication. On peut en déduire que ~~(p | q) <=> ~(~p & ~q), mais bien entendu on ne peut pas aller jusqu'à déduire (p | q) <=> ~(~p & ~q) sans l'axiome de la double négation.

Il existe de très nombreux exercices de ce genre qu'on peut trouver dans les ouvrages de mathématique intuitionniste ou de théorie des topos (et dans la bibliothèque Coq !).

Pour l'heure, avançons un peu avec la notion d'égalité. Soient a et b deux termes de même type T.

Envoyé par Leibniz

a = b est une abbréviation pour ?p:T -> O (p(a) => p(b)).

Voici encore un exercice super classique, mais il faut bien en passer par là.

Question 20. Montrer que l'égalité est réflexive, symétrique et transitive.

Question 21. Trouver un terme de type W(~(vrai = faux)).

Soient T et U deux types. (Pour les notations en rapport avec les types sommes, voir le résumé.)

Question 22. Trouver un terme de type W(?x:T ?y:U ~(x+U = T+y)).

[Steki-kun]

Il se trouve qu'on a posté exactement en même temps sans pourtant s'être mis d'accord avec le DrTopos mais c'est bien, ça me fait moins de commentaires à faire sur les questions 17 et 18

Reprenons donc :
Question 17:
La question 17 consiste à montrer que l'axiome du tiers exclu est équivalent à celui de la double négation, ie. celui qui permet de montrer des choses par l'absurde (et par la contraposée également). Il faut donc montrer l'équivalence suivante : (?q:O.~~q=>q) <=> (?q:O.(q | ~q)), ce que nous faisons naturellement en montrant chaque implication séparément.
Voilà le terme que je propose pour l'implication <=, qui est la plus simple :

Envoyé par Steki-kun

De la droite vers la gauche, c'est plus simple :
(EM : W(?q:O.(q | ~q))) |-> (q: O) |-> (nnq : W(~~q)) |->
EM q ((p : W(q)) |-> p) ((np : W(~q)) |-> nnq np q).

On suppose donc une preuve du tiers-exclu, que j'appelle EM (excluded middle), une proposition q et une preuve de ~~q que j'appelle nnq. On veut donc construire une preuve de q, et bien évidemment c'est comme à l'école, vu qu'on a une seule hypothèse (le tiers exclu) il faut bien qu'on se débrouille pour s'en servir
Revenons donc un moment sur ce tiers-exclu : il donne pour toute proposition r (je change volontairement de notation pour ne pas "capturer" la proposition q sur laquelle on est en train de travailler) une preuve de (r|~r). Or, la disjonction (r|~r) est un raccourci pour ?p:O.(r=>p) => (~r=>p) => p. Donc, cette disjonction permet de prouver n'importe quelle proposition p, du moment que l'on peut prouver p sachant r, et que l'on peut aussi prouver p sachant ~r. Nous, on veut prouver q, donc on va utiliser cette propriété de la disjonction avec comme proposition p notre proposition q. En bref, on est ramené à se trouver un r sur lequel appliquer le tiers-exclu, ie tel que :

• on peut prouver r => q
• on peut aussi prouver ~r => q

Si on a ça, il suffira d'appliquer EM r pour obtenir une preuve de (r|~r), puis d'appliquer cette disjonction à q et à nos deux preuves ci-dessus pour obtenir une preuve de q ! Il se trouve qu'on peut facilement s'en sortir en prenant tout simplement r=q :

• une preuve de q => q s'obtient trivialement par le terme (p : W(q)) |-> p
• on peut aussi prouver ~q => q, car on s'était également donné le terme nnq de type W(~~q) (eh oui, au final on est en train de prouver ~~q => q, il ne faut pas l'oublier). Cela veut dire que si l'on considère une preuve np de ~q, on peut lui appliquer nnq et obtenir une preuve de Faux, avec laquelle on prouve n'importe quoi, et en particulier q. On a donc le terme suivant comme preuve de ~q => q : (np : W(~q)) |-> nnq np q

Cette fois, on a tous les morceaux et on a bien construit, étant donné le tiers-exclu EM et une proposition q quelconque, un terme de type W(~~q => q) :
(nnq : W(~~q)) |-> EM q ((p : W(q)) |-> p) ((np : W(~q)) |-> nnq np q).

/============================================

Voilà ensuite le terme que je propose pour l'autre implication =>, juste un peu plus difficile :

Envoyé par Steki-kun

Gauche vers droite :
(EM : W(?q:O.~~q => q)) |-> (q : O) -> (p : O) ->
(Hq : W(q => p)) |-> (Hnq : W(~q => p)) |->
EM p ((np : W(~p)) |-> (np (Hnq (aux q p Hq np)))).

où aux est un terme qui prouve en gros (A -> B) -> ~B -> ~A, soit la seule partie de la contraposition qui est vraie en logique intuitionniste :

(a: O) |-> (b : O) |-> (H : W(a => b)) |-> (H' : W(~b)) |-> (abs : W(a)) |-> (r: O) |-> H' (H abs) r).

Je ne détaille pas la construction du terme aux qui ne devrait pas poser de problème : d'une preuve de A => B, de ~B et de A, on déduit d'abord une preuve de B (car A => B), et donc une preuve de Faux (car ~B). Ce qui nous intéresse c'est qu'au final il ait le type suivant : W(?a:0.?b:O.(a=>b) => ~b => ~a).

Revenons donc à l'implication qu'on souhaite montrer : (?q:O.~~q=>q) => (?q:O.(q | ~q)).
On prend donc une preuve de la double-négation (que j'appelle EM comme le tiers exclu, puisqu'au final on aura montré qu'ils sont équivalents ), une propriété q, et on veut montrer la disjonction q | ~q. Pour montrer cette disjonction, on prend donc une proposition quelconque p, une preuve Hq de (q => p) et une autre Hnq de (~q => p), et l'on veut montrer p.
Même combat que tout à l'heure : si l'on a supposé EM, c'est qu'il faut s'en servir ! S'en servir ça peut être en particulier montrer ~~p : en effet si l'on montre ~~p, on aura plus qu'à appliquer EM pour avoir p. Montrons donc ~~p, c'est-à-dire supposons une preuve np de ~p et montrons Faux.
Récapitulons, on a une preuve de np de ~p, une preuve Hq de (q => p), une preuve Hnq de (~q => p), et on veut montrer Faux. Notre lemme aux nous donne déjà une preuve de ~q : il suffit pour cela de l'appliquer à Hq et à np. Muni de cette preuve de ~q, Hnq nous donne une preuve de p, et enfin on montre Faux en appliquant np à cette preuve de p. Cela donne bien le terme suivant : ((np : W(~p)) |-> (np (Hnq (aux q p Hq np)))) qui prouve ~~p, et permet de conclure par application de EM.

Questions 18/19 à venir !

Envoyé par DrTopos

Pour l'heure, avançons un peu avec la notion d'égalité. Soient a et b deux termes de même type T.

Voici encore un exercice super classique, mais il faut bien en passer par là.

Question 20. Montrer que l'égalité est réflexive, symétrique et transitive.

La réflexivité signifie que pour tout a, a = a. On a assez trivialement que ?p:T -> O (p(a) => p(a)) grace à l'identité.

La symétrie signifie que si a = b alors b = a. On suppose donc que l'on a ?p:T -> O (p(a) => p(b)). On prend pour propriété "être égal à a". On a bien que a est égal à a, donc b est égal à a.

La transitivité signifie que si a = b et b = c, alors a = c. Par symétrie, on sait que toute propriété vraie pour b est vraie pour a. La propriété "être égal à c" est donc vraie pour a et donc a = c

Envoyé par DrTopos

Question 21. Trouver un terme de type W(~(vrai = faux)).

On sait que pour tout p (vrai => p) => p en appliquant la preuve de vrai => p a une preuve de vrai On sait que faux a la propriété d'impliquer n'importe quoi, en particulier faux. Donc si vrai = faux, vrai a la même propriété (il faut d'abord appliquer la réflexivité). Donc vrai => faux. Reste à appliquer le fait que (vrai => faux) => faux et on a gagné.

J'avoue avoir un peu la flemme d'écrire les termes complets :-) Mais je vais ptet le faire..

[Steki-kun]

Question 18:
La question 18 propose de prouver ?p:O.?q:O.~(p|q) => (~p & ~q). Voilà le terme que je propose :

Envoyé par Steki-kun

(p : O) |-> (q : O) |-> (H : W(~(p|q))) |->
(r : O) |-> (Hpqr : W(~p => ~q => r)) |->
Hpqr
((tp : W(p)) |-> H ((s : 0) |-> (Hp : W(p=>s)) |-> (_ : W(q=>s)) |-> Hp tp))
((tq : W(q)) |-> H ((s : 0) |-> (_ : W(p=>s)) |-> (Hq : W(q=>s)) |-> Hq tq))

On commence donc par considérer deux propositions p et q, ainsi qu'une preuve H du fait que ~(p|q). Pour montrer la conjonction ~p & ~q, il faut considérer une nouvelle proposition r et montrer que sous l'hypothèse ~p => ~q => r, on peut montrer r.
On prend donc une nouvelle proposition r et une preuve Hpqr de ~p => ~q => r. Pour prouver r, on va essayer d'appliquer cette hypothèse Hpqr, il nous faut donc d'une part une preuve de ~p et d'autre part une preuve de ~q (c'est logique vu qu'on prouve la conjonction ~p & ~q ).
Les deux se montrent de manière très similaire, prenons le cas de ~p :
on suppose tp une preuve de p, et on veut établir Faux. Comme on a comme hypothèse le fait que (p|q) => Faux, on va donc montrer (p|q) sous l'hypothèse p, ce qui est trivial : ((s : 0) |-> (Hp : W(p=>s)) |-> (_ : W(q=>s)) |-> Hp tp) a le type W(p|q) lorsque tp est une preuve de p. Similairement, (_ : W(p=>s)) |-> (Hq : W(q=>s)) |-> Hq tq) est une preuve de (p|q) lorsque q est une preuve de q.
On établit ainsi des preuves de ~p et de ~q, et l'on applique Hpqr pour conclure comme expliqué au début de ce paragraphe.

Question 19:
La question 19 propose de prouver ?q:O.~~(q|~q).. Voilà le terme que je propose :

Envoyé par Steki-kun

(q: O) |-> (H : W(~(q|~q))) |-> (r : O) |->
(Q18 q (~q) H) r ((urd : W(~q)) |-> (abs : W(~~q)) |-> abs urd r).

où Q18 est le terme de la question précédente.

Ici, on commence par supposer une proposition q et une preuve H de ~(q|~q), sous l'hypothèse desquelles on veut obtenir une preuve de Faux. Or le terme de la question 18 peut nous transformer cette preuve H de ~(q|q) en une preuve (Q18 q (~q) H) de (~q & ~~q).
Une fois que l'on dispose de la preuve de cette conjonction, on peut montrer Faux comme suit : on suppose n'importe quelle proposition r, et on va la montrer en appliquant la conjonction. Il suffit donc de prouver que ~q => ~~q => r, ce qui est trivial puisque supposer à la fois ~q et ~~q permet de montrer Faux, donc on peut faire comme cela : ((urd : W(~q)) |-> (abs : W(~~q)) |-> abs urd r) comme à la Question 15.
En passant ce terme à notre preuve (Q18 q (~q) H) de (~q & ~~q), on obtient bien le terme suivant :
(r : O) |-> (Q18 q (~q) H) r ((urd : W(~q)) |-> (abs : W(~~q)) |-> abs urd r)
qui est une preuve de ?r:O.r, autrmeent dit une preuve de Faux.

Voilà Sur ce je vous laisse réfléchir aux questions concernant l'égalité de Leibniz.

[DrTopos]

Envoyé par alex_pi

J'avoue avoir un peu la flemme d'écrire les termes complets :-) Mais je vais ptet le faire..

Comme je te comprends !

On aura remarqué que j'emploie délibérément l'expression ``Trouver un terme de type W(...)'', plutôt que ``Prouver que ...''. Ma principale motivation pour conserver cette nuance est que le but de ce fil est de montrer aux informaticiens que démontrer c'est programmer, et qu'il est donc illogique qu'un informaticien se prétende réfractaire aux maths (ce qui arrive trop souvent, je crois).

Ceci-dit, ce qu'on fait ici est une programmation un peu spéciale. Il apparaît clairement dans les posts précédents que le fait de trouver la preuve, peu importe laquelle d'ailleurs, est plus important que de l'écrire. C'est bien entendu une conséquence du fait que je ne demande pas de trouver un terme de type W(...) ayant telle ou telle propriété, mais simplement un terme de type W(...) sans plus de précision. On aura compris que la raison en est que j'ai proof-irrelevance en tête, ou plus raisonnablement que j'ai toujours fait des mathématiques de cette façon, c'est à dire sans me préoccuper de savoir si je trouve une preuve ou une autre pour le même énoncé.

proof-irrrelevance (indiscernabilité des preuves) est indecidable dans le système exposés jusqu'ici (bien qu'il soit vrai dans tous les topos pour l'interprétation que j'ai en tête). C'est pourquoi cet axiome sera ajouté au système. On peut d'ailleurs l'ajouter de suite:

proof-irrelevance est un terme de type W(?q:O ?x:W(q) ?y:W(q) x = y).

Envoyé par alex_pi

Donc si vrai = faux, vrai a la même propriété

Je trouve que tu triches un peu avec cette affirmation. C'est là justement qu'il serait intéressant d'écrire le terme qui prouve ce fait. Il se peut que tu t'aperçoive que ce n'est pas aussi évident que tu l'as peut-être pensé.

[DrTopos]

Merci à Steki-kun pour ses explications très pédagogiques. Il a manifestement une vocation de prof.

On a déjà fait remarquer plusieurs fois que les termes de preuves sont un peu lourds. C'est dû surtout au fait qu'on ne s'est pas donné la peine de nommer certaines preuves, et donc qu'on redémontre la même chose plusieurs fois.

On a déjà prouvé que E entraine E | F. C'était une question non officielle (non numérotée) posée dans le post #60. La réponse a été donnée par alex_pi dans le post #62: le terme:

(x:W(E)) |-> (q:O) |-> (r:W(E) -> W(q)) |-> (s:W(F) -> W(q)) |-> r(x)

est en effet de type W(E) -> W(E | F). On va poser:

x | F = (q:O) |-> (r:W(E) -> W(q)) |-> (s:W(F) -> W(q)) |-> r(x)

de telle sorte que si x prouve E alors x | F prouve E | F. De la même façon on introduit la notation E | y comme preuve de E | F dans le cas où y prouve F.

On va également abbréger la notation x:W(E) en x |- E (lire: ``x prouve E'').

Dans ces conditions, et en utilisant de plus la notation des paires de Heyting, on peut donner la réponse suivante pour la question 18:

(r |- ~(p | q)) |-> <(x |- p) |-> r(x | q), (y |- q) |-> r(p | y)>

En effet, r étant déclaré de type W(~(p | q)), c'est à dire de type W(p | q) -> W(faux), et x étant déclaré de type W(p), on voit que x | q est de type W(p | q), donc que r(x | q) est de type W(faux), donc que (x |- p) |-> r(x | q) prouve ~p. De même (y |- q) |-> r(p | y) prouve ~q. Bien entendu, si x prouve E et y prouve F, la paire de Heyting <x,y> prouve E & F, puisque son type est W(!x:W(E) F).

Comme je l'ai signalé, la réciproque est aussi vraie pour la question 18, et peut se prouver comme suit:

(r |- ~p & ~ q) |-> (s |- p | q) |-> s(faux)(p1(r))(p2(r))

où p1 et p2 sont des termes de types respectifs W(E&F) -> W(E) et W(E&F) -> W(F) (ceci quels que soient E et F), lequels ont déjà été construits dans le post ... ah ! on a oublié de les faire ceux-là ... bon alors les voici:

D'abord rappelons la définition de la conjonction:

E & F = !x:W(E) F

C'est l'une des deux définitions données par alex_pi. Elle est simplement réécrite ici avec le quantificateur existentiel. Intuitivement, l'enoncé !x:W(E) F se lit: ``il existe une preuve de E telle que F'', autrement dit ``E et F''. Bien sûr c'est une conjonction éventuellement dépendante. Note: on verra plus tard quel est l'intérêt de la conjonction dépendante et de l'implication dépendante quand on aura l'opérateur de description.

Alors supposons que p |- E & F. p est donc une preuve de ?q:O ((?x:W(E) (F => q)) => q). Donc p(E) prouve (?x:W(E) (F => E)) => E. Par ailleurs, (x:W(E)) |-> (y:W(F)) |-> x prouve ?x:W(E) (F => E). Finalement, p(E)((x:W(E)) |-> (y:W(F)) |-> x) prouve E. Pour tous énoncés E et F, F pouvant dépendre d'une variable x de type W(E), on pose donc:

p1 = (p |- E & F) |-> p(E)((x:W(E)) |-> (y:W(F)) |-> x)

qui est un terme de type W(E & F) -> W(E). Je vous laisse construire vous même un terme p2 de type (p:W(E & F)) -> W(F[ p1(p)/x ]) (où il est toujours entendu que F peut avoir des occurrences de x de type W(E)).

[DrTopos]

Bonjour à tous.

Soyez gentil, quand vous donnez des solutions, de les donner complètes, une solution seulement esquissée devant de toute façon être complétée. Aussi, je demande à alex_pi de bien vouloir détailler les solutions qu'il a données pour les questions 20 et 21. Par ailleurs, la question 22, qui exprime le fait qu'une somme est une union disjointe n'a pas été résolue. Mais voici d'autres questions sur l'égalité, qui vont aussi nous permettre de soulever le problème assez délicat de l'égalité entre types.

Soient a et b deux termes de type T, et E un terme de type U, E et U pouvant dépendre de x:T. Enfin, soit r de type W(a=b).

Question 23. Trouver un terme de type W(E[ a/x ] = E[ b/x ]).

Question 24. Soit c un terme de type W(E[ a/x ]). Est-il aussi de type W(E[ b/x ]) ? (Toujours sous l'hypothèse a=b bien sûr.)

A propos de la question 24, je demande aux spécialistes de nous expliquer comment tout cela se passe en Coq.

On définit le type des booléens par Boole = One+One. On pose également Bfaux = *+One et Bvrai = One+* (j'utilise les symboles Bfaux et Bvrai pour éviter la surcharge et rendre ainsi la lecture plus facile). Je rappelle que les notations et concepts concernant les sommes sont définis avec précision dans le résumé. Bien sûr dans un langage utilisable en pratique, Boole serait un clône de One+One et non pas One+One lui-même, et la définition prendrait la forme d'un type énuméré.

Question 25. Construire un terme f de type Boole -> O tel que f(Bfaux) = faux et f(Bvrai) = vrai.

Question 26. En utilisant le tiers exclu, construire la fonction réciproque de f construite dans la question 25.

Question 27. Que pensez-vous d'une fonction constructive (donc construite en particulier sans utilisation du tiers exclu) de type O -> Boole ?

Ces fonctions (question 27) ont une propriété très remarquable. Toutefois, prouver qu'elles l'ont requiert des moyens importants hors de porté de ce quizz. C'est dû au fait que cette propriété, bien que vraie dans un modèle constructif n'a pas de démonstration interne, puisqu'elle n'est pas vraie dans d'autres modèles. Il s'agit donc non pas d'un théorème, mais d'un méta-théorème. La seule chose que je demande ici est de ``sentir'' (et donc de deviner) cette propriété, ce qui peut se faire (me semble-t-il) après avoir fait quelques essais de programmation d'une telle fonction sans utilisation de principes non constructifs. On doit se rendre compte de quelque chose et être capable d'énoncer la propriété (sans la prouver bien sûr) et de donner quelques arguments en faveur de cette propriété.

[Steki-kun]

Envoyé par DrTopos

Question 24. Soit c un terme de type W(E[ a/x ]). Est-il aussi de type W(E[ b/x ]) ? (Toujours sous l'hypothèse a=b bien sûr.)

A propos de la question 24, je demande aux spécialistes de nous expliquer comment tout cela se passe en Coq.

Sans donner la réponse à la question proprement dite, la réponse à votre sous question est que ce terme c n'est pas de type W(E[b/x]) puisqu'un terme de preuve de W(E[b/x]) s'obtiendra ici par "application" de l'hypothèse d'égalité entre a et b à la proposition E (une application directe ici, et une application de l'hypothèse d'induction associée à l'égalité en Coq, mais je le donne "à la Topos" plutôt qu'"à la Coq") :
eq (a |-> E[a/x]) c . Ce terme dépend évidemment de la preuve de a=b, donc de eq, et n'a aucune raison d'être égal à c.

Coq dispose bien d'une règle dite de "conversion" qui dit que si t est de type A, et que A est convertible en B, alors t est de type B. Mais la conversion ne comprend pas l'égalité, elle est régie par les règles de calcul (réductions) du langage : par exemple, cela correspondrait dans votre formalisme au fait que

si c est une preuve de [x > A, y > B](x+U), alors c est une preuve de A car le premier type se réduit en le second.

NB aux malins : je viens de donner une sacrée info pour résoudre la question 22

[DrTopos]

Envoyé par Steki-kun

Sans donner la réponse à la question proprement dite, ...

Donc, si j'ai bien compris, la réponse à la question 24 si elle était formulée en Coq serait ``non''. Comme il n'y a pas de W(...) en Coq, on doit donc en déduire que a=b n'entraine pas E[ a/x ] = E[ b/x ] dans le cas où E est de type Prop. Est-ce bien cela ?

Envoyé par Steki-kun

Coq dispose bien d'une règle dite de "conversion" qui dit que si t est de type A, et que A est convertible en B, alors t est de type B. Mais la conversion ne comprend pas l'égalité, elle est régie par les règles de calcul (réductions)

Donc si a et b ont même forme normale on aura E[ a/x ] = E[ b/x ], alors que ce n'est pas forcément le cas si on a seulement une preuve de a=b. Ai-je bien compris ?

[Steki-kun]

Oui c'est exactement ça :-)