Commit b65f1321 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

TD1: minor changes

parent 27fca7e2
...@@ -33,7 +33,7 @@ Un point `.` sert de terminateur à chaque phrase Coq. ...@@ -33,7 +33,7 @@ Un point `.` sert de terminateur à chaque phrase Coq.
#### Exercice 1 : composition #### Exercice 1 : composition
Définir la fonction `compose : forall A B C, (B->C)->(A->B)->(A->C)`. Définir la fonction `compose : forall A B C, (B->C)->(A->B)->(A->C)`. La tester avec les fonctions `S` et `pred` des entiers `nat`.
#### Exercice 2 : pseudo-booléens #### Exercice 2 : pseudo-booléens
...@@ -42,7 +42,7 @@ Définir (sans utiliser `bool`): ...@@ -42,7 +42,7 @@ Définir (sans utiliser `bool`):
- un type `mybool : Type` - un type `mybool : Type`
- deux constantes `mytrue` et `myfalse` de type `mybool` - deux constantes `mytrue` et `myfalse` de type `mybool`
- une fonction `myif : forall A, mybool -> A -> A -> A` telle que `myif mytrue x y` se réduise en `x` et `myif myfalse x y` se réduise en `y` - une fonction `myif : forall A, mybool -> A -> A -> A` telle que `myif mytrue x y` se réduise en `x` et `myif myfalse x y` se réduise en `y`
#### Exercice 3 : entiers de Church #### Exercice 3 : entiers de Church
On cherche à encoder en Coq les entiers de Church, pour lesquels l'entier naturel `n` est représenté par `λfλx.(f (f (... (f x))))``f` est appliqué `n` fois. On cherche à encoder en Coq les entiers de Church, pour lesquels l'entier naturel `n` est représenté par `λfλx.(f (f (... (f x))))``f` est appliqué `n` fois.
...@@ -67,6 +67,7 @@ Définir également deux fonctions `nat2church : nat -> church` et `church2nat : ...@@ -67,6 +67,7 @@ Définir également deux fonctions `nat2church : nat -> church` et `church2nat :
- Même chose avec `checktauto2` et `checktauto3` pour des fonctions booléennes à 2 puis 3 arguments. On peut faire ça en énumerant à la main tous les cas, mais il y a évidemment plus malin, par exemple réutiliser `checktauto`. - Même chose avec `checktauto2` et `checktauto3` pour des fonctions booléennes à 2 puis 3 arguments. On peut faire ça en énumerant à la main tous les cas, mais il y a évidemment plus malin, par exemple réutiliser `checktauto`.
- Tester si `fun a b c => a || b || c || negb (a && b) || negb (a && c)` est une tautologie. - Tester si `fun a b c => a || b || c || negb (a && b) || negb (a && c)` est une tautologie.
NB: la commande `Open Scope bool_scope.` permet de disposer des notations `||` et `&&` (en lieu et place de `orb` et `andb`)
#### Exercice 5 : fonctions usuelles sur les entiers #### Exercice 5 : fonctions usuelles sur les entiers
......
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