(**************************************************************************)
(*       ___	                                                          *)
(*      ||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         *)
(*                                                                        *)
(**************************************************************************)

(* ESERCITAZIONE 5 *)

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

   Compilare i seguenti campi:

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

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

*)


(* ATTENZIONE
   ==========
   
   Non modificare quanto segue 
*)

include "didactic/support/natural_deduction.ma".

definition And_elim: ∀A,B,C: CProp. A ∧ B → (A → B → C) → C.
 intros; cases H; apply H1; assumption.
qed.

notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp abc \emsp) c (mstyle color #ff0000 (∧\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
for @{ 'And_elim_ko_1 $ab $c (λ${ident Ha}:$ta.λ${ident Hb}:$tb.$abc) }.
interpretation "And_elim_ko_1" 'And_elim_ko_1 ab c \eta.\eta.abc =
  (show c (cast ? ? (And_elim ? ? ? (cast ? ? ab) (cast ? ? abc)))).

notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp abc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∧\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
for @{ 'And_elim_ko_2 $ab (λ${ident Ha}:$ta.λ${ident Hb}:$tb.$abc) $c }.
interpretation "And_elim_ko_2" 'And_elim_ko_2 ab \eta.\eta.abc c =
  (cast ? ? (show c (cast ? ? (And_elim ? ? ? (cast ? ? ab) (cast ? ? abc))))).

notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp abc \emsp) c (∧\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
for @{ 'And_elim_ok_1 $ab (λ${ident Ha}:$ta.λ${ident Hb}:$tb.$abc) $c }.
interpretation "And_elim_ok_1" 'And_elim_ok_1 ab \eta.\eta.abc c =
  (show c (And_elim ? ? ? ab abc)).

notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp abc \emsp) mstyle color #ff0000 (c) (∧\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
for @{ 'And_elim_ok_2 $ab (λ${ident Ha}:$ta.λ${ident Hb}:$tb.$abc) $c }.
interpretation "And_elim_ok_2" 'And_elim_ok_2 ab \eta.\eta.abc c =
  (cast ? ? (show c (And_elim ? ? ? ab abc))).

notation > "∧#'e' term 90 ab [ident Ha] [ident Hb] term 90 c" with precedence 19
for @{ 'And_elim (show $ab ?) (λ${ident Ha}.λ${ident Hb}.show $c ?) }.
interpretation "And_elim KO" 'And_elim ab abc =
  (cast ? ? (And_elim ? ? ?
    (cast (And unit unit) ? ab)
    (cast (unit_to (unit_to unit)) (unit_to ?) abc))).
interpretation "And_elim OK" 'And_elim ab abc = (And_elim ? ? ? ab abc).

(*
TEMPLATE PER L'ELIMINAZIONE DI ∧ (non presente nel menù)

apply rule (∧#e (…) […] […] (…));
	[ 
	| 
	]

*)

theorem EM: ∀A:CProp. A ∨ ¬ A.
(* Il comando assume è necessario perchè dimostriamo A∨¬A
   per una A generica. *)
assume A: CProp.
(* Questo comando inizia a disegnare l'albero *)
apply rule (prove (A ∨ ¬A));
(* qui inizia l'albero, eseguite passo passo osservando come
   si modifica l'albero. *)
apply rule (RAA [H] (⊥)).
apply rule (¬#e (…) (…));
 [ …
 | …
]
qed.

theorem ex2 : (A ⇒ B) ∨ (B ⇒ A).
apply rule (prove (A ⇒ B)∨(B ⇒ A));
…
qed.

theorem ex3: (¬A ∨ ¬B) ⇒ ¬(A ∧ B).
apply rule (prove ((¬A ∨ ¬B) ⇒ ¬(A ∧ B)));
…
qed.

(* Per dimostrare questo teorema torna comodo il lemma EM
   dimostrato in precedenza. *)
theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
…
qed.

theorem ex5: ((A ⇒ B) ⇒ A) ⇒ A.
apply rule (prove (((A ⇒ B) ⇒ A) ⇒ A));
…
qed.

theorem ex6 : (D ⇒ A) ⇒ (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ D ⇒ C.
apply rule (prove ((D ⇒ A) ⇒ (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ D ⇒ C));
…
qed.