Preuves élémentaires

Exercice 61

Définir un type proposition avec Vrai, Faux, conjonction, disjonction, négation, implication, équivalence et variable.

Solution 61

type proposition =
  True
| False
| Or  of proposition * proposition
| And of proposition * proposition 
| Not of proposition
| Imply of proposition * proposition
| Equivalent of proposition * proposition
| Variable of string;;
Type proposition defined.

Exercice 62

Définir un type environnement associant à des variables des valeurs true ou false. Définir dans la même foulée une fonction retrouvant à partir d'une variable et d'un environnement sa valeur associée.

Solution 62

type environnement == liaison list
and liaison = \camlbslash{}{variable : proposition ; valeur : bool\camlbslash{}};;
Type environnement defined.
Type liaison defined.
let rec valeur_variable variable environnement =
  match environnement with
    [] -> failwith "No such variable"
  | \camlbslash{}{variable = v; valeur = valeur\camlbslash{}} :: reste -> 
        if v = variable then valeur else valeur_variable variable reste;;
valeur_variable : proposition -> liaison list -> bool = <fun>

Exercice 63

Écrire la fonction evaluer prenant une proposition et un environnement et calculant la valeur de vérité de la proposition vis-à-vis des valeurs conférées aux variables par l'environnement.

Solution 63

Notez dans ce qui suit la fonction eval interne partageant la variable par le contexte lexical.

let evaluer proposition environnement =
  let rec eval = function 
    True -> true
  | False -> false
  | Or(p1, p2) -> eval p1 or eval p2
  | And(p1, p2) -> eval p1 & eval p2
  | Not(p) -> not (eval p)
  | Imply(p1, p2) -> not (eval p1) or eval p2
  | Equivalent(p1, p2) -> eval p1 = eval p2
  | Variable(_) as p -> valeur_variable p environnement
  in eval proposition;;
evaluer : proposition -> liaison list -> bool = <fun>

La seule chose complexe est la définition de l'implication. La proposition p -> q est équivalente à ( NOT p) OR q car l'implication est toujours vraie quand p est faux mais n'est vraie, lorsque p est vraie, que si q est vraie.

Exercice 64

Définir une fonction extrayant les variables d'une proposition. Tâchez que votre solution ne consomme que l'exact nombre de :: nécessaires bref, qu'elle soit linéaire en le nombre de variables extraites. Attention aux variables qui apparaissent plusieurs fois, elles ne doivent être comptées qu'une unique fois.

Solution 64

let extraire_variables p =
  let rec extraire p variables =
    match p with
      True -> variables
    | False -> variables
    | Or(p1, p2) -> extraire p1 (extraire p2 variables)
    | And(p1, p2) -> extraire p1 (extraire p2 variables)
    | Not(p) -> extraire p variables
    | Imply(p1, p2) -> extraire p1 (extraire p2 variables)
    | Equivalent(p1, p2) -> extraire p1 (extraire p2 variables)
    | Variable(_) as p -> if mem p variables then variables
                          else p :: variables
  in extraire p [];;
extraire_variables : proposition -> proposition list = <fun>

Exercice 65

Pour vérifier une formule ayant p, q, ... comme variables, il suffit de la vérifier pour toutes les combinaisons de valeurs que peuvent prendre p, q, .... Définissez donc une fonction prenant une proposition et vérifiant si elle est une tautologie. On pourra éprouver sa solution sur:

let p = Variable("p")
and q = Variable("q")
and r = Variable("r");;
p : proposition = Variable "p"
q : proposition = Variable "q"
r : proposition = Variable "r"
verifier_tautologie p;;
- : bool = false
verifier_tautologie (Or(p, Not(p)));;
- : bool = true
verifier_tautologie (Imply(p, p));;
- : bool = true
verifier_tautologie (Equivalent(p, Not(Not(p))));;
- : bool = true
(* Loi de Morgan *)
verifier_tautologie (Imply (Not(And(p,q)), Or(Not(p),Not(q))));;
- : bool = true
(* Plus complexe *)
verifier_tautologie 
  (Imply (Imply(Imply(Variable("p"), Variable("q")),Variable("r")),
          Imply(Variable("p"), Imply(Variable("q"),Variable("r")))) );;
- : bool = true
verifier_tautologie 
  (Imply (Imply(Variable("p"), Imply(Variable("q"),Variable("r"))),
          Imply(Imply(Variable("p"), Variable("q")),Variable("r")) ));;
- : bool = false

Solution 65

let verifier_tautologie p =
  let variables = extraire_variables p in
  let rec conferer_valeur variables environnement = 
    match variables with
      [] -> evaluer p environnement
    | v :: autres -> 
          conferer_valeur autres
                          (\camlbslash{}{variable = v; valeur = true\camlbslash{}} :: environnement)
        & conferer_valeur autres
                          (\camlbslash{}{variable = v; valeur = false\camlbslash{}} :: environnement)
  in conferer_valeur variables [];;
verifier_tautologie : proposition -> bool = <fun>

Exercice 66

L'implication et l'équivalence peuvent être considérées comme non primitives. Définir une fonction les convertissant en leur équivalent plus simple.

Solution 66

let rec simplifier = function
  True -> True
| False -> False
| Or(p1, p2) -> Or( simplifier(p1), simplifier(p2) )
| And(p1, p2) -> And( simplifier(p1), simplifier(p2) )
| Not(p) -> Not( simplifier(p) )
| Imply(p1, p2) -> Or( Not(simplifier(p1)), simplifier(p2) )
| Equivalent(p1, p2) -> simplifier (And(Imply(p1, p2), Imply(p2, p1)))
| Variable(_) as p -> p;;
simplifier : proposition -> proposition = <fun>

Exercice 67

Lorsqu'une proposition n'est pas une tautologie, produire une réfutation c'est-à-dire l'environnement tel que la proposition soit fausse. Dans le cas d'une tautologie, la fonction retournera l'environnement vide. On utilisera avec fruit des exceptions.

refuter p;;
- : liaison list = [\camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}]
refuter (simplifier
  (Imply (Imply(Variable("p"), Imply(Variable("q"),Variable("r"))),
          Imply(Imply(Variable("p"), Variable("q")),Variable("r")) )) );;
- : liaison list =
 [\camlbslash{}{variable = Variable "r"; valeur = false\camlbslash{}};
  \camlbslash{}{variable = Variable "q"; valeur = true\camlbslash{}};
  \camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}]

Solution 67

Cette fonction retourne l'environnement de réfutation ou [] si la proposition est une tautologie.

exception Refutation of environnement;;
Exception Refutation defined.
let refuter p = 
  let variables = extraire_variables p in
  let rec conferer_valeur variables environnement = 
    match variables with
      [] -> if not (evaluer p environnement)
            then raise (Refutation environnement)
    | v :: autres -> 
         let env1 = \camlbslash{}{variable = v; valeur = true\camlbslash{}} :: environnement 
         and env2 = \camlbslash{}{variable = v; valeur = false\camlbslash{}} :: environnement in
         conferer_valeur autres env1;
         conferer_valeur autres env2
  in try begin conferer_valeur variables []; [] end
     with Refutation(env) -> env
     |    _ -> [];;
refuter : proposition -> liaison list = <fun>
refuter p;;
- : liaison list = [\camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}]
refuter (simplifier
  (Imply (Imply(Variable("p"), Imply(Variable("q"),Variable("r"))),
          Imply(Imply(Variable("p"), Variable("q")),Variable("r")) )) );;
- : liaison list =
 [\camlbslash{}{variable = Variable "r"; valeur = false\camlbslash{}};
  \camlbslash{}{variable = Variable "q"; valeur = true\camlbslash{}};
  \camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}]