Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Langages fonctionnels Discussion :

[Coq] Travail sur les listes


Sujet :

Langages fonctionnels

  1. #1
    Nouveau Candidat au Club
    [Coq] Travail sur les listes
    Bonjours à tous,

    Je suis débutant en Coq, et je voudrais écrire une fonction tous_satisfont qui construit la proposition : tous les éléments d’une liste satisfont une proposition donnée.

    Après avoir essayé pdt plusieurs heures, je crois que mon prob vient de la non compréhension de ce que représentent exactement les fonctions / propositions etc...

    Y aurait-il une âme charitable prête à me donner la correction de ma fonction que je puisse décortiquer tout seul ? Voilà ce que j'ai tapé...

    Fixpoint tous_satisfont (l : liste) (P : int -> Prop) : Prop :=
    match l with
    | [ ] => tous_satisfont [ ] P
    | x :: l' => P x
    end.

  2. #2
    Membre émérite
    Citation Envoyé par HeatBurns
    Je suis débutant en Coq
    Moi aussi.
    Ton véritable handicap c'est que tu es également débutant en programmation fonctionnelle.

    Code Coq :Sélectionner tout -Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    Require Import Coq.Lists.List.
    
    Fixpoint for_all (A:Type) l (p : A -> bool) :=
      match l with
      | nil => true
      | h :: t => if p h then for_all A t p else false  
      end.
    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.