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_predicats


Logique des prédicats sans quantificateur

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.
Proof.
  intros t1 t2.
  split; intro H.
  - destruct t1;destruct t2.
    destruct (eq_nat_dec n n0);auto.
    simpl in H.
    rewrite (internal_nat_dec_bl n n0 H).
    reflexivity.
  - subst.
    destruct t2;simpl;auto.
    induction n;simpl;auto.
Qed.

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.
Proof.
  induction l1;simpl;intros.
  - destruct l2;simpl;auto.
    + split;intros.
      × constructor.
      × constructor.
    + split;intros.
      × inversion H.
      × inversion H.
  - destruct l2;simpl;auto.
    + split;intros.
      × inversion H.
      × inversion H.
    + split;intros.
      × { constructor.
          - inversion H;subst;auto.
            apply terme_eq_ok;assumption.
          - inversion H;subst.
            apply IHl1.
            assumption. }
      × { constructor.
          - inversion H;subst;auto.
            apply terme_eq_ok.
            reflexivity.
          - inversion H;subst.
            apply IHl1.
            assumption. }
Qed.

Lemma formule_eq_okr : ∀ φ ψ:formule, formule_beq φ ψ = true → φ = ψ.
Proof.
  intros φ ψ H.
  functional induction formule_beq φ ψ;auto.
  - rewrite beq_nat_true_iff in H;subst;auto.
  - apply Bool.andb_true_iff in H.
    destruct H.
    rewrite IHb,IHb0;auto.
  - apply Bool.andb_true_iff in H.
    destruct H.
    rewrite IHb,IHb0;auto.
  - apply Bool.andb_true_iff in H.
    destruct H.
    rewrite IHb,IHb0;auto.
  - rewrite IHb;auto.
  - apply Bool.andb_true_iff in H.
    destruct H.
    rewrite beq_nat_true_iff in H;subst;auto.
    apply Forall2_forallb2_iff in H0.
    apply f_equal2;auto.
    rewrite terme_eq_true_eq_iff in H0.
    apply Forall2_eq_eq_iff.
    assumption.
  - discriminate.
Qed.

Lemma formule_eq_okl : ∀ φ ψ:formule, φ = ψ → formule_beq φ ψ = true.
Proof.
  intros φ ψ H.
  subst.
  induction ψ;simpl;subst;auto.
  - rewrite <- beq_nat_refl.
    reflexivity.
  - rewrite IHψ1.
    rewrite IHψ2.
    reflexivity.
  - rewrite IHψ1.
    rewrite IHψ2.
    reflexivity.
  - rewrite IHψ1.
    rewrite IHψ2.
    reflexivity.
  - rewrite <- beq_nat_refl.
    simpl.
    apply Forall2_forallb2_iff.
    apply terme_eq_true_eq_iff.
    apply Forall2_eq_eq_iff.
    reflexivity.
Qed.

Lemma formule_eq_ok : ∀ φ ψ:formule, φ = ψ ↔ formule_beq φ ψ = true.
Proof.
  intros φ ψ.
  split;intros.
  apply formule_eq_okl;auto.
  apply formule_eq_okr;auto.
Qed.

Lemma formule_neq_ok : ∀ φ ψ:formule, φ ≠ ψ ↔ formule_beq φ ψ = false.
Proof.
  intros φ ψ.
  split;intros.
  - destruct (formule_beq φ ψ) eqn:heq;auto.
    apply formule_eq_ok in heq.
    subst.
    elim H;auto.
  - intro abs;subst.
    rewrite → (formule_eq_okl ψ ψ) in H.
    + discriminate.
    + reflexivity.
Qed.

Lemma formule_eq_dec : ∀ f1 f2: formule, {f1 = f2} + {f1≠f2}.
Proof.
  intros f1 f2.
  destruct (formule_beq f1 f2) eqn:heq.
  - left.
    eapply formule_eq_ok.
    assumption.
  - right.
    apply formule_neq_ok.
    assumption.
Qed.

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.


Arguments Valuation [D].

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.
  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 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).
  intros p1 p2.
  unfold equivalent.
  smpl×.
  split.
  - intros [h1 h2] v.
    specialize (h1 v).
    specialize (h2 v).
    destruct (interp_def v p2);destruct (interp_def v p1);simpl;intros;auto;try reflexivity;try now discriminate.
    + discriminate h2;reflexivity.
    + discriminate h1;reflexivity.
  - intros h.
    split; intros v h'.
    + apply h;assumption.
    + apply h;assumption.
Qed.


Module Exemples_modeles.
  Lemma modele1 : ∀ v n, ⊧[v] (Var n) ∨ ¬ (Var n).
  Proof.
    intros v n.
    red.
    smpl.
    destruct (propositions v n);simpl.
    - reflexivity.
    - reflexivity.
  Qed.

  Lemma modele2 : ∀ v, ⊧[v] (X1 ∨ ¬ X2) ∨ X2.
  Proof.
    intros v.
    red.
    smpl.
    destruct (v.(propositions) 1).
    - destruct (v.(propositions) 2).
      + reflexivity.
      + reflexivity.
    - destruct (v.(propositions) 2).
      + reflexivity.
      + reflexivity.
  Qed.

End Exemples_modeles.

Module Exemples_conseq.
  Lemma conseq1: (X1∨¬X2) ∧ X2 ⊧ X1.
  Proof.
    repeat red.
    smpl×.
    intros v H.
    simpl in ×.
    destruct (propositions v 1).
    - reflexivity.
    - destruct (propositions v 2).
      + discriminate H.
      + discriminate H.
  Qed.

End Exemples_conseq.

Preuves d'équivalences entre formules


Lemma eq_implique : ∀ x y : formule, x ⇒ y ≡ ¬x ∨ y.
Proof.
  intros x y.
  smpl×.
  split;intros.
  - functional inversion H;subst;clear H;simpl.
    + reflexivity.
    + destruct (interp_def v y);reflexivity.
  - destruct (interp_def v x);simpl in ×.
    + assumption.
    + reflexivity.
Qed.

Lemma eq_et : ∀ x y: formule, (x ∧ y) ≡ ¬ (¬x ∨ ¬y).
Proof.
  intros x y.
  smpl×.
  split;intros.
  - destruct (interp_def v x).
    + destruct (interp_def v y).
      × reflexivity.
      × discriminate.
    + simpl in H. destruct (interp_def v y); discriminate.
  - destruct (interp_def v x).
    + destruct (interp_def v y).
      × reflexivity.
      × discriminate.
    + destruct (interp_def v y);discriminate.
Qed.

Lemma eq_not : ⊥ ≡ ¬ ⊤.
Proof.
  simpl.
  unfold equiv,consequence,est_modele. simpl.
  split;intros.
  - discriminate.
  - discriminate.
Qed.


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


Lemma conseq_by_contradiction': ∀ f1 f2: formule, f1 ⊧ f2 → f1 ∧ ¬f2 ⊧ ⊥.
Proof.
  intros f1 f2.
  smpl×.
  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) ; discriminate.
Qed.

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

Lemma conseq_by_contradiction: ∀ f1 f2: formule, ¬f2 ∧ f1 ⊧ ⊥ → f1 ⊧ f2.
Proof.
  intros f1 f2.
  smpl×.
  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 : ∀ v f1 f2, ⊧[v] f1∧f2 → ⊧[v]f1.
Proof.
  intros v f1 f2 H.
  smpl×.
  destruct (interp_def v f1).
  - reflexivity.
  - simpl in H. destruct (interp_def v f2);discriminate H.
Qed.

Lemma and_affaiblissement_contr : ∀ 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 : ∀ f1 f2, f1 ∧ f2 ≡ f2 ∧ f1.
Proof.
  intros f1 f2.
  smpl×.
  split;intros.
  - destruct (interp_def v f1).
    + destruct (interp_def v f2).
      × assumption.
      × discriminate H.
    + simpl in H. destruct (interp_def v f2); discriminate 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 : ∀ f1 f2 f3, f1 ∧ (f2 ∧ f3) ≡ (f1 ∧ f2) ∧ f3.
Proof.
  intros f1 f2 f3.
  smpl×.
  split.
  - intros v H.
    destruct (interp_def v f1); destruct (interp_def v f2); destruct (interp_def v f3); try assumption; try discriminate.
  - intros v 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_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 ∧ ⊤.
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 :
  ∀ 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.
  - apply formule_eq_ok in e0.
    inversion H;subst;reflexivity.
  - apply formule_eq_ok in e1.
    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 : ∀ F f1 f2,
                     (f1 ∧ F ⊧ ⊥)
                     ∧ (f2 ∧ F ⊧ ⊥)
                     → (f1 ∨ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 H.
  smpl×.
  destruct H as [h h'].
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);simpl in *;
  destruct (interp_def v F);auto.
Qed.

Lemma tableau_Ou' : ∀ f1 f2,
                     (f1 ⊧ ⊥)
                     ∧ (f2 ⊧ ⊥)
                     → (f1 ∨ f2) ⊧ ⊥.
Proof.
  intros f1 f2 H.
  smpl×.
  destruct H as [h h'].
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);simpl in *;auto.
Qed.

Lemma tableau_nonEt : ∀ F f1 f2,
                        (¬f1 ∧ F ⊧ ⊥) ∧ (¬f2 ∧ F ⊧ ⊥)
                        → ¬(f1 ∧ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 H.
  smpl×.
  destruct H as [h h'].
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);simpl in *;
  destruct (interp_def v F);auto.
Qed.

Lemma tableau_nonEt' : ∀ f1 f2,
                        (¬f1 ⊧ ⊥) ∧ (¬f2 ⊧ ⊥)
                        → ¬(f1 ∧ f2) ⊧ ⊥.
Proof.
  intros f1 f2 H.
  smpl×.
  destruct H as [h h'].
  intros v H0.
  specialize (h v).
  specialize (h' v).
  apply h.
  simpl in ×.
  destruct (interp_def v f1);destruct (interp_def v f2);simpl in *;auto.
Qed.

Lemma tableau_implique : ∀ F f1 f2,
                           (¬f1 ∧ F ⊧ ⊥) ∧ (f2 ∧ F ⊧ ⊥)
                           → (f1 ⇒ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 H.
  smpl×.
  destruct H as [h h'].
  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' : ∀ f1 f2,
                           (¬f1 ⊧ ⊥) ∧ (f2 ⊧ ⊥)
                           → (f1 ⇒ f2) ⊧ ⊥.
Proof.
  intros f1 f2 H.
  smpl×.
  destruct H as [h h'].
  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 : ∀ F f1 f2, f1 ∧ f2 ∧ F ⊧ ⊥ → (f1 ∧ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 h.
  smpl×.
  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_Et' : ∀ f1 f2, f1 ∧ f2 ⊧ ⊥ → (f1 ∧ f2) ⊧ ⊥.
Proof.
  intros f1 f2 h.
  smpl×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_nonimplique : ∀ F f1 f2, f1 ∧ ¬f2 ∧ F ⊧ ⊥ → ¬(f1 ⇒ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 h.
  smpl×.
  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' : ∀ f1 f2, f1 ∧ ¬f2 ⊧ ⊥ → ¬(f1 ⇒ f2) ⊧ ⊥.
Proof.
  intros f1 f2 h.
  smpl×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_nonOu : ∀ F f1 f2, ¬f1 ∧ ¬f2 ∧ F ⊧ ⊥ → ¬(f1 ∨ f2) ∧ F ⊧ ⊥.
Proof.
  intros F f1 f2 h.
  smpl×.
  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' : ∀ f1 f2, ¬f1 ∧ ¬f2 ⊧ ⊥ → ¬(f1 ∨ f2) ⊧ ⊥.
Proof.
  intros f1 f2 h.
  smpl×.
  intros v H0.
  specialize (h v).
  destruct (interp_def v f1);destruct (interp_def v f2);auto.
Qed.

Lemma tableau_ferme_branche : ∀ F f, (F ∧ f) ∧ ¬f ⊧ ⊥.
Proof.
  intros F f v H.
  smpl×.
  destruct (interp_def v F);destruct (interp_def v f);discriminate.
Qed.

Lemma tableau_ferme_branche' : ∀ 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'' : ∀ F f, (f ∧ ¬f) ∧ F ⊧ ⊥.
Proof.
  intros F f.
  setoid_rewrite <- Et_assoc.
  apply tableau_ferme_branche'.
Qed.

Lemma tableau_ferme_branche''' : ∀ f, f ∧ ¬f ⊧ ⊥.
Proof.
  intros f.
  intros.
  intros v h.
  unfold consequence,est_modele,equiv in ×.
  smpl×.
  destruct (interp_def v f);discriminate.
Qed.

Lemma p_et_p_eq : ∀ a, a∧a ≡ a.
Proof.
  intros a.
  unfold equiv,consequence,est_modele.
  simpl.
  split.
  - intros v H.
    destruct (interp_def v a);auto.
  - intros v H.
    destruct (interp_def v a);auto.
Qed.


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