Initiation aux preuves formelles 2024 (en cours)
Fichiers (en cours de modification) pour le cours d'initiation aux
preuves formelles en L1 double-licence mathématiques et informatique
(premier semestre) pour l'année 2023 - 2024.
Pour utiliser ces fichiers, vous pouvez soit :
- installer Coq depuis
Coq platform
(sur Linux, nécessite le paquet
snap ou
passer
directement par opam)
et éditer les fichiers sources donnés ci-dessous avec un éditeur
de texte compatible (par exemple CoqIDE, qui est fourni avec).
- éditer et exécuter directement dans votre navigateur, mais la
sauvegarde et le chargement de votre travail
n'est pas encore prise en charge (vous devez sauvegarder à
côté ce que vous avez écrit).
- copier-coller les fichiers dans
le scratchpad de
jscoq et vous pourrez alors sauvegarder et charger comme avec un
éditeur de texte classique.
- Logique de base en Coq
- Cours magistral 1
- Entiers Naturels
- Devoir du 1er octobre 2024
- Sujets de TD (débranché) d'octobre
- Calcul des prédicats
- Cours magistral 2
- Logique classique
- Les réels comme corps
- Tactiques pour le raisonnement vers l'avant
- Les réels comme corps totalement ordonné
- Valeur absolue et distance sur le corps des réels
- Tactiques automatiques
- Convergence des suites numériques
- Devoir du 30 novembre 2024
- Sujets de TD (débranché) de novembre
- Sujets 0 de partiel sur papier