From: Enrico Tassi Date: Sat, 18 Oct 2008 18:07:37 +0000 (+0000) Subject: more doc X-Git-Tag: make_still_working~4672 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a602cce3fbd1e3c3725ea93541516a2070537d05;p=helm.git more doc --- diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index d8b64d7df..a4864b6ef 100644 --- a/helm/software/matita/contribs/didactic/induction.ma +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -25,93 +25,94 @@ *) (*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 - - ::= "+" | "*" | "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 + + ::= "+" | "*" | "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 @@ -229,7 +230,7 @@ definition v1101 ≝ λx. 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 @@ -242,7 +243,7 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ 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) @@ -287,18 +288,24 @@ interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). (*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*) @@ -317,6 +324,7 @@ assume x : ℕ. 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). @@ -326,6 +334,7 @@ case FBot. 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 : (ℕ → ℕ). @@ -334,6 +343,7 @@ case FTop. 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