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

   Compilare i seguenti campi:

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

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

   Prima di abbandonare la postazione:

   * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella)
     /public/ con nome logica_Account1.ma, ad esempio Mario Rossi, il cui
     account è mrossi, deve salvare il file in /public/logica_mrossi.ma.
     ATTENZIONE: non salvare nella directory Public contenuta nella home.

   * mandatevi via email o stampate il file. Per stampare potete usare
     usare l'editor gedit che offre la funzionalità di stampa
     
   * per l'esercitazione svolta a casa, inviatemi il file per posta
     (tranquil@cs.unibo.it) con oggetto `[Logica] esercitazione 3`.
*)



(* ATTENZIONE
   ==========
   
   
   Non modificare quanto segue 
*)
include "nat/minus.ma".
definition if_then_else ≝ λT:Type.λe,t,F.match e return λ_.T with [ true ⇒ t | false ⇒ F].
notation > "'if' term 19 e 'then' term 19 t 'else' term 90 F" non associative with precedence 19 for @{ 'if_then_else $e $t $F }.
notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 F \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $F }.
interpretation "Formula if_then_else" 'if_then_else e t F = (if_then_else ? e t F).
definition max ≝ λn,m. if leb n m then m else n. 
definition min ≝ λn,m. if leb n m then n else m. 

(* Ripasso 1
   =========
   
   Il linguaggio delle formule, dove gli atomi sono
   rapperesentati da un numero naturale
*)
inductive Formula : Type ≝
| FBot: Formula
| FTop: Formula
| FAtom: nat → Formula
| FAnd: Formula → Formula → Formula
| FOr: Formula → Formula → Formula
| FImpl: Formula → Formula → Formula
| FNot: Formula → Formula
.

(* Ripasso 2
   =========
   
*) 
let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
 match F with
  [ FBot ⇒ 0
  | FTop ⇒ 1
  | FAtom n ⇒ min (v n) 1
  | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  | FNot F1 ⇒ 1 - (sem v F1)
  ]
.

(* ATTENZIONE
   ==========
   
   Non modificare quanto segue.
*)
notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
notation > "[[ term 19 a ]]_  term 90 v" non associative with precedence 90 for @{ sem $v $a }.
interpretation "Semantic of Formula" 'semantics v a = (sem v a).




(* ATTENZIONE
   ==========
   
   Non modificare quanto segue.
*)
lemma sem_bool : ∀F,v. [[ F ]]_ v = 0 ∨ [[ F ]]_ v = 1.  intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ].  |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed.
lemma min_Sn_Sm : ∀n,m. min (1 + n) (1 + m) = 1 + min n m.  intros; whd in match (min ??) in ⊢ (???%);  whd in match (min ??); whd in match (leb ??); elim (leb n m); reflexivity. qed.
lemma min_n_O : ∀n. min n 0 = 0.  intros; cases n; reflexivity. qed.
lemma min_max : ∀F,G,v.  min (1 - [[F]]_ v) (1 - [[G]]_ v) = 1 - max [[F]]_ v [[G]]_ v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
lemma max_min : ∀F,G,v.  max (1 - [[F]]_ v) (1 - [[G]]_ v) = 1 - min [[F]]_ v [[G]]_ v.  intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed.
lemma sem_1_1 : ∀F,v.1 - (1 - [[ F ]]_ v) = [[ F ]]_ v. intros; cases (sem_bool F v); rewrite > H; reflexivity. qed.


(* Esercizio 1
   ===========
   
   Definire per ricorsione strutturale la funzione `negate_atoms`
   che presa una formula `F` ne nega gli atomi.
   
   Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare
   `¬A ∨ (⊤ → ¬B)`.

   Sintassi: [ caso1 sottormule_caso1 ⇒ trasformazione1
             | caso2 sottormule_caso2 ⇒ trasformazione2
             ].
*)
let rec negate_atoms (F: Formula) on F : Formula ≝
 match F with
  [ …
  ].

(* Test 1
   ======
  
   Testare la funzione `negate_atoms`. Il risultato atteso è:
   
       FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
       
   Se la dimostrazione non funziona vuol dire che la definizione è sbagliata. 
*)

lemma test1 : negate_atoms (FOr (FAtom 0) (FImpl FTop (FAtom 1))) = FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))).
normalize.
done.
qed.

(* ATTENZIONE
   ==========
   
   Non modificare quanto segue
*)
definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_ v = [[ F2 ]]_ v.
notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
notation > "a ≡ b" non associative with precedence 50 for @{ 'equivF $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F2 ≡ F3 → F1 ≡ F3. intros; intro; autobatch. qed.
lemma equiv_sym : ∀F1,F2. F1 ≡ F2 → F2 ≡ F1. intros; intro; autobatch. qed.
definition equivv ≝ λv1,v2 : ℕ → ℕ. ∀n : ℕ.min (v1 n) 1 = min (v2 n) 1.
notation "hvbox(a \nbsp break mstyle color #0000ff (≃) \nbsp b)"  non associative with precedence 45 for @{ 'equivW $a $b }.
notation > "a ≃ b" non associative with precedence 50 for @{ 'equivW $a $b }.
interpretation "equivalence for worlds" 'equivW a b = (equivv a b).
lemma sem_invariance : ∀F,v1,v2. v1 ≃ v2 → [[ F ]]_ v1 = [[ F ]]_ v2. intros; elim F; [1,2: done; | change with (min (v1 n) 1 = min (v2 n) 1). apply H. |4,5,6,7: normalize; rewrite > H1; [4: done.] rewrite > H2; done.] qed.


(* Esercizio 2
   ===========
   
   Definire per ricorsione strutturale la funzione di
   dualizzazione di una formula `F`. Tale funzione:
   
   * Scambia FTop con FBot e viceversa
   
   * Scambia il connettivo FAnd con FOr e viceversa
   
   * Sostituisce il connettivo FImpl con FAnd e nega la
     prima sottoformula. L'idea è che `FImpl A B`
     è semanticamente equivalente a `FOr (FNot A) B` il
     cui duale è `FAnd (FNot A) B`.
   
   Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in
   `¬A ∧ (B ∨ ⊤)`. 
*)  
let rec dualize (F : Formula) on F : Formula ≝
  match F with
  [ …
  ].

(* Test 2
   ======
   
   Testare la funzione `dualize`. Il risultato atteso è:
   
       FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) 
       
   Se la dimostrazione non funziona vuol dire che la definizione è sbagliata. 
*)

lemma test2 : dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot)) = FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop).
normalize.
done.
qed.

(* Spiegazione
   ===========
   
   La funzione `invert` permette di invertire un mondo `v`.
   Ovvero, per ogni indice di atomo `i`, se `v i` restituisce
   `1` o più allora `(invert v) i` restituisce `0`, e se `v i`
   restituisce `0` allora restituisce `1`. Una notazione che si
   può usare è `v^-1` per `invert v`. È fornito un lemma
   che mostra che `invert (invert v) ≃ v` per ogni `v`.
   
*)
definition invert ≝
 λv:ℕ → ℕ. λx. if eqb (v x) 0 then 1 else 0.
 
interpretation "Inversione del mondo" 'invert v = (invert v).
lemma invert_invert : ∀v : ℕ → ℕ.v^-1^-1 ≃ v. repeat intro; normalize; cases (v n); normalize; [reflexivity] cases n1; normalize; reflexivity. qed.

(* Esercizio 3
   ===========
   
   Dimostrare il lemma `negate_invert` che asserisce che
   la semantica in un mondo `v` associato alla formula
   con atomi negati di `F` e uguale alla semantica associata
   a `F` in un mondo invertito.
*) 

lemma negate_invert:
  ∀F:Formula.∀v:ℕ→ℕ.[[ negate_atoms F ]]_ v=[[ F ]]_ (invert v).
assume F:Formula.
assume v:(ℕ→ℕ).
we proceed by induction on F to prove ([[ negate_atoms F ]]_ v=[[ F ]]_ (invert v)).
  case FBot.
    …
  case FTop.
    …
  case FAtom.
    assume n : ℕ.
    the thesis becomes ([[ negate_atoms (FAtom n) ]]_ v=[[ FAtom n ]]_ (invert v)).
    the thesis becomes (1 - (min (v n) 1)= min (invert v n) 1).
    the thesis becomes (1 - (min (v n) 1)= min (if eqb (v n) 0 then 1 else 0) 1).
    (* dovrete procedere per casi su `v n` (o è 0 o è il successore di un
       numero). Nei due casi `eqb` si espande direttamente in `true` o `false`.
       Userete min_Sn_Sm e min_n_O per procedere *)
    …
  case FAnd.
    assume F1 : Formula.
    by induction hypothesis we know
      ([[ negate_atoms F1 ]]_ v=[[ F1 ]]_ (invert v)) (H).
    assume F2 : Formula.
    by induction hypothesis we know
     ([[ negate_atoms F2 ]]_ v=[[ F2 ]]_ (invert v)) (H1).
    the thesis becomes
     ([[ negate_atoms (FAnd F1 F2) ]]_ v=[[ FAnd F1 F2 ]]_ (invert v)).
    …
  case FOr.
    …
  done.
  case FImpl.
    …
  done.
  case FNot.
    …
  done.  
qed.

(* Esercizio 4
   ===========
   
   Dimostrare che la funzione negate_atoms rispetta l'equivalenza.
   Cioé se la F è equivalente a G allora 
   negate_atoms F è equivalente a negate_atoms G.

   Nota bene: dovrete utilizzare il lemma appena dimostrato.
   NON procedere per induzione.

*)
lemma negate_fun:
 ∀F:Formula.∀G:Formula.F ≡ G → negate_atoms F ≡ negate_atoms G.
 …
qed.


(* Esercizio 5
   ===========
   Ora dimostriamo la relazione tra dualize e invert. Dovrete usare i lemmi
   `max_min` e `min_max`.
   
*)
lemma dualize_invert_to_not :
  ∀F:Formula.∀v : ℕ → ℕ.[[ dualize F ]]_ (invert v) = [[ FNot F ]]_ v.
 assume F:Formula.
 assume v:(ℕ→ℕ).
 we proceed by induction on F to prove ([[dualize F]]_ (invert v)=[[FNot F]]_ v).
 case FBot.
   …
 case FTop.
   …
 case FAtom.
   …
 case FAnd.
   …
 case FOr.
   …
 case FImpl.
   …
 case FNot.
   …
qed.

(* Esercizio 6
   ===========
   
   Combinare brevemente i due risultati precedenti per ottenere il seguente
   risultato.
*)
theorem negate_dualize : ∀F : Formula.FNot F ≡ negate_atoms (dualize F).
assume F : Formula.
the thesis becomes (∀v : ℕ → ℕ.[[ FNot F ]]_ v = [[ negate_atoms (dualize F) ]]_ v).
assume v : (ℕ → ℕ).
conclude ([[ FNot F ]]_ v)
  …
done.
qed. 

(* Esercizio 7
   ===========
   
   Dimostrare che la negazione della dualizzazione equivale a negare gli atomi.
   Qui utilizzeremo una catena di uguaglianze, e un ingrediente importante sarà
   il fatto che `[[ dualize F ]]_ v = [[ dualize F ]]_ (invert (invert v))`,
   da mettere quindi nel contesto prima di `conclude` con una serie di
   `by ... we proved ... (...)`. Gli altri ingredienti sono il lemma `sem_1_1`
   e gli altri lemmi dimostrati in precedenza.
   NON procedere per induzione.
*)
lemma not_dualize_eq_negate : ∀F : Formula.FNot (dualize F) ≡ negate_atoms F.
assume F : Formula.
the thesis becomes (∀v : ℕ → ℕ.[[ FNot (dualize F) ]]_ v = [[ negate_atoms F ]]_ v).
assume v : (ℕ → ℕ).
the thesis becomes ([[ FNot (dualize F) ]]_ v = [[ negate_atoms F ]]_ v).
…
qed.


(* Esercizio 8
   ===========
   
   Dimostrare che la negazione è iniettiva. Cioé che se FNot F ≡ FNot G allora F≡G.
   NON procedere per induzione, visto che `sem_1_1` basta.

*)
theorem not_inj:
 ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G.
 assume F:Formula.
 assume G:Formula.
 suppose (FNot F ≡ FNot G) (H).
 the thesis becomes (F ≡ G).
 the thesis becomes (∀v:ℕ→ℕ.[[ F ]]_ v=[[ G ]]_ v).
 assume v:(ℕ→ℕ).
 …
qed.



(* Esercizio 9
   ============
   
   Dimostrare il teorema di dualità. La parte importante della dimostrazione
   userà esclusivamente comandi `by ... we proved ... (...)`.
*)
theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
 assume F1:Formula.
 assume F2:Formula.
 suppose (F1 ≡ F2) (H).
 the thesis becomes (dualize F1 ≡ dualize F2).
 …
qed.