Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 16 sur 16
  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 :
    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 :
    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 :
    Lemma sortedEq : forall l, sorted_i l <-> sorted_d l.
    J'ai commencé par :
    Code :
    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 Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 569
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 569
    Points : 2 571
    Points
    2 571

    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 projet, 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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 :
    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 :
    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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 009
    Points
    1 009

    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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 :
    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 009
    Points
    1 009

    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 :
    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 :
    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 :
    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 :
    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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 009
    Points
    1 009

    Par défaut

    Code :
    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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 :
    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 009
    Points
    1 009

    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 :
    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 Nicolas Vallée
    Ingénieur d'études
    Inscrit en
    décembre 2005
    Messages
    10 162
    Détails du profil
    Informations personnelles :
    Nom : Homme Nicolas Vallée
    Âge : 29
    Localisation : France

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

    Informations forums :
    Inscription : décembre 2005
    Messages : 10 162
    Points : 18 669
    Points
    18 669

    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 chevronné
    Inscrit en
    mars 2010
    Messages
    281
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 281
    Points : 756
    Points
    756

    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 :
    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 chevronné
    Inscrit en
    mars 2010
    Messages
    281
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 281
    Points : 756
    Points
    756

    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 009
    Points
    1 009

    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 chevronné
    Inscrit en
    mars 2010
    Messages
    281
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 281
    Points : 756
    Points
    756

    Par défaut

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

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •