[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.

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:

---

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.

---