New tactic [setoid_]rewrite ... in ... [generate side conditions ...].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 30 insertions, 26 deletions

diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index a57f7f2d1e..86f54406e3 100644
--- a/test-suite/success/setoid_test2.v8
+++ b/test-suite/success/setoid_test2.v8
@@ -3,22 +3,18 @@ Require Export Setoid.
 (* Testare:
    +1. due setoidi con ugualianza diversa sullo stesso tipo
    +2. due setoidi sulla stessa uguaglianza
-    3. due morfismi sulla stessa funzione ma setoidi diversi
+   +3. due morfismi sulla stessa funzione ma setoidi diversi
    +4. due morfismi sulla stessa funzione e stessi setoidi
    +5. setoid_replace
-    6. solo cammini mal tipati (attualmente non verifico mai che il
-       cammino trovato prendendo a caso sia mal-tipato)
-       ==> non riesco ancora a fare l'esempio perche' mi manca la sintassi.
-       Dovrei giocare con i moduli...
+   +6. solo cammini mal tipati
    +7. esempio (f (g (h E1)))
        dove h:(T1,=1) -> T2, g:T2->(T3,=3), f:(T3,=3)->Prop
    +8. test con occorrenze non lineari del pattern
    +9. test in cui setoid_replace fa direttamente fallback su replace
    10. sezioni
    11. setoid_rewrite invocata su una Leibniz equality ritorna un errore
-       invece di provare rewrite. Provare rewrite divergerebbe ==> trovare
-       una soluzione.
-   12. goal con Imp
+       invece di provare rewrite.
+  +12. goal con impl
   +13. testare *veramente* setoid_replace (ora testato solamente il caso
        di fallback su replace)
 
@@ -28,24 +24,35 @@ Require Export Setoid.
     3. iff invece di if in "Add Morphism" nel caso di predicati
     4. setoid_replace poteva riscrivere sia c1 in c2 che c2 in c1
 
-### setoid_replace ... with ... dovrebbe tentare le due vie;
-    che fare se entrambe funzionano?
-### coq_impl (in mark_occur) ha implicitamente tipo 'a -> 'a
-    dove 'a = (Prop,iff) oppure 'a = (Prof,impl). Altri tipi (e.g.
-    (Prop,iff) -> (Prop,impl)) non sono ammessi.
-### Pre-dichiarare il morfismo impl.
+### Come evitare di dover fare "Require Setoid" prima di usare la
+    tattica?
+
+### scelta: quando ci sono piu' scelte dare un warning oppure fallire?
+    difficile quando la tattica e' rewrite ed e' usata in tattiche
+    automatiche
+
+### in test4.v il setoid_rewrite non si puo' sostituire con rewrite
+    perche' questo ultimo fallisce per via dell'unificazione
+
+### ??? <-> non e' sottorelazione di ->. Quindi ora puo' capitare
+    di non riuscire a provare goal del tipo A /\ B dove (A, <->) e
+    (B, ->) (per esempio)
+
 ### Dichiarazione dentro a un module type e a una sezione: ???
 ### Relazioni universalmente quantificate: ???
 ### Implementare zucchero sintattico per partial setoids.
+    Stessa cosa per ogni relazione transitiva? In effetti basta lo
+    zucchero sintattico per le transitive.
 ### Nota: il parsing e pretty printing delle relazioni non e' in synch!
     eq contro (ty,eq). Uniformare
 
+### il messaggio di errore non e' assolutamente significativo quando
+    nessuna marcatura viene trovata
+
   Implementare:
    -1. user-defined subrelations && user-proved subrelations
     0. trucco di Bruno
-    1. rewrite ... in ...
     2. setoid_replace ... with ... in ...
-    3. perche' rewrite ma non replace?
     4. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?)
 
   Sorgenti di inefficacia:
@@ -69,9 +76,9 @@ Require Export Setoid.
     6. permette di gestire riscritture ove ad almeno una funzione venga
        associato piu' di un morfismo. Vengono automaticamente calcolate
        le scelte globali che rispettano il tipaggio.
-   #7. se esistono piu' scelte globali che rispettano le regole di tipaggio
+    7. se esistono piu' scelte globali che rispettano le regole di tipaggio
        l'utente puo' esplicitamente disambiguare la scelta globale fornendo
-       esplicitamente la scelta per alcune occorrenze di una funzione.
+       esplicitamente la scelta delle side conditions generate.
     8. nel caso in cui la setoid_replace sia stata invocata al posto
        della replace la setoid_replace invoca direttamente la replace
     9. permette di gestire termini in cui il prefisso iniziale dell'albero
@@ -80,14 +87,11 @@ Require Export Setoid.
        Ovvero ammette anche morfismi il cui dominio e/o codominio sia
        l'uguaglianza di Leibniz. (Se entrambi sono uguaglianze di Leibniz
        allora il setoide e' una semplice funzione).
-  ?10. maggiore uniformita' sintattica: rewrite == setoid_rewrite;
-       replace == setoid_replace; symmetry == setoid_symmetry;
-       reflexivity == setoid_reflexivity. Nota: in tal caso, pero',
-       si e' sempre in presenza di ambiguita' per tutte le tattiche tranne
-       che la rewrite (in quanto c'e' sempre almeno la scelta setoide vs
-       Leibniz). Dare un comando che permette
-       di indicare il setoide di default associato a una funzione in un
-       determinato momento?
+  ?10. [setoid_]rewrite ... in ...
+       setoid_replace ... in
+       [setoid_]reflexivity???
+       [setoid_]transitivity???
+       [setoid_]symmetry???
 *)
 
 Axiom S1: Set.