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.
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'applicazione 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)
.
Prendete il file exercise-substitution.ma e apritelo con l'editor di Matita, troverete una serie di esercizi da completare seguendo quanto letto finora.
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
.