logique_predicats_avec_quantificateurs

Ce module formalise la logique des prédicats avec quantificateur, les prédicats sont n-aires (nombre quelconque d'arguments) mais les termes (arguments des prédicats) ne contiennent pas de symboles de fonctions: ce sont uniquement des variables.

Les formules

Les 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.

Exemples de termes

Check (TVar 7).

: terme

Les formules

Le type des formules logique avec prédicats (sans symbole de fonction) avec quantificateur. Les noms de prédicats sont représentés par des numéros, un prédicat prend un seul argument: une liste de termes. Les quantificateurs prennent en argument le numéro de la variable quantifiée.

Exemples de formules

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

: formule

Check (Ou (Ou (Pred 1 (cons (TVar 1) (cons (TVar 2) nil))) Faux) Vrai).
Check (FORALL 1 (Ou (Ou (Pred 1 (cons (TVar 1) (cons (TVar 2) nil))) Faux) Vrai)).
Check (EXIST 1 (Ou (Ou (Pred 1 (cons (TVar 1) (cons (TVar 2) nil))) Faux) Vrai)).

Notations usuelles pour les formules.

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 "´X₁´":= (Var 1).
Notation "´X₂´":= (Var 2).

Notation "´x₁´":= (TVar 1).
Notation "´x₂´":= (TVar 2).

Notation "´p₁´ l":= (Pred 1 l).
Notation "´p₂´ l":= (Pred 2 l).

Notation "´∀x₁´ frm":= (FORALL 1 frm).
Notation "´∀x₂´ frm":= (FORALL 2 frm).

Notation "´∃x₁´ frm":= (EXIST 1 frm).
Notation "´∃x₂´ frm":= (EXIST 2 frm).

Exemples avec et sans notations:

Check (Var 7).
Check X₇.
Check (Pred 1 (x₁ ::nil)).
Check (p₁ [x₁ , x₂ , x₃ ]).
Check (p₁ [x₁ , x₂ , x₃ ]).
Check (∀x₁ p₁ [x₁ , x₂ , x₃ ]).
Check (∀x₁ ∃x₂ p₁ [x₁ , x₂ , x₃ ]).

termes:

Check (TVar 7).
Check x₇.

Scheme Equality for terme.

Décision de l'égalité sur les formules, Attention ce n'est pas la vraie égalité de formule puisque les noms de variables ne sont pas ignorés.

Function formule_beq (φ ψ:formule) {struct φ}: bool :=
  match φ,ψ with
    | ⊤,⊤ ⇒ true
    | ⊥,⊥ ⇒ true
    | Var p,Var q ⇒ beq_nat p q
    | φ₁ ⇒ φ₂, ψ₁ ⇒ ψ₂ ⇒ formule_beq φ₁ ψ₁ && formule_beq φ₂ ψ₂
    | φ₁ ∧ φ₂,ψ₁ ∧ ψ₂ ⇒ formule_beq φ₁ ψ₁ && formule_beq φ₂ ψ₂
    | φ₁ ∨ φ₂,ψ₁ ∨ ψ₂ ⇒ formule_beq φ₁ ψ₁ && formule_beq φ₂ ψ₂
    | ¬φ,¬ψ ⇒ formule_beq φ ψ
    | (Pred n1 l1) , (Pred n2 l2) ⇒ beq_nat n1 n2 &&
                                     forallb2 terme_beq l1 l2
    | FORALL i φ, FORALL j ψ ⇒ beq_nat i j && formule_beq φ ψ
    | EXIST i φ, EXIST j ψ ⇒ beq_nat i j && formule_beq φ ψ
    | _,_ ⇒ 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 }.

Définition de l'interprétation d'une formule

Valuation

Pour interpréter une formule on a besoin des éléments suivants:

une valuation I des variables propositionnelles,
un domaine d'interprétation pour les termes (D),
une valuation pour les termes, c'est-à-dire les variables de terme puisqu'on n'a pas de symbole de fonction. La valuation interp_t prend donc un numéro de variable de terme en argument et retourne un élément de D.
une valuation pour les prédicats. Un prédicat est désigné par un entier, la valuation interp_p prend donc un entier et retourne l'interprétation du prédicat correspondant: une fonction de DxDxD... -> bool, où D est le domaine d'interprétation des terme.

Par ailleurs on aura besoin de s'assurer que le domaine d'interprétation des termes est non vide, on se donne donc un témoin.

Record Valuation {D:Type} :=
  { vpredicat: nat → (list D → bool);
    vterme: terme → D;
    vproposition: nat → bool;
    temoin:D }.

Substitution dans la valuation des termes

Ajout (où modification) de la valeur d'une variable dans une interprétation. Utile pour l'interprétation des quantificateurs. On se place dans Z pour écrire la fonction.

Definition subst_in_interp interp i (n:Z) :=
  {| vpredicat := interp .(vpredicat ) ;
     vproposition :=interp .(vproposition );
     temoin :=interp .(temoin );

On retourne n si Var i est demandée, sinon on passe la main à l'ancienne fonction.

     vterme := fun trm :terme ⇒
                  let ´(TVar j ) := trm in
                  if beq_nat j i then n
                  else (interp .(vterme )) trm |}.

Notation "I [ i <- x ]" := (subst_in_interp I i x) (at level 89).

Interprétation d'une formule

La sémantique ne peut plus se définir comme une fonction car elle ne peut pas être le résultat d'un calcul (comment calculer la valeur de ∀x∈ℕ,P(x) si le domaine de x est infini).

On définit donc l'interprétation comme une relation entre une formule, une interprétation et un booléen. On prouvera plus bas que cette relation est "fonctionnelle" en utilisant le tiers-exclu. Par ailleurs on prend Z comme domaine d'interprétation des termes mais cette définition est valable pour n'importe quel ensemble non vide.

Inductive interp_def (I:@Valuation Z): formule → bool → Prop :=
| I_Vrai: interp_def I ⊤ table_Vrai
| I_Faux: interp_def I ⊥ table_Faux
| I_Var: ∀ i b, I.(vproposition) i = b → interp_def I (Var i) b
| I_Pred: ∀ i l b, I.(vpredicat) i (map I.(vterme) l) = b
                        → interp_def I (Pred i l) b
| I_Non: ∀ frm b₁ b, interp_def I frm b₁ →
                          negb b₁ = b →
                          interp_def I (¬ frm) b
| I_Ou: ∀ f₁ f₂ b₁ b₂ b, interp_def I f₁ b₁
                               → interp_def I f₂ b₂
                               → orb b₁ b₂ = b
                               → interp_def I (f₁ ∨ f₂) b
| I_Et: ∀ f₁ f₂ b₁ b₂ b, interp_def I f₁ b₁
                               → interp_def I f₂ b₂
                               → andb b₁ b₂ = b
                               → interp_def I (f₁ ∧ f₂) b
| I_Implique: ∀ f₁ f₂ b₁ b₂ b, (interp_def I f₁ b₁)
                                    → (interp_def I f₂ b₂)
                                    → implb b₁ b₂ = b
                                    → (interp_def I (f₁ ⇒ f₂) b)
| I_Forall: ∀ f₁ n, (∀ x:Z, interp_def (subst_in_interp I n x) f₁ true)
                         → interp_def I (FORALL n f₁) true
| I_NotForall: ∀ f₁ n, (∃ x:Z , interp_def (subst_in_interp I n x) f₁ false)
                            → interp_def I (FORALL n f₁) false
| I_Exist: ∀ f₁ n, (∃ x:Z , interp_def (subst_in_interp I n x) f₁ true)
                        → interp_def I (EXIST n f₁) true
| I_NotExist: ∀ f₁ n, (∀ x:Z, interp_def (subst_in_interp I n x) f₁ false)
                           → interp_def I (EXIST n f₁) false.

On utilisera l'abus de notation suivant: I[f]->b à la place de (interp_def I g b). 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.

Notation "I [ f ]-> b" := (interp_def I f b) (at level 50).

Déterminisme et totalité de l'interprétation d'une formule.

Pour les logique précédente ces deux propriétés étaient des conséquences du fait que l'interprétation était définie par une fonction. Maintenant que l'interprétation est une relation il faut démontrer que cette relation correspond en fa it à une fonction (non calculable).

Lemma interp_def_det :
  ∀ f₁ interp b₁,
    interp_def interp f₁ b₁
    → ∀ b₂, interp_def interp f₁ b₂ → b₁ = b₂.

Ceci introduit l'axiome suivant: ∀ P : Prop, P ∨ ¬ P.

Require Import Classical.

La relation d'interprétation est totale: pour toute formule et toute interprétation il existe une valeur interprétation booléenne. Pour information cette preuve utilise le tiers-exclu.

Lemma interp_def_tot :
∀ f₁ interp,
interp_def interp f₁ true ∨ interp_def interp f₁ false.

Corollaire du déterminisme + totalité de l'interpétation.

Lemma interp_not_true :
∀ f₁ interp,
¬ interp_def interp f₁ true ↔ interp_def interp f₁ false.

Exemples d'interprétations

Module Exemples.
  Definition v₁ (n:nat): bool :=
    match n with
      | 1 ⇒ true
      | 2 ⇒ false
      | 3 ⇒ true
      | _ ⇒ false
    end.

  Definition v₂ (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 := {| vpredicat :=vp ; vterme :=vt ; vproposition :=v₁ ; temoin :=0%Z |}.
  Definition III´:Valuation := {| vpredicat :=vp ; vterme :=vt ; vproposition :=v₂ ; temoin :=0%Z |}.

  Lemma Ex1: interp_def III (⊤ ⇒ (⊤ ∨ ⊥)) true.

  Lemma Ex1´: interp_def III (⊤ ⇒ (⊤ ∨ ⊥)) false.

  Lemma Ex2: interp_def III´ (⊤ ⇒ (⊤ ∨ ⊥)) true.

  Lemma Ex3: interp_def III´ (p₁ [x₁ ]) true.

  Lemma Ex4: interp_def III´ (p₁ [x₁ ] ⇒ ⊥) false.

  Lemma Ex5: interp_def III´ (p₁ [x₁ ] ⇒ (⊥ ∧ ⊥)) false.

  Lemma Ex5´: interp_def III´ (p₁ [x₁ ] ⇒ (⊥ ∧ ⊥)) true.

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.

l'interprétation n'est pas nécessairement décidable. En effet l'ensemble sur lequel sont quantifiées les variables peut être infini.

  Definition valuation: Type:= @Valuation Z.
  Definition interpretation: valuation → formule → bool → Prop := interp_def.

Module Exemples_modeles.

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

  Lemma modele2 : ∀ v, ⊧[v ] (X₁ ∨ ¬ X₂ ) ∨ X₂.

End Exemples_modeles.

Module Exemples_conseq.

  Lemma conseq1: (X₁ ∨¬X₂ ) ∧ X₂ ⊧ X₁.

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 : ⊥ ≡ ¬ ⊤.

Lemma eq_not_exist : ∀ i, ∀ f : formule, (¬ (FORALL i f )) ≡ EXIST i (¬f).

Lemma eq_not_forall : ∀ i, ∀ f : formule, (¬ (EXIST i f )) ≡ FORALL i (¬f).

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

Lemma conseq_by_contradiction´: ∀ f₁ f₂: formule, f₁ ⊧ f₂ → f₁ ∧ ¬f₂ ⊧ ⊥.

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

Lemma conseq_by_contradiction: ∀ f₁ f₂: formule, ¬f₂ ∧ f₁ ⊧ ⊥ → f₁ ⊧ f₂.

Preuve par la méthode des tableaux

Lemmes auxilaires pour la méthode des tableaux

Lemma and_affaiblissement_conseq : ∀ v f₁ f₂, v [f₁ ∧f₂ ]->true → v [f₁ ]->true.

Lemma and_affaiblissement_contr : ∀ f₁ f₂, f₁ ⊧ ⊥ → f₁ ∧f₂ ⊧ ⊥ .

Lemma Et_sym : ∀ f₁ f₂, f₁ ∧ f₂ ≡ f₂ ∧ f₁.

Lemma Et_assoc : ∀ f₁ f₂ f₃, f₁ ∧ (f₂ ∧ f₃ ) ≡ (f₁ ∧ f₂ ) ∧ f₃.

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 (¬X₁) (((X₁ ∨ ¬X₂ ) ∧ X₂ ) ∧ ¬X₁ ∧ X₂)).
Eval compute in (extraction_disjuntion (¬X₁) (((X₁ ∨ ¬X₂ ) ∧ X₂ ) ∧ ¬X₁)).
Eval compute in (extraction_disjuntion ((X₁ ∨ ¬X₂ ) ∧ X₂) (((X₁ ∨ ¬X₂ ) ∧ X₂ ) ∧ ¬X₁)).

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 f₁ f₂,
                     ((f₁ ∧ F ⊧ ⊥)
                      ∧ (f₂ ∧ F ⊧ ⊥))
                     → (f₁ ∨ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_Ou´ : ∀ f₁ f₂,
                     (f₁ ⊧ Faux )
                     ∧ (f₂ ⊧ Faux )
                     → (f₁ ∨ f₂ ) ⊧ Faux.

Lemma tableau_nonEt : ∀ F f₁ f₂,
                        (¬f₁ ∧ F ⊧ ⊥) ∧ (¬f₂ ∧ F ⊧ ⊥)
                        → ¬(f₁ ∧ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_nonEt´ : ∀ f₁ f₂,
                        (¬f₁ ⊧ ⊥) ∧ (¬f₂ ⊧ ⊥)
                        → ¬(f₁ ∧ f₂ ) ⊧ ⊥.

Lemma tableau_implique : ∀ F f₁ f₂,
                           (¬f₁ ∧ F ⊧ ⊥) ∧ (f₂ ∧ F ⊧ ⊥)
                           → (f₁ ⇒ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_implique´ : ∀ f₁ f₂,
                           (¬f₁ ⊧ ⊥) ∧ (f₂ ⊧ ⊥)
                           → (f₁ ⇒ f₂ ) ⊧ ⊥.

Lemma tableau_Et : ∀ F f₁ f₂, f₁ ∧ f₂ ∧ F ⊧ ⊥ → (f₁ ∧ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_Et´ : ∀ f₁ f₂, f₁ ∧ f₂ ⊧ ⊥ → (f₁ ∧ f₂ ) ⊧ ⊥.

Lemma tableau_nonimplique : ∀ F f₁ f₂, f₁ ∧ ¬f₂ ∧ F ⊧ ⊥ → ¬(f₁ ⇒ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_nonimplique´ : ∀ f₁ f₂, f₁ ∧ ¬f₂ ⊧ ⊥ → ¬(f₁ ⇒ f₂ ) ⊧ ⊥.

Lemma tableau_nonOu : ∀ F f₁ f₂, ¬f₁ ∧ ¬f₂ ∧ F ⊧ ⊥ → ¬(f₁ ∨ f₂ ) ∧ F ⊧ ⊥.

Lemma tableau_nonOu´ : ∀ f₁ 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 ∧ ¬f ) ∧ F ⊧ ⊥.

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

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

Les règles pour les quantificateurs

Ces règles sont plus compliquées à exprimer et à démontrer car elle font appelle à la notion de variables liées, libre et fraîches. On commence par définir ces notions et leur propriétés, puis on énonce les règles pour les quantificateurs.

Notions de variables (de terme) fraîches, liées etc.

Inductive is_fresh_terme_list (i:nat): list terme → Prop :=
| isFreshTrmNil : is_fresh_terme_list i nil
| isFreshTrmCons : ∀ j l, is_fresh_terme_list i l → i≠j
→ is_fresh_terme_list i (TVar j ::l).

Une variable de terme i est fraîche dans la formule φ si elle n'apparaît nulle part dans φ.

Inductive is_fresh i: formule → Prop :=
| isFreetrue: is_fresh i ⊤
| isFreefalse: is_fresh i ⊥
| isFreeV: ∀ j, is_fresh i (Var j)
| isFreeNon: ∀ φ, is_fresh i φ → is_fresh i (¬φ)
| isFreeEt: ∀ φ ψ, is_fresh i φ →is_fresh i ψ → is_fresh i (φ ∧ψ)
| isFreeOr: ∀ φ ψ, is_fresh i φ → is_fresh i ψ → is_fresh i (φ ∨ψ)
| isFreeImplique: ∀ φ ψ, is_fresh i φ → is_fresh i ψ → is_fresh i (φ ⇒ ψ)
| isFreePred: ∀ p lt, is_fresh_terme_list i lt → is_fresh i (Pred p lt)
| isFreeFORALL: ∀ j φ, is_fresh i φ → i≠j → is_fresh i (FORALL j φ)
| isFreeEXIST: ∀ j φ, is_fresh i φ → i≠j → is_fresh i (EXIST j φ).

Une variable i est non-liée dans une formule φ si elle n'a pas d'occurrence dans un quantificateur.

Inductive is_not_bound i: formule → Prop :=
| isNotBoundtrue: is_not_bound i ⊤
| isNotBoundfalse: is_not_bound i ⊥
| isNotBoundV: ∀ j, is_not_bound i (Var j)
| isNotBoundNon: ∀ φ, is_not_bound i φ → is_not_bound i (¬φ)
| isNotBoundEt: ∀ φ ψ, is_not_bound i φ →is_not_bound i ψ → is_not_bound i (φ ∧ψ)
| isNotBoundOr: ∀ φ ψ, is_not_bound i φ → is_not_bound i ψ → is_not_bound i (φ ∨ψ)
| isNotBoundImplique: ∀ φ ψ, is_not_bound i φ
→ is_not_bound i ψ → is_not_bound i (φ ⇒ ψ)
| isNotBoundPred: ∀ p lt, is_not_bound i (Pred p lt)
| isNotBoundFORALL: ∀ j φ, is_not_bound i φ → i≠j → is_not_bound i (FORALL j φ)
| isNotBoundEXIST: ∀ j φ, is_not_bound i φ → i≠j → is_not_bound i (EXIST j φ).

Une variable fraîche est également non-liée

Lemma fresh_is_not_bound : ∀ φ i, is_fresh i φ → is_not_bound i φ.

On peut changer l'interprétation d'une variable fraîche sans changer l'interprétation (puisqu'elle n'appraît pas dans la formule).

Lemma subst_fresh_id: ∀ i φ,
                        is_fresh i φ
                        → ∀ b v x, (subst_in_interp v i x ) [φ ]-> b
                                         ↔ v [φ ]-> b.

Substitution de variable dans une formule

On se donne une opération de substitution de variable par un terme dans une formule.

Function substtermvar (n:nat) (v:nat) (fr:formule) {struct fr}: formule :=
  match fr with
      ⊤ ⇒ ⊤
    | ⊥ ⇒ ⊥
    | Var x ⇒ Var x
    | Non x ⇒ Non (substtermvar n v x)
    | Ou x x0 ⇒ Ou (substtermvar n v x) (substtermvar n v x0)
    | Et x x0 ⇒ Et (substtermvar n v x) (substtermvar n v x0)
    | Implique x x0 ⇒ Implique (substtermvar n v x) (substtermvar n v x0)
    | (Pred i l) ⇒
      Pred i (List.map (fun trm´ ⇒
                          let ´(TVar v´) := trm´ in
                          if beq_nat v´ n then TVar v else TVar v´) l)
    | FORALL i fr´ ⇒ if beq_nat n i || beq_nat v i then fr else FORALL i (substtermvar n v fr´)
    | EXIST i fr´ ⇒ if beq_nat n i || beq_nat v i then fr else EXIST i (substtermvar n v fr´)
  end.

Notation "f [ i <= trm ]" := (substtermvar i trm f) (at level 85).

Eval compute in (substtermvar 1 2 (p₁ [x₁ ,x₁ ,x₃ ])).
Eval compute in (substtermvar 1 2 (p₁ [x₂ ,x₁ ,x₃ ])).
Eval compute in (substtermvar 1 2 (∀x₁ p₁ [x₁ ,x₁ ,x₃ ])).
Eval compute in (substtermvar 1 3 ((∀x₁ p₁ [x₁ ,x₁ ,x₃ ]) ∨ ∃x₃ p₁ [x₁ ,x₁ ,x₃ ])).
Eval compute in (substtermvar 1 2 ((∀x₁ p₁ [x₁ ,x₁ ,x₃ ]) ∨ ∃x₃ p₁ [x₁ ,x₁ ,x₃ ])).
Eval compute in (substtermvar 1 2 ((∀x₁ p₁ [x₁ ,x₁ ,x₃ ]) ∨ ∀x₃ p₁ [x₁ ,x₁ ,x₃ ])).

Lemma subst_substterm_pred:
  ∀ n l i v var b,
    (v [substtermvar i var (Pred n l)]-> b )
    ↔ (subst_in_interp v i (vterme v (TVar var)) [Pred n l ]-> b ).

Lemma substinterp_substvar_eq:
  ∀ i v φ var b (hfreshv:is_not_bound var φ) (hfreshi:is_not_bound i φ),
    ((v [substtermvar i var φ ]-> b ) ↔ (subst_in_interp v i (v.(vterme) (TVar var)) [φ ]-> b )).

Lemma tableau_forall :
  ∀ F f₁ i var,
    is_not_bound var f₁
    → is_not_bound i f₁
    → substtermvar i var f₁ ∧ (FORALL i f₁ ) ∧ F ⊧ ⊥
    → (FORALL i f₁ ) ∧ F ⊧ ⊥.

Lemma tableau_exist:
  ∀ F f₁ i j,
    is_fresh j f₁
    → is_not_bound i f₁
    → is_fresh j F
    → substtermvar i j f₁ ∧ F ⊧ ⊥
    → EXIST i f₁ ∧ F ⊧ ⊥.

Lemma tableau_exist´:
  ∀ f₁ i j,
    is_fresh j f₁
    → is_not_bound i f₁
    → substtermvar i j f₁ ⊧ ⊥
    → EXIST i f₁ ⊧ ⊥.

Exemples d'application des tableaux.

Module Exemple_Tableaux.
  Lemma conseq1: (X₁ ∨¬X₂ ) ∧ X₂ ⊧ X₁.
  Proof.
    apply conseq_by_contradiction.
    do_Ou X₁ (¬X₂).
    - do_ferme X₁.
    - do_ferme X₂.
  Qed.

  Lemma conseq1´: (X₁ ∨¬(p₁ [x₁ ])) ∧ p₁ [x₁ ] ⊧ X₁.
  Proof.
    apply conseq_by_contradiction.
    do_Ou X₁ (¬p₁ [x₁ ]).
    - do_ferme X₁.
    - do_ferme (p₁ [x₁ ]).
  Qed.

  Lemma conseq1´´´´: (∃x₁ ((X₁ ∨¬(p₁ [x₁ ])) ∧ p₁ [x₁ ])) ⊧ X₁.
  Proof.
    apply conseq_by_contradiction.
    do_exist (∃x₁ ((X₁ ∨ ¬p₁ [x₁ ]) ∧ p₁ [x₁ ])) 9.
    do_Et ((X₁ ∨ ¬p₁ [x₉ ]))(p₁ [x₉ ]).
    do_Ou X₁ (¬p₁ [x₉ ]).
    - do_ferme X₁.
    - do_ferme (p₁ [x₉ ]).
  Qed.

  Lemma conseq1´´´: p₁ [x₃ ] ∧ (∃x₁ ((X₁ ∨¬(p₁ [x₁ ])) ∧ p₁ [x₁ ])) ⊧ X₁.
  Proof.
    apply conseq_by_contradiction.
    do_exist (∃x₁ ((X₁ ∨ ¬p₁ [x₁ ]) ∧ p₁ [x₁ ])) 9.
    do_Et ((X₁ ∨ ¬p₁ [x₉ ]))(p₁ [x₉ ]).
    do_Ou X₁ (¬p₁ [x₉ ]).
    - do_ferme X₁.
    - do_ferme (p₁ [x₉ ]).
  Qed.

  Lemma conseq1´´: (X₁ ∨¬(p₁ [x₁ ])) ∧ (∀x₁ p₁ [x₁ ]) ⊧ X₁.
  Proof.
    apply conseq_by_contradiction.
    do_Ou X₁ (¬p₁ [x₁ ]).
    - do_ferme X₁.
    - do_Forall (∀x₁ (p₁ [x₁ ])) 1.
      do_ferme (p₁ [x₁ ]).
  Qed.

  Lemma foralneg: (¬∀x₁ p₁ [x₁ ]) ⊧ ∃x₂ ¬p₁ [x₂ ].
  Proof.
    apply conseq_by_contradiction.
    rewrite eq_not_exist.
    do_exist (∃x₁ ¬(p₁ [x₁ ])) 3.
    rewrite eq_not_forall.
    do_Forall (∀x₂ (¬(¬p₁ [x₂ ]))) 3.
    do_ferme (¬p₁ [x₃ ]).
  Qed.

  Lemma existneg: (¬∃x₁ p₁ [x₁ ]) ⊧ ∀x₂ ¬p₁ [x₂ ].
  Proof.
    apply conseq_by_contradiction.
    rewrite eq_not_exist.
    do_exist (∃x₂ (¬(¬(p₁ [x₂ ])))) 3.
    rewrite eq_not_forall.
    do_Forall (∀x₁ (¬p₁ [x₁ ])) 3.
    do_ferme (¬p₁ [x₃ ]).
  Qed.

  Lemma conseq2 : (X₁ ∧ X₃ ) ∧ (¬X₁ ∨ X₂ ) ⊧ ⊥.
  Proof.
    do_Ou (¬X₁) X₂.
    - do_ferme X₁.
    -

Echec

  Abort.

  Lemma conseq3 : (¬ (X₁ ⇒ (X₂ ⇒ X₁ ))) ∧ ⊤ ⊧ ⊥.
  Proof.
    do_NonImplique X₁ (X₂ ⇒ X₁).
    do_NonImplique X₂ X₁.
    do_ferme X₁.
  Qed.

  Lemma conseq4 : (¬ (X₁ ∨ X₂ )) ∧ X₁ ⊧ ⊥.
  Proof.
    do_nonOu X₁ X₂.
    do_ferme X₁.
  Qed.

  Lemma conseq5 : (¬ (X₁ ∧ X₂ )) ∧ X₁ ∧ X₂ ⊧ ⊥.
  Proof.
    do_nonEt X₁ X₂.
    - do_ferme X₁.
    - do_ferme X₂.
  Qed.

  Lemma conseq5´ : (¬ ((p₂ ((TVar 1::nil )) ) ∧ X₂ )) ∧ (p₂ ((TVar 1::nil )) ) ∧ X₂ ⊧ ⊥.
  Proof.
    do_nonEt (p₂ ((TVar 1::nil )) ) X₂.
    - do_ferme (p₂ ((TVar 1::nil )) ).
    - do_ferme X₂.
  Qed.

  Lemma conseq6 : (X₁ ∧ (p₂ ((TVar 1::nil )) ) ) ∧ (¬X₁ ∨ X₂ ) ⊧ ⊥.
  Proof.
    do_Ou (¬X₁) X₂.
    - do_ferme X₁.
    -

Echec

Abort.

End Exemple_Tableaux.

Print Assumptions tableau_forall.
Print Assumptions tableau_exist.
Print Assumptions interp_def_tot.

This page has been generated by coqdoc