Travaux dirigés du 15 février 2011 (TD3)

Petits énoncés logiques

Prouver les formules logiques suivantes :

• forall A B, A -> B -> A.

• forall (P Q : nat -> Prop), (forall x, P x) \/ (forall x, Q x) -> forall x, P x \/ Q x.

• forall (A B C : Prop), A /\ B -> C -> A /\ C.

• forall (A B C D : Prop), A \/ B -> (A -> C) -> (B -> D) -> C \/ D.

• forall (P Q : nat -> Prop), (exists x, P x /\ Q x) -> (exists x, P x) /\ (exists x, Q x).

• forall A m n, ((S n = m) -> A) -> ((1 + n = m) -> A).

• forall (A : Prop), A -> ~ ~ A.

• Question bonus, à ne traiter que si vous avez tout fini :

  forall (A : Prop), ~ ~ (A \/ ~ A).

Preuves de programmes

• Imprimer les valeurs de negb et xorb
• Prouver

  forall x, negb (negb x) = x
  

• Prouver

  forall x y, xorb x y = xorb y x
  

• Prouver

  forall x y, xorb (negb x) y = negb (xorb y x)
  

• En utilisant la définition suivante

  Fixpoint ff (n:nat) :=
    match n with
      0 => true
    | S p => negb (ff p)
    end.
  

  Prouver

  forall x y, ff (x + y) = negb (xorb (ff x) (ff y))