(**************************************************************************)
(*       ?__                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)



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


(* Esercizio risolto di esempio *)

theorem ex0 : (B ⇒ ¬A) ⇒ (A ⇒ ¬B).
(* Questo comando disegna l'ultima riga dell'albero *)
apply rule (prove ((B ⇒ ¬A) ⇒ (A ⇒ ¬B)));
(* Applico una regola di introduzione dell'implica*)
apply rule (⇒#i [h3] (A ⇒ ¬B));
(* Applico una regola di introduzione dell'implica*)
apply rule (⇒#i [h2] (¬ B));
(* Applico una regola di introduzione del not*)
apply rule (¬#i [h1] (⊥));
(* Applico una regola di eliminazione del not*)
apply rule (¬#e (A) (¬A));
	[(*Applico una regola di eliminazione dell'implica*)
	  apply rule (⇒#e (B ⇒ ¬A) (B));
	  [ apply rule (discharge [h3]); (*Scarico B ⇒ ¬A con l'ipotesi h3*)
	  | apply rule (discharge [h1]); (*Scarico B con l'ipotesi h1*)
	  ]
	| apply rule (discharge [h2]); (*Scarico A con l'ipotesi h2*)
	]
qed.


theorem ex1 : (A ⇒ (B ⇒ C)) ⇒ (A ∧ B) ⇒ C.

apply rule (prove ((A ⇒ (B ⇒ C)) ⇒ (A ∧ B) ⇒ C));
…
qed.

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

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

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


theorem ex5 :  (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E .
apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
…
qed. 

theorem ex6 :  (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
…
qed. 

(*Attenzione la regola di eliminazione dell'and è binaria! *)
theorem ex7 :  ¬(A ∧ ( (¬A ∨ B ∨ C) ∧  ( (¬B ∨ D) ∧   (¬C ∧ ¬D) ))).
apply rule (prove (¬(A ∧ ( (¬A ∨ B ∨ C) ∧  ( (¬B ∨ D) ∧   (¬C ∧ ¬D) )))));
…
qed.