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.

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)
    | f₁ ∨ f₂ => table_Ou (interp_def f₁) (interp_def f₂)
    | f₁ ∧ f₂ => table_Et (interp_def f₁) (interp_def f₂)
    | f₁ ⇒ f₂ => table_Implique (interp_def f₁) (interp_def f₂)
  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
    | f₁ ∨ f₂ => if interp f₁ then true else interp f₂
    | f₁ ∧ f₂ => if interp f₁ then interp f₂ else false
    | f₁ ⇒ f₂ => if interp f₁ then interp f₂ else true
  end.

Eval compute in interp (Implique ⊤ (Ou ⊤ ⊥)).
Eval compute in interp (Ou ⊥ ⊥).

Preuve de correction de la version optimisée.

Lemma interp_correct: forall f:formule, interp_def f = interp f.

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 : formule ⟶ Prop :=
Vrai_is_red: is_reduced ⊤
| Non_is_red: forall f,is_reduced f ⟶ is_reduced (¬ f)
| Or_is_red: forall f g,is_reduced f ⟶ is_reduced g ⟶ is_reduced (f ∨ g).

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

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 : formule ⟶ Prop :=
Faux_is_red2: is_reduced2 ⊥
| Implique_is_red2: forall f g,is_reduced2 f ⟶ is_reduced2 g ⟶ is_reduced2 (f ⇒ g).

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

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