tactic language documented;

[helm.git] / helm / software / matita / contribs / didactic / induction.ma

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 3b6d66519b22820cbb72f49430da32d1b3bce1b6..99a0e8a5a07b55768b5266f4a799f3de965e4419 100644 (file)
--- 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*)