helm/software/matita/contribs/didactic/shannon.ma

   1 (* Esercizio -1
   2    ============
   3
   4    1. Leggere ATTENTAMENTE, e magari stampare, la documentazione reperibile
   5       all'URL seguente:
   6
   7         http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html
   8
   9    2. Questa volta si fa sul serio:
  10       l'esercizio proposto è molto difficile, occorre la vostra massima
  11       concentrazione (leggi: niente cut&paste selvaggio, cercate di capire!)
  12
  13 *)
  14
  15
  16 (* Esercizio 0
  17    ===========
  18
  19    Compilare i seguenti campi:
  20
  21    Nome1: ...
  22    Cognome1: ...
  23    Matricola1: ...
  24    Account1: ...
  25
  26    Nome2: ...
  27    Cognome2: ...
  28    Matricola2: ...
  29    Account2: ...
  30
  31 *)
  32
  33 (* ATTENZIONE
  34    ==========
  35
  36    Non modificare quanto segue
  37 *)
  38 include "nat/minus.ma".
  39 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  40 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 }.
  41 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 }.
  42 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
  43 definition max ≝ λn,m. if eqb (n - m) 0 then m else n.
  44 definition min ≝ λn,m. if eqb (n - m) 0 then n else m.
  45
  46 (* Ripasso 1
  47    =========
  48
  49    Il linguaggio delle formule, dove gli atomi sono
  50    rapperesentati da un numero naturale
  51 *)
  52 inductive Formula : Type ≝
  53 | FBot: Formula
  54 | FTop: Formula
  55 | FAtom: nat → Formula
  56 | FAnd: Formula → Formula → Formula
  57 | FOr: Formula → Formula → Formula
  58 | FImpl: Formula → Formula → Formula
  59 | FNot: Formula → Formula
  60 .
  61
  62 (* Ripasso 2
  63    =========
  64
  65    La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v`
  66 *)
  67 let rec sem (v: nat → nat) (F: Formula) on F : nat ≝
  68  match F with
  69   [ FBot ⇒ 0
  70   | FTop ⇒ 1
  71   | FAtom n ⇒ min (v n) 1
  72   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  73   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  74   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  75   | FNot F1 ⇒ 1 - (sem v F1)
  76   ]
  77 .
  78
  79 (* ATTENZIONE
  80    ==========
  81
  82    Non modificare quanto segue.
  83 *)
  84 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  85 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  86 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
  87 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
  88 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.
  89
  90 (* Ripasso 3
  91    =========
  92
  93    L'operazione di sostituzione di una formula `G` al posto dell'atomo
  94    `x` in una formula `F`: `F[G/x]`
  95 *)
  96
  97 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  98  match F with
  99   [ FBot ⇒ FBot
 100   | FTop ⇒ FTop
 101   | FAtom n ⇒ if eqb n x then G else (FAtom n)
 102   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
 103   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
 104   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
 105   | FNot F ⇒ FNot (subst x G F)
 106   ].
 107
 108 (* ATTENZIONE
 109    ==========
 110
 111    Non modificare quanto segue.
 112 *)
 113 notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 114 notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }.
 115 interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
 116 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
 117 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
 118 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 119 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 120 lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
 121 lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
 122 definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C).
 123
 124 (*DOCBEGIN
 125
 126 La libreria di Matita
 127 =====================
 128
 129 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 130
 131 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
 132 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 133 * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true`
 134 * lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v`
 135 * lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v`
 136
 137 Il teorema di espansione di Shannon
 138 ===================================
 139
 140 Si definisce un connettivo logico `IFTE A B C` come `FOr (FAnd A B) (FAnd (FNot A) C)`.
 141
 142 Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente
 143 formula è equivalente a `F`:
 144
 145         IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])
 146
 147 Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso
 148 in un mondo mondo `v`, altrimenti lo sostituisco con `FTop`.
 149
 150 La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`.
 151
 152 Vediamo la dimostrazione del primo, che asserisce
 153
 154         ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v
 155
 156 Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver supposto
 157 che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`.
 158 I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`,
 159 una volta assunte le sottofrmule e le ipotesi induttive, si conclude
 160 con una catena di uguaglianze.
 161
 162 Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo,
 163 occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi
 164 aggiuntiva `n = x ∨ n ≠ x` su cui si procede poi per casi.
 165 In entrambi i casi, usanto i lemmi `eq_to_eqb_true` e `not_eq_to_eqb_false`
 166 si ottengolo le ipotesi aggiuntive `(eqb n x = true)` e `(eqb n x = false)`.
 167 Entrambi i casi si concludono con una catena di uguaglianze.
 168
 169 Il teorema principale si dimostra utilizzando il lemma `sem_bool` per
 170 ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui
 171 si procede poi per casi. Entrambi i casi si cncludono con
 172 una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza
 173 e i lemmi `min_1_sem` e `max_0_sem`.
 174
 175 DOCEND*)
 176
 177 lemma shannon_false:
 178   ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v.
 179 (*BEGIN*)
 180 assume F : Formula.
 181 assume x : ℕ.
 182 assume v : (ℕ → ℕ).
 183 suppose ([[ FAtom x ]]_v = 0) (H).
 184 we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v).
 185 case FBot.
 186   the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v).
 187   the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
 188   done.
 189 case FTop.
 190   the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v).
 191   the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
 192   done.
 193 case FAtom.
 194   assume n : ℕ.
 195   the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v).
 196   the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 197   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
 198   we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 199     case Left.
 200       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
 201       conclude
 202           ([[ if eqb n x then FBot else (FAtom n) ]]_v)
 203         = ([[ if true then FBot else (FAtom n) ]]_v) by H3.
 204         = ([[ FBot ]]_v).
 205         = 0.
 206         = ([[ FAtom x ]]_v) by H.
 207         = ([[ FAtom n ]]_v) by H2.
 208     done.
 209     case Right.
 210       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
 211       conclude
 212           ([[ if eqb n x then FBot else (FAtom n) ]]_v)
 213         = ([[ if false then FBot else (FAtom n) ]]_v) by H3.
 214         = ([[ FAtom n ]]_v).
 215     done.
 216 case FAnd.
 217   assume f1 : Formula.
 218   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 219   assume f2 : Formula.
 220   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 221   the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v).
 222   conclude
 223       ([[ (FAnd f1 f2)[FBot/x] ]]_v)
 224     = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 225     = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v).
 226     = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1.
 227     = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
 228     = ([[ FAnd f1 f2 ]]_v).
 229   done.
 230 case FOr.
 231   assume f1 : Formula.
 232   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 233   assume f2 : Formula.
 234   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 235   the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v).
 236   conclude
 237       ([[ (FOr f1 f2)[FBot/x] ]]_v)
 238     = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 239     = (max [[ f1[FBot/x] ]]_v  [[ f2[FBot/x] ]]_v).
 240     = (max [[ f1 ]]_v  [[ f2[FBot/x] ]]_v) by H1.
 241     = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
 242     = ([[ FOr f1 f2 ]]_v).
 243   done.
 244 case FImpl.
 245   assume f1 : Formula.
 246   by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1).
 247   assume f2 : Formula.
 248   by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2).
 249   the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v).
 250   conclude
 251       ([[ (FImpl f1 f2)[FBot/x] ]]_v)
 252     = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v).
 253     = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v).
 254     = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1.
 255     = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
 256     = ([[ FImpl f1 f2 ]]_v).
 257   done.
 258 case FNot.
 259   assume f : Formula.
 260   by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1).
 261   the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v).
 262   conclude
 263       ([[ (FNot f)[FBot/x] ]]_v)
 264     = ([[ FNot (f[FBot/x]) ]]_v).
 265     = (1 - [[ f[FBot/x] ]]_v).
 266     = (1 - [[ f ]]_v) by H1.
 267     = ([[ FNot f ]]_v).
 268   done.
 269 (*END*)
 270 qed.
 271
 272 lemma shannon_true:
 273   ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v.
 274 (*BEGIN*)
 275 assume F : Formula.
 276 assume x : ℕ.
 277 assume v : (ℕ → ℕ).
 278 suppose ([[ FAtom x ]]_v = 1) (H).
 279 we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v).
 280 case FBot.
 281   the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v).
 282   the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v).
 283   done.
 284 case FTop.
 285   the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v).
 286   the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v).
 287   done.
 288 case FAtom.
 289   assume n : ℕ.
 290   the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v).
 291   the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 292   by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1).
 293   we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v).
 294     case Left.
 295       by H2, eq_to_eqb_true we proved (eqb n x = true) (H3).
 296       conclude
 297           ([[ if eqb n x then FTop else (FAtom n) ]]_v)
 298         = ([[ if true then FTop else (FAtom n) ]]_v) by H3.
 299         = ([[ FTop ]]_v).
 300         = 1.
 301         = ([[ FAtom x ]]_v) by H.
 302         = ([[ FAtom n ]]_v) by H2.
 303     done.
 304     case Right.
 305       by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3).
 306       conclude
 307           ([[ if eqb n x then FTop else (FAtom n) ]]_v)
 308         = ([[ if false then FTop else (FAtom n) ]]_v) by H3.
 309         = ([[ FAtom n ]]_v).
 310     done.
 311 case FAnd.
 312   assume f1 : Formula.
 313   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 314   assume f2 : Formula.
 315   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 316   the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v).
 317   conclude
 318       ([[ (FAnd f1 f2)[FTop/x] ]]_v)
 319     = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 320     = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v).
 321     = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1.
 322     = (min [[ f1 ]]_v [[ f2 ]]_v) by H2.
 323     = ([[ FAnd f1 f2 ]]_v).
 324   done.
 325 case FOr.
 326   assume f1 : Formula.
 327   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 328   assume f2 : Formula.
 329   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 330   the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v).
 331   conclude
 332       ([[ (FOr f1 f2)[FTop/x] ]]_v)
 333     = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 334     = (max [[ f1[FTop/x] ]]_v  [[ f2[FTop/x] ]]_v).
 335     = (max [[ f1 ]]_v  [[ f2[FTop/x] ]]_v) by H1.
 336     = (max [[ f1 ]]_v  [[ f2 ]]_v) by H2.
 337     = ([[ FOr f1 f2 ]]_v).
 338   done.
 339 case FImpl.
 340   assume f1 : Formula.
 341   by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1).
 342   assume f2 : Formula.
 343   by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2).
 344   the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v).
 345   conclude
 346       ([[ (FImpl f1 f2)[FTop/x] ]]_v)
 347     = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v).
 348     = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v).
 349     = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1.
 350     = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2.
 351     = ([[ FImpl f1 f2 ]]_v).
 352   done.
 353 case FNot.
 354   assume f : Formula.
 355   by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1).
 356   the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v).
 357   conclude
 358       ([[ (FNot f)[FTop/x] ]]_v)
 359     = ([[ FNot (f[FTop/x]) ]]_v).
 360     = (1 - [[ f[FTop/x] ]]_v).
 361     = (1 - [[ f ]]_v) by H1.
 362     = ([[ FNot f ]]_v).
 363   done.
 364 (*END*)
 365 qed.
 366
 367 theorem shannon :
 368   ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F.
 369 (*BEGIN*)
 370 assume F : Formula.
 371 assume x : ℕ.
 372 assume v : (ℕ → ℕ).
 373 the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
 374 by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H).
 375 we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v).
 376 case Left.
 377   conclude
 378       ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
 379     = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 380     = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 381     = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
 382     = (max (min  0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H.
 383     = (max 0 (min 1 [[ F[FBot/x] ]]_v)).
 384     = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem.
 385     = ([[ F[FBot/x] ]]_v).
 386     = ([[ F ]]_v) by H1, shannon_false.
 387   done.
 388 case Right.
 389   conclude
 390       ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v)
 391     = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 392     = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
 393     = (max (min  [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
 394     = (max (min  1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H.
 395     = (max (min  1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)).
 396     = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem.
 397     = (max [[ F[FTop/x] ]]_v 0).
 398     = ([[ F[FTop/x] ]]_v) by max_0_sem.
 399     = ([[ F ]]_v) by H1, shannon_true.
 400   done.
 401 (*END*)
 402 qed.
 403
 404 (*DOCBEGIN
 405
 406 Note generali
 407 =============
 408
 409 Si ricorda che:
 410
 411 1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un
 412    simbolo `→` è opportuno usare il comando `assume` oppure `suppose` (che
 413    vengono nuovamente spiegati in seguito).
 414
 415 2. Ogni caso (o sotto caso) della dimostrazione:
 416
 417    1. Inizia con una sequenza di comandi `assume` o `suppose` oppure
 418       `by induction hypothesis we know`. Tale sequenza di comandi può anche
 419       essere vuota.
 420
 421    2. Continua poi con almeno un comando `the thesis becomes`.
 422
 423    3. Eventualmente seguono vari comandi `by ... we proved` per combinare le
 424       ipotesi tra loro o utilizzare i teoremi già disponibili per generare nuove
 425       ipotesi.
 426
 427    4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`.
 428
 429    5. Se necessario un comando `conclude` seguito da un numero anche
 430       molto lungo di passi `= (...) by ... .` per rendere la parte
 431       sinistra della vostra tesi uguale alla parte destra.
 432
 433    6. Ogni caso termina con `done`.
 434
 435 3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot)
 436    avrà tante ipotesi induttive quante sono le sue sottoformule e tali
 437    ipotesi sono necessarie per portare a termine la dimostrazione.
 438
 439 I comandi da utilizzare
 440 =======================
 441
 442 * `the thesis becomes (...).`
 443
 444   Afferma quale sia la tesi da dimostrare. Se ripetuto
 445   permette di espandere le definizioni.
 446
 447 * `we proceed by cases on (...) to prove (...).`
 448
 449   Permette di andare per casi su una ipotesi (quando essa è della forma
 450   `A ∨ B`).
 451
 452   Esempio: `we proceed by cases on H to prove Q.`
 453
 454 * `case ... .`
 455
 456   Nelle dimostrazioni per casi o per induzioni si utulizza tale comando
 457   per inizia la sotto prova relativa a un caso. Esempio: `case Fbot.`
 458
 459 * `done.`
 460
 461   Ogni caso di una dimostrazione deve essere terminato con il comando
 462   `done.`
 463
 464 * `assume ... : (...) .`
 465
 466   Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume
 467   un numero naturale `n`.
 468
 469 * `by ..., ..., ..., we proved (...) (...).`
 470
 471   Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi.
 472   Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi
 473   `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`.
 474
 475 * `conclude (...) = (...) by ... .`
 476
 477   Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
 478   con cui si inizia una catena di uguaglianze. La prima formula che si
 479   scrive deve essere esattamente uguale alla parte sinistra della conclusione
 480   originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
 481   Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
 482   di una definizione, la parte `by ...` deve essere omessa.
 483
 484 * `= (...) by ... .`
 485
 486   Continua un comando `conclude`, lavorando sempre sulla parte sinistra della
 487   tesi.
 488
 489 DOCEND*)