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.
| Non: formule ⟶ formule
| Ou: formule ⟶ formule ⟶ formule
| Et: formule ⟶ formule ⟶ formule
| Implique: formule ⟶ formule ⟶ formule.

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.

Inductive is_reduced : formule ⟶ Prop :=
  Vrai_is_red: is_reduced ⊤
| Var_is_red: forall i, is_reduced (Var i)
| 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).

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] f1∧f2 ⟶ ⊧[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 ⊧ ⊥ ⟶ f1∧f2 ⊧ ⊥.
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, p∧p ≡ 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