Logic

Logique propositionnelle

on suppose quatre propositions logiques pour la suite

Parameters A B C D: Prop.

les différents connecteurs logiques permettent de former de plus grosses propositions

Check A /\ B.
Check A \/ B.
Check A -> B.
Check A <-> B.
Check ~ A.
Check A /\ (B \/ C ).

Notes sur l'implication:

une séquence d'implications A->B->C->D correspond intuitivement à une implication dont la prémisse est une conjonction: (A/\B/\C)->D
pour le parenthésage, A->B->C dénote la proposition A->(B->C), qui est très différente de (A->B)->C

Tactiques de base pour les connecteurs logiques

preuves sur l'implication

Theorem i1: A -> A.
Proof.
  intros H.
  apply H.
Qed.

Theorem i2: (A -> B) -> (B -> C) -> A -> C.
Proof.
  intros H1 H2 H3.
  apply H2.
  apply H1.
  apply H3.
Qed.

Theorem i3: (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
  intros H1 H2 H3.
  apply H1.
  apply H3.
  apply H2.
  apply H3.
Qed.

preuves sur la conjonction

Theorem c1: A -> B -> A /\B.
Proof.
  intros H1 H2.
  split.
  apply H1.
  apply H2.
Qed.

Theorem c2: A /\ B -> A.
Proof.
  intros H.
  destruct H as [H1 H2].
  apply H1.
Qed.

Theorem c3: A /\ B -> B /\ A.
Proof.
  intros H.
  destruct H as [H1 H2].
  split.
  apply H2.
  apply H1.
Qed.

Theorem c4: A /\ (B /\ C ) -> (C /\ A ) /\ B.
Proof.
  intros [a [b c]].
  split. split.
  apply c.
  apply a.
  apply b.
Qed.

preuves sur la disjonction

Theorem d1: A -> A \/ B.
Proof.
  intros Ha.
  left.
  apply Ha.
Qed.

Theorem d2: B -> A \/ B.
Proof.
  intros Hb.
  right.
  apply Hb.
Qed.

Theorem d3: A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
  intros H Ha Hb.
  destruct H as [H1|H2].
  apply Ha. apply H1.
  apply Hb. apply H2.
Qed.

Theorem d4: A \/ (B \/ C ) -> (C \/ B ) \/ A.
Proof.
  intros [a|[b|c]].
   right. apply a.
   left. right. apply b.
   left. left. apply c.
Qed.

Exercices de rabe

Indices:

l'équivalence propositionelle (<->) est juste la conjonction des deux implications
la négation (~A) est en fait une implication du faux: A->False

Theorem r1: A \/B <-> B \/A.
Proof.
  split.
   intros [Ha|Hb].
    right. apply Ha.
    left. apply Hb.
   intros [Hb|Ha].
    right. apply Hb.
    left. apply Ha.
Qed.

Theorem r2: A -> ~~A.
Proof.
  intros a Na. apply Na. apply a.
Qed.

Theorem r3: ~(A /\ ~A ).
Proof.
  intros [H H'].
  apply H'.
  apply H.
Qed.

Theorem r4: ~(A \/ B ) <-> ~A /\ ~B.
Proof.
  split.
   intro H. split.
    intro a. apply H. left. apply a.
    intro b. apply H. right. apply b.
   intros [Na Nb] [a|b].
    apply Na. apply a.
    apply Nb. apply b.
Qed.

Theorem r5: ~~~A -> ~A.
Proof.
  intros NNNa a. apply NNNa. apply r2. apply a.
Qed.

Logique classique

le tiers-exclu est équivalent à la double négation, mais aucun d'entre eux n'est prouvable en logique intuitioniste

Theorem classic: (forall P, ~~P -> P ) <-> (forall P, P \/ ~P ).
Proof.
  split.
   intros NN P. apply NN. intro H. apply H.
   right. intro H'. apply H. left. apply H'.

   intros TE P. intro H. destruct (TE P) as [H'|H'].
    apply H'.
    exfalso. apply H. apply H'.
Qed.

Coq est intuitioniste, mais on peut poser l'un ou l'autre comme axiome

Axiom NN: forall P, ~~P -> P.

cela permet de prouver des théorèmes valides seulement en logique classique

Theorem not_and: ~(A /\ B ) -> ~A \/ ~B.
Proof.
  intro H. apply NN.   intro H'.
  apply H'. left. intro a.
  apply H'. right. intro b.
  apply H. split. apply a. apply b.
Qed.

This page has been generated by coqdoc