From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Sep 2002 15:22:28 +0000 (+0000)
Subject: List of tactics implemented and to implement (italian only).
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa3b2266649e824dd61152b74b274528bd3646bb;p=helm.git

List of tactics implemented and to implement (italian only).
---

diff --git a/helm/gTopLevel/TATTICHE b/helm/gTopLevel/TATTICHE
new file mode 100644
index 000000000..88d989ded
--- /dev/null
+++ b/helm/gTopLevel/TATTICHE
@@ -0,0 +1,144 @@
+V7.2:
+
+Da valutare:
+ * MetaLinguaggio di David Delayale per l'implementazione di tattiche
+
+V6.3:
+
+Da valutare:
+ * Print
+ * Extraction
+ * Opaque/Transparent
+ * SearchIsos
+ * Load di script di tattiche
+ * "Pretty" Parsing
+ * Log dei tempi per ogni possibile richiesta
+ * Undo
+ * Focus/Unfocus (nella prova completa in linguaggio naturale)
+ * Show Tree (resa dell'albero dei sequenti)
+ * Tatticali:
+    - OrElse
+    - Repeat
+    - Do
+    - Info
+    - Try
+    - First
+    - Solve
+    - Abstract
+    - ;
+    - ; [ ... | ... | ... ]
+    - (...)
+ * Assumption
+ * Apply with
+ * LApply
+ * Absurd
+ * Contradiction
+ * Cbv/Lazy Beta Delta Iota Zeta
+ * Red (riduzione di un backbone con delta della testa + beta e iota)
+ * Unfold (equivalente a Hnf dell'occorrenza)
+ * Pattern
+ * Constructor n / Split / Left/ Right/ Exists/ Reflexivity
+ * Elim term quando term ha come tipo un Pi
+ * ElimType (fatta da Zack; metterla disponibile)
+ * Induction su una applicazione
+ * Induction su una ipotesi
+ * Case su una applicazione e su una ipotesi
+ * Intros destrutturante
+ * Decompose
+ * Double Induction
+ * Rewrite (ma eliminare un'uguaglianza o applicare eq_ind_r non funziona gia'?)
+ * Replace (che prende due termini _NON_ convertibili e genera come goal
+   l'uguaglianza dei due). Unificarla con la change, che diventa la replace
+   non overkilling?
+ * Symmetry e Transitivity (basta applicare i due teoremi giusti)
+ * Decide Equality (ma non dovrebbe essere un teorema???)
+ * Compare
+ * Discriminate
+ * Injection
+ * Simplify_eq (== Discriminate o Injection su una ipotesi)
+ * Dependent Rewrite
+ * Inversion [Nota: Derive Inversion genera e salva il teorema!]
+ * Quote (per implementare tattiche riflessive senza scrivere codice ML!!!!)
+ * Tauto/Intuition
+ * Linear
+ * AutoRewrite
+ * Realizer/Program
+ * Scheme
+ * Omega
+
+Implementate:
+ * Enunciare un teorema
+ * (Ri)aprire un teorema gia' dimostrato per modificarne certe parti
+ * Check (e successiva possibilita' di applicare reduction tactics)
+ * Exact
+ * Apply/EApply
+ * Cut
+ * Change [Una conversion tactic. Problema: il termine digitato viene
+    parsato nel contesto della conclusione e non in quello della selezione!!!]
+ * Conversion tactics, sia nelle ipotesi che nella conclusione:
+   - Reduce (== Compute)
+   - Hnf
+   - Simpl
+ * Fold
+ * ElimIntrosSimpl
+ * Let...In (= LetTac)
+ * Salvare e caricare una prova incompleta (ma nel posto sbagliato!)
+ * ClearBody
+ * Clear
+ * Ring
+
+Da implementare:
+ * Implicit: quando si usano gli implicit, l'input non puo' piu' essere
+   type-checkato, ma bisogna fare una refine (ancora non implementata).
+   Di conseguenza _OGNI_ tattica si rompe. Inoltre l'implementazione di
+   Implicit e' ancora errata in quanto il contesto canonico delle nuove
+   variabili e' sempre vuoto anche se dovrebbe essere uguale a quello
+   di partenza + le nuove variabili introdotte durante il parsing.
+ * Nella type_of NON viene controllato che il metasenv di una current-proof
+   sia ben formato. PUNTO IMPORTANTE: farlo nel metasenv parziale, cosi' da
+   evitare cicli; ma dopo e' un bordello l'unificazione. Oppure fare un
+   semplice controllo di aciclicita'.
+ * ClearBody e Clear NON restringono ancora altre metavariabili. Invece viene
+   sollevata un'eccezione di tipaggio. Esempio: n:nat |- ?1[n] se faccio clear
+   di n dovrei restringere ?1. Se invece prima faccio clear di n in ?1, quando
+   torno su questo goal e faccio clear di n ottengo un'eccezione di CicPp.
+ * La reduction_tactic (in ProofEngine.ml) e' bacatissima, come descritto
+   nei commenti. Fixare.
+ * Reimplementare Cut usando LetIn + applicazione + Intro oppure usando
+   LetIn + ClearBody (soluzione piu' elegante IMHO)
+ * Refine
+ ? Sia [x:=t]r il tipo di [x:t]k e x non occorra mai libera in r.
+   Dovrei forse tornare semplicemente r?
+ ? Cambiare il nome delle META da int a una stringa?
+   [ATTENZIONE: CAMBIAMENTO NELLA DTD]
+ * Fold e' l'inverso di Reduce e quindi non disfa cio' che viene fatto da
+   Simpl e da Whd. Generalizzarlo facendo Reduce e poi Change con ogni termine?
+   Oppure fare una FoldWhd, una FoldHnf, una FoldSimpl, etc.?
+ * Fold localizzato in un termine selezionato
+ * Move e "Unclear" (che fa l'undo di Clear/Move e conversioni nelle ipotesi)
+   Non sono implementabili. Ma avrebbero senso?
+ * queries e roba basata sulle queries:
+   - Search
+   - Locate (anche di tipi induttivi e costruttori)
+   - Auto
+   - EAuto
+   - Prolog (???????????)
+ * Save con tanto di esportazione: esportare nel posto giusto!
+ * Dare una definizione (quasi equivalente a check + unfold, ma mancano
+   gli inner-types)
+ * Dare una definizione induttiva
+ * Intro (Come scegliere i nomi freschi?) e Intros until
+ * Generalize
+ * Fissare il bug di change (ovvero il problema del contesto in cui viene
+   parsato l'input dell'utente)
+ * Tornare un errore se si cerca di applicare una reduction tactic in una
+   ipotesi nella scratch area
+ * Field
+ * JProver. Che rapporto c'e' fra JProver e Tauto/Intuition?
+ * altre contrib da integrare?
+
+Da non implementare:
+  * Print All
+  * Compile/Read/Require
+  * Print/Save/Restore States
+  * Let