Initiation aux preuves formelles

Initiation aux preuves formelles 2023 (in progress)

Fichiers (en cours de modification) pour le cours d'initiation aux preuves formelles en L1 double-licence mathématiques et informatique (premier semestre). 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 intuitionniste

Entiers Naturels

Calcul des prédicats

Devoir à la maison d'Octobre

Logique classique

Les réels comme corps

Tactiques pour le raisonnement vers l'avant

Les réels comme corps totalement ordonné

Devoir de Décembre

Partiel du 12 décembre

Valeur absolue et distance sur le corps des réels

Tactiques automatiques

Convergence des suites numériques

Initiation aux preuves formelles 2022

These are the 2022 "initiation aux preuves formelles" files, as given to the students. They are in french and are given "as is", they need polishing.
I'd be happy if you try these out and give feedbacks (questions are also welcome!) To do so:

You may use a jscoq website as this one https://coq.vercel.app/ and copy-paste a file in a scratchpad
You can install Coq from Coq platform and open the files in CoqIDE (or in your favorite editor with a Coq plugin).

Additional material:

A list of useful lemmas in N

A list of useful lemmas in R