Come scrivere i simboli

Per inserire i simboli matematici è necessario digitare il loro nome e poi premere ALT-L. In generale i nomi dei simboli sono della forma \nome, ad esempio \equiv. Alcuni simboli molto frequenti hanno dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome \Rightarrow sia =>.

Segue un 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, ->
• ⇒ : \Rightarrow, =>
• ℕ : \naturals
• ≝ : \def, :=
• ≡ : \equiv
• ∀ : \forall

La sintassi ∀x.P significa "per tutti gli x vale P".

La sintassi F → G dove F e G sono proposizioni nel metalinguaggio significa "F implica G". Attenzione, il simbolo ⇒ (usato a lezione) non ha lo stesso significato in Matita.

La sintassi ℕ → ℕ è il tipo delle funzioni che preso un numero naturale restituiscono un numero naturale.

La sintassi di Matita

Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si differenzia in vari aspetti da quella che solitamente viene utilizzata per fare matematica, e ricorda quella di Scheme che state vedendo nel corso di programmazione.

• applicazione

  Se f è una funzione che si aspetta due argomenti, l'applucazione di f agli argomenti x e y si scrive (f x y) e non f(x,y). Le parentesi possono essere omesse se il senso è chiaro dal contesto. In particolare vengono omesse quando l'applicazione è argomento di un operatore binario. Esempio: f x y + f y x si legge (f x y) + (f y x).

• minimo e massimo

  Le funzioni min e max non fanno eccezione, per calcolare il massimo tra x e y si scrive (max x y) e non max{x,y}

• Le funzioni definite per ricorsione strutturale utilizzano il costrutto let rec (ricorsione) e il costrutto match (analisi per casi).

  Ad esempio la funzione count definita a lezione come

  count ⊤ ≝ 1
  count (F1 ∧ F2) ≝ 1 + count F1 + count F2 
  ...
  

  la si esprime come

  let rec count F on F ≝ 
    match F with 
    [ ⊤ ⇒ 1 
    | F1 ∧ F2 ⇒ 1 + count F1 + count F2 
    ...
    ].
  

• Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi simile a BNF. Per esempio per definire

  <A> ::= <A> "+" <A> | <A> "*" <A> | "0" | "1"
  

  si usa il seguente comando

  inductive A : Type ≝
  | Plus : A → A → A    
  | Times : A → A → A   
  | Zero : A
  | One : A
  .
  

La ratio è che Plus prende due argomenti di tipo A per darmi un A, mentre Zero non prende nessun argomento per darmi un A. Al posto di usare operatori infissi (0 + 0) la definizione crea operatori prefissi (funzioni). Quindi (0+0) si scriverà come (Plus Zero Zero).

Il linguaggio di dimostrazione di Matita

Alcuni degli esercizi seguenti richiedono di scrivere una dimostrazione. Tale dimostrazione deve essere scritta utilizzando il linguaggio di dimostrazione di Matita. Tale linguaggio è composto dai seguenti comandi, chiamati tattiche dichiarative. I comandi sono anche descritti nel manuale on-line, consultabile a partire dal menu Help/Contents sotto la voce Declarative tactics.

• assume nome : tipo

  Quando si deve dimostrare un tesi come ∀F : Formula.P, il comando assume F : Formula fissa una generica Formula F e la tesi diventa P dove F è fissata.

• suppose P (nome)

  Quando si deve dimostrare una tesi come P → Q (da leggersi come se vale P allora vale Q), il comando suppose P (Ipotesi1) da il nome Ipotesi1 a P e cambia la tesi Q, che ora può essere dimostrata facendo riferimento all'assunzione P tramite il nome Ipotesi1.

• we procede by induction on F to prove Q

  Se F è il nome di una (ad esempio) Formula precedentemente assunta tramite il comando assume, inizia una prova per induzione su F.

• case name (var1 : type1) ... (varn : typen)

  Nelle prove per induzione o per casi, ogni caso deve iniziare con il comando case. Ad esempio se si procede per induzione su un numero naturale, uno dei casi sarà case O e l'altro case S (x: nat). Analogamente, nel caso di liste si può usare Cons (n: nat) (L: list) per dare nomi agli argomenti, come visto a lezione.

• we procede by cases on x to prove Q

  Analogo a we procede by induction on F to prove Q

• by induction hypothesis we know P (name)

  Nei casi non base di una prova per induzione sono disponibili delle ipotesi induttive, quindi la tesi è della forma P → Q, ed è possibile dare un nome a P e procedere a dimostrare Q. Equivale a suppose.

• we need to prove P

  Dice esplicitamente cosa dobbiamo dimostrare. Matita verifica che sia vero. È particolarmente interessante nella variante

• that is equivalent to Q

  dopo aver usato un comando we need to prove P, un comando suppose P (H) o un comando by induction hypothesis we know P (H) potete riscrivere P in Q usando il comando that is equivalent to Q. Quesot è possibile solo se Q si ottiene da P semplicemente espandendo le definizioni (eventualmente ricorsive), ma senza l'uso di lemmi. Ad esempio dopo il comando we need to prove (min 3 5 = max 1 3) si può usare il comando that is equivalent to (3 = max 1 3) in quanto per definizione di minimo, il minimo tra 3 e 5 è 3.

• by name1,...,namen we proved P (namehyp)

  Permette di dimostrare P a partire da name,…,namen e successivamente chiamare namehyp l'ipotesi che dice che P è vera. (Nota: non è una vera ipotesi in quanto P è già stata dimostrata. È piuttosto una formula intermedia nel ragionamento.

• `conclude (P)

  Usabile solo quando la tesi è della forma P = Q. Inizia una catena di equazioni che da P condurrà fino a Q.

  Quando la tesi è della forma P = Q, si possono utilizzare delle ipotesi della forma A = B riscrivendo A in B (o viceversa) in P. Per esempio se la tesi fosse sin π + 3 = 7 - 4 e si avesse una ipotesi sin π = 0 dal nome H, si potrebbe usare il comando conclude (sin π + 3) = (0 + 3) by H per cambiare la conclusione in 0 + 3 = 7 - 4.

• = (R) by name1,…,namen

  Effettua un passo di una catena di equazioni il cui passo precedente era giunto a P. La combinazione dei lemmi name1,…,namen deve poter concludere che P = R. Per esempio se l'ultimo passo avesse concluso sin π + 3 e si avesse una ipotesi sin π = 0 dal nome H, si potrebbe usare il comando = (0 + 3) by H.

  La lista di lemmi (e il corrispondente by) possono essere omessi se il passo di riscrittura corrisponde ad espandere definizioni ricorsive o meno.

• = (Q) by name1,…,namen done

  Effettua l'ultimo passo di una catena di equazioni. È utilizzabile esclusivamente quando la tesi al momento dell'apertura della catena era della forma P = Q.

• done

  Termina un caso della dimostrazione quando la conclusione è ovvia. Una variante è

  by name1,…,namen done

  che usa le ipotesi/teoremi name1,…,namen per concludere la tesi.