*)
(*DOCBEGIN
+
+Come scrivere i simboli
+=======================
+
+Per inserire i simboli matematici è necessario digitare il loro nome
+e poi premere CTRL-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 '∀v.P' significa "per tutti i 'v' 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
- Come scrivere i simboli
- =======================
-
- Per inserire i simboli matematici è necessario digitare il loro nome
- e poi premere CTRL-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 '∀v.P' significa "per tutti i 'v' 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
+ count ⊤ ≝ 1
+ count (F1 ∧ F2) ≝ 1 + count F1 + count F2
+ ...
- 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"
+ la si esprime come
+
+ let rec count F on F ≝
+ match F with
+ [ ⊤ ⇒ 1
+ | F1 ∧ F2 ⇒ 1 + count F1 + count F2
+ ...
+ ].
- si usa il seguente comando
+* 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
+ .
- 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).
+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).
+
DOCEND*)
(* ATTENZIONE
definition esempio1 ≝ (FImpl (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
-(* eval normalize on [[ esempio1 ]]_v1101. *)
+eval normalize on [[ esempio1 ]]_v1101.
(* Esercizio 3
match F with
[ FBot ⇒ FBot
| FTop ⇒ (*BEGIN*)FTop(*END*)
- | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else (*BEGIN*)(FAtom n)(*END*)
+ | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*))
(*BEGIN*)
| FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
| FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
(*DOCBEGIN
- 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'
- * 'suppose nome : tipo'
- * we procede by induction on x to prove Q'
- * the thesis becomes
-
+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'
+* 'suppose P (nome)'
+* 'by induction hypothesis we know P (name)'
+* 'we procede by induction on x to prove Q'
+* 'we procede by cases on x to prove Q'
+* 'case name'
+* 'the thesis becomes P'
+* 'by name we proved P (name)'
+* 'conclude (P) = (Q) by name'
+* '= (P) by name'
+* 'done'
DOCEND*)
suppose (G1 ≡ G2) (H).
we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]).
case FBot.
+ the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]).
the thesis becomes (FBot ≡ FBot[ G2/x ]).
the thesis becomes (FBot ≡ FBot).
the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v).
done.
case FTop.
(*BEGIN*)
+ the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]).
the thesis becomes (FTop ≡ FTop).
the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v).
assume v : (ℕ → ℕ).
done.
case FAtom.
assume n : ℕ.
+ the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]).
the thesis becomes
(if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]).
the thesis becomes
projects / helm.git / commitdiff