Propositions-fr.pml

Calcul propositional : définitions et sémantique

open bool
open unary_nat

Propositions

(line=10, char=231) Les propositions logiques sont l'analogues des polynômes, mais lorsque l'on travaille avec les booléens ({0,1}, {Vrai,Faux}, ...) et leurs opérations usuelles (et, ou, non, ...) au lieu des nombres.

(line=15, char=446) Une proposition est contruite à partir d'un ensemble fini de variables (dites variables propositionnelles) et donc des opérations usuelles que l'on nomme connecteur logique. Comme pour les polynômes, il faut bien distinguer l'expression de la proposition (qui est un arbre avec des décorations pour noter le nom des variables et des connecteurs) de la valeur de la proposition (vraie au fausse) qui ne peut se calculer que lorsque l'on connait la valeur des variables.

(line=24, char=956) Si dessous on définit le type des propositions en considérant quatre connecteurs logique (conjonction, disjonction, implication et négation). Par ailleurs, le type est paramétré par le type des variables qui peuvent ainsi être représenter par des chaînes, des entiers, etc ...

type rec prop var = [
| PTrue[] | PFalse[]
| Var[var]
| Neg[prop var]
| Conj[prop var * prop var]
| Disj[prop var * prop var]
| Impl[prop var * prop var]
| Equi[prop var * prop var]
]

(line=41, char=1455) Le type précédent permet de définit quelques propositions:

val A:(prop unat) = Var[1]
val B:(prop unat) = Var[2]
val C:(prop unat) = Var[3]

val excluded_middle:(prop unat) = Disj[A, Neg[A]]
val pierce_law:(prop unat) = Impl[Impl[Impl[A,B],A],A]
val eq_associative:(prop unat) =
  Equi[Equi[A,Equi[B,C]],Equi[Equi[A,B],C]]

Exercise: 1 star

(line=53, char=1819) Écrivez quelques proposition supplémentaires.

(* FILL IN HERE *)

(line=56, char=1894) Le type précédent définit juste un ensemble d'arbre avec

Semantique des propositions: valuation, tautologie and satisfaction

(line=69, char=2422) Une valuation est une fonction totales de variables dans les booléens a value to each variable:

type valuation var = (var => bool)

(line=73, char=2566) Voici deux valuations particulière:

val true__val x = true
val false__val x = false

(line=77, char=2659) Here is a function to change only the value of one variable in a valuation:

val (var) set :(var => bool => valuation var => valuation var)
=
   fun x b v -> (fun y -> if x == y then b else v y)

private test _ |- (set 2 true false__val) 2 == true
proof 8<
private test _ |- (set 2 true false__val) 3 == false
proof 8<

(line=88, char=2989) Enfin voici la définition de la sémantique d'une proposition. La valeur d'une variable est fournie par la valuation, dans tous les autres cas, on utilise la fonction booléenne correspondantes, qui est définie dans le module bool de PML dont voici un extrait:

(line=93, char=3267) type bool = True[] | False[]

(line=95, char=3303) val not x = match x with true -> false | false -> true

(line=97, char=3363) val or x y = ( synonyme: a || b ) match x with true -> true | false -> y

(line=100, char=3448) val and x y = ( synonyme: a && b ) match x with false -> false | true -> y

(line=103, char=3535) val imply x y = ( synonyme: a => b ) match x with false -> true | true -> y

(line=106, char=3623) val equiv x y = ( synonyme: a <=> b ) ...

(line=109, char=3677) Attention 'A => B' est utilisé à la fois dans le monde des types pour les fonctions totales du type A dans le type B, mais aussi pour l'implication entre le booléen A et le booléen B. Le syntaxe de PML fait que l'on sait toujours, à une position données, si l'on attend un type ou une valeur.

(line=115, char=3997) La notation (var) en début de fonction indique que cette fonction est définie quelque-soit le type var que l'on choisit pour les variables. On parle de fonctions polymorphes.

val rec (var) value:(valuation var => prop var => bool) v p =
  match p with
  | Var[x] -> v x
  | Neg[p] -> not (value v p)
  | Conj[p,q] -> (value v p) && (value v q)
  | Disj[p,q] -> (value v p) || (value v q)
  | Impl[p,q] -> (value v p) => (value v q)
  | Equi[p,q] -> (value v p) <=> (value v q)
  | PTrue[] -> true
  | PFalse[] -> false

(line=130, char=4544) On peut tester cette sémantique

private test _ |- value $true excluded_middle == true proof 8<
private test _ |- value $false excluded_middle == true proof 8<

Exercise: 1 star

(line=135, char=4741) Écrivez plus de tests.

(* FILL IN HERE *)

Normal Forms

Reduire le jeu de connecteurs

(line=144, char=4936) On va d'abord montrer que l'on peut encoder une formule avec seulement le et, le ou et la négation. On définit le type réduit.

type rec and_or_prop var = [
| PTrue[] | PFalse[]
| Var[var]
| Neg[and_or_prop var]
| Conj[and_or_prop var * and_or_prop var]
| Disj[and_or_prop var * and_or_prop var]
]

Exercise: 2 star

(*  Avec PML, on a du sous-typage et toute valeur de type [and_or_prop var]
    peut être utilisé comme une valeur de type [prop var]. Comme l'illustre
    la définition suivante, qu'il vous faut compléter.
*)

private (var) test_subtype:(and_or_prop var => prop var) =
  fun p -> p

val rec (var) prop_to_and_or:(prop var => and_or_prop var) f =
  match (f:prop var) with
    | (PTrue[] | PFalse[] | Var[_]) as g -> g
    | Neg[g]    -> Neg[prop_to_and_or g]
    | Conj[g,h] -> Conj[prop_to_and_or g, prop_to_and_or h]
    | Disj[g,h] -> Disj[prop_to_and_or g, prop_to_and_or h]
    | Impl[g,h] -> Disj[Neg[prop_to_and_or g], prop_to_and_or h]
    | Equi[g,h] -> ({- FILL IN HERE -}: and_or_prop var)

private test _ |- prop_to_and_or Impl[A,B] == Disj[Neg[A],B]
proof 8<

(line=177, char=6056) Une subtilité dans la définition précédente: f dans match f with a le type prop var et si on avait écrit

(line=181, char=6181) | (PTrue[] | PFalse[] | Var[_]) -> f

(line=183, char=6227) PML n'aurait pas accepté, car le type du résultat doit être

(line=185, char=6295) and_or_prop var. Au lei de faire trois cas, on a écrit

(line=187, char=6358) | (PTrue[] | PFalse[] | Var[_]) as g -> g

(line=189, char=6408) et PML donne le type PTrue[] | PFalse[] | Var[var] à la variable g . Cela suffit car ce type est une sous-type du type and_or_prop var.

(line=193, char=6574) On peut maintenant montrer que le fonction précédente est correcte, c'est à dire qu'elle ne change pas la sémantique. Il faut décommenter le 8< lorsque vous avez fini la fonction précédente.

val rec (var) prop_to_and_or_correct v:(valuation var) f:(prop var)
  |- value v f == value v (prop_to_and_or f)
proof
  match f with
  | PTrue[] -> deduce prop_to_and_or f == f; 8<
  | PFalse[] -> 8<
  | Var[_] -> 8<
  | Neg[g as h] | Conj[g,h]   | Disj[g,h] | Impl[g,h]   | Equi[g,h] ->

(line=204, char=7078) Ici, on va dire que l'on applique l'hypothèse d'induction pour les deux sous-formules g et h. On écrit explicitement ce que l'on obtient pour avoir une preuve plus lisible. On laisse ensuite faire PML.

(line=209, char=7305) Remarquez l'astuce dans le cas de la négation pour que g et h soit bien tous les deux définis

    deduce value v g == value v (prop_to_and_or g) by prop_to_and_or_correct v g;
    deduce value v h == value v (prop_to_and_or h) by prop_to_and_or_correct v h;

(line=214, char=7591) Le proof_depth ci-dessous indique à PML de chercher lui même une analyse de cas en ce basant sur les évaluations qui sont bloquées. En fait, l'analyse de cas est simple, il suffit de distinguer 4 cas suivant les valeurs de value v g et value v h

    #set proof_depth = 2 in {- FILL IN HERE -}

Faire descendre les négations

(line=223, char=7971) En utilisant les lois de De Morgan (cf https://fr.wikipedia.orgwikiLoisdeDe_Morgan), on peut amener toutes les négations au niveau des variables (et en même temps éliminer les doubles négations

(line=228, char=8193) Voici d'abord la définition du type des formules avec les négations au niveau des feuilles de l'arbre:

(line=231, char=8303) On définit d'abord le type des litteraux: une variable ou sa négation.

type only_var var = [ Var[var] ]
type litteral var =
  [ Var[var]
  | Neg[only_var var] ]

(line=239, char=8483) On garde le constructeur Var[var] dans le cas de la négation pour q'un litteral soit encore de type prop var

(line=242, char=8609) On peut alors donner le type des propositions que l'on cherche:

type rec and_or_lit_prop var = [
  litteral var
| PTrue[] | PFalse[]
| Conj[and_or_lit_prop var * and_or_lit_prop var]
| Disj[and_or_lit_prop var * and_or_lit_prop var]
]

(line=250, char=8852) Ce type reste un sous-type du type des propositions

private (var) test_subtype:(and_or_lit_prop var => prop var) =
  fun p -> p

Exercise: 2 star

(line=255, char=9017) Finissez les deux fonctions suivantes, qui font la conversion. Pourquoi a-t-on utilisé deux fonctions mutuellement récursives ? Aurait-on pu faire autrement?

val rec (var) and_or_to_lit:(and_or_prop var => and_or_lit_prop var) f =
  match f with
    | (PTrue[] | PFalse[] | Var[_]) as g -> g
    | Neg[g] -> neg_and_or_to_lit g
    | Conj[g,h] -> ({- FILL IN HERE -}:and_or_lit_prop var)
    | Disj[g,h] -> ({- FILL IN HERE -}:and_or_lit_prop var)

and (var) neg_and_or_to_lit:(and_or_prop var => and_or_lit_prop var) f =
  match f with
    PTrue[] -> PFalse[]
  | PFalse[] -> PTrue[]
  | Var[_] as f -> Neg[f]
  | Neg[g] -> ({- FILL IN HERE -}:and_or_lit_prop var)
  | Conj[g,h] -> ({- FILL IN HERE -}:and_or_lit_prop var)
  | Disj[g,h] -> ({- FILL IN HERE -}:and_or_lit_prop var)

Exercise: 2 star

(line=277, char=9847) Comprenez la preuve ci-dessous. Il faut décommenter 8< lorsque l'exercice précédent est fini. FILL IN HERE

val rec (var) and_or_to_lit_correct v:(valuation var) f:(and_or_prop var)
  |- value v f == value v (and_or_to_lit f)
proof
  match f with
  | (PTrue[] | PFalse[] | Var[_]) -> #set proof_depth = 1 in 8<
  | Neg[g] ->
     deduce value v g == not (value v (neg_and_or_to_lit g))
       by neg_and_or_to_lit_correct v g;
     #set proof_depth = 1 in {- FILL IN HERE -}
  | Conj[g,h] | Disj[g,h] ->
     deduce (value v g) == value v (and_or_to_lit g)
       by and_or_to_lit_correct v g;
     deduce (value v h) == value v (and_or_to_lit h)
       by and_or_to_lit_correct v h;
     #set proof_depth = 1 in {- FILL IN HERE -}

and (var) neg_and_or_to_lit_correct v:(valuation var) f:(and_or_prop var)
  |- value v f == not (value v (neg_and_or_to_lit f))
proof
  match f with
  | (PTrue[] | PFalse[] | Var[_]) -> #set proof_depth = 1 in 8<
  | Neg[g] ->
     deduce (value v g) == value v (and_or_to_lit g)
       by and_or_to_lit_correct v g;
     #set proof_depth = 1 in {- FILL IN HERE -}
  | Conj[g,h] | Disj[g,h] ->
     deduce value v g == not (value v (neg_and_or_to_lit g))
       by neg_and_or_to_lit_correct v g;
     deduce value v h == not (value v (neg_and_or_to_lit h))
       by neg_and_or_to_lit_correct v h;
     #set proof_depth = 2 in {- FILL IN HERE -}

(line=314, char=11245) Un seul connecteur

(line=316, char=11272) On peut, au lieu d'enlever les négations, ne garder qu'un seul connecteur, ici la conjonction. On peut aussi éviter les doubles négations. Voici le type, qu'il faut alors écrire. Le second type allow_neg_and_prop var indique les propositions que l'on autorise sous une négation.

type rec and_prop var = [
| PTrue[] | PFalse[]
| Var[var]
| Conj[and_prop var * and_prop var]
| Neg[allow_neg_and_prop var]
]

and allow_neg_and_prop var = [
| Var[var]
| Conj[and_prop var * and_prop var]
]

(*  on peut encore vérifier le sous-typage.
*)

private (var) test_subtype:(and_prop var => prop var) =
  fun p -> p

Exercise: 2 star

(line=341, char=11937) Compléter les fonctions suivantes

val rec (var) prop_to_and:(and_or_prop var => and_prop var) f =
  match f with
    | (PTrue[] | PFalse[] | Var[_]) as g -> (g : and_prop var)
    | Neg[g]    -> neg_prop_to_and g
    | Conj[g,h] -> ({- FILL IN HERE -}:and_prop var)
    | Disj[g,h] -> ({- FILL IN HERE -}:and_prop var)

and (var) neg_prop_to_and:(and_or_prop var => and_prop var) f =
  match f with
    | Var[_] as g -> Neg[g]
    | PTrue[]   -> PFalse[]
    | PFalse[]  -> ({- FILL IN HERE -}:and_prop var)
    | Neg[g]    -> ({- FILL IN HERE -}:and_prop var)
    | Conj[g,h] -> ({- FILL IN HERE -}:and_prop var)
    | Disj[g,h] -> ({- FILL IN HERE -}:and_prop var)


private test _ |- prop_to_and (prop_to_and_or Impl[A,B]) == Neg[Conj[A,Neg[B]]]
proof {- FILL IN HERE -}

Exercise: 2 star

(line=364, char=12750) On peut maintenant montrer que le fonction précédente est correcte, compléter la preuve.

val rec (var) prop_to_and_correct v:(valuation var) f:(and_or_prop var)
  |- value v f == value v (prop_to_and f)
proof
  match f with
  | PTrue[] -> {- FILL IN HERE -}
  | PFalse[] -> {- FILL IN HERE -}
  | Var[_] -> {- FILL IN HERE -}
  | Neg[g as h] -> {- FILL IN HERE -}
  | Conj[g,h] ->  {- FILL IN HERE -}
                  {- FILL IN HERE -}
  | Disj[g,h] -> {- FILL IN HERE -}
                 {- FILL IN HERE -}

and (var) neg_prop_to_and_correct v:(valuation var) f:(and_or_prop var)
  |- value v f == not (value v (neg_prop_to_and f))
proof
   match f with
  | PTrue[] -> {- FILL IN HERE -}
  | PFalse[] -> {- FILL IN HERE -}
  | Var[_] -> {- FILL IN HERE -}
  | Neg[g as h] -> {- FILL IN HERE -}
  | Conj[g,h] -> {- FILL IN HERE -}
                 {- FILL IN HERE -}
  | Disj[g,h] -> {- FILL IN HERE -}
                  {- FILL IN HERE -}