p
u
b
l
i
c
i
t
é
publicité
  1. #1
    Invité de passage
    Homme Profil pro
    Inscrit en
    mai 2011
    Messages
    10
    Détails du profil
    Informations personnelles :
    Sexe : Homme

    Informations forums :
    Inscription : mai 2011
    Messages : 10
    Points : 0
    Points
    0

    Par défaut [Coq] établir preuve : équivalence de 2 ordres

    J'ai commencé à peine 1 semaine avec Coq. Je dois établir des preuves pour prouver l'équivalence deux notions.
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    Inductive sorted_i : list nat -> Prop :=
        sorted_i_nil : sorted_i nil
      | sorted_i_cons : forall (a : nat) (l : list nat),
                        (forall b : nat, In b l -> a <= b) ->
                        sorted_i l -> sorted_i (a :: l)
    et

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    sorted_d = 
    fun l : list nat =>
    forall i j : nat,
    i < j ->
    forall a b : nat, nth_error l i = Some a -> nth_error l j = Some b -> a <= b
         : list nat -> Prop
    Donc je dois montrer un Lemme qui est :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    Lemma sortedEq : forall l, sorted_i l <-> sorted_d l.
    J'ai commencé par :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    Proof.
    split.
    intros.
    pour découper l'équivalence, et puis monter les introductions.
    Mais ensuite, je me suis bloqué car je n'ai aucune idée pour quel tactique sur quel truc à applique.
    J'ai essayé avec
    Coq l'a monté comme un sorted_d : nat en haut et laisse en bas le corps de sorted_d.
    Mais après, vraiment, je suis perdu. Quelqu'un pourrait me donner un coup de main?

  2. #2
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 618
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 618
    Points : 2 777
    Points
    2 777

    Par défaut

    Quand on a une propriété construite de façon inductive, généralement (ma connaissance de Coq est très très superficielle et très empirique) on la détruit avec induction.
    induction l
    Après on doit prouver le lemme pour le cas de base sorted_i_nil puis pour le cas inductif sorted_i_cons.

    Après, je dis ça je dis rien hein, si c'est pas ça alors c'est autre chose, va savoir quoi
    Citation Envoyé par minhkhue
    Mais ensuite, je suis bloqué car je n'ai aucune idée pour quelle tactique sur quel truc à appliquer.
    Alors on est au moins deux !
    Quand tu sens que tu es allé dans une impasse tu peux annuler la(les) dernière(s) commande(s) avec Undo.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  3. #3
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    tu connais forcément replace

    connais-tu la commande unfold ?
    http://coq.inria.fr/V8.1/tutorial.html

    selon moi, il te faudra aussi inversion
    http://coq.inria.fr/refman/Reference...013.html#toc75

    et prouver

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    Lemma egal_some: (T:Set) (a,b:T) ((Some ? a)=(Some ? b)) -> (a=b).

    au passage es-tu sûr de sorted_d ?

    je verrais plutôt ceci :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    Definition sorted_d : list nat -> Prop := 
    fun l : list nat => l = nil \/ 
    forall i j : nat, 
    i < j ->
    forall a b : nat, nth_error l i = Some a -> nth_error l j = Some b -> a <= b    
    .


    penses aussi à regarder le_refl dans Coq.Arith.Le
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  4. #4
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    pour infos, j'ai essayé de la faire en entier... et je suis tombé sur un point non constructible :'(

    mais peut-être y a-t-il une autre manière de procéder... je ne suis pas expert en Coq
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  5. #5
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    Le problème ici est un problème de bibliothèques. Les spécifications utilisent d'une part "nth_error" et de l'autre "In", mais évidemment dans la lib standard de Coq il n'y a rien de déjà prêt sur le lien entre "nth_error" et "In", il faut faire à la main le lien entre "nth_error" et "nth", ce qui est très pénible (parce que "nth" est laid pour commencer), et ensuite passer de "In" à "nth". Ou alors faire directement la preuve soi-même.
    Mais bref tout ça c'est réimplémenter un petit bout de la bibliothèque standard, et ça n'a rien à avoir avec le domaine qui nous concerne qui est de parler de listes triées.

    gorgonite > ton ajout de "l = nil \/" n'est pas nécessaire puisque `sorted_d` est vraie en particulier pour une liste vide.

    Je n'ai pas essayé donc je ne sais pas pour la constructivité, mais à priori c'est plutôt une question de comment les définitions sont posées. Normalement comme les deux listes sont finies on doit pouvoir tout faire constructivement.

  6. #6
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    Citation Envoyé par bluestorm Voir le message
    gorgonite > ton ajout de "l = nil \/" n'est pas nécessaire puisque `sorted_d` est vraie en particulier pour une liste vide.
    mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide


    Citation Envoyé par bluestorm Voir le message
    Le problème ici est un problème de bibliothèques. Les spécifications utilisent d'une part "nth_error" et de l'autre "In", mais évidemment dans la lib standard de Coq il n'y a rien de déjà prêt sur le lien entre "nth_error" et "In", il faut faire à la main le lien entre "nth_error" et "nth", ce qui est très pénible (parce que "nth" est laid pour commencer), et ensuite passer de "In" à "nth". Ou alors faire directement la preuve soi-même.
    Mais bref tout ça c'est réimplémenter un petit bout de la bibliothèque standard, et ça n'a rien à avoir avec le domaine qui nous concerne qui est de parler de listes triées.

    [...]

    Je n'ai pas essayé donc je ne sais pas pour la constructivité, mais à priori c'est plutôt une question de comment les définitions sont posées. Normalement comme les deux listes sont finies on doit pouvoir tout faire constructivement.

    justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile

    EDIT: en gros, une fois que je prouve ce lemme, je m'en sors... mais je n'y arrive pas

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    Lemma nth_not_error_impl_In :
      forall (b : nat) l,
      (exists n, nth_error l n = value b) ->
      In b l.
    enfin, c'est dans ces situations où l'on comprend pourquoi il ne faut pas utiliser Coq si la constructivité n'est pas nécessaire... Isabelle/HOL est nettement plus adaptée pour faire des preuves non corrélées à des implantations
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  7. #7
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    Non, c'est toi qui est obsédé par la constructivité. Si tu veux juste raisonner comme d'habitude sans te prendre la tête, tu ajoutes le tiers exclu, on en a déjà parlé, c'est consistent, c'est prévu par la bibliothèque standard (qui apporte des tactiques de raisonnement classique), etc. Sur ce point ton raisonnement n'est pas rationnel.
    (Par ailleurs si tu t'intéresses à Isabelle/HOL c'est très bien, hein, il faut avoir une vision un peu large et essayer des alternatives; je veux bien croire qu'Isabelle/HOL soit plus agréable à utiliser que Coq, je n'en sais rien malheureusement, je n'ai pas encore essayé ces outils. Mais l'argument n'est pas "bouh on n'a pas le tiers exclu".)

    mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide
    Ce n'est pas ce qu'il faut montrer ici. On te donne deux indices qui "ont des éléments" (nth_error renvoie Some) dans la liste vide, et on te demande de montrer quelque chose. Mais nth_error sur la liste vide renvoie toujours None, donc l'hypothèse qu'ils ont des éléments est fausse, donc implique n'importe quoi.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    Goal sorted_d nil.
      intros i j Hij a b Ha Hb.
    En regardant le code de nth_error on voit qu'il pattern-matche d'abord sur l'indice (si c'est 0 ou pas) et ensuite sur la liste, et que dans les deux branches du filtrage, la liste vide renvoie None. Pour exhiber la contradiction il faut donc commencer par détruire l'indice.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    destruct i. simpl in Ha.
    On a alors l'hypothèse ("error" veut dire None ici, c'est son nom dans la monade d'exception) :
    Ha : error = Some a
    La tactique `discriminate` voit la contradiction (deux constructeurs différents d'un inductif ne peuvent être égaux). En fait on peut l'utiliser dans les deux branches.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    Goal sorted_d nil.
      intros i j Hij a b Ha Hb.
      destruct i; discriminate Ha.
    Qed.
    justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile.
    Comme je l'ai déjà dit, il n'est pas nécessaire de se poser des questions philosophiques sur la constructivité en Coq. Si on a l'impression d'avoir un problème et qu'on ne veut *pas* se prendre la tête, on admet le tiers-exclu.
    Cependant, ici, si tu as envie de faire ton puriste constructiviste, et c'est intéressant aussi, tu vois que la preuve qu'on te demande repose fondamentalement sur un objet fini. Tu as une liste "l" finie et tu veux montrer que si une condition décidable est vraie, alors une autre condition décidable est vraie. Il n'y a rien de non-constructif là-dedans, et un bon moyen de ne pas avoir d'ennui et de raisonner sur la liste qu'on sait finie.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    Lemma nth_not_error_impl_In :
      forall (b : nat) l n, nth_error l n = value b -> In b l.
      induction l.
      (* Cas nil *) destruct n; discriminate.
      (* Cas a::l *)
        destruct n.
        (* Cas 0 *)
          injection 1; intro H0.
          constructor; exact H0.
        (* Cas (S n) *)
          intro Hn.
          right.
          apply (IHl _ Hn).
    Qed.
    NB: j'ai viré le "exists" là parce qu'il alourdit la preuve en forçant à empaqueter/dépaqueter des types existentiels et qu'on n'en a de toute façon pas besoin dans l'exercice demandé, mais ça ne change rien à la prouvabilité.

  8. #8
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    Citation Envoyé par bluestorm Voir le message
    Non, c'est toi qui est obsédé [... ] Sur ce point ton raisonnement n'est pas rationnel.
    j'ai réservé ma place à l'asile, mais il y a une longue liste d'attente


    Citation Envoyé par bluestorm Voir le message
    Mais l'argument n'est pas "bouh on n'a pas le tiers exclu".
    l'argument serait plutôt... quand j'ai besoin de quelque chose, y a sûrement le système logique ad-hoc déjà tout prêt à utiliser

    Citation Envoyé par bluestorm Voir le message
    La tactique `discriminate` voit la contradiction (deux constructeurs différents d'un inductif ne peuvent être égaux). En fait on peut l'utiliser dans les deux branches.
    ok c'est celle qui me manquait... depuis si longtemps

    Citation Envoyé par bluestorm Voir le message
    Cependant, ici, si tu as envie de faire ton puriste constructiviste, et c'est intéressant aussi,
    ben c'est à mes yeux le seul intérêt de Coq... pour le reste il y a d'autres outils plus agréables selon moi

    Citation Envoyé par bluestorm Voir le message
    tu vois que la preuve qu'on te demande repose fondamentalement sur un objet fini. Tu as une liste "l" finie et tu veux montrer que si une condition décidable est vraie, alors une autre condition décidable est vraie. Il n'y a rien de non-constructif là-dedans, et un bon moyen de ne pas avoir d'ennui et de raisonner sur la liste qu'on sait finie.
    j'étais parti aussi sur cette voie, mais différemment... à croire que j'adore me recréer le même pattern planteur

    en tout cas, tu utilises des tactiques de plus haut niveau que moi, ce qui raccourcit considérablement les preuves. il faut avouer que je me sers juste des bases... c'est carrément pas mon domaine (je suis plus dans l'interprétation abstraite et l'exécution symbolique )

    Citation Envoyé par bluestorm Voir le message
    NB: j'ai viré le "exists" là parce qu'il alourdit la preuve en forçant à empaqueter/dépaqueter des types existentiels et qu'on n'en a de toute façon pas besoin dans l'exercice demandé, mais ça ne change rien à la prouvabilité.
    ok ce n'était pas l'exercice ici, mais aurais-tu un lien qui montre cet alourdissement ?
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  9. #9
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    Lemma nth_not_error_impl_In_exists :
      forall (b : nat) l, (exists n, nth_error l n = value b) -> In b l.
      induction l.
      (* Cas nil *)
        destruct 1 as [n Hn]. destruct n; discriminate.
      (* Cas a::l *)
        destruct 1 as [n Hn]. destruct n.
          injection Hn; intro H0.
          constructor; exact H0.
          right. apply IHl.
          exists n. apply Hn.
    Qed.

  10. #10
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    au fait minhkhue, où en es-tu ?

    parce qu'on parle (j'ai un peu fait digressé le sujet), mais on ne sait pas si de ton côté ça avance ?

    as-tu au moins compris où allait servir nth_not_error_impl_In ?

    en gros, à un moment, avec les tactiques que je t'ai citées (bluestorm ferait sûrement mieux en moins de ligne mais bon ), tu vas arriver à un stade de ce style:

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    a : nat
    l : list nat
    H : sorted_i (a :: l)
    a0 : nat
    b : nat
    H2 : nth_error (a :: l) (S n) = value b
    H4 : a = a0
    H5 : nth_error l n = value b
    H7 : forall b : nat, In b l -> a <= b
    ______________________________________(1/3)
    a0 <= b
    c'est juste un petit coup de pouce (les grandes lignes pour arriver jusqu'à un point où son utilité saute aux yeux)

    dis-nous où tu en es...
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  11. #11
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    PS : je suis flatté d'entendre dire de mon code Coq "il utilise des techniques avancées, moi je fais avec les outils de base", parce que c'est ce que je passe mon temps à me dire du code *des autres*. Comme quoi tout est une question de point de vue :p

    Je ne l'ai pas fait dans le code de mon développement ci-dessus, car c'était juste un petit hack temporaire pour vérifier (et de préférence contredire hein, sinon c'est pas drôle) ce que disait gorgonite, mais j'encourage l'utilisation des macros "Case", que je tire du cours Software Foundations de Benjamin Pierce (c'est LE document pour apprendre Coq par la pratique, avec le Coq'Art éventuellement si vous avez la chance d'avoir une copie papier). La définition des macros en question est ici, et ça s'utilise comme ça :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    Lemma nth_not_error_impl_In :
      forall (b : nat) l n, nth_error l n = value b -> In b l.
      induction l.
      Case "nil". destruct n; discriminate.
      Case "a::l".
        destruct n.
        SCase "0".
          injection 1; intro H0.
          constructor; exact H0.
        SCase "S n".
          intro Hn.
          right.
          apply (IHl _ Hn).
    Qed.

  12. #12
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 264
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 31
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 264
    Points : 17 724
    Points
    17 724

    Par défaut

    Citation Envoyé par bluestorm Voir le message
    cours Software Foundations de Benjamin Pierce (c'est LE document pour apprendre Coq par la pratique, avec le Coq'Art éventuellement si vous avez la chance d'avoir une copie papier).
    au fait y a-t-il une version pdf de ce cours en ligne ?
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  13. #13
    Membre émérite
    Inscrit en
    mars 2010
    Messages
    308
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 308
    Points : 890
    Points
    890

    Par défaut

    Citation Envoyé par gorgonite Voir le message
    mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide
    Euh, vraiment ?

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    Goal forall A (x:A) P, In x nil -> P x.
    Proof.
      intros * IN.
      inversion IN.
    Qed.
    
    Require Import Ensembles.
    
    Goal forall A (x:A) P, In _ (Empty_set A) x -> P x.
    Proof.
      intros * IN.
      inversion IN.
    Qed.

    Citation Envoyé par gorgonite Voir le message
    justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile
    Ca m'intéresserait beaucoup de tomber sur un "problème de constructivité" quand tu fais une preuve sur les listes. Ce sont des ensembles finis, que l'on peut trivialement parcourir.

    Citation Envoyé par gorgonite Voir le message
    enfin, c'est dans ces situations où l'on comprend pourquoi il ne faut pas utiliser Coq si la constructivité n'est pas nécessaire... Isabelle/HOL est nettement plus adaptée pour faire des preuves non corrélées à des implantations
    Dans toutes les preuves que j'ai faites, la constructivité n'a pour ainsi dire jamais été un problème. Les seuls axiomes dont j'ai eu besoin, ça a été extensionnalité et proof irrelevence. Je veux bien que tu me cites des "vrais" problèmes...

  14. #14
    Membre émérite
    Inscrit en
    mars 2010
    Messages
    308
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 308
    Points : 890
    Points
    890

    Par défaut

    Citation Envoyé par gorgonite Voir le message
    au fait y a-t-il une version pdf de ce cours en ligne ?
    Ca ne correspondrait pas du tout à l'esprit, qui est de jouer le code et de compléter les preuves.

  15. #15
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    D'ailleurs TropMDR je me souviens être tombé il y a quelques temps sur une page assez cool liée à Software Foundations, des gens avaient codé une variante de "coqdoc" telle que quand on passe la souris sur la preuve, à côté tu as les buts qui défilent selon la tactique sur laquelle tu es. Malheureusement j'ai cherché à retrouver cette démo récemment, et pas moyen.... Si jamais tu as un lien, ça m'intéresse.

  16. #16
    Membre émérite
    Inscrit en
    mars 2010
    Messages
    308
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 308
    Points : 890
    Points
    890

    Par défaut

    Proof general 4 fait ça. Pour le reste, je ne sais pas !

Discussions similaires

  1. [postgreSQL] équivalent de la function 'instr'
    Par Dra_Gun dans le forum Requêtes
    Réponses: 2
    Dernier message: 17/01/2003, 16h09
  2. Ordre de parcours de l'arbre...
    Par Sylvain James dans le forum XML/XSL et SOAP
    Réponses: 3
    Dernier message: 01/12/2002, 18h41
  3. Équivalent du #IFDEF
    Par agh dans le forum Langage
    Réponses: 4
    Dernier message: 14/10/2002, 18h44
  4. [] Tri d'un tableau par ordre alphabétique
    Par cafeine dans le forum VB 6 et antérieur
    Réponses: 3
    Dernier message: 17/09/2002, 08h43
  5. Je ne peux établir une connexion cliente sous Linux.
    Par Anonymous dans le forum CORBA
    Réponses: 5
    Dernier message: 16/04/2002, 15h57

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo