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

Dimostreremo un altro risultato importante: negare una formula equivale a negare gli atomi della sua dualizzazione. Ad esempio,

  ¬(A ∨ (B ∧ C)) ≡ ¬A ∧ (¬B ∨ ¬C)

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_1_1 : ∀F.1 - (1 - [[ F ]]_ v) = [[ F ]]_ v
• 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 → F2 ≡ F3 → F1 ≡ F3
• lemma equiv_sym : ∀F1,F2. F1 ≡ F2 → F2 ≡ F1
• lemma min_Sn_Sm : ∀n,m. min (1 + n) (1 + m) = 1 + min n m
• lemma min_n_O : ∀n. min n 0 = 0
• lemma sem_invariance : ∀F,v1,v2. v1 ≃ v2 → [[ F ]]_ v1 = [[ F ]]_ v2

dove la notazione v1 ≃ v2 (ottenibile col comando \simeq) è sinonimo di ∀n.min (v1 n) 1 = min (v2 n).

Avrete anche a disposizione il lemma

• lemma invert_invert : ∀v.invert (invert v) ≃ v

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.

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

2. lemma negate_fun, conseguenza di negate_invert

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

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

   ∀F:Formula.∀v:ℕ→ℕ.[[ dualize F ]]_ (invert v) ≡ [[ FNot F ]]_ v.
   

4. lemma not_dualize_eq_negate, conseguenza dei precedenti e di sem_invariance

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

5. lemma not_inj, conseguenza di sem_1_1

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

Una volta dimostrati tali lemmi, la prova del primo risultato importante, ∀F.FNot F ≡ negate_atoms (dualize F) è immediata. La prova del teorema di dualità procede come di seguito:

1. Assume l'ipotesi

   F1 ≡ F2
   

2. Utilizza negate_fun per ottenere

   negate_atoms F1 ≡ negate_atoms F2
   

3. Utilizzando i lemmi not_dualize_eq_negate, equiv_rewrite e equiv_sym si 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.

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