La libreria di Matita

Per portare a termine l'esercitazione sono necessari i seguenti lemmi:

• lemma decidable_eq_nat : ∀x,y.x = y ∨ x ≠ y
• lemma sem_bool : ∀F,v. [[ F ]]_ v = 0 ∨ [[ F ]]_ v = 1
• lemma not_eq_to_eqb_false : ∀x,y.x ≠ y → eqb x y = false
• lemma eq_to_eqb_true : ∀x,y.x = y → eqb x y = true
• lemma min_1_sem : ∀F,v.min 1 [[ F ]]_ v = [[ F ]]_ v
• lemma max_0_sem : ∀F,v.max [[ F ]]_ v 0 = [[ F ]]_ v

oltre al lemma trovato all'esercitazione precedente

• lemma sem_sostituzione : ∀F,G,x,v. [[ F[G/x] ]]_ v = [[F]]_ (v[ x ↦ [[G]]_ v])

I lemmi si usano esattamente come se facessero parte del contesto.

Nota su x = y e eqb x y

Se vi siete mai chiesti la differenza tra x = y ed eqb x y quanto segue prova a chiarirla.

Presi due numeri x e y in ℕ, dire che x = y significa i due numeri sono lo stesso numero, ovvero che se x è il numero 3, anche y è il numero 3.

eqb è una funzione, un programma, che confronta due numeri naturali e restituisce true se sono uguali, false se sono diversi. L'utilizzo di tale programma è necessario per usare il costrutto (che è a sua volta un programma) if E then A else B, che lancia il programma E, e se il suo risultato è true si comporta come A altrimenti come B. Come ben sapete i programmi possono contenere errori. In particolare anche eqb potrebbe essere sbagliato, e per esempio restituire sempre true. I teoremi eq_to_eqb_true e not_eq_to_eqb_false sono la dimostrazione che il programma eqb è corretto, ovvero che che se x = y allora eqb x y restituisce true, se x ≠ y allora eqb x y restituisce false.

Il teorema di espansione di Shannon

Si definisce un connettivo logico IFTE A B C come

    FOr (FAnd A B) (FAnd (FNot A) C)

Il teorema dice che data una formula F, e preso un atomo x, la seguente formula è equivalente a F:

    IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])

Ovvero, fissato un mondo v, sostituisco l'atomo x con FBot se tale atomo è falso, lo sostituisco con FTop se è vero.

La dimostrazione è composta da due lemmi princiali, shannon_false e shannon_true.

Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo. Il lemma asserisce quanto segue:

    ∀F,x,v. [[ FAtom x ]]_ v = 0 → [[ F[FBot/x] ]]_ v = [[ F ]]_ v

Una volta assunte la formula F, l'atomo x, il mondo v e aver supposto che [[ FAtom x ]]_ v = 0 si procede utilizzando il lemma sem_sostituzione ricavato all'esercitazione scorsa. A questo punto però serve un lemma addizionale, sem_invariance, che permetterà di dimostrare i due lemmi shannon_false e shannon_true con una semplice catena di uguaglianze.

sem_invariance asserisce:

    ∀F,v1,v2. (∀x.min 1 (v1 x) = min 1 (v2 x)) → [[ F ]]_ v1 = [[ F ]]_ v2.

Quindi dimostriamo questo lemma per induzione.

A questo punto nella dimostrazione di shannon_false e shannon_true, per dimostrare l'ipotesi necessaria per sem_invariance, occorre utilizzare il lemma decidable_eq_nat per ottenere l'ipotesi aggiuntiva n = x ∨ n ≠ x (dove x è l'atomo su cui predica il teorema). Si procede per casi sull'ipotesi appena ottenuta. In entrambi i casi, usando i lemmi eq_to_eqb_true oppure not_eq_to_eqb_false si ottengolo le ipotesi aggiuntive (eqb n x = true) oppure (eqb n x = false). Entrambi i casi si concludono con una catena di uguaglianze.

Il teorema principale si dimostra utilizzando il lemma sem_bool per ottenre l'ipotesi [[ FAtom x ]]_ v = 0 ∨ [[ FAtom x ]]_ v = 1 su cui si procede poi per casi. Entrambi i casi si concludono con una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza e i lemmi min_1_sem oppure max_0_sem.

Note generali

Si ricorda che:

1. Ogni volta che nella finestra di destra compare un simbolo ∀ oppure un simbolo → è opportuno usare il comando assume oppure suppose oppure (se si è in un caso di una dimostrazione per induzione) il comando by induction hypothesis we know (che vengono nuovamente spiegati in seguito).

2. Ogni caso (o sotto caso) della dimostrazione:

   1. Inizia con una sequenza di comandi assume o suppose oppure by induction hypothesis we know. Tale sequenza di comandi può anche essere vuota.

   2. Continua poi con almeno un comando the thesis becomes.

   3. Eventualmente seguono vari comandi by ... we proved per utilizzare i teoremi già disponibili per generare nuove ipotesi.

   4. Eventualmente uno o più comandi we proceed by cases on (...) to prove (...).

   5. Se necessario un comando conclude seguito da un numero anche molto lungo di passi = (...) by ... . per rendere la parte sinistra della vostra tesi uguale alla parte destra.

   6. Ogni caso termina con done.

3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot) avrà tante ipotesi induttive quante sono le sue sottoformule e tali ipotesi sono necessarie per portare a termine la dimostrazione.

I comandi da utilizzare

• the thesis becomes (...).

  Afferma quale sia la tesi da dimostrare. Se ripetuto permette di espandere le definizioni.

• we proceed by cases on (...) to prove (...).

  Permette di andare per casi su una ipotesi (quando essa è della forma A ∨ B).

  Esempio: we proceed by cases on H to prove Q.

• we proceed by induction on (...) to prove (...).

  Permette di andare per casi con una dimostrazione per induzione.

  Esempio: we proceed by induction on F to prove Q.

• case ... .

  Nelle dimostrazioni per casi o per induzioni si utulizza tale comando per inizia la sotto prova relativa a un caso. Esempio: case Fbot.

• done.

  Ogni caso di una dimostrazione deve essere terminato con il comando done.

• assume ... : (...) .

  Assume una formula o un numero, ad esempio assume n : (ℕ). assume un numero naturale n.

• we need to prove ... (...) .

  Introduce un nuovo goal da dimostrare per poi poterlo usare nel contesto. Ad esempio we need to prove F ≡ G (H1). apre un goal per dimostrare F ≡ G, dopodiché si ritorna al goal precedente con in più l'ipotesi H1.

• by ..., ..., ..., we proved (...) (...).

  Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi. Ad esempio by H, H1 we prove (F ≡ G) (H2). ottiene una nuova ipotesi H2 che dice che F ≡ G componendo insieme H e H1.

• conclude (...) = (...) by ... .

  Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando con cui si inizia una catena di uguaglianze. La prima formula che si scrive deve essere esattamente uguale alla parte sinistra della conclusione originale. Esempio conclude ([[ FAtom x ]]_ v) = ([[ FAtom n ]]_ v) by H. Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione di una definizione, la parte by ... deve essere omessa.

• = (...) by ... .

  Continua un comando conclude, lavorando sempre sulla parte sinistra della tesi.