(**************************************************************************)
(*       ___	                                                            *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU Lesser General Public License Version 2.1         *)
(*                                                                        *)
(**************************************************************************)

(* DEDUZIONE NATURALE: PRIMO ORDINE *)

(* Esercizio 0
   ===========

   Compilare i seguenti campi:

   Nome1: ...
   Cognome1: ...
   Matricola1: ...
   Account1: ...

   Nome2: ...
   Cognome2: ...
   Matricola2: ...
   Account2: ...

*)




include "didactic/support/natural_deduction.ma".

(* Il nostro linguaggio del primo ordine prevede le seguenti 
   - costanti: c
   - funzioni: f, g (unarie), h (binaria)
   - predicati: P, Q (unari), R, S (binari) 
*)
axiom c : sort.
axiom f : sort → sort.
axiom g : sort → sort.
axiom h : sort → sort → sort.
axiom P : sort → CProp.
axiom Q : sort → CProp.
axiom R : sort →sort → CProp.
axiom S : sort →sort → CProp.

(* assumiamo il terzo escluso *)
theorem EM: ∀A:CProp. A ∨ ¬ A.
assume A: CProp.
apply rule (prove (A ∨ ¬A));
apply rule (RAA [H] (⊥)).
apply rule (¬#e (¬¬A) (¬A));
        [ apply rule (¬#i [K] (⊥)).
          apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
              [ apply rule (discharge [H]).
              | apply rule (∨#i_r (¬A)).
                apply rule (discharge [K])
              ]
        | apply rule (¬#i [K] (⊥)).
          apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
              [ apply rule (discharge [H]).
              | apply rule (∨#i_l (A)).
                apply rule (discharge [K]).
              ]
        ]
qed.

(* intuizionista *)
lemma ex1: ∀P : sort → CProp.¬(∃x.P x) ⇒ ∀x.¬ P x.
assume P : (sort → CProp).
apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
…
qed.

(* classico *)
lemma ex2: ∀P: sort → CProp. ¬(∀x.P x) ⇒ ∃x.¬ P x.
assume P : (sort → CProp).
apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
…
qed.

(* intuizionista *)
lemma ex3: ∀P,Q.((∃x.P x) ⇒ Q) ⇒ ∀x.P x ⇒ Q.
assume P : (sort → CProp).
assume Q : CProp.
apply rule (prove (((∃x.P x) ⇒ Q) ⇒ ∀x.P x ⇒ Q));
…
qed.

(* classico *)
lemma ex4: ∀P,Q.((∀x.P x) ⇒ Q) ⇒ ∃x.P x ⇒ Q.
assume P : (sort → CProp).
assume Q : CProp.
apply rule (prove (((∀x.P x) ⇒ Q) ⇒ ∃x.P x ⇒ Q));
…
qed.

(* classico *)
(* il paradosso del bevitore: in un bar esiste sempre qualcuno tale che se lui
   beve, allora bevono tutti *)
(* suggerimento : guardate sopra... *)
lemma ex5 : ∃x.P x ⇒ ∀y.P y.
apply rule (prove (∃x.P x ⇒ ∀y.P y));
…
qed.