Creative Commons License Copyright Pierre Courtieu et Olivier Pons. This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International public License.

logique_propositionnelle







Ce module formalise la logique propositionnelle sans variable (calcul propositionnel).


Les formules propositionnelles (sans variables)

Défintion des formules

Les formules sont définies (par induction) par la grammaire suivante.

Inductive formule : Type :=
| Vrai: formule
| Faux: formule
| Non: formuleformule
| Ou: formuleformuleformule
| Et: formuleformuleformule
| Implique: formuleformuleformule.

Exemples de formule sans notation


Check Vrai.
Check Faux.
Check (Ou Vrai Vrai).
Check (Ou Faux Vrai).
Check (Ou (Ou Vrai Faux) Vrai).

Notations usuelles



Notation "⊤":= Vrai.
Notation "⊥":= Faux.
Notation "¬ X":= (Non X).
Notation "X ∨ Y":= (Ou X Y).
Notation "X ∧ Y":= (Et X Y).
Notation "X ⇒ Y":= (Implique X Y).

Exemples avec les notations usuelles


Check .
Check .
Check ( ).
Check ( ).
Check (( ) ).
Check ( ).
Check ( ( )).

Interprétation d'une formule (Sémantique)

Définition de l'interprétation d'une formule

Définition de l'interprétation d'une formule: on applique les tables de vérité des feuilles jusqu'à la racine.
Function interp_def (f:formule) : bool :=
  match f with
    | => table_Vrai
    | => table_Faux
    | ¬ f => table_Non (interp_def f)
    | f1 f2 => table_Ou (interp_def f1) (interp_def f2)
    | f1 f2 => table_Et (interp_def f1) (interp_def f2)
    | f1 f2 => table_Implique (interp_def f1) (interp_def f2)
  end.

Eval compute in interp_def (Implique (Ou )).
Eval compute in interp_def (Implique (Ou )).
Version "optimisée" qui n'évalue la sous-formule de droite que si nécessaire.
Function interp (f:formule) : bool :=
  match f with
    | => true
    | => false
    | ¬f => if interp f then false else true
    | f1 f2 => if interp f1 then true else interp f2
    | f1 f2 => if interp f1 then interp f2 else false
    | f1 f2 => if interp f1 then interp f2 else true
  end.

Eval compute in interp (Implique (Ou )).
Eval compute in interp (Ou ).
Preuve de correction de la version optimisée.

Preuves d'équivalences entre formules

Dans le calcul propositionnel deux formules sont équivalentes si leurs interprétations sont égales. Dans les logiques avec variables nous verrons que la notion d'équivalence fait intervenir la notion de valuation des variables.

Notation "f ≡ g" := ((interp f) = (interp g)) (at level 180).

Lemma eq_implique : forall x y : formule, x y ¬x y.

Lemma eq_et : forall x y: formule, x y ¬(¬x ¬y).

Lemma eq_not : ¬.

Lemma eq_not2 : forall x : formule, ¬x x .

Lemma eq_ou : forall x y : formule, x y ¬x y.

Réduction des connecteurs au sous-ensemble {⊤,¬,∨}

Les différents connecteurs correspondent à des constructions logiques essentiellement issues du langage naturel. En réalité ces constructions sont redondantes et un très petit nombre de connecteurs permet d'exprimer tous les autres. Par exemple on voit dans la suite que les trois connecteurs {⊤,¬,∨} peuvent être combinés pour remplacer tous les autres en utilisant les propriétés d'équivalence prouvées plus haut.
Définition de la propriété "être formé uniquement avec des ¬, ∨ et ⊤".

Inductive is_reduced : formuleProp :=
  Vrai_is_red: is_reduced
| Non_is_red: forall f,is_reduced fis_reduced (¬ f)
| Or_is_red: forall f g,is_reduced fis_reduced gis_reduced (f g).

Fonction qui remplace les formules contenant les autres connecteurs par des formule réduites équivalentes.

Function reduce (f:formule) : formule :=
  match f with
    | =>
    | => ¬
    | ¬ f => ¬ (reduce f)
    | f1 f2 => (reduce f1) (reduce f2)
    | f1 f2 => ¬ (reduce f1) ¬ (reduce f2))
    | f1 f2 => ¬ (reduce f1) (reduce f2)
  end.

la transformation est toujours équivalente.

Lemma reduce_correct: forall f:formule, f (reduce f).

La transformation produit bien une formule réduite, c'est-à-dire ne contenant que les connecteurs {⊤,¬,∨}.

Lemma reduce_complete : forall f, is_reduced (reduce f).

cet ensemble de connecteur n'est pas unique; Par exemple, on peut aussi se limiter aux connectuer ⊥ et ⇒ . Comme le montre les lemme ci-dessous:
Définition de la propriété "être formé uniquement avec ⊥ et ⇒ ".

Inductive is_reduced2 : formuleProp :=
  Faux_is_red2: is_reduced2
| Implique_is_red2: forall f g,is_reduced2 fis_reduced2 gis_reduced2 (f g).

Fonction qui remplace les formules contenant les autres connecteurs par des formule réduites équivalentes.

Function reduce2 (f:formule) : formule :=
  match f with
    | =>
    | =>
    | ¬ f => (reduce2 f)
    | f1 f2 => ((reduce2 f1) ) (reduce2 f2)
    | f1 f2 => ((reduce2 f1) ((reduce2 f2)⇒ ))⇒
    | f1 f2 => (reduce2 f1) (reduce2 f2)
  end.

la transformation est toujours équivalente.

Lemma reduce_correct2: forall f:formule, f (reduce2 f).

La transformation produit bien une formule réduite, c'est-à-dire ne contenant que les connecteurs {⊥ et ⇒}.

Lemma reduce_complete2 : forall f, is_reduced2 (reduce2 f).


This page has been generated by coqdoc