X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Finduction.ma;h=aa7b7aff6d7a742d4ac5359bb34434c890b0ba64;hb=f0643b9fd4160f49c0d368855d0e3e638f2d58ca;hp=3b6d66519b22820cbb72f49430da32d1b3bce1b6;hpb=aba1baf85bb8e6b3ea3e66a8c2d07601066d26bc;p=helm.git diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index 3b6d66519..aa7b7aff6 100644 --- a/helm/software/matita/contribs/didactic/induction.ma +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -30,7 +30,7 @@ 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 +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 `=>`. @@ -46,7 +46,7 @@ l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`. * `≡` : `\equiv` * `∀` : `\forall` -La sintassi `∀v.P` significa "per tutti i `v` vale `P`". +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) @@ -221,14 +221,15 @@ interpretation "Semantic of Formula" 'semantics v a = (sem v a). definizione di `sem` e prima di continuare è necessario che la sistemiate. *) definition v1101 ≝ λx. - if eqb x 0 then 1 (* Atom 0 ↦ 1 *) - else if eqb x 1 then 1 (* Atom 1 ↦ 1 *) - else if eqb x 2 then 0 (* Atom 2 ↦ 0 *) - else if eqb x 3 then 1 (* Atom 3 ↦ 1 *) - else 0. (* Atom _ ↦ 0 *) + if eqb x 0 then 1 (* FAtom 0 ↦ 1 *) + else if eqb x 1 then 1 (* FAtom 1 ↦ 1 *) + else if eqb x 2 then 0 (* FAtom 2 ↦ 0 *) + else if eqb x 3 then 1 (* FAtom 3 ↦ 1 *) + else 0. (* FAtom _ ↦ 0 *) -definition esempio1 ≝ (FImpl (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))). +definition esempio1 ≝ + (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))). eval normalize on [[ esempio1 ]]_v1101. @@ -252,8 +253,6 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ | FNot F ⇒ FNot (subst x G F) ]. -(* AGGIUNGERE ALCUNI TEST *) - (* NOTA ==== @@ -285,6 +284,25 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associat notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). +(* Test 2 + ====== + + Viene fornita una formula di esempio `esempio2`, + e una formula `esempio3` che rimpiazzerà gli atomi + `FAtom 2` di `esempio2`. + + Il risultato atteso è la formula: + + FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1)) + (FOr (FAtom O) (FAtom 1)) + +*) + +definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). + +definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)). + +eval normalize on (esempio2 [ esempio3 / 2]). (*DOCBEGIN @@ -296,16 +314,69 @@ 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)` -* `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` + + 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` -* `by name we proved P (name)` + + 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`. DOCEND*)