Commit 3ca9a16d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

adaptation, renumérotation

parent 067199ea
TD2 : Premiers pas en Coq
======================
TD1 : Premieres preuves Coq
===========================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......@@ -95,7 +95,7 @@ Lemma E1F8 : (A -> B) -> ~B -> ~A.
Lemma E1F9 : ~~(A \/ ~A).
```
### Exercice 2 : Calcul des prédicats ###
### Exercice 2 : Calcul des prédicats ###
Après avoir effectué les déclarations suivantes:
```
......@@ -110,9 +110,9 @@ Lemma E2F2 : (exists x, A x \/ B x) <-> (exists x, A x) \/ (exists x, B x).
Lemma E2F3 : (exists y, forall x, R x y) -> forall x, exists y, R x y.
```
### Exercice 3 : Reprise ! ###
### Exercice 3 : Formalisation ###
Refaire en Coq les exercices 1 et 4 de la feuille de TD 1. Pour simuler la règle de raisonnement par l'absurde, on pourra déclarer l'axiome suivant:
Enoncer en Coq et prouver quelques questions des exercices 1 et 4 de ce [TD de logique](https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td1.pdf). Pour simuler la règle de raisonnement par l'absurde, on pourra déclarer l'axiome suivant:
```
Axiom not_not_elim : forall A : Prop, ~~A -> A.
```
TD4 : Mathématiques élémentaires en Coq
=======================================
TD1bis : Mathématiques élémentaires en Coq
==========================================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......
TD5 : Les entiers naturels en Coq
======================
TD2 : Preuves arithmétiques en Coq
==================================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......
TD6 : Les listes en Coq
=======================
TD3 : Preuves sur les listes Coq
================================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......
TD8 : Définitions inductives de prédicats
TD4 : Définitions inductives de prédicats
=========================================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......
TD9 : Définitions inductives de prédicats et analyse par cas
TD5 : Définitions inductives de prédicats et analyse par cas
============================================================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après A. Miquel)
......
Le Damier de Cachan
===================
TD6 : Le Damier de Cachan
=========================
M1 Informatique - Preuves Assistées par Ordinateur
M2 LMFI
Pierre Letouzey (d'après C. Paulin)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment