loglangcoq.logique.logique_predicats_avec_quantificateurs

Logique des prédicats avec quantificateur (sans fonction)

Ce module formalise la logique des prédicats avec quantificateurs, 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.
Open Scope bool_scope.

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.
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 f_equal2;auto.
    apply Forall2_forallb2_iff in H0.
    rewrite terme_eq_true_eq_iff in H0.
    apply Forall2_eq_eq_iff.
    assumption.
  - apply Bool.andb_true_iff in H.
    destruct H.
    symmetry in H.
    rewrite (beq_nat_eq _ _ H).
    rewrite IHb;auto.
  - apply Bool.andb_true_iff in H.
    destruct H.
    symmetry in H.
    rewrite (beq_nat_eq _ _ H).
    rewrite IHb;auto.
  - 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.
  - rewrite <- (beq_nat_refl n).
    simpl.
    assumption.
  - rewrite <- (beq_nat_refl n).
    simpl.
    assumption.
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.

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 50).

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.

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

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

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₂.
Proof.
  intros f₁.
  induction f₁;intros interp b₁ h b₂ h';try solve [simp1].
  - simp1. rewrite (IHf₁ _ _ H0 _ H1). reflexivity.
  - simp1. rewrite (IHf₁1 _ _ H1 _ H3). rewrite (IHf₁2 _ _ H2 _ H4). reflexivity.
  - simp1. rewrite (IHf₁1 _ _ H1 _ H3). rewrite (IHf₁2 _ _ H2 _ H4). reflexivity.
  - simp1. rewrite (IHf₁1 _ _ H1 _ H3). rewrite (IHf₁2 _ _ H2 _ H4). reflexivity.
  - simp1.
    + destruct H3. specialize (H2 x).
      rewrite (IHf₁ _ _ H2 _ H). reflexivity.
    + destruct H2. specialize (H3 x).
      rewrite (IHf₁ _ _ H3 _ H). reflexivity.
  - simp1.
    + destruct H2. specialize (H3 x).
      rewrite (IHf₁ _ _ H3 _ H). reflexivity.
    + destruct H3. specialize (H2 x).
      rewrite (IHf₁ _ _ H2 _ H). reflexivity.
Qed.

Ltac finish := solve[left;econstructor;eauto 3
                    |right;econstructor;eauto 3].

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.
Proof.
  intros f₁.
  induction f₁;intros interp.   - left. constructor 1.
  - right. constructor 2.
  - destruct (vproposition interp n) eqn:heq; finish.
  - destruct (IHf₁ interp);finish.
  - destruct (IHf₁1 interp);destruct (IHf₁2 interp); finish.
  - destruct (IHf₁1 interp);destruct (IHf₁2 interp); finish.
  - destruct (IHf₁1 interp);destruct (IHf₁2 interp); finish.
  - destruct (interp.(vpredicat) n (map interp.(vterme) l)) eqn:heq.
    + left. constructor. assumption.
    + right. constructor. assumption.
  - destruct (classic (∀ x : Z, interp_def (subst_in_interp interp n x) f₁ true)).
    + left. constructor. assumption.
    + right. apply I_NotForall.
      apply not_all_ex_not in H.
      destruct H.
      destruct (IHf₁ (subst_in_interp interp n x)).
      × contradiction.
      × { ∃ x. assumption. }
  - destruct (classic (∃ x : Z , interp_def (subst_in_interp interp n x) f₁ true)).
    + left. constructor. assumption.
    + right. apply I_NotExist.
      intros x.
      apply not_ex_all_not with (n:=x) in H.
      destruct (IHf₁ (subst_in_interp interp n x)).
      × contradiction.
      × assumption.
Qed.

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.
Proof.
  intros f₁ interp.
  split;intro h.
  - destruct (interp_def_tot f₁ interp).
    + contradiction.
    + assumption.
  - intro abs.
    assert (true =false).
    + apply (interp_def_det f₁ interp).
      × assumption.
      × assumption.
    + discriminate.
Qed.

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

  Hint Constructors interp_def: interp.

  Lemma Ex1: interp_def III (⊤ ⇒ (⊤ ∨ ⊥)) true.
  Proof.
    eauto with interp.
  Qed.

  Lemma Ex1': interp_def III (⊤ ⇒ (⊤ ∨ ⊥)) false.
  Proof.
    eauto with interp.
  Abort.

  Lemma Ex2: interp_def III' (⊤ ⇒ (⊤ ∨ ⊥)) true.
  Proof.
    eauto with interp.
  Qed.

  Lemma Ex3: interp_def III' (p₁ [x₁ ]) true.
  Proof.
    eauto with interp.
  Qed.

  Lemma Ex4: interp_def III' (p₁ [x₁ ] ⇒ ⊥) false.
  Proof.
    eauto with interp.
  Qed.

  Lemma Ex5: interp_def III' (p₁ [x₁ ] ⇒ (⊥ ∧ ⊥)) false.
  Proof.
    eauto with interp.
  Qed.

  Lemma Ex5': interp_def III' (p₁ [x₁ ] ⇒ (⊥ ∧ ⊥)) true.
  Proof.
    eauto with interp.
  Abort.

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 ).
  Proof.
    intros v n.
    destruct (vproposition v n) eqn:heq.
    - econstructor;eauto with interp.
    - econstructor;eauto with interp.
  Qed.

  Lemma modele2 : ∀ v, ⊧[v ] (X₁ ∨ ¬ X₂ ) ∨ X₂.
  Proof.
    intros v.
    destruct (v.(@vproposition Z) 1) eqn:heq.
    - destruct (v.(@vproposition Z) 2) eqn:heq'.
      + econstructor;eauto with interp.
      + econstructor;eauto with interp.
    - destruct (v.(@vproposition Z) 2) eqn:heq'.
      + econstructor;eauto with interp.
      + econstructor;eauto with interp.
  Qed.

End Exemples_modeles.

Module Exemples_conseq.

  Lemma conseq1: (X₁ ∨¬X₂ ) ∧ X₂ ⊧ X₁.
  Proof.
    unfold consequence,est_modele.
    intros v h;simp.
    case_eq (vproposition v 1);intros.
    - constructor. assumption.
    - rewrite hb0 in ×.
      rewrite H in ×.
      simpl in ×.
      discriminate.
  Qed.

End Exemples_conseq.

Preuves d'équivalences entre formules

Lemma eq_implique : ∀ x y : formule, x ⇒ y ≡ ¬x ∨ y.
Proof.
  intros x y.
  simpl.
  unfold equiv,consequence,est_modele. simpl.
  split;intros.
  - simp.
    destruct b₁;simp.
    + apply I_Ou with false true;auto.
      apply I_Non with true;auto.
    + apply I_Ou with true b₂;auto.
      apply I_Non with false;auto.
  - simp.
    destruct b₁0;simp.
    + apply I_Implique with true true;auto.
    + apply I_Implique with false b₂;auto;simp.
Qed.

Lemma eq_et : ∀ x y: formule, (x ∧ y ) ≡ ¬ (¬x ∨ ¬y ).
Proof.
  intros x y.
  unfold equiv,consequence,est_modele. simpl.
  split;intros.
  - simp. apply I_Non with false;auto.
    apply I_Ou with false false;auto.
    + apply I_Non with true;auto.
    + apply I_Non with true;auto.
  - simp.
    apply I_Et with true true;auto.
Qed.

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

Lemma eq_not_exist : ∀ i, ∀ f : formule, (¬ (FORALL i f )) ≡ EXIST i (¬f).
Proof.
  intros i f.
  unfold equiv,consequence,est_modele.
  split;intros;simp.
  - discriminate.
  - destruct H4.
    apply I_Exist.
    ∃ (x).
    apply I_Non with false.
    + assumption.
    + reflexivity.
  - destruct H1.
    apply I_Non with false. simp.
    + eapply I_NotForall.
      ∃ (x).
      assumption.
    + reflexivity.
Qed.

Lemma eq_not_forall : ∀ i, ∀ f : formule, (¬ (EXIST i f )) ≡ FORALL i (¬f).
Proof.
  intros i f.
  unfold equiv,consequence,est_modele.
  split;intros;simp.
  - discriminate.
  - apply I_Forall.
    intros x.
    apply I_Non with false.
    + auto.
    + reflexivity.
  - apply I_Non with false.
    + apply I_NotExist.
      intros x.
      specialize (H1 x).
      simp.
    + reflexivity.
Qed.

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

Lemma conseq_by_contradiction': ∀ f₁ f₂: formule, f₁ ⊧ f₂ → f₁ ∧ ¬f₂ ⊧ ⊥.
Proof.
  intros f₁ f₂.
  unfold consequence, est_modele.
  intros H v H0.
  simpl in H0.
  exfalso.
  destruct (interp_def_tot f₁ v);simp.
  - eapply interp_true_false;eauto.
  - discriminate.
Qed.

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

Lemma conseq_by_contradiction: ∀ f₁ f₂: formule, ¬f₂ ∧ f₁ ⊧ ⊥ → f₁ ⊧ f₂.
Proof.
  intros f₁ f₂.
  unfold consequence, est_modele.
  simpl.
  intros H v heq.
  specialize (H v).
  destruct (interp_def_tot f₂ v).
  - assumption.
  - absurd (interp_def v ⊥ true).
    + intro abs. simp.
    + apply H.
      apply I_Et with true true.
      × econstructor;eauto.
      × assumption.
      × reflexivity.
Qed.

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.
Proof.
  intros v f₁ f₂ H.
  simp.
Qed.

Lemma and_affaiblissement_contr : ∀ f₁ f₂, f₁ ⊧ ⊥ → f₁ ∧f₂ ⊧ ⊥ .
Proof.
  intros f₁ f₂ H.
  unfold consequence, est_modele.
  intros v H0.
  simp.
  apply H.
  assumption.
Qed.

Lemma Et_sym : ∀ f₁ f₂, f₁ ∧ f₂ ≡ f₂ ∧ f₁.
Proof.
  intros f₁ f₂.
  split.
  - intros v H.
    inversion H. subst. clear H.
    simp.
    econstructor;eauto.
  - intros v H.
    inversion H. subst. clear H.
    simp.
    econstructor;eauto.
Qed.

Lemma Et_assoc : ∀ f₁ f₂ f₃, f₁ ∧ (f₂ ∧ f₃ ) ≡ (f₁ ∧ f₂ ) ∧ f₃.
Proof.
  intros f₁ f₂ f₃.
  split.
  - repeat red; simpl.
    intros v H.
    inversion H. subst. clear H.
    simp. repeat (econstructor;eauto).
  - repeat red; simpl.
    intros v H.
    inversion H. subst. clear H.
    simp. repeat (econstructor;eauto).
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 (¬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 ∧ ⊤.
Proof.
  intros f.
  rewrite Et_sym.
  unfold equiv,consequence,est_modele.
  split;intros.
  - apply I_Et with true true.
    + constructor.
    + assumption.
    + reflexivity.
  - inv H.
    inv H2.
    subst;simpl in ×.
    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 f₁ f₂,
                     ((f₁ ∧ F ⊧ ⊥)
                      ∧ (f₂ ∧ F ⊧ ⊥))
                     → (f₁ ∨ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  inversion H0. subst. clear H0. simp.
  apply Bool.orb_true_iff in hb. destruct hb as [hb | hb];subst.
  - apply h. repeat (econstructor;eauto).
  - apply h'. repeat (econstructor;eauto).
Qed.

Lemma tableau_Ou' : ∀ f₁ f₂,
                     (f₁ ⊧ Faux )
                     ∧ (f₂ ⊧ Faux )
                     → (f₁ ∨ f₂ ) ⊧ Faux.
Proof.
  intros f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  inversion H0. subst. clear H0.
  apply Bool.orb_true_iff in H5. destruct H5 as [hb | hb];subst.
  - apply h. assumption.
  - apply h'. assumption.
Qed.

Lemma tableau_nonEt : ∀ F f₁ f₂,
                        (¬f₁ ∧ F ⊧ ⊥) ∧ (¬f₂ ∧ F ⊧ ⊥)
                        → ¬(f₁ ∧ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  simp.
  apply Bool.andb_false_iff in hb. destruct hb as [hb | hb];subst.
  - apply h. repeat (econstructor;eauto).
  - apply h'. repeat (econstructor;eauto).
Qed.

Lemma tableau_nonEt' : ∀ f₁ f₂,
                        (¬f₁ ⊧ ⊥) ∧ (¬f₂ ⊧ ⊥)
                        → ¬(f₁ ∧ f₂ ) ⊧ ⊥.
Proof.
  intros f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  simp.
  apply Bool.andb_false_iff in H2. destruct H2 as [hb | hb];subst.
  - apply h. repeat (econstructor;eauto).
  - apply h'. repeat (econstructor;eauto).
Qed.

Lemma tableau_implique : ∀ F f₁ f₂,
                           (¬f₁ ∧ F ⊧ ⊥) ∧ (f₂ ∧ F ⊧ ⊥)
                           → (f₁ ⇒ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  simp.
  apply Bool.leb_implb in hb.
  destruct b₁0.
  - apply h'. repeat (econstructor;eauto). simp.
  - apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_implique' : ∀ f₁ f₂,
                           (¬f₁ ⊧ ⊥) ∧ (f₂ ⊧ ⊥)
                           → (f₁ ⇒ f₂ ) ⊧ ⊥.
Proof.
  intros f₁ f₂ H.
  destruct H as [h h'].
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  specialize (h' v).
  simp.
  apply Bool.leb_implb in H5.
  destruct b₁.
  - apply h'. repeat (econstructor;eauto). simp.
  - apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_Et : ∀ F f₁ f₂, f₁ ∧ f₂ ∧ F ⊧ ⊥ → (f₁ ∧ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  simp.
  apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_Et' : ∀ f₁ f₂, f₁ ∧ f₂ ⊧ ⊥ → (f₁ ∧ f₂ ) ⊧ ⊥.
Proof.
  intros f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  simp.
  apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_nonimplique : ∀ F f₁ f₂, f₁ ∧ ¬f₂ ∧ F ⊧ ⊥ → ¬(f₁ ⇒ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  simp.
  destruct b₁.
  - apply h. repeat (econstructor;eauto). simp.
  - apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_nonimplique' : ∀ f₁ f₂, f₁ ∧ ¬f₂ ⊧ ⊥ → ¬(f₁ ⇒ f₂ ) ⊧ ⊥.
Proof.
  intros f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  simpl in ×.
  intros v H0.
  specialize (h v).
  simp.
  destruct b₁0.
  - apply h. repeat (econstructor;eauto). simp.
  - apply h. repeat (econstructor;eauto).
Qed.

Lemma tableau_nonOu : ∀ F f₁ f₂, ¬f₁ ∧ ¬f₂ ∧ F ⊧ ⊥ → ¬(f₁ ∨ f₂ ) ∧ F ⊧ ⊥.
Proof.
  intros F f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  simp.
  apply h.
  repeat (econstructor;eauto).
Qed.

Lemma tableau_nonOu' : ∀ f₁ f₂, ¬f₁ ∧ ¬f₂ ⊧ ⊥ → ¬(f₁ ∨ f₂ ) ⊧ ⊥.
Proof.
  intros f₁ f₂ h.
  unfold consequence,est_modele,equiv in ×.
  intros v H0.
  specialize (h v).
  simp.
  apply h.
  repeat (econstructor;eauto).
Qed.

Lemma tableau_ferme_branche : ∀ F f, (F ∧ f ) ∧ ¬f ⊧ ⊥.
Proof.
  unfold consequence,est_modele,equiv in ×.
  intros F f v H.
  simp.
  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 ×.
  simp.
  discriminate.
Qed.

Lemma p_et_p_eq : ∀ a, a ∧a ≡ a.
Proof.
  intros a.
  unfold equiv,consequence,est_modele.
  simpl.
  split;intros;simp.
  repeat (econstructor;eauto).
Qed.

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 φ.
Proof.
intros φ i H.
induction H;try constructor;auto.
Qed.

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.
Proof.
  intros i φ H b v x.
  destruct b.
  - apply subst_fresh_id_true.
    assumption.
  - split;intros h;apply interp_not_true in h.
    + apply interp_not_true.
      intro abs.
      apply <- (subst_fresh_id_true i φ H v x) in abs.
      contradiction.
    + apply interp_not_true.
      intro abs.
      apply (subst_fresh_id_true i φ H v x) in abs.
      contradiction.
Qed.

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 ).
Proof.
  induction l;simpl;intros;split.
  - constructor.
    simpl.
    inv H.
    reflexivity.
  - constructor.
    simpl.
    inv H.
    reflexivity.
  - constructor.
    simpl.
    inv H.
    apply f_equal.
    apply f_equal2.
    + destruct a.
      destruct (beq_nat n0 i);simpl;reflexivity.
    + rewrite map_map.
      apply map_ext.
      intros a0.
      destruct a0.
      destruct (beq_nat n0 i);reflexivity.
  - constructor.
    simpl.
    inv H.
    apply f_equal.
    apply f_equal2.
    + destruct a.
      destruct (beq_nat n0 i);simpl;reflexivity.
    + rewrite map_map.
      apply map_ext.
      intros a0.
      destruct a0.
      destruct (beq_nat n0 i);auto.
Qed.

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 )).
Proof.
  intros i v φ.
  revert i v.
  induction φ;intros;split;intro h; try inversion hfreshv; try inversion hfreshi;subst.
  - inv h. constructor.
  - inv h. constructor.
  - inv h. constructor.
  - inv h. constructor.
  - inv h.
    constructor.
    unfold subst_in_interp.
    simpl.
    reflexivity.
  - inv h.
    constructor.
    reflexivity.
  - inv h.
    econstructor;auto.
    apply IHφ;auto.
  - inv h.
    econstructor;eauto.
    apply IHφ;auto.
  - inv h.
    econstructor;eauto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.
  - inv h.
    econstructor;eauto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.
  - inv h.
    econstructor;eauto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.
  - inv h.
    econstructor;eauto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.
  - inv h.
    econstructor;eauto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.

  - inv h.
    econstructor;auto.
    + apply IHφ1;auto.
    + apply IHφ2;auto.
  - apply subst_substterm_pred.
    assumption.
  - apply subst_substterm_pred.
    assumption.
  - rename H1 into hfreshv'.
    rename H5 into hfreshi'.
    rename H2 into hvn.
    rename H6 into hin.
    simpl in h.
    rewrite (beq_nat_diff _ _ hvn) in h.
    rewrite (beq_nat_diff _ _ hin) in h.
    simpl in h.
    inv h.
    + constructor.
      intro x.
      assert (h':=H2 x).
      apply IHφ in h'.
      × rewrite subst_permut in h';auto.
        unfold subst_in_interp at 3 in h'.
        simpl in h'.
        rewrite (beq_nat_diff _ _ hvn) in h'.
        assumption.
      × inversion hfreshv.
        assumption.
      × inversion hfreshi.
        assumption.
    + constructor.
      destruct H2 as [x h'].
      apply IHφ in h'.
      × rewrite subst_permut in h';auto.
        unfold subst_in_interp at 3 in h'.
        simpl in h'.
        rewrite (beq_nat_diff _ _ hvn) in h'.
        ∃ x.
        assumption.
      × inversion hfreshv.
        assumption.
      × inversion hfreshi.
        assumption.
  - rename H1 into hfreshv'.
    rename H5 into hfreshi'.
    rename H2 into hvn.
    rename H6 into hin.
    simpl.
    rewrite (beq_nat_diff _ _ hvn).
    rewrite (beq_nat_diff _ _ hin).
    simpl.
    inv h.
    + constructor.
      intro x.
      assert (h':=H2 x).
      rewrite subst_permut in h';auto.

      inversion hfreshv.
      inversion hfreshi.
      specialize (IHφ i (subst_in_interp v n x) var true H1 H6).
      unfold subst_in_interp at 4 in IHφ.
      simpl in IHφ.
      rewrite (beq_nat_diff var n H3) in IHφ.
      apply IHφ.
      assumption.
    + constructor.
      destruct H2 as [x h'].
      rewrite subst_permut in h';auto.

      inversion hfreshv.
      inversion hfreshi.
      specialize (IHφ i (subst_in_interp v n x) var false H1 H5).
      unfold subst_in_interp at 4 in IHφ.
      simpl in IHφ.
      rewrite (beq_nat_diff var n H2) in IHφ.
      ∃ x.
      apply IHφ.
      assumption.

  - rename H1 into hfreshv'.
    rename H5 into hfreshi'.
    rename H2 into hvn.
    rename H6 into hin.
    simpl in h.
    rewrite (beq_nat_diff _ _ hvn) in h.
    rewrite (beq_nat_diff _ _ hin) in h.
    simpl in h.
    inv h.
    + constructor.
      destruct H2 as [x h'].
      apply IHφ in h'.
      × rewrite subst_permut in h';auto.
        unfold subst_in_interp at 3 in h'.
        simpl in h'.
        rewrite (beq_nat_diff _ _ hvn) in h'.
        ∃ x.
        assumption.
      × inversion hfreshv.
        assumption.
      × inversion hfreshi.
        assumption.
    + constructor.
      intros x.
      assert (h':=H2 x).
      apply IHφ in h'.
      × rewrite subst_permut in h';auto.
        unfold subst_in_interp at 3 in h'.
        simpl in h'.
        rewrite (beq_nat_diff _ _ hvn) in h'.
        assumption.
      × inversion hfreshv.
        assumption.
      × inversion hfreshi.
        assumption.
  - rename H1 into hfreshv'.
    rename H5 into hfreshi'.
    rename H2 into hvn.
    rename H6 into hin.
    simpl.
    rewrite (beq_nat_diff _ _ hvn).
    rewrite (beq_nat_diff _ _ hin).
    simpl.
    inv h.
    + constructor.
      destruct H2 as [x h'].
      rewrite subst_permut in h';auto.

      inversion hfreshv.
      inversion hfreshi.
      specialize (IHφ i (subst_in_interp v n x) var true H1 H5).
      unfold subst_in_interp at 4 in IHφ.
      simpl in IHφ.
      rewrite (beq_nat_diff var n H2) in IHφ.
      ∃ x.
      apply IHφ.
      assumption.
    + constructor.
      intro x.
      assert (h':=H2 x).
      rewrite subst_permut in h';auto.

      inversion hfreshv.
      inversion hfreshi.
      specialize (IHφ i (subst_in_interp v n x) var false H1 H6).
      unfold subst_in_interp at 4 in IHφ.
      simpl in IHφ.
      rewrite (beq_nat_diff var n H3) in IHφ.
      apply IHφ.
      assumption.
Qed.

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 ⊧ ⊥.
Proof.
  intros F f₁ i var hfreshv hfreshi hv.
  intros v hforall.
  unfold consequence,est_modele,equiv in ×.
  simp.
  - apply hv with (v:=v).
    apply I_Et with true true;try reflexivity.
    + apply substinterp_substvar_eq.
      × assumption.
      × assumption.
      × apply H5.
    + apply I_Et with true true;try reflexivity.
      × apply I_Forall. intros x. apply H5.
      × assumption.
  - discriminate.
Qed.

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 ⊧ ⊥.
Proof.
  intros F f₁ i j jfreshinf₁ ifreshinf₁ jfreshinF h.
  unfold consequence,est_modele,equiv in ×.
  intros v H0.

  inv H0.
  inversion_bool.
  subst.
  inv H2.
  destruct H0.
  exfalso.
  apply (interp_true_false ⊥ (subst_in_interp v j x)).
  + constructor.
  + apply h.
    apply I_Et with true true.
    × apply substinterp_substvar_eq.
      { apply fresh_is_not_bound;assumption. }
      { assumption. }
      unfold subst_in_interp at 3.
      simpl.
      rewrite <- (beq_nat_refl).
      { destruct (eq_nat_dec i j).
        - subst.
          assert (Interp_eq (subst_in_interp (subst_in_interp v j x) j x) (subst_in_interp v j x)).
          { unfold subst_in_interp;simpl.
            constructor;simpl;auto.
            - reflexivity.
            - intro t.
              destruct t.
              destruct (beq_nat n j);auto.
            - reflexivity.
          }
          rewrite H0.
          assumption.
        - rewrite (subst_permut v i j).
          + apply subst_fresh_id;auto.
          + assumption. }
    × apply subst_fresh_id;auto.
    × reflexivity.
Qed.

Lemma tableau_exist':
  ∀ f₁ i j,
    is_fresh j f₁
    → is_not_bound i f₁
    → substtermvar i j f₁ ⊧ ⊥
    → EXIST i f₁ ⊧ ⊥.
Proof.
  intros f₁ i j jfreshinf₁ ifreshinf₁ h.
  unfold consequence,est_modele,equiv in ×.
  intros v H0.

  inv H0.
  destruct H1.
  exfalso.
  apply (interp_true_false ⊥ (subst_in_interp v j x)).
  + constructor.
  + apply h.
    apply substinterp_substvar_eq.
    { apply fresh_is_not_bound;assumption. }
    { assumption. }
    unfold subst_in_interp at 3.
    simpl.
    rewrite <- (beq_nat_refl).
    { destruct (eq_nat_dec i j).
      - subst.
        assert (Interp_eq (subst_in_interp (subst_in_interp v j x) j x) (subst_in_interp v j x)).
        { unfold subst_in_interp;simpl.
          constructor;simpl;auto.
          - reflexivity.
          - intro t.
            destruct t.
            destruct (beq_nat n j);auto.
          - reflexivity. }
        rewrite H0.
        assumption.
      - rewrite (subst_permut v i j).
        + apply subst_fresh_id;auto.
        + assumption. }
Qed.

Ltac do_exist P n :=
  (extrait_ P;
   match goal with
     | |- context [TVar n] ⇒ fail
     | _ ⇒
       (eapply tableau_exist with (j:=n)
        ;[repeat progress constructor;try omega
         |repeat progress constructor;try omega
         |repeat progress constructor;try omega
         |simpl])
   end).

Ltac do_Forall P n :=
  (extrait_ P;
   match goal with
     | |- context [TVar n] ⇒ fail
     | _ ⇒
       (eapply tableau_forall with (var:=n)
        ;[repeat progress constructor;try omega
         |repeat progress constructor;try omega
         |simpl])
   end).

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