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.

loglangcoq.logique.logique_propositionnelle_avec_variables







Logique propositionnelle

Ce module formalise la logique propositionnelle (calcul propositionnel avec variables propositionnelles).

Notation := nat.

Require Import logique_generique.
Require Import Morphisms FunInd.
Require Import Setoid.
Require Import EqNat.
Require Import tables_de_verite.
Require Import OrderedType.

Le formules propositionnelle avec variables propositionnelles

Définition des formules

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

Inductive formule : Type :=
| Vrai: formule
| Faux: formule
| Var: formule
On désigne les variables par des entiers.

Exemples de formules sans notation


Check Vrai.
Check Faux.
Check (Var 23).
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).

Les variables seront également plus lisibles en notant le numéro de la variable en indice de la lettre X ('x' majuscule).

Notation "'X1'":= (Var 1).
Notation "'X2'":= (Var 2).

Exemples avec les notations usuelles


Check .
Check .
Check X7.
Check ( ).
Check ( X3).
Check (X9 X2).
Check (( X4) ).

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. Pour interpréter les variables propositionnelles on a besoin d'une valuation v des variables vers les valeurs de vérité (bool), ensuite on applique les tables de vérité des feuilles jusqu'à la racine comme le calcul propositionnel.

Function interp_def (v:nat bool) (f:formule) : bool :=
  match f with
    | => table_Vrai
    | => table_Faux
    | Var i => v i
    | ¬ f => table_Non (interp_def v f)
    | f1 f2 => table_Ou (interp_def v f1) (interp_def v f2)
    | f1 f2 => table_Et (interp_def v f1) (interp_def v f2)
    | f1 f2 => table_Implique (interp_def v f1) (interp_def v f2)
  end.

quelques exemples

Voir plus bas pour plus d'exemples.

  Eval compute in interp_def (fun x => true) (Implique (Ou )).
→ true

  Eval compute in interp_def (fun x => false) (Implique (Ou )).
→ true

  Eval compute in interp_def (fun x => false) (Implique (Ou )).
→ false

  Definition val_X1_true := (fun x => match x with 1 => true | _ => false end).

  Definition val_X1_false := (fun x => match x with 1 => false | _ => false end).

  Eval compute in interp_def val_X1_true (Implique (Ou X1)).
→ true

  Eval compute in interp_def val_X1_false (Implique (Ou X1)).
→ false


Version optimisée qui n'évalue la sous-formule de droite que si nécessaire.

Function interp (v:nat bool) (f:formule) : bool :=
  match f with
    | => true
    | => false
    | Var i => v i
    | ¬f => if interp v f then false else true
    | f1 f2 => if interp v f1 then true else interp v f2
    | f1 f2 => if interp v f1 then interp v f2 else false
    | f1 f2 => if interp v f1 then interp v f2 else true
  end.

Preuve de correction de la version optimisée.


Lemma interp_correct: forall I: bool,forall f:formule, interp_def I f = interp I f.
Proof.
  induction f.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. repeat rewrite IHf.
    simpl. destruct (interp I f);simpl;reflexivity.
  - simpl. repeat rewrite IHf1, IHf2.
    simpl. destruct (interp I f2); destruct (interp I f1);simpl;reflexivity.
  - simpl. repeat rewrite <- IHf1, <- IHf2.
    destruct (interp I f2); destruct (interp I f1);simpl;
    repeat rewrite IHf1, IHf2;simpl; reflexivity.
  - simpl. repeat rewrite IHf1, IHf2.
    simpl. destruct (interp I f2); destruct (interp I f1);simpl;reflexivity.
Qed.

Exemples d'interprétations

  Definition v1 (n:nat): bool :=
    match n with
      | 1 => true
      | 2 => false
      | 3 => true
      | _ => false
    end.

  Definition v2 (n:nat): bool :=
    match n with
      | 1 => false
      | 2 => true
      | 3 => true
      | _ => false
    end.

  Eval compute in interp_def v1 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp_def v2 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp_def v1 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp_def v2 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp_def v1 X2.
→ false

  Eval compute in interp_def v1 X2.
→ false

  Eval compute in interp_def v2 X2.
→ true

  Eval compute in interp_def v1 (Implique X1 (Ou Faux Faux)).
→ false

  Eval compute in interp_def v2 (Implique X1 (Ou Faux Faux)).
→ true

  Eval compute in interp v1 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp v2 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp v1 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp v2 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp v1 X2.
→ false

  Eval compute in interp v1 X2.
→ false

  Eval compute in interp v2 X2.
→ true

  Eval compute in interp v1 (Implique X1 (Ou Faux Faux)).
→ false

  Eval compute in interp v2 (Implique X1 (Ou Faux Faux)).
→ true


Conséquence, modèle etc

On applique les définitions de conséquence, modèle etc du chapitre logique_generique avec les notions de valuation et d'interprétation ci-dessous.


  Definition valuation: Type:= bool.

Dans la suite on écrira interpretation v φ b plutôt que interp_def v φ = b.

  Definition interpretation := fun v φ b => interp_def v φ = b.


Résultat supplémentaire: l'interprétation est décidable. Ce ne sera pas le cas pour la logique des prédicats avec quantificateurs

  Lemma interpretation_dec:
    forall v φ, interpretation v φ true interpretation v φ false.
  Proof.
    intros v f.
    unfold interpretation.
    destruct (interp_def v f);simpl;auto.
  Qed.


Une autre définition pour l'équivalence: l'interprétation des deux formules est toujours identique.

Definition equivalent φ1 φ2 :=
  forall I b, (interpretation I φ1 b)<->(interpretation I φ2 b).

Preuve d'equivalence entre les deux notions d'équivalence.

Lemma equivEquivalence :forall φ1 φ2,(DEFS.equiv φ1 φ2) (equivalent φ1 φ2).
  intros φ1 φ2.
  unfold equivalent.
  smpl×.
  split.
  - intros [h1 h2] I.
    specialize (h1 I).
    specialize (h2 I).
    destruct (interp_def I φ2);destruct (interp_def I φ1);simpl;intros;auto;try reflexivity;try now discriminate.
    + discriminate h2;reflexivity.
    + discriminate h1;reflexivity.
  - intros h.
    split; intros I h'.
    + apply h;assumption.
    + apply h;assumption.
Qed.

Exemple de modèles et de conséquences


  Lemma modele1 : forall v, ⊧[v] X1 ¬ X1.
  Proof.
    intros v.
    red.
    simpl.
    destruct (v 1).
    - reflexivity.
    - reflexivity.
  Qed.

  Lemma modele2 : forall v, ⊧[v] (X1 ¬ X2) X2.
  Proof.
    intros v.
    red.
    simpl.
    destruct (v 1).
    - destruct (v 2);simpl.
      + reflexivity.
      + reflexivity.
    - destruct (v 2).
      + reflexivity.
      + reflexivity.
  Qed.

  Lemma conseq1: (X1¬X2) X2 X1.
  Proof.
    repeat red.
    simpl.
    intros I H.
    red in H.
    simpl in ×.
    destruct (I 1).
    - reflexivity.
    - destruct (I 2).
      + discriminate H.
      + discriminate H.
  Qed.


Preuves d'équivalences entre formules


Lemma eq_implique : forall φ ψ : formule, φ ψ ¬φ ψ.
Proof.
  intros φ ψ.
  simpl.
  unfold equiv,consequence,est_modele. simpl.
  split;intros v h.
  - functional inversion h;subst;clear h.
    + reflexivity.
    + simpl.
      destruct (interp_def v ψ);simpl;auto.
  - destruct (interp_def v φ).
    + assumption.
    + reflexivity.
Qed.

Lemma eq_et : forall φ ψ: formule, (φ ψ) ¬ φ ¬ψ).
Proof.
  intros φ ψ.
  unfold equiv,consequence,est_modele. simpl.
  split;intros v h.
  - functional inversion h;subst;clear h.
    reflexivity.
  - destruct (interp_def v φ).
    + destruct (interp_def v ψ).
      × reflexivity.
      × discriminate.
    + destruct (interp_def v ψ).
      × discriminate.
      × discriminate.
Qed.

Lemma eq_not_true : ¬ .
Proof.
  simpl.
  unfold equiv,consequence,est_modele. simpl.
  split;intros.
  - discriminate.
  - discriminate.
Qed.

Lemma eq_not_false : ¬ .
Proof.
  simpl.
  unfold equiv,consequence,est_modele. simpl.
  split;intros.
  - reflexivity.
  - reflexivity.
Qed.


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

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

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

Lemma reduce_correct:
  forall v, forall f:formule, interp_def v f = interp_def v (reduce f).
Proof.
  intros v f.
  induction f.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite IHf. reflexivity.
  - simpl. rewrite IHf1, IHf2. reflexivity.
  - simpl. repeat rewrite <- IHf1, <- IHf2.
    destruct (interp_def v f1).
    + destruct (interp_def v f2).
      × reflexivity.
      × reflexivity.
    + destruct (interp_def v f2).
      × reflexivity.
      × reflexivity.
  - simpl. rewrite <- IHf1, <- IHf2.
    destruct (interp_def v f1).
    + reflexivity.
    + destruct (interp_def v f2).
      × reflexivity.
      × reflexivity.
Qed.

Lemma reduce_equiv : forall f:formule, f (reduce f).
Proof.
  intros f.
  unfold equiv , consequence, est_modele.
  split;intros.
  - rewrite <- reduce_correct.
    assumption.
  - rewrite reduce_correct.
    assumption.
Qed.

Propriété d'être formé uniquement avec des ¬, ∨ et ⊤ ou Var.
la fonction reduce retourne bien une formule de cette forme.

Lemma reduce_complete : forall f, is_reduced (reduce f).
Proof.
  induction f.
  - simpl. apply Vrai_is_red.
  - simpl. apply Non_is_red. apply Vrai_is_red.
  - apply Var_is_red.
  - simpl. apply Non_is_red. assumption.
  - simpl. apply Or_is_red.
    + assumption.
    + assumption.
  - simpl. apply Non_is_red. apply Or_is_red.
    + apply Non_is_red. assumption.
    + apply Non_is_red. assumption.
  - simpl. apply Or_is_red.
    + apply Non_is_red. assumption.
    + assumption.
Qed.

Preuve par réfutation (Utile pour la preuve par tableau plus loin).


Lemma conseq_by_contradiction': forall f1 f2: formule, f1 f2 f1 ¬f2 .
Proof.
  intros f1 f2.
  unfold consequence, est_modele.
  intros H v H0.
  simpl in H0.
  destruct (interp_def v f1) eqn:heq.
  - assert (heq':interp_def v f2 = true).
    { apply H. apply heq. }
    rewrite heq' in H0.
    discriminate H0.
  - simpl in H0.
    destruct (interp_def v f2);auto.
Qed.

Pour prouver f ⊧ g on peut prouver f ∧ ¬g ⊧ ⊥.

Lemma conseq_by_contradiction: forall f1 f2: formule, f1 ¬f2 f1 f2.
Proof.
  intros f1 f2.
  unfold consequence, est_modele.
  simpl.
  intros H v heq.
  specialize (H v).
  rewrite heq in H.
  destruct (interp_def v f2) eqn:heq'.
  - reflexivity.
  - discriminate H. reflexivity.
Qed.

Preuve par la méthode des tableaux



Lemmes auxilaires


Lemma and_affaiblissement_conseq : forall v f1 f2, ⊧[v] f1f2 ⊧[v]f1.
Proof.
  intros v f1 f2 H.
  red in H. red. simpl in ×.
  destruct (interp_def v f1).
  - reflexivity.
  - destruct (interp_def v f2);auto; try discriminate .
Qed.

Lemma and_affaiblissement_contr : forall f1 f2, f1 f1f2 .
Proof.
  intros f1 f2 H.
  red in H. red.
  intros v H0.
  apply H.
  apply and_affaiblissement_conseq with (f2 := f2).
  assumption.
Qed.

Lemma Et_sym : forall f1 f2, f1 f2 f2 f1.
Proof.
  intros f1 f2.
  split.
  - red;red;simpl.
    intros v H.
    red in H.
    simpl in H.
    destruct (interp_def v f1).
    + destruct (interp_def v f2).
      × assumption.
      × discriminate H.
    + destruct (interp_def v f2).
      × assumption.
      × discriminate H.
  - red;red;simpl.
    intros v H.
    red in H.
    simpl in H.
    destruct (interp_def v f1).
    + destruct (interp_def v f2).
      × assumption.
      × discriminate H.
    + destruct (interp_def v f2).
      × discriminate H.
      × discriminate H.
Qed.

Lemma Et_assoc : forall f1 f2 f3, f1 (f2 f3) (f1 f2) f3.
Proof.
  intros f1 f2 f3.
  split.
  - repeat red; simpl.
    intros v H.
    red in H.
    simpl in H.
    destruct (interp_def v f1); destruct (interp_def v f2); destruct (interp_def v f3); try assumption; try discriminate.
  - repeat red; simpl.
    intros v H.
    red in H.
    simpl in H.
    destruct (interp_def v f1); destruct (interp_def v f2); destruct (interp_def v f3); try assumption; try discriminate.
Qed.

Function extraction_disjuntion (f F: formule): option formule :=
  match F with
    | g F' =>
      if formule_eq_dec f g then Some F'
      else
        if formule_eq_dec f F' then Some g
        else
          match extraction_disjuntion f F' with
              None => None
            | Some F'' => Some (g F'')
          end
    | g => if formule_eq_dec f g then Some else None
  end.

Eval compute in (extraction_disjuntion (¬X1) (((X1 ¬X2) X2) ¬X1 X2)).
Eval compute in (extraction_disjuntion (¬X1) (((X1 ¬X2) X2) ¬X1)).
Eval compute in (extraction_disjuntion ((X1 ¬X2) X2) (((X1 ¬X2) X2) ¬X1)).

Lemma Et_et_true : forall f, f f .
Proof.
  intros f.
  rewrite Et_sym.
  unfold equiv,consequence,est_modele.
  split;intros;simpl.
  - rewrite H.
    reflexivity.
  - functional inversion H.
    functional inversion H2.
    subst;simpl in ×.
    symmetry.
    assumption.
Qed.

Lemma extraction_disjuntion_ok :
  forall f F F', extraction_disjuntion f F = Some F' (F f F').
Proof.
  intros f F.
  functional induction (extraction_disjuntion f F);simpl;intros; try discriminate.
  - inversion H;subst;reflexivity.
  - inversion H;clear H.
    subst.
    setoid_rewrite Et_sym at 1.
    reflexivity.
  - inversion H;clear H.
    subst.
    rewrite (IHo _ e2).
    rewrite Et_assoc at 1.
    setoid_rewrite Et_sym at 2.
    rewrite <- Et_assoc at 1.
    reflexivity.
  - inversion H. clear H.
    subst.
    apply Et_et_true.
Qed.

Les règles des tableaux


Lemma tableau_Ou :
  forall F f1 f2, ((f1 F ) (f2 F )) (f1 f2) F .
Proof.
  intros F f1 f2 [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  simpl in ×.
  specialize (h v).
  specialize (h' v).
  apply h.
  destruct (interp_def v f1);destruct (interp_def v f2);destruct (interp_def v F);auto.
Qed.

Lemma tableau_Ou' : forall f1 f2, (f1 ) (f2 ) (f1 f2) .
Proof.
  intros f1 f2 [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  simpl in ×.
  specialize (h v).
  specialize (h' v).
  apply h.
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_nonEt:
  forall F f1 f2, (¬f1 F ) (¬f2 F ) ¬(f1 f2) F .
Proof.
  intros F f1 f2 H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);destruct (interp_def v F);auto.
Qed.

Lemma tableau_nonEt' : forall f1 f2, (¬f1 ) (¬f2 ) ¬(f1 f2) .
Proof.
  intros f1 f2 H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_implique :
  forall F f1 f2, (¬f1 F ) (f2 F ) (f1 f2) F .
Proof.
  intros F f1 f2 H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2)
  ;destruct (interp_def v F);auto.
Qed.

Lemma tableau_implique' : forall f1 f2, (¬f1 ) (f2 ) (f1 f2) .
Proof.
  intros f1 f2 H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_Et: forall F f1 f2, f1 f2 F (f1 f2) F .
Proof.
  intros F f1 f2 h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);destruct (interp_def v F);auto.
Qed.


Lemma tableau_nonimplique : forall F f1 f2, f1 ¬f2 F ¬(f1 f2) F .
Proof.
  intros F f1 f2 h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);destruct (interp_def v F);auto.
Qed.

Lemma tableau_nonimplique' : forall f1 f2, f1 ¬f2 ¬(f1 f2) .
Proof.
  intros f1 f2 h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_nonOu : forall F f1 f2, ¬f1 ¬f2 F ¬(f1 f2) F .
Proof.
  intros F f1 f2 h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);destruct (interp_def v F);auto.
Qed.

Lemma tableau_nonOu' : forall f1 f2, ¬f1 ¬f2 ¬(f1 f2) .
Proof.
  intros f1 f2 h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_ferme_branche : forall F f, (F f) ¬f .
Proof.
  intros F f.
  red.
  intros v H.
  red in H.
  simpl in H.
  destruct (interp_def v F);destruct (interp_def v f).
  - discriminate H.
  - discriminate H.
  - discriminate H.
  - discriminate H.
Qed.

Lemma tableau_ferme_branche' : forall F f, f ¬f F .
Proof.
  intros F f.
  setoid_rewrite Et_sym at 2.
  setoid_rewrite Et_assoc.
  setoid_rewrite Et_sym at 2.
  apply tableau_ferme_branche.
Qed.

Lemma tableau_ferme_branche'' : forall F f, (f ¬f) F .
Proof.
  intros F f.
  setoid_rewrite <- Et_assoc.
  apply tableau_ferme_branche'.
Qed.

Lemma p_et_p_eq : forall p, pp p.
Proof.
  intros p.
  unfold equiv,consequence,est_modele.
  simpl.
  split.
  - intros v H.
    destruct (interp_def v p);auto.
  - intros v H.
    destruct (interp_def v p);auto.
Qed.


Exemples d'application des tableaux.


Lemma conseq1: (X1¬X2) X2 X1.
Proof.
  apply conseq_by_contradiction.
  do_Et (X1 ¬X2) X2.
  do_Ou X1 (¬X2).
  - do_ferme X1.
  - do_ferme X2.
Qed.

  Lemma conseq2 : (X1 X3 ) (¬X1 X2) .
Proof.
  do_Ou (¬X1) X2.
  - do_ferme X1.
Echec
Abort.

Lemma conseq3 : (¬ (X1 (X2 X1))) .
Proof.
  do_NonImplique X1 (X2 X1).
  do_NonImplique X2 X1.
  do_ferme X1.
Qed.

Lemma conseq4 : (¬ (X1 X2)) X1 .
Proof.
  do_nonOu X1 X2.
  do_ferme X1.
Qed.

Lemma conseq5 : (¬ (X1 X2)) X1 X2 .
Proof.
  do_nonEt X1 X2.
  - do_ferme X1.
  - do_ferme X2.
Qed.

Lemma conseq_exam_2014 : (¬X2¬X3) (X2 X3) X1.
Proof.
  apply conseq_by_contradiction.
  do_NonImplique (X2 X3) (X1).
  do_Et (X2)(X3).
  do_Ou (¬X2) (¬X3).
  - do_ferme X2.
  - do_ferme X3.
Qed.

Lemma conseq6 : (X1 X2)∧(¬X1 ¬X2) .
Proof.

    do_Ou X1 X2.
    - do_ferme X1.
    - do_ferme X2.
Qed.

Lemma conseq7 : (X1 (X2 X3)) ((X1 X2) (X1 X3)).
  Proof.
  apply conseq_by_contradiction.
  do_NonImplique (X1 (X2 X3)) ((X1 X2) (X1 X3)).
  do_Implique X1 (X2 X3).
  - do_NonImplique (X1 X2) (X1 X3).
    do_Implique X1 X2.
    + do_NonImplique X1 X3.
      do_ferme X1.
    + do_NonImplique X1 X3.
      do_ferme X1.
  - do_NonImplique (X1 X2) (X1 X3).
    do_Implique X1 X2.
    + do_NonImplique X1 X3.
      do_ferme X1.
    + do_Implique X2 X3.
       × do_ferme X2.
       × do_NonImplique X1 X3.
         do_ferme X3.
Qed.


This page has been generated by coqdoc