exame_coq

(** 1) [3 pontos] Prove ou refute, pelo método do tableux analíticos da LPC, os seguintes sequentes:**)

(** a) p -> q, q -> r |- p -> r**)

(** b) p, p /\ q -> r |- r **)

Require Import List.
Import ListNotations.
Require Import Arith.

(** 2) [1 ponto] Prove o seguinte teorema sobre rev de listas*)
(** Dica: rev_involutive e f_equal podem ajudar *)
Theorem rev_exercise1 : forall (l l' : list nat),
Admitted.

(** 3) [1 ponto] Prove este exercício do doit3. Os teoremas necessários já estão no espaço de nome.
 Utilize Search para encontra-los. PS: Não utilize o teorema PeanoNat.Nat.add_comm ou outro equivalente
a esta questão. *)
Theorem plus_comm : forall n m : nat, n + m = m + n.
Admitted.

(** 4) [1 ponto] Prove a seguinte implicação *)
Theorem  implication_massacration : forall P Q R T K S : Prop, (P -> Q) -> (Q -> R) -> (R -> S) -> (S -> T) -> (T -> K) -> P -> K.
Admitted.

(** 5) [1 ponto] Prove este exercício do doit12. *)
(** Prove that "[P] holds for all [x]" implies "there is no [x] for
    which [P] does not hold."  (Hint: [destruct H as [x E]] works on
    existential assumptions!)  *)
Theorem dist_not_exists : forall (X:Type) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Admitted.

(** 6) [0.5 ponto] Prove este exercício do doit11. *)
Theorem not_implies_our_not : forall (P:Prop),
  ~ P -> (forall (Q:Prop), P -> Q).
Admitted.

(** 7) [0.5 ponto] Prove este exercício do doit11. *)
Lemma proj1 : forall P Q : Prop,
  P /\ Q -> P.
Admitted.

(** 8) [1 ponto] Prove este existencial *)
Theorem whatM : forall m, (exists x, 2 + m = x) -> (exists x,x = 3 + m).
Admitted.

(** 9) [1 ponto] Prove este exercício do doit11  *)
Lemma mult_eq_0 :
  forall n m, n * m = 0 -> n = 0 \/ m = 0.
Admitted.