From a4e18d465037106982d84a85194c4593dad530b8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 18 Oct 2008 19:08:25 +0000 Subject: [PATCH] tactic language documented; --- .../matita/contribs/didactic/Makefile | 1 + .../matita/contribs/didactic/induction.ma | 60 +++++++++++++++++-- 2 files changed, 57 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile index f2aefca04..e2d1a0f0f 100644 --- a/helm/software/matita/contribs/didactic/Makefile +++ b/helm/software/matita/contribs/didactic/Makefile @@ -17,5 +17,6 @@ depend.opt: exercise-%: % cp $< $@ perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/.../msg;print' -i $@ + perl -ne 'undef $$/;s/\(\*DOCBEGIN.*?DOCEND\*\)//msg;print' -i $@ (echo ''; awk 'BEGIN { p = 0; } /DOCEND/ { p = 0; } { if (p == 1) print $$0; } /DOCBEGIN/ { p = 1;}' < $< | markdown; echo '') > $@.html diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index 3b6d66519..99a0e8a5a 100644 --- a/helm/software/matita/contribs/didactic/induction.ma +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -296,16 +296,68 @@ 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 = 3` e si avesse una ipotesi `sin π = 0` dal + nome `H`, si potrebbe usare il comando `conclude (0 + 3) = 3 by H`. + * `= (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*) -- 2.39.2