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

L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione deve essere scritta utilizzando il linguaggio di dimostrazione di Matita. Tale linguaggio è composto dai seguenti comandi:

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

  Nelle prove per induzione o per casi, ogni caso deve iniziare con il comando case nome, ad esempio se si procede per induzione di una formula uno dei casi sarà quello in cui la formula è ⊥, si deve quindi iniziare la sotto dimostrazione per tale caso con case ⊥.

• 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. Simile a suppose.

• the thesis becomes P

  Permette di modificare la tesi, utilizzando le definizioni (eventualmente ricorsive) che vi compaiono. Ad esempio se la tesi fosse min 3 5 = max 1 3 si potrebbe usare il comando the thesis becomes (3 = max 1 3) in quanto per definizione di minimo, il minimo tra 3 e 5 è 3.

• by name1 we proved P (name2)

  Permette di ottenere una nuova ipotesi P chiamandola name2 utilizzando l'ipotesi name1.

• conclude (P) = (Q) by name

  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.

• = (P) by name

  Da utilizzare in seguito a un comando conclude per riscrivere con altre ipotesi.

• done

  Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi è della forma t = t, ad esempio 0 = 0 oppure v x = v x.