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_predicats

Ce module formalise la logique des prédicats sans quantificateur. Les termes ne contiennent pas de symboles de fonctions, un terme est donc une variable. Les prédicats sont d'arité quelconque.

Les formules

Les termes

Le type des termes. Les termes ne sont que des variables. La logique propositionnelle inclut en principe les symboles de fonctions mais cela compliquerait la présentation.

Inductive terme: Type :=
| TVar: ℕ → terme.

Les formules

Le type des formules logique avec prédicats (sans symbole de fonction) et sans quantification. Les noms de prédicats sont représentés par des numéros, un prédicat prend un seul argument: une liste de termes.

Inductive formule : Type :=
| Vrai: formule
| Faux: formule
| Var: ℕ → formule
| Non: formule → formule
| Ou: formule → formule → formule
| Et: formule → formule → formule
| Implique: formule → formule → formule
| Pred: ℕ → list terme → formule.

Exemples de formules:



Check (Pred 1 (TVar 1::nil)).
: formule

Check (Ou (Ou (Pred 1 (cons (TVar 1) (cons (TVar 2) nil))) 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).

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

Notation "´x1´":= (TVar 1).
Notation "´x2´":= (TVar 2).



Notation "´p1´ l":= (Pred 1 l).
Notation "´p2´ l":= (Pred 2 l).


Exemples avec notations


Check (Var 7).
Check X7.
Check (Pred 1 (x1::nil)).
Check (p1 [x1 , x2 , x3]).
Check (p1 [x1 , x2 , x3]).

termes:


Check x7.

Scheme Equality for terme.

Décision de l'égalité sur les formules
Function formule_beq (φ ψ:formule) {struct φ}: bool :=
  match φ,ψ with
    | ⊤,⊤ ⇒ true
    | ⊥,⊥ ⇒ true
    | Var p,Var q ⇒ beq_nat p q
    | φ1 ⇒ φ2, ψ1 ⇒ ψ2 ⇒ formule_beq φ1 ψ1 && formule_beq φ2 ψ2
    | φ1 ∧ φ2,ψ1 ∧ ψ2 ⇒ formule_beq φ1 ψ1 && formule_beq φ2 ψ2
    | φ1 ∨ φ2,ψ1 ∨ ψ2 ⇒ formule_beq φ1 ψ1 && formule_beq φ2 ψ2
    | ¬φ,¬ψ ⇒ formule_beq φ ψ
    | (Pred n1 l1) , (Pred n2 l2) ⇒ beq_nat n1 n2 &&
                                     forallb2 terme_beq l1 l2
    | _,_ ⇒ false
  end.

Lemma terme_eq_ok : ∀ t1 t2:terme, terme_beq t1 t2 = true ↔ t1 = t2.

Lemma terme_eq_true_eq_iff: ∀ l1 l2,
              Forall2 (fun x y : terme ⇒ terme_beq x y = true) l1 l2
              ↔ Forall2 Logic.eq l1 l2.
Lemma formule_eq_okr : ∀ φ ψ:formule, formule_beq φ ψ = true → φ = ψ.

Lemma formule_eq_okl : ∀ φ ψ:formule, φ = ψ → formule_beq φ ψ = true.

Lemma formule_eq_ok : ∀ φ ψ:formule, φ = ψ ↔ formule_beq φ ψ = true.

Lemma formule_neq_ok : ∀ φ ψ:formule, φ ≠ ψ ↔ formule_beq φ ψ = false.

Lemma formule_eq_dec : ∀ f1 f2: formule, {f1 = f2} + {f1≠f2}.

Pour définir l'interprétation d'une formule nous avons de trois fonctions de valuation: celle pour les propositions (comme pour la logique propositionnelle avec variables), celle pour les termes et celle pour les prédicats. Les prédicats ont leur valeur dans les fonctions n-aires (DxD..xD -> bool). En effet u prédicat p à deux argument doit s'interpréter vers une fonction prenant deux entiers et retournant un booléen. Par exemple le prédicat "<" prend deux entier et retourne true si le premier est plus petit que le deuxième.

Definition val_propositions :=(nat → bool).
Definition val_termes D :=(terme → D).
Definition val_predicat D :=nat → (list D → bool).


Record Valuation (D:Type) :=
  { predicats: val_predicat D;
    termes: val_termes D;
    propositions: val_propositions }.


Définition de l'interprétation d'une formule: on applique les tables de vérité des feuilles jusqu'à la racine.

Function interp_def (v:Valuation Z) (f:formule) : bool :=
  match f with
    | ⊤ ⇒ table_Vrai
    | ⊥ ⇒ table_Faux
    | Var i ⇒ (v.(propositions) i)
    | Pred i l ⇒ (v.(predicats) i) (map v.(termes) l)
    | ¬ 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.

On utilisera l'abus de notation suivant: I[f] à la place de (interp_def I f). Attention toutefois à garder en mémoire qu'une interprétation I ne s'applique pas à une formule mais à une variable, c'est la fonction interp_def qui permet de généraliser une interprétation aux formules.



Module Exemples.
  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.

  Definition is_zero l :=
    match l with
      | 0%Z::_ ⇒ true
      | _ ⇒ false
    end.

  Definition vp (n:nat): (list Z → bool) :=
    match n with
      | 1 ⇒ is_zero
      | _ ⇒ (fun _ ⇒ false)
    end.

  Definition vt trm :=
    match trm with
      | TVar i ⇒ (0)%Z
    end.

  Definition III:Valuation := {| predicats:=vp; termes:=vt; propositions:=v1|}.
  Definition III´:Valuation := {| predicats:=vp; termes:=vt; propositions:=v2|}.

  Eval compute in interp_def III (Implique ⊤ (Ou ⊤ ⊥)).
  Eval compute in interp_def III´ (Implique ⊤ (Ou ⊤ ⊥)).
  Eval compute in interp_def III (Implique ⊤ (Ou ⊥ ⊥)).
  Eval compute in interp_def III´ (p1[x1]).
  Eval compute in interp_def III´ (Implique (p1[x1]) ⊥).
  Eval compute in interp_def III´ (Implique (p1[x1]) (Ou ⊥ ⊥)).

End Exemples.

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:= @Valuation Z.
  Definition interpretation: valuation → formule → bool → Prop :=
    fun v f b ⇒ interp_def v f = b.


Résultat supplémentaire: l'interprétation est décidable (ce ne ser pas le cas pour la logique des prédicats avec quantificateurs
  Lemma interpretation_dec : ∀ v f,
                               interpretation v f true ∨ interpretation v f false.


Une autre définition pour l'équivalence: l'interprétation des deux formules est toujours identique.
Definition equivalent p1 p2 :=
  ∀ v b, (interpretation v p1 b)<->(interpretation v p2 b).

Preuve d'equivalence entre equiv et equivalence.

Lemma equivEquivalence :∀ p1 p2,(DEFS.equiv p1 p2) ↔ (equivalent p1 p2).


Module Exemples_modeles.
  Lemma modele1 : ∀ v n, ⊧[v] (Var n) ∨ ¬ (Var n).

  Lemma modele2 : ∀ v, ⊧[v] (X1 ∨ ¬ X2) ∨ X2.

End Exemples_modeles.

Module Exemples_conseq.
  Lemma conseq1: (X1∨¬X2) ∧ X2 ⊧ X1.

End Exemples_conseq.

Preuves d'équivalences entre formules


Lemma eq_implique : ∀ x y : formule, x ⇒ y ≡ ¬x ∨ y.

Lemma eq_et : ∀ x y: formule, (x ∧ y) ≡ ¬ (¬x ∨ ¬y).

Lemma eq_not : ⊥ ≡ ¬ ⊤.


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


Lemma conseq_by_contradiction´: ∀ f1 f2: formule, f1 ⊧ f2 → f1 ∧ ¬f2 ⊧ ⊥.

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

Lemma conseq_by_contradiction: ∀ f1 f2: formule, ¬f2 ∧ f1 ⊧ ⊥ → f1 ⊧ f2.

Preuve par la méthode des tableaux

Lemmes auxilaires


Lemma and_affaiblissement_conseq : ∀ v f1 f2, ⊧[v] f1∧f2 → ⊧[v]f1.

Lemma and_affaiblissement_contr : ∀ f1 f2, f1 ⊧ ⊥ → f1∧f2 ⊧ ⊥ .

Lemma Et_sym : ∀ f1 f2, f1 ∧ f2 ≡ f2 ∧ f1.

Lemma Et_assoc : ∀ f1 f2 f3, f1 ∧ (f2 ∧ f3) ≡ (f1 ∧ f2) ∧ f3.

Function extraction_disjuntion (f F: formule): option formule :=
  match F with
    | g ∧ F´ ⇒
      if formule_beq f g then Some F´
      else
        if formule_beq 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 : ∀ f, f ≡ f ∧ ⊤.

Lemma extraction_disjuntion_ok :
  ∀ f F F´, extraction_disjuntion f F = Some F´ → (F ≡ f ∧ F´).

Les règles des tableaux


Lemma tableau_Ou : ∀ F f1 f2,
                     (f1 ∧ F ⊧ ⊥)
                     ∧ (f2 ∧ F ⊧ ⊥)
                     → (f1 ∨ f2) ∧ F ⊧ ⊥.

Lemma tableau_Ou´ : ∀ f1 f2,
                     (f1 ⊧ ⊥)
                     ∧ (f2 ⊧ ⊥)
                     → (f1 ∨ f2) ⊧ ⊥.

Lemma tableau_nonEt : ∀ F f1 f2,
                        (¬f1 ∧ F ⊧ ⊥) ∧ (¬f2 ∧ F ⊧ ⊥)
                        → ¬(f1 ∧ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonEt´ : ∀ f1 f2,
                        (¬f1 ⊧ ⊥) ∧ (¬f2 ⊧ ⊥)
                        → ¬(f1 ∧ f2) ⊧ ⊥.

Lemma tableau_implique : ∀ F f1 f2,
                           (¬f1 ∧ F ⊧ ⊥) ∧ (f2 ∧ F ⊧ ⊥)
                           → (f1 ⇒ f2) ∧ F ⊧ ⊥.

Lemma tableau_implique´ : ∀ f1 f2,
                           (¬f1 ⊧ ⊥) ∧ (f2 ⊧ ⊥)
                           → (f1 ⇒ f2) ⊧ ⊥.

Lemma tableau_Et : ∀ F f1 f2, f1 ∧ f2 ∧ F ⊧ ⊥ → (f1 ∧ f2) ∧ F ⊧ ⊥.

Lemma tableau_Et´ : ∀ f1 f2, f1 ∧ f2 ⊧ ⊥ → (f1 ∧ f2) ⊧ ⊥.

Lemma tableau_nonimplique : ∀ F f1 f2, f1 ∧ ¬f2 ∧ F ⊧ ⊥ → ¬(f1 ⇒ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonimplique´ : ∀ f1 f2, f1 ∧ ¬f2 ⊧ ⊥ → ¬(f1 ⇒ f2) ⊧ ⊥.

Lemma tableau_nonOu : ∀ F f1 f2, ¬f1 ∧ ¬f2 ∧ F ⊧ ⊥ → ¬(f1 ∨ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonOu´ : ∀ f1 f2, ¬f1 ∧ ¬f2 ⊧ ⊥ → ¬(f1 ∨ f2) ⊧ ⊥.

Lemma tableau_ferme_branche : ∀ F f, (F ∧ f) ∧ ¬f ⊧ ⊥.

Lemma tableau_ferme_branche´ : ∀ F f, f ∧ ¬f ∧ F ⊧ ⊥.

Lemma tableau_ferme_branche´´ : ∀ F f, (f ∧ ¬f) ∧ F ⊧ ⊥.

Lemma tableau_ferme_branche´´´ : ∀ f, f ∧ ¬f ⊧ ⊥.

Lemma p_et_p_eq : ∀ a, a∧a ≡ a.


Exemples d'application des tableaux.

Module Exemple_Tableaux.

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

Lemma conseq2 : (X1 ∧ X3 ) ∧ (¬X1 ∨ X2) ⊧ ⊥.
Proof.
  do_Et X1 X3.
  do_Ou (¬X1) X2.
  - do_ferme X1.
  -
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 conseq5´ : (¬ ((p2((TVar 1::nil)) ) ∧ X2)) ∧ (p2((TVar 1::nil)) ) ∧ X2 ⊧ ⊥.
Proof.
  do_nonEt (p2((TVar 1::nil)) ) X2.
  - do_ferme (p2((TVar 1::nil)) ).
  - do_ferme X2.
Qed.

Lemma conseq6 : (X1 ∧ (p2((TVar 1::nil)) ) ) ∧ (¬X1 ∨ X2) ⊧ ⊥.
Proof.
  do_Ou (¬X1) X2.
  - do_ferme X1.
  -
Abort.

End Exemple_Tableaux.

This page has been generated by coqdoc