Il linguaggio di dimostrazione di Matita

Come abbiamo già visto, Matita utilizzi i simboli →, ∧, ∨, ¬, ∀ per esprimere i connettivi logici del metalinguaggio. Nelle dimostrazioni delle esercitazioni passate, l'implicazione, la disgiunzione e la quantificazione universale sono già state utilizzate ampiamente: oggi ci soffermeremo maggiormente su congiunzione e negazione.

Congiunzione

Dovendo dimostrare P ∧ Q, è necessario prima di tutto dimostrare P e Q separatamente. Se, per esempio, P non comparisse tra le ipotesi, è possibile utilizzare la tattica

    we need to prove P (H1).

questa tattica sospende temporaneamente la dimostrazione corrente, consentendo di dimostrare prima di tutto P; al termine della dimostrazione di P, si ritornerà alla dimostrazione precedente, nella quale però sarà possibile utilizzare una nuova ipotesi H1 avente tipo P.

Se il contesto della dimostrazione contiene due ipotesi H1 : P e H2 : Q, è possibile dimostrare immediatamente P ∧ Q utilizzando la sintassi

    by conj,H1,H2 we proved (P ∧ Q) (H3).

dove conj è un lemma della libreria utilizzato per derivare congiunzioni di formule.

Quando si ha un'ipotesi H : P ∧ Q, è spesso necessario spezzare H in due ipotesi separate. In questo caso, utilizzeremo la tattica

    by H we have P (H1) and Q (H2).

che deriva due nuove ipotesi H1 : P e H2 : Q.

Negazione

In Matita, la costante False rappresenta l'assurdo logico, un'asserzione incoerente che non può essere dimostrata.

La negazione ¬P è definita come P → False ("P implica l'assurdo"). Pertanto, date due ipotesi H1 : P e H2 : ¬P è perfettamente legale utilizzare la tattica

    by H1,H2 we proved False (H3).

per derivare una nuova ipotesi H3 : False (contraddizione).

Se False compare tra le ipotesi, vuol dire che il contesto corrente della dimostrazione è incoerente/contraddittorio, pertanto il goal può essere chiuso (stiamo considerando un caso che non si può verificare, pertanto non c'è nulla da dimostrare!). In particolare, se abbiamo H : False e la tesi corrente è Q chiuderemo immediatamente il goal con la tattica

    we proceed by cases on H to prove Q.

Solo quando procediamo per casi su un'ipotesi di tipo False, non bisogna fare seguire alla tattica alcun passo case (la ratio è che False non è derivabile in nessun caso).

Se False è la tesi che dobbiamo dimostrare, l'unica speranza che abbiamo è quella che il contesto delle ipotesi sia incoerente/contraddittorio (cioè, per esempio, contenga due ipotesi P e ¬P).

Il tipo di dato list

In modo simile a molti linguaggi di programmazione, Matita consente di ragionare su liste di oggetti. Dato un qualunque tipo T, è definito il tipo list T delle liste di oggetti aventi tipo T.

Le liste sono definite induttivamente mediante due costruttori:

• nil : list T, corrispondente alla lista vuota
• cons : T → list T → list T, che costruisce una nuova lista aggiungendo un nuovo elemento a una lista data

In genere i costruttori vengono indicati con una notazione compatta:

• [] per la lista vuota (nil)
• x::y per la lista che ha in testa l'oggetto x e in coda la lista y (cioè cons x y)
• [x1; x2; x3; ...; xk] per la lista ottenuta mettendo in sequenza gli oggetti x1, x2, x3, ..., xk (cioè cons x1 (cons x2 (cons x3 ... (cons xk nil) ...)))

La notazione compatta va utilizzata in ogni situazione, eccetto che alla sinistra del simbolo ⇒ all'interno dei costrutti match, dove è obbligatorio utilizzare nil e cons.

Date due liste l1 e l2 aventi lo stesso tipo, la notazione l1 @ l2 viene utilizzata per produrre la lista che si ottiene concatenando l1 ed l2: ad esempio, [1;2] @ [3;4] = [1;2;3;4].

Induzione strutturale su liste

Il principio di induzione strutturale può essere utilizzato anche nel caso delle liste. Se dobbiamo dimostrare una proposizione P l (ovvero qualunque proprietà che menzioni una certa l avente tipo list T) possiamo utilizzare l'usuale tattica we proceed by induction on l secondo lo schema seguente:

    we proceed by induction on l to prove (P l)

    case nil.
      ...dimostrazione di P []

    case cons.
      assume hd : T.
      assume tl : (list T).
      by induction hypothesis we know (P tl) (IH).
      ...dimostrazione di P (hd::tl)

Si noti la somiglianza del principio di induzione su liste con quello classico sui numeri naturali.

Appartenenza a una lista

La notazione x ∈ l viene utilizzata per asserire che un oggetto x compare come elemento della lista l (naturalmente, se il tipo di x è T, il tipo di l deve essere list T). Per scrivere il simbolo ∈, digitare \in e quindi schiacciare ALT+L.

La libreria di Matita

Per portare a termine l'esercitazione utilizzate i seguenti lemmi (già dimostrati):

• conj : ∀P,Q.P → Q → P ∧ Q
• sem_bool : ∀F,v. [[ F ]]v = 0 ∨ [[ F ]]v = 1
• in_list_singleton : ∀T.∀a:T. a ∈ [a]
• in_list_head : ∀T.∀x:T.∀l:list T.x ∈ x::l
• in_list_cons : ∀T.∀x,y:T.∀l:list T. x ∈ l → x ∈ y::l
• in_list_cons_case : ∀T.∀x,y:T.∀l:list T. x ∈ y::l → x = y ∨ x ∈ l
• in_list_to_in_list_append_l: ∀T.∀x:T.∀l1,l2:list T.x ∈ l1 → x ∈ (l1@l2)
• in_list_to_in_list_append_r: ∀T.∀x:T.∀l1,l2:list T.x ∈ l2 → x ∈ (l1@l2)

Il teorema di deduzione semantica

Diciamo che una formula F è conseguenza semantica di una lista di formule Gamma se per ogni mondo v che assegna il valore semantico "vero" alle formule di Gamma, si ha che F è vera in v. Utilizziamo la notazione Gamma ⊧ F definendola come

    ∀v.(∀F0.F0 ∈ Gamma → [[ F0 ]]v = 1) → [[ F ]]v = 1.

Il simbolo ⊧ può essere inserito digitando \models e quindi schiacciando ALT+L. Il teorema di deduzione semantica afferma che, se [F1;F2;F3;...;Fk] ⊧ F, allora [] ⊧ FImpl Fk (... (FImpl F3 (FImpl F2 (FImpl F1 F)))...).

Per dimostrare il teorema:

• per prima cosa proviamo il lemma deduction_step : F1::Gamma ⊧ F2 → Gamma ⊧ FImpl F1 F2; la dimostrazione utilizza il lemma sem_bool per ragionare per casi sui valori di verità [[ F1 ]]v e [[ F2 ]]v.
• definiamo quindi una funzione ricorsiva mk_impl [F1;F2;F3;...;Fk] F che restituisca la formula FImpl Fk (... (FImpl F3 (FImpl F2 (FImpl F1 F)))...)
• mediante la definizione precedente, enunciamo il teorema di deduzione come ∀Gamma,F. Gamma ⊧ F → [] ⊧ mk_impl Gamma F.

La dimostrazione del teorema di deduzione procede per induzione sulla lista Gamma utilizzando, nel caso cons, il lemma deduction_step appena dimostrato.

Insieme degli atomi di una formula

Si definisce ricorsivamente la funzione atoms : Formula → list nat che calcola la lista degli atomi che occorrono in una determinata formula.

Il lemma v_equiv chiede di dimostrare che dati due mondi v1 e v2 e una formula F, se v1 e v2 assegnano gli stessi valori di verità a tutti gli atomi che occorrono in F, allora [[ F ]]v1 = [[ F ]]v2.

La dimostrazione procede per induzione su F. E' possibile utilizzare i lemmi della libreria in_list_singleton, in_list_to_in_list_append_l, in_list_to_in_list_append_r.

Insieme delle sottoformule di una formula

Si definisce ricorsivamente la funzione subformulas : Formula → list Formula che calcola la lista delle sottoformule di una formula data. Si noti che la lista delle sottoformule di una formula F comprende anche la formula F stessa (pertanto subset F non è mai una lista vuota, per nessuna F).

Si definiscono inoltre le formule positive come segue

positive F sse (¬ FBot ∈ subformulas F) ∧ (∀F'.¬ FNot F' ∈ subformulas F)

Informalmente, una formula è positiva se e solo se tra le sue sottoformule non contiene né costanti FBot, né formule negate. La definizione fa uso della funzione subformulas. In pratica, una formula positiva è ottenuta combinando atomi, costanti FTop, connettivi FAnd, FOr e FImpl, e nient'altro.

Il lemma positive_and_l chiede di dimostrare che se FAnd F1 F2 è una formula positiva, allora anche F1 è una formula positiva. La dimostrazione si ottiene espandendo la definizione di positive e utilizzando i lemmi della libreria in_list_to_in_list_append_l, in_list_to_in_list_append_r, in_list_cons e conj.

Si assumano poi assiomaticamente le proprietà

• positive_and_r : ∀F1,F2.positive (FAnd F1 F2) → positive F2
• positive_or_l : ∀F1,F2.positive (FOr F1 F2) → positive F1
• positive_or_r : ∀F1,F2.positive (FOr F1 F2) → positive F2
• positive_impl_l : ∀F1,F2.positive (FImpl F1 F2) → positive F1
• positive_impl_r : ∀F1,F2.positive (FImpl F1 F2) → positive F2

Date queste proprietà (il lemma positive_and_l e i cinque assiomi), si dimostri il teorema positive_satisfiable, che stabilisce che ogni formula positiva è vera nel mondo true_v che assegna il valore di verità 1 a tutti gli atomi. La dimostrazione è per induzione strutturale sulla formula positiva F. E' possibile utilizzare il lemma della libreria in_list_head.

Come scrivere i simboli

Elenco dei simboli più comuni e i loro nomi separati da virgola, Se sono necessari dei simboli non riportati di seguito si può visualizzare l'intera lista dal menù a tendina View ▹ TeX/UTF8 table.

• → : \to, ->
• ∧ : \land
• ∨ : \lor
• ¬ : \lnot
• ⇒ : \Rightarrow, =>
• ℕ : \naturals
• ≝ : \def, :=
• ≡ : \equiv
• ∀ : \forall
• ⊧ : \models
• ∈ : \in

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.

• by ... we have ... (...) and ... (...).

  Permette di spezzare un'ipotesi in forma di congiunzione: ad esempio, data un'ipotesi H : P ∧ Q, possiamo ottenere nuove ipotesi H1 : P e H2 : Q mediante la tattica by H we have P (H1) and Q (H2).

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

  Sospende temporaneamente la dimostrazione corrente per dimostrare un lemma ausiliario. Al termine della dimostrazione del lemma, il suo enunciato verrà aggiunto alle ipotesi della dimostrazione originaria. Ad esempio la tattica we need to prove P (H) comincia immediatamente la dimostrazione di P; al termine della dimostrazione di P, si torna al goal precedente, che conterrà una nuova ipotesi H : P.