Il teorema di dualità

Il teorema di dualizzazione dice che date due formule F1 ed F2, se le due formule sono equivalenti (F1 ≡ F2) allora anche le loro dualizzate lo sono (dualize F1 ≡ dualize F2).

L'ingrediente principale è la funzione di dualizzazione di una formula F:

• 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.

  Ad esempio la formula A → (B ∧ ⊥) viene dualizzata in ¬A ∧ (B ∨ ⊤).

Per dimostrare il teorema di dualizzazione in modo agevole è necessario definire altre nozioni:

• La funzione negate che presa una formula F ne nega gli atomi. Ad esempio la formula (A ∨ (⊤ → B)) deve diventare ¬A ∨ (⊤ → ¬B).

• La funzione invert permette di invertire un mondo v. Ovvero, per ogni indice di atomo i, se v i restituisce 1 allora (invert v) i restituisce 0 e viceversa.

La libreria di Matita

Gli strumenti per la dimostrazione assistita sono corredati da librerie di teoremi già dimostrati. Per portare a termine l'esercitazione sono necessari i seguenti lemmi:

• lemma sem_le_1 : ∀F,v. [[ F ]]v ≤ 1
• lemma minus_1_1 : ∀x. x ≤ 1 → 1 - (1 - x) = x
• lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1
• lemma min_max : ∀F,G,v.min (1 - [[F]]v) (1 - [[G]]v) = 1 - max [[F]]v [[G]]v
• lemma max_min : ∀F,G,v.max (1 - [[F]]v) (1 - [[G]]v) = 1 - min [[F]]v [[G]]v
• lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3
• lemma equiv_sym : ∀F1,F2. F1 ≡ F2 → F2 ≡ F1

Il linguaggio di dimostrazione di Matita

Per dimostrare il lemma negate_invert in modo agevole è necessario utilizzare il seguente comando:

• by H1, H2 we proved P (H)

  Il comando by ... we proved visto nelle precedenti esercitazioni permette di utilizzare più ipotesi o lemmi alla volta separandoli con una virgola.

La prova del teorema di dualità

Il teorema di dualità accennato a lezione dice che se due formule F1 ed F2 sono equivalenti, allora anche le formule duali lo sono.

∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2.

Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi

1. lemma negate_invert, dimostrato per induzione su F, utilizzando min_bool

   ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]v=[[ F ]](invert v).
   

2. lemma negate_fun, conseguenza di negate_invert

   ∀F,G:Formula. F ≡ G → negate F ≡ negate G.
   

3. lemma not_dualize_eq_negate, dimostrato per induzione su F, utilizzando max_min e min_max

   ∀F:Formula. negate F ≡ FNot (dualize F)
   

4. lemma not_inj, conseguenza di sem_bool

   ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G
   

Una volta dimostrati tali lemmi la prova del teorema di dualità procede come di seguito:

1. Assume l'ipotesi

   F1 ≡ F2
   

2. Utilizza negate_fun per ottenere

   negate F1 ≡ negate F2
   

3. Utilizzando due volte il lemma not_dualize_eq_negate e il lemma equiv_rewrite ottiene

   FNot (dualize F1) ≡ FNot (dualize F2)
   

4. Conclude utilizzando il lemma not_inj per ottenere la tesi

   dualize F1 ≡ dualize F2
   

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.

• 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.

• 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.