Discussion :

[HeatBurns]

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.

[SpiceGuid]

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.