Questions sur le projet de Coq. ******************************* Q: Plusieurs de mes camarades et moi même ne voyons pas vraiment ce qu'il faut mettre dans le rapport du projet de coq. Par exemple pour les explications des preuves, j'imagine que nous ne devons pas faire un listing de nos tactiques et dire par exemple : J'ai utilisé telle tactique qui me donne ce résultat ce qui nous permet d'utiliser telle autre tactique etc... Mais bon si nous ne devons pas faire ça alors que dire ? Donc si vous pouviez éclaircir vos attentes avec je ne sais pas un exemple ou n'importe quoi qui puisse nous faire y voir plus clair. R: Les étapes importantes dans une preuve sont : appliquer un théorème déjà prouvé (ou un axiome) appliquer un principe de récurrence (comme Nat_ind ou LE_ind, etc ...) utiliser (par rewrite) des égalités déjà prouvées ou dans la liste des hypothèses, décider de passer par un lemme intermédiaire (par assert) faire un raisonnement par l'absurde Dans chacun des cas, on peut présenter le but avant, et les nouveaux buts que ça engendre. Une chose intéressante est aussi un discours du genre. " Je donne la commande 'Hint Resolve mon_theoreme', qui est utilisé dans le "auto" de la preuve de mon_autre_theoreme" (il y a plusieurs exemples de ça dans le fichier distribué) Q: Je pense qu'il est normal qu'après un "absurd" on arrive à une contradiction, mais comment signaler à Coq que l'on est arrivé à la contradiction que l'on cherche ? R: Rappel sur la tactique "absurd" Supposons que la proprité a prouver soit "A" dans un contexte Gamma, mais qu'en fait c'est parce que le contexte Gamma est incohérent (et donc ca n'a rien à voir avec A). Une façon de résoudre ce problème est de trouver (à l'intuition) une proposition B telle que Gamma|- B et Gamma |- ~B; on aura alors trivialement Gamma |- False et donc Gamma |- A. La tactique coq à éxecuter est "absurd B" elle engendre de'ux sous-buts : a) prouver B b) prouver ~B Q: au sujet de l'induction que j'ai beaucoup de mal à appréhender. Quel est le résultat exact de la tactique "induction H using Le_ind" ? Ou "using Nat_ind" ? J'ai essayé de m'en servir intuitivement et me trouve à nouveau dans une situation déroutante avec cette preuve : Lemma Le_n_S_p : forall n p, n <= S p -> n = S p \/ n <= p. Proof. intros. induction H using Le_ind. left ; reflexivity. destruct IHLe. left. Je me retrouve avec le sous-but courant suivant : n : Nat p : Nat p0 : Nat H : n <= p0 H0 : n = p0 ============================ n = S p0 Les hypothèses sont en totale contradiction avec le sous-but. Je ne sais pas vraiment quelle conclusion dois-je en tirer. R: -- Bonjour, La tactique "induction H using Le_ind sert quand on a un but de la forme H : n <= p ======== P p alors elle engendre les deux buts (preuve par recurrence à partir de n): ===== P n et H : n <= p IHn : P p ====== P (S p) La tactique "induction n using Nat_ind " sert si on veut faire une recurrence a partir de zero Si le but est n : Nat ====== P n alors elle engendre les deux buts (preuve par recurrence à partir de zero): ===== P zero et n : Nat IHn : P p ====== P (S p) Bon, mais dans ton exemple, tu as l'hypothèse H : n <= S p et le but n = S p \/ n <= p. Tu ne peux pas mettre ça sous la forme utilisable par Le_ind (il aurait fallu H: n<= p) En revanche, tu peux utiliser Le_inv (prouvé plus haut) qui permet à partir de n<=S p de deduire deux cas qui permettent de finir la preuve.