Commit 067199ea authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

fichiers repris du depot cours-preuves

parent 211d905f
Cours de Preuves Assistées par Ordinateurs - Seance 1
=====================================================
## Quelques problèmes mathématiques célèbres
#### Théorème des 4 couleurs
<https://en.wikipedia.org/wiki/Four_color_theorem>
- Une carte plane et pas trop irrégulière (pas d'enclaves, de frontières fractales...) peut se colorier avec au plus 4 couleurs sans que deux pays avec une frontière commune aient la même couleur.
- Enoncé : 1852
- Pleins de preuves fausses ensuite...
- Preuve complète : 1976 par K. Appel et W. Haken
- Premier théorème important utilisant l'ordinateur, ~2000 sous-cas finis traités en ~100h de calculs à l'époque
- Pour beaucoup de mathématiciens, ceci n'était pas une preuve (les calculs sont-ils fiables ?)
- Preuve unifiée en Coq : 2005 par Georges Gonthier (et B. Werner). Raisonnement infini + calcul de 600 cas finis.
50k lignes de code Coq : <https://github.com/math-comp/fourcolor>
#### Théorème de Feit-Thompson
<https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem>
Tout groupe fini d'ordre impair est résoluble.
- Conjecture : Burnside 1911
- Démonstration : Feit et Thompson 1963 (250 pages)
- Etape essentielle pour la classification des groupes finis simples.
Fait intervenir beaucoup d'algèbre moderne.
- Preuve Coq : 2006-2012 G. Gonthier et son équipe (40k lignes)
<https://github.com/math-comp/odd-order>
#### Conjecture de Kepler
<https://en.wikipedia.org/wiki/Kepler_conjecture>
Maintenant Théorème de Kepler...
La manière la plus compacte de disposer des sphères dans l'espace est CFC (Cubique Face Centrée).
Densité obtenue : `π/√18` (environ 70%)
Enoncé : 1611
Preuve : Thomas Hales 1998 (+100 pages, 3Go de programmes et données)
Publication : seulement 2006, avec avertissement des relecteurs (99% confiants, mais pas sur les calculs informatiques)
Preuve formelle : projet flyspeck 2003-2014.
HOL Light (avec des bouts intermediaires en Isabelle, Coq utilisé aussi à un moment).
Un morceau demandant ~5000h CPU à l'époque ! Le reste de l'ordre de l'heure CPU.
<https://github.com/flyspeck/flyspeck>
<https://arxiv.org/abs/1501.02155>
#### Théorème de Fermat
<https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem>
Enoncé : Fermat, vers 1670
Preuve : Andrew Wiles en 1994.
Utilise directement ou indirectement une large partie des mathématiques du 20e siècle (courbes elliptiques, ...).
Preuve formelle : non
## Au fait, il reste encore des conjectures à prouver !
#### Conjecture de Goldbach
<https://fr.wikipedia.org/wiki/Conjecture_de_Goldbach>
Tout nombre entier pair > 3 peut s’écrire comme la somme de deux nombres premiers.
Enoncé : C. Goldbach (1742)
#### Conjecture de Collatz (ou de Syracuse)
<https://en.wikipedia.org/wiki/Collatz_conjecture>
En partant d'un entier > 0, et en répétant le processus suivant, on atteint toujours 1 un jour :
division par deux des nombres pairs et passage à `3x+1` pour les autres nombres `x`.
Enoncé : Lothar Collatz (1937)
#### Hypothèse de Riemann
<https://en.wikipedia.org/wiki/Riemann_hypothesis>
## Du côté Informatique
## Complexité de gros projets informatiques modernes
- Noyau linux : 20 Mloc
- GCC : 7 Mloc
En comparaison, Coq c'est 270kloc de sources OCaml et 230 kloc de bibliothèques de preuves.
Et son noyau sur lequel repose la validation des preuves c'est environ 30 kloc.
#### Projet Compcert
Compilateur certifié de C vers différents assembleurs (ppc, arm, x86, x86_64, RISC-V).
Quelques détails de C manquent (mais traite 99% de la norme).
Efficacité proche de `gcc -O1`, nettement meilleur que `gcc -O0`.
Auteur : Xavier Leroy et son équipe
Première version : 2008
Taille : environ 180k lignes de Coq
<https://en.wikipedia.org/wiki/CompCert>
## Des situations plus quotidiennes
#### split
Au détour d'un autre cours, une preuve d'équivalence de deux fonctions OCaml:
```ocaml
let rec split1 = function
| [] -> ([],[])
| a::l -> let (l1,l2) = split1 l in (a::l2,l1)
let rec split2 = function
| [] -> ([],[])
| [a] -> ([a],[])
| a::b::l -> let (l1,l2) = split2 l in (a::l1,b::l2)
```
#### Une fonction d'Hofstadter
<https://www.irif.fr/~letouzey/hofstadter_g/>
<https://hal.inria.fr/hal-01195587/document>
Au départ, une "simple" étude de la fonction récursive `g(n) = n - g(g(n-1))` (avec valeur initiale `g 0 = 0`).
Mais on tombe vite sur des choses délicates (multiples cas, plusieurs pages de preuves).
Et au moins un article publié sur le sujet (en 1986) a son résultat principal totalement faux!
Donc ici Coq vient en renfort pour s'assurer que les preuves de cette étude sont justes
#### Sudoku
Un bon exemple pour montrer que même sur un domaine fini, tout traduire en formules booléennes et lancer un sat-solver peut donner des résultats rapides, mais qui peuvent être difficiles à relire et à croire par un humain (formules à milliers de variables, programmes boites-noires ne détaillant pas pourquoi une formule est "unsat").
module Demo where
-- NB: Attention aux conventions syntaxiques d'agda:
-- A part ( ) et { } tout peut faire parti d'un nom d'identifieur
-- Par exemple 1+2x représente un identifieur valide
-- qui diffère de 1 + 2 * x.
-- Bref, il faut des blancs presque partout !!
-- NB: Attention aussi aux symboles unicodes
-- (p.ex. lors de copier-coller depuis le web) :
-- * et ∗ ne sont pas les mêmes caractères !!
-- Les entiers : definitions
data Nat : Set where
O : Nat
S : Nat -> Nat
_+_ : Nat -> Nat -> Nat
O + m = m
S n + m = S (n + m)
_*_ : Nat -> Nat -> Nat
O * m = O
S n * m = m + (n * m)
infixl 6 _+_
infixl 8 _*_
-- Pour utiliser les entiers habituels 0 1 2 3 4 ...
{-# BUILTIN NATURAL Nat #-}
example : Nat
example = 1 + 2 * 3
-- Un peu de logique...
data True : Set where
tt : True
data False : Set where -- pas de constructeur, False est donc vide
FalseElim : {A : Set} -> False -> A
FalseElim ()
-- ce () est le pattern vide, impossible (donc sans code à droite)
-- on peut aussi ecrire : FalseElim = λ ()
data And (A B : Set) : Set where
conj : A -> B -> And A B
data Or (A B : Set) : Set where
left : A -> Or A B
right : B -> Or A B
OrElim : {A B C : Set} -> Or A B -> (A -> C) -> (B -> C) -> C
OrElim (left a) ac bc = ac a
OrElim (right b) ac bc = bc b
data Exists (A : Set) (P : A -> Set) : Set where
exintro : (x : A) -> P x -> Exists A P
-- On a plusieurs possibilités pour énoncer des égalités d'entiers
-- (et en faire les preuves)
module LeibnizEq where
-- Une définition générique de l'égalité (dite de Leibniz)
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
infix 4 _≡_
what-is-example : example ≡ 7
what-is-example = refl
sym : forall {A} -> {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl
trans : forall {A} -> {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
trans refl refl = refl
cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
cong f refl = refl
eqS : {n m : Nat} -> n ≡ m -> S n ≡ S m
eqS = cong S
injS : forall {n m} -> S n ≡ S m -> n ≡ m
injS refl = refl
plusO : forall n -> n + O ≡ n
plusO O = refl
plusO (S n) = eqS (plusO n)
plusS : forall n m -> n + S m ≡ S (n + m)
plusS O m = refl
plusS (S n) m = eqS (plusS n m)
-- NB: pour pluscom, c'est mieux d'analyser m,
-- ça nous amène exactement à plusO et plusS.
-- Si on analyse n, il faudra insérer des sym.
pluscom : forall n m -> n + m ≡ m + n
pluscom n O = plusO n
pluscom n (S m) = trans (plusS n m) (eqS (pluscom n m))
plusassoc : forall n m p -> n + (m + p) ≡ n + m + p
plusassoc O m p = refl
plusassoc (S n) m p = eqS (plusassoc n m p)
module ComputeEq where
-- Autre possibilité: une égalité définie comme une
-- fonction répondant True ou False.
-- Interet : des calculs dans les goals
-- Souci : les arguments implicites marchent mal (cf Refl...)
infix 4 _==_
_==_ : Nat -> Nat -> Set
O == O = True
S n == S m = n == m
_ == _ = False
what-is-example : example == 7
what-is-example = tt
refl : {n : Nat} -> n == n
refl {O} = tt
refl {S n} = refl {n}
sym : {n m : Nat} -> n == m -> m == n
sym {O} {O} tt = tt
sym {S n} {S m} h = sym {n} {m} h
sym {O} {S _} h = h
sym {S _} {O} h = h
trans : {n m p : Nat} -> n == m -> m == p -> n == p
trans {O} {O} {_} h g = g
trans {O} {S _} {_} h g = FalseElim h
trans {S _} {O} {_} h g = FalseElim h
trans {S _} {S _} {O} h g = FalseElim g
trans {S n} {S m} {S p} h g = trans {n} {m} {p} h g
plusO : forall n -> n + O == n
plusO O = tt
plusO (S n) = plusO n
plusS : forall n m -> n + S m == S (n + m)
plusS O m = refl {m}
plusS (S n) m = plusS n m
pluscom : forall n m -> n + m == m + n
pluscom n O = plusO n
pluscom n (S m) =
trans {n + S m} {_} {_}
(plusS n m)
(pluscom n m)
plusassoc : forall n m p -> n + (m + p) == n + m + p
plusassoc O m p = refl {m + p}
plusassoc (S n) m p = plusassoc n m p
-- Preuves d'equivalence avec Leibniz
open LeibnizEq using (_≡_) renaming (refl to leib-refl; eqS to leib-eqS)
toLeibniz : {n m : Nat} -> n == m -> n ≡ m
toLeibniz {O} {O} h = leib-refl
toLeibniz {S n} {S m} h = leib-eqS (toLeibniz h)
toLeibniz {O} {S _} h = FalseElim h
toLeibniz {S _} {O} h = FalseElim h
fromLeibniz : {n m : Nat} -> n ≡ m -> n == m
fromLeibniz {n} leib-refl = refl {n}
module IndEq where
-- Une dernière possibilité à la mode actuellement:
-- l'égalité sur les entiers vue comme prédicat inductif
-- spécialisé aux entiers.
-- Fonctionne de façon similaire à Leibniz
infix 4 _==_
data _==_ : Nat -> Nat -> Set where
eqO : O == O
eqS : forall {n m} -> n == m -> S n == S m
what-is-example : example == 7
what-is-example = eqS (eqS (eqS (eqS (eqS (eqS (eqS eqO))))))
refl : {n : Nat} -> n == n
refl {O} = eqO
refl {S n} = eqS refl
what-is-example-bis : example == 7
what-is-example-bis = refl
injS : forall { n m } -> S n == S m -> n == m
injS (eqS h) = h
sym : {n m : Nat} -> n == m -> m == n
sym eqO = eqO
sym (eqS h) = eqS (sym h)
trans : {n m p : Nat} -> n == m -> m == p -> n == p
trans eqO eqO = eqO
trans (eqS h) (eqS g) = eqS (trans h g)
plusO : forall n -> n + O == n
plusO O = eqO
plusO (S n) = eqS (plusO n)
plusS : forall n m -> n + S m == S (n + m)
plusS O m = refl
plusS (S n) m = eqS (plusS n m)
pluscom : forall n m -> n + m == m + n
pluscom n O = plusO n
pluscom n (S m) = trans (plusS n m) (eqS (pluscom n m))
plusassoc : forall n m p -> n + (m + p) == n + m + p
plusassoc O m p = refl
plusassoc (S n) m p = eqS (plusassoc n m p)
-- Preuves d'equivalence avec Leibniz
open LeibnizEq using (_≡_) renaming (refl to leib-refl; eqS to leib-eqS)
toLeibniz : {n m : Nat} -> n == m -> n ≡ m
toLeibniz eqO = leib-refl
toLeibniz (eqS h) = leib-eqS (toLeibniz h)
fromLeibniz : {n m : Nat} -> n ≡ m -> n == m
fromLeibniz leib-refl = refl
-- NB: pour les preuves automatisables, il y a un système
-- de "reflection" (meta-programming), qui se rapproche fortement
-- des tactiques de Coq !!
-- Voir:
-- https://agda.readthedocs.io/en/v2.5.4.1/language/reflection.html
-- https://oisdk.github.io/agda-ring-solver/README.html
module TypeDep where
-- Rappel: le type vide représentant la proposition False
data False : Set where
-- Rappel: l'egalité de Leibniz
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
infix 4 _≡_
-- Rappel: les entiers et l'addition
data Nat : Set where
O : Nat
S : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}
_+_ : Nat -> Nat -> Nat
O + m = m
S n + m = S (n + m)
infixl 6 _+_
-- Pour comparer, une structure de donnée non-dépendante : les listes
data List (A : Set) : Set where
Nil : List A
Cons : A -> List A -> List A
exampleList : List Nat
exampleList = Cons 3 (Cons 5 Nil)
-- Type dependant : les vecteurs de taille n
data Vec (A : Set) : Nat -> Set where
VNil : Vec A O
VCons : {n : Nat} -> A -> Vec A n -> Vec A (S n)
exampleVec : Vec Nat 2
exampleVec = VCons 3 (VCons 5 VNil)
head : forall {n A} -> Vec A (S n) -> A
head (VCons x _) = x
-- Interet: head VNil est exclu par typage !
app : forall {n m A} -> Vec A n -> Vec A m -> Vec A (n + m)
app VNil v = v
app (VCons x v1) v2 = VCons x (app v1 v2)
-- Inconvenient: Vec A (n+1) n'est pas la meme chose que Vec A (1+n)
-- donc la definition suivante de rev est refusee
--rev : forall {n A} -> Vec A n -> Vec A n
--rev VNil = VNil
--rev (VCons x v) = app (rev v) (VCons x VNil)
-- Il faut une coercion entre ces types, soit manuelle:
coerc_one : forall {n A} -> Vec A (n + 1) -> Vec A (S n)
coerc_one {O} v = v
coerc_one {S n} (VCons x v) = VCons x (coerc_one v)
rev : forall {n A} -> Vec A n -> Vec A n
rev VNil = VNil
rev (VCons x v) = coerc_one (app (rev v) (VCons x VNil))
-- Soit une coercion generale basee sur l'egalite:
coerc : forall {n m A} -> Vec A n -> n ≡ m -> Vec A m
coerc v refl = v
cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y
cong f refl = refl
plusone : forall {n} -> n + 1 ≡ S n
plusone {O} = refl
plusone {S n} = cong S plusone
rev' : forall {n A} -> Vec A n -> Vec A n
rev' VNil = VNil
rev' (VCons x v) = coerc (app (rev' v) (VCons x VNil)) plusone
-- Autre type dependant : des ensembles à cardinal donné
-- (Fin n) est un type à exactement n element.
-- (Fin n) peut aussi être vu comme le type des entiers naturels < n
data Fin : Nat → Set where
zero : {n : _} → Fin (S n)
suc : {n : _} → Fin n → Fin (S n)
-- Fin 0 est vide : on a ex-falso-quodlibet, tout comme pour False
noFin0 : {A : Set} -> Fin 0 -> A
noFin0 ()
uniqFin1 : Fin 1
uniqFin1 = zero
Fin1Singleton : (n m : Fin 1) -> n ≡ m
Fin1Singleton zero zero = refl
Fin1Singleton (suc ()) _
Fin1Singleton _ (suc ())
firstOf3 : Fin 3
firstOf3 = zero
secondOf3 : Fin 3
secondOf3 = suc zero
thirdOf3 : Fin 3
thirdOf3 = suc (suc zero)
-- Utilisation de Fin : acces garanti dans les bornes d'un vecteur
nth : forall {A n} -> Vec A n -> Fin n -> A
nth (VCons a _) zero = a
nth (VCons _ l) (suc m) = nth l m
-- Conversion List<->Vec
Vec2List : forall {A n} -> Vec A n -> List A
Vec2List VNil = Nil
Vec2List (VCons x l) = Cons x (Vec2List l)
len : forall {A} -> List A -> Nat
len Nil = O
len (Cons _ l) = S (len l)
List2Vec : forall {A} -> (l : List A) -> Vec A (len l)
List2Vec Nil = VNil
List2Vec (Cons a l) = VCons a (List2Vec l)
(** Rules of HOL Light : https://en.wikipedia.org/wiki/HOL_Light *)
(** See also Hol-light Tutorial :
http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
*)
#use "hol.ml";;
(* or use a saved snapshot, for instance via dmtcp: ./dmtcp_restart_script.sh *)
(o);;
`x+1`;;
#remove_printer pp_print_qterm;;
`x+10`;;
#install_printer pp_print_qterm;;
REFL `x:num`;;
ARITH_RULE
`(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
(a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 =
(a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 +
(a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;
TAUT `p \/ ~p ==> F <=> ~T`;;
infixes();;
`(x:'a)=y ==> y=x`;;
(** preuves en style "pedestre" *)
let sym1 =
MK_COMB (REFL `(=):'a->'a->bool`,
ASSUME `(x:'a)=y`);;
let sym2 = MK_COMB (sym1, REFL `x:'a`);;
let sym3 = EQ_MP sym2 (REFL `x:'a`);;
let full_sym =
EQ_MP (MK_COMB (MK_COMB (REFL `(=):'a->'a->bool`,
ASSUME `(x:'a)=y`),
REFL `x:'a`))
(REFL `x:'a`);;
(** Et la transitivité (règle de base, mais "superflue"...) *)
let trans =
EQ_MP
(MK_COMB (REFL `(=) (x:'a)`, ASSUME `(y:'a)=z`))
(ASSUME `(x:'a)=y`);;
TRANS (ASSUME `(x:'a)=y`) (ASSUME `(y:'a)=z`);;
(** version abstraite de la symetrie *)
let SYM th =
let tm = concl th in
let l,r = dest_eq tm in
let eq = rator (rator tm) in
let lth = REFL l in
EQ_MP (MK_COMB(MK_COMB (REFL eq,th),lth)) lth;;
let sym_again = SYM (ASSUME `(x:'a)=y`);;
(** preuves "interactives" *)
g `(x:'a)=y ==> y=x`;;
e DISCH_TAC;;
e (ASM_REWRITE_TAC[]);;
b () (* backtrack in the proof *)
e (CLAIM_TAC "helper" `((x:'a)=x) <=> (y=x)`);;
e MK_COMB_TAC;;
e MK_COMB_TAC;;
e REFL_TAC;;
e (FIRST_ASSUM ACCEPT_TAC);;
e REFL_TAC;;
e (FIRST_ASSUM (fun h -> ACCEPT_TAC (EQ_MP h (REFL `x:'a`))));;
(*ou:
(USE_THEN "helper" (fun h -> ACCEPT_TAC (EQ_MP h (REFL `x:'a`))));;
*)