Initiation aux preuves formelles 2025 (en cours)

1. Semaine 1 (9 septembre)
• Transparents du CM1
• Logique1 (.v)
• Logique1 (web)
• Logique1, exercices supplémentaires (.v)
• Logique1, exercices supplémentaires (web)
2. Semaine 2 (16 septembre)
• Logique2 (.v)
• Logique2 (web)
• Logique2, exercices supplémentaires (.v)
• Logique2, exercices supplémentaires (web)
• Naturels1 (.v)
• Naturels1 (web)
• Naturels1, exercices supplémentaires (.v)
• Naturels1, exercices supplémentaires (web)
3. Semaine 3 (23 septembre)
• Naturels2 (.v)
• Naturels2 (web)
• Naturels2, exercices supplémentaires (.v)
• Naturels2, exercices supplémentaires (web)
• (Début de) Calcul des prédicats (.v)
• (Début de) Calcul des prédicats (web)
• (Début de) Calcul des prédicats, exercices supplémentaires (.v)
• (Début de) Calcul des prédicats, exercices supplémentaires (web)
4. Semaine 4 (30 septembre)
• (Suite et fin de) Calcul des prédicats (.v)
• (Suite et fin de) Calcul des prédicats (web)
• (Suite et fin de) Calcul des prédicats, exercices supplémentaires (.v)
• (Suite et fin de) Calcul des prédicats, exercices supplémentaires (web)
5. Devoir d'Octobre
À rendre sur moodle avant dimanche 12 octobre à 23h59
• Devoir à la maison d'octobre (.v)
• Devoir à la maison d'octobre (web)
6. Semaine 5 (7 octobre)
• TD1 (calcul, induction)
• Logique classique (.v)
• Logique classique (web)
7. Semaine 6 (14 octobre)
• TD1bis (preuves, encore)
• Raisonnement vers l'avant avec apply in (.v)
• Raisonnement vers l'avant avec apply in (web)
• Devoir numéro 2 (.v)
• Devoir numéro 2 (web)
8. Semaine 7 (4 novembre)
• Les réels comme corps (.v)
• Les réels comme corps (.html)
9. Semaine 8 (1O novembre)
• TD2 (apply et rewrite)
• Corps ordonné (.v)
• Corps ordonné (web)
10. Semaine 9 (18 novembre)
• Suite TD2 (apply et rewrite)
• Valeur absolue et distance (.v)
• Valeur absolue et distance (web)
11. Semaine 11 (2 décembre)
• Suites (.v)
Pour pouvoir utiliser la bibliothèque Pebble avec ce sujet~:

mkdir tp_suites
cd tp_suites
wget https://www.math.univ-paris13.fr/~rousselin/ipf/RSeq_sujet.v
git clone --depth 1 https://depot.lipn.univ-paris13.fr/rousselin/pebble
make -C pebble/
printf '%s\n' '-R pebble/theories/ Pebble' >_CoqProject
          

12. Pour réviser
• Sujet du partiel 1 2024
• Corrigé du partiel 1 2024
• TP noté de 2024 (.v)
• TP noté de 2024 (.html)