(* ========================================================================= *)
(*                                                                           *)
(* * Logica del primo ordine                                                 *)
(*                                                                           *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Notazioni:                                                                *)
(*                                                                           *)
(*   X : Set               X e' un insieme                                   *)
(*   P : X -> Prop         P e' un predicato su X                            *)
(*   P : X -> Y -> Prop    P e' una relazione binaria su X e Y               *)
(*   P x                   x verifica il predicato P                         *)
(*                                                                           *)
(*   forall x : X, ...     comunque preso x in X ...                         *)
(*   exists x : X, ...     esiste x in X tale che ...                        *)
(* ------------------------------------------------------------------------- *)

Lemma fol1 : forall (X : Set) (P Q : X -> Prop),
  (forall x : X, P x -> Q x) ->
  (exists x : X, P x) ->
  (exists x : X, Q x).
intros.
destruct H0.     (* Distrugge l'ipotesi "exists x : X, P X"                  *)
exists x.
apply H.
apply H0.
Qed.

Lemma fol2 : forall (X : Set) (P : X -> Prop),
  (forall x, ~ P x) -> (~ exists x, P x).
(* Tauto non e' capace di dimostrare enunciati del primo ordine.             *)
(* tauto.                                                                    *)
(*   ==> User error: Tauto failed                                            *)
intros.
unfold not.
intros.
destruct H0.     (* Distrugge l'ipotesi "exists x : X, P X"                  *)
unfold not in H.
Check (H x).     (* H x : P x -> False                                       *)
apply (H x).     (* Utilizza H applicato a x                                 *)
apply H0.
Qed.

Lemma fol3 : forall (X : Set) (P : X -> Prop),
  (exists x, ~ P x) -> (~ forall x, P x).
intros.
unfold not.
intros.
destruct H.      (* Distrugge l'ipotesi "exists".                            *)
unfold not in H.
apply H.
apply H0.
Qed.

(* Esercizio *)
Lemma fol4 : forall (X : Set) (P : X -> Prop),
  (~ exists x, P x) -> (forall x, ~ P x).

Qed.


(* ------------------------------------------------------------------------- *)
(* ** Relazioni binarie                                                      *)
(* ------------------------------------------------------------------------- *)

Lemma fol5 : forall (X Y : Set) (P : X -> Y -> Prop),
  (exists y, forall x, P x y) ->
  (forall x, exists y, P x y).
intros.
destruct H.
exists x0.
apply H.
Qed.

(* Esercizio* *)
Lemma fol6 : forall (X Y : Set) (P : X -> Y -> Prop),
  (exists y, exists x, P x y) ->
  (exists x, exists y, P x y).

Qed.