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

   Compilare i seguenti campi:

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

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

   Come sempre, salvate il file come `/public/logica_nomeutente.ma` alla fine dell'esercitazione,
   eventualmente sovrascrivendo il vecchio.

*)

(* 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 eqb (n - m) 0 then m else n. 
definition min ≝ λn,m. if eqb (n - m) 0 then n else m. 
definition update ≝ λv:ℕ→ℕ.λx:ℕ.λy:ℕ.λx'.if eqb x' x then y else (v x').

(* 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
   =========
   
   La semantica di una formula `F` in un mondo `v`: `[[ F ]]_ v` 
*)
let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
 match F with
  [ FBot ⇒ 0
  | FTop ⇒ 1
  | FAtom n ⇒ min 1 (v n) (* <--- qui è diverso dall'esercitazione precedente *)
  | 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).
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.


(* Ripasso 3
   =========
   
   L'operazione di sostituzione di una formula `G` al posto dell'atomo
   `x` in una formula `F`: `F[G/x]` 
*)

let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 match F with
  [ FBot ⇒ FBot
  | FTop ⇒ FTop
  | FAtom n ⇒ if eqb n x then G else (FAtom n)
  | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
  | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
  | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
  | FNot F ⇒ FNot (subst x G F)
  ].

(* ATTENZIONE
   ==========
   
   Non modificare quanto segue.
*)  
notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }.
interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
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 @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
lemma min_1_sem: ∀F,v.min 1 ([[ F ]]_ v) = [[ F ]]_ v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
lemma max_0_sem: ∀F,v.max ([[ F ]]_ v) 0 = [[ F ]]_ v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C).
notation > "v [ term 90 x ↦ term 90 y ]" non associative with precedence 90 for @{'update $v $x $y}.
notation < "v [ \nbsp term 19 x ↦ term 19 y \nbsp ]" non associative with precedence 90 for @{'update $v $x $y}.
interpretation "nat function update" 'update v x y = (update v x y).
lemma sem_sostituzione: ∀F,G,x,v. [[ F[G/x] ]]_ v = [[F]]_ (v[ x ↦ [[G]]_ v]). intros. elim F; [1,2: done | change with ([[ if eqb n x then G else (FAtom n) ]]_ v = min 1 (if eqb n x then ([[G]]_ v) else (v n))); elim (eqb n x); done. |*: intros; normalize; rewrite > H; [4:|*: rewrite > H1; ] done. ] qed.



(* Decommentate questo inizio di dimostrazione e provate ad andare avanti *)
(*
lemma shannon_false: 
  ∀F,x,v. [[ FAtom x ]]_ v = 0 → [[ F[FBot/x] ]]_ v = [[ F ]]_ v.
…
conclude
  ([[ F [FBot/x] ]]_ v)
= (…) by sem_sostituzione.
= ([[ F ]]_ v[x ↦ 0]).
*)
(* Qui o si prcode per induzione, o si dimostra qualcosa di più generale da
   usare anche negli altri risultati.
   ATTENZIONE: ora spostate tutto questo inizio di dimostrazione più sotto. *)

(* dimostriamo quindi questo lemma, che ci servirà più tardi *)
(* ricopiando la struttura delle dimostrazioni dell'esercitazione scorsa
   vi risparmiate un po' di testo da battere. *)
lemma sem_invariance : ∀F,v1,v2. (∀x. min 1 (v1 x) = min 1 (v2 x)) → [[ F ]]_ v1 = [[ F ]]_ v2.
…
qed.

  
lemma shannon_false: 
  ∀F,x,v. [[ FAtom x ]]_ v = 0 → [[ F[FBot/x] ]]_ v = [[ F ]]_ v.
…
conclude
  ([[ F [FBot/x] ]]_ v)
= (…) by sem_sostituzione.
= ([[ F ]]_ v[x ↦ 0]).
(* in order to use sem_invariance *)
we need to prove (…) (G).
case proof.
  …
  case eq.
    …
  case neq.
    …
conclude
…
done.
qed.

lemma shannon_true: 
  ∀F,x,v. [[ FAtom x ]]_ v = 1 → [[ F[FTop/x] ]]_ v = [[ F ]]_ v.
…
qed.

theorem shannon : 
  ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F.
…
qed.