+ Répondre à la discussion
Affichage des résultats 1 à 11 sur 11
  1. #1
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut [COQ débutant] récursion polymorphe

    Bonjour amis COQeurs au grand cœur,

    Au départ j'ai du code ocaml pour un conteneur multimap bijectif entre 2 types:
    Code OCaml 3.12 :
    1
    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
    type ('a, 'b) rev_map =
      | Nil 
      | Node of ('b, 'a) rev_map * 'a * 'b * ('b, 'a) rev_map
    
    let rec insert : 'a 'b . 'a -> 'b -> ('a, 'b) rev_map -> ('a, 'b) rev_map =
      fun x y -> function 
      | Nil -> Node(Nil,x,y,Nil) 
      | Node (l,u,v,r) ->
          if x < u then Node (insert y x l,u,v,r)
          else if y > v then Node (l,u,v,insert y x r)
          else Node (l,u,y,insert v x r)
      
    let rec member : 'a 'b . 'a -> 'b -> ('a, 'b) rev_map -> bool =
      fun x y -> function 
      | Nil -> false
      | Node (l,u,v,r) ->
          (x = u && y = v) or member y x (if x < u then l else r)
        
    let interleave f w  = function
      | Nil -> []
      | Node (l, u, v, r) ->
          f w l @ (if v = w then [u] else []) @ f w r
    (* find all values with the given key, in sorted order *)
    let rec find_all k = function
      | Nil -> []
      | Node (l, u, v, r) ->
        if k < u then interleave find_all k l
        else (if k = u then [v] else []) @ interleave find_all k r
    (* find all values y with key x (even levels) *)
    let find_all_y x t =
      find_all x t
    (* find all keys x with value y (interleaved version, odd levels) *)
    let find_all_x y t =
      interleave find_all y t

    Comme j'ai la chance d'avoir éventuellement tout un week-end à perdre, j'ai décidé de passer en mode "COQ pour les nuls".
    Ça donne ceci pour commencer en douceur (oui oui vous pouvez cracher dessus) :
    Code COQ 8.1 :
    1
    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
    Variable   C : Set.  
    Inductive  order : Set := Less | Equal | More.
    Hypothesis compare : C -> C -> order.
    
    Inductive rev_map (A B:Set) : Set :=
      | Nil:  rev_map A B
      | Node: rev_map B A -> A -> B -> rev_map B A -> rev_map A B.
    
    Fixpoint insert x y t {struct t} :=
      match t with
      | Nil => Node Nil x y Nil
      | Node l u v r =>
          match compare x u with
          | Less => Node (insert y x l) u v r 
          | _ => match compare y v with
                 | More => Node l u v (insert y x r)
                 | _ => Node l u y (insert v x r)
                 end
          end
      end.
    
    Fixpoint member x y t {struct t} :=
      match t with
      | Nil => false
      | Node l u v r =>
          match compare x u, compare y v with
          | Equal,Equal => true
          | Less,_ => member y x l 
          | _,_    => member y x r 
          end
      end.
    Ça n'était pas censé bien se passer du premier coup.
    Et sans surprise, en effet ça se passe mal.
    Soit ça ne passe pas du tout comme insert.
    Soit ça passe mal comme member.
    Code :
    1
    2
    3
    Coq < Check member.
    member
         : C -> C -> rev_map C C -> bool
    J'aurais préféré:
    Code :
    1
    2
    3
    Coq < Check member.
    member
         : A -> B -> rev_map A B -> bool
    Bien évidemment j'ai un problème de syntaxe avec la récursion polymorphe.
    Il y a éventuellement (certainement) d'autres incompréhensions de ma part, merci de prendre du temps pour m'expliquer lesquelles.
    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.

  2. #2
    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

    Ton erreur est de définir "Variable (C : Set)." puis "Hypothesis compare : C -> C -> order". Du coup C est une globale et tous les arguments passés à "compare" sont inférés de type C. Une imprudence supplémentaire est de te reposer autant sur l'inférence de types dans tes déclarations; avec un petit
    Fixpoint insert A B x y (t : rev_map A B) := ...
    tu aurais eu un rapport d'erreur assez explicite.

    Bref, la solution est de retirer la constante C et de définir
    Hypothesis compare : forall (C : Set), C -> C -> order.


    PS: merci de redonner un peu de vie à ce forum.

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

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut Merci.

    J'ai terminé la traduction, y compris rectangle_to_list
    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.

  4. #4
    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

    C'est bien, mais maintenant il faut prouver la correction

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

    Par défaut

    Citation Envoyé par gasche Voir le message
    Bref, la solution est de retirer la constante C et de définir
    Hypothesis compare : forall (C : Set), C -> C -> order.
    Euh, je crois que tu ne veux surtout pas faire ça ! La tu demandes l'existence d'une fonction de comparaison universelle. Le jour où tu vas vouloir ajouter le fait que c'est bien une fonction de comparaison (du genre compare a a = Equal, compare a b = Equal -> compare b a = equal, compare a b = Less -> compare b a = More (et l'opposé)), tu vas un peu en chier pour écrire une version polymorphe (et par "un peu en chier", je veux évidement dire que tu ne pourras pas l'écrire).

    Il te faut une fonction de comparaison par type (A et B). Pour ça, il y a deux grande méthodes

    La méthode camleuse: un foncteur
    La méthode haskellienne: une typeclass

    C'est une question de gout.

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

    Par défaut

    Allez tiens, une version imbitable pour le débutant, avec typeclasses et type dépendants (youhou)

    Code :
    1
    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
    Generalizable Variables A B.
    
    Definition relation (A:Type) := A -> A -> Prop.
    
    Inductive  order {A: Type} (LT: relation A) (a b: A) :=
    | Less: LT a b -> order LT a b
    | Equal: a = b -> order LT a b
    | More: LT b a -> order LT a b.
    
    
    
    Class Comparable (A: Type) :=
      { LT: relation A;
        compare: forall a b, order LT a b}.
    
    Notation "a < b" := (LT a b).
    
    
    Inductive rev_map (A B:Type) : Type :=
      | Nil:  rev_map A B
      | Node: rev_map B A -> A -> B -> rev_map B A -> rev_map A B.
    
    Implicit Arguments Nil [[A] [B]].
    Implicit Arguments Node [[A] [B]].
    
    
    Fixpoint insert `{Comparable A} `{Comparable B} (a:A) (b:B) (t: rev_map A B): rev_map A B :=
      match t with
      | Nil => Node Nil a b Nil
      | Node l u v r =>
          match compare a u with
          | Less _ => Node (insert b a l) u v r
          | _ => match compare b v with
                 | More _ => Node l u v (insert b a r)
                 | _ => Node l u b (insert v a r)
                 end
          end
      end.
    
    Fixpoint member `{Comparable A} `{Comparable B} (a:A) (b:B) (t: rev_map A B): bool:=
      match t with
      | Nil => false
      | Node l u v r =>
          match compare a u, compare b v with
          | Equal _ ,Equal _=> true
          | Less _ ,_ => member b a l
          | _,_    => member b a r
          end
      end.
    Après, je persiste à penser que pour débuter, http://www.cis.upenn.edu/~bcpierce/sf/ est l'idéal !!

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

    Par défaut

    Alors, tu en es où ?

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

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

    Comme je l'ai dit, grâce à l'aide de gasche, j'ai pu terminer la traduction en COQ dans le délai que je m'étais fixé.

    Citation Envoyé par gasche
    C'est bien, mais maintenant il faut prouver la correction
    Citation Envoyé par TropMDR
    Alors, tu en es où ?
    J'ai prouvé la terminaison
    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.

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

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    Comme je l'ai dit, grâce à l'aide de gasche, j'ai pu terminer la traduction en COQ dans le délai que je m'étais fixé.
    Sauf que comme je disais plus haut, son conseil de rajouter
    Code :
    Hypothesis compare : forall (C : Set), C -> C -> order.
    est mauvais puisque tu n'arriveras jamais à écrire une telle fonction !

    Citation Envoyé par SpiceGuid Voir le message
    J'ai prouvé la terminaison
    Tu as écrit la fonction donc :-D

  10. #10
    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

    TropMDR : j'ai proposé cet axiome dans le but de modéliser l'opérateur de comparaison polymorphe de OCaml. C'est effectivement un mauvais conseil (... et un mauvais opérateur) si le but est de tout implémenter en Coq, mais ça me semble un choix raisonnable dans une optique de spécification partielle; j'ai interprété le choix de SpiceGuid de définir la fonction de comparaison en axiome comme une optique "je me prends pas la tête sur cet aspect de l'algorithme", et dans ce cadre le choix me semble justifié.

    Je suis tout à fait d'accord sur le fait que ta version avec typeclasses est meilleure (en plus elle est tout à fait lisible). Cependant, je ne suis pas convaincu qu'elle permette intrinsèquement d'avoir plus d'assurance dans les bonnes propriétés de la version l'algorithme déjà codé en OCaml, comme j'ai l'impression que c'était le but ici.

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

    Par défaut

    Effectivement, si le but est de modéliser les fonctions de comparaison polymorphe de caml, cet axiome semble raisonnable, en l'extrayant proprement. J'étais resté dans une vision purement "coq" !

+ Répondre à la discussion
Cette discussion est résolue.

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
  •