Several tests for the bug-fixed and improved new version of

setoid_{replace,rewrite}.


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

1 files changed, 89 insertions, 0 deletions

diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
new file mode 100644
index 000000000..ce240c742
--- /dev/null
+++ b/test-suite/success/setoid_test2.v8
@@ -0,0 +1,89 @@
+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
+   +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...
+   +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
+
+  Implementare:
+    ?. unificare nozione di ACFunction con ACSetoid quando gli argomenti
+       sono tutti Leibniz?
+   -1. scelta dei cammini con backtracking.
+       Nota: in effetti ogni morfismo puo' essere anche interpretato
+       semplicemente come avente Leibniz in input e, quando ha Leibniz
+       in input, come avente qualunque setoide o Leibniz come output.
+       Nel caso di rewrite e' l'uguaglianza usata che va a imporre un vincolo
+       sulle scelte globali. Nel caso di replace tale vincolo non c'e' e si e'
+       sempre in presenza di ambiguita'. Dare un comando che permette
+       di indicare il setoide di default associato a una funzione in un
+       determinato momento?
+    0. trucco di Bruno
+    1. rewrite ... in ...
+    2. setoid_replace ... with ... in ...
+    3. perche' rewrite ma non replace?
+    4. [setoid_]symmetry, [setoid_]reflexivity
+
+  Sorgenti di inefficacia:
+    1. quando la tattica decide di fare replace e in testa c'e' un'uguaglianza
+       di Leibniz puo' capitare che venga generato lo stesso identico goal!
+       e.g.  E1 = t   tattica rewrite E1 with E2
+    2. quando ci sono cammini che contengono sequenze di ACFunction si
+       potrebbe fare un'unica replace sui sottoalberi che hanno come tipo
+       un setoide; invece attualmente vengono fatte tante replace, anche
+       per le ACFunction (i.e. per Leibniz)
+    3. scelta del setoide di default per un sostegno: per farlo velocemente
+       ci vorrebbe una tabella hash; attualmente viene fatta una ricerca
+       lineare sul range della setoid_table
+
+  Vantaggi rispetto alla vecchia tattica:
+    1. permette di avere setoidi differenti con lo stesso sostegno,
+       ma equivalenza differente
+    2. accetta setoidi differenti con lo stesso sostegno e stessa
+       equivalenza, scegliendo a caso quello da usare (proof irrelevance)
+    3. permette di avere morfismi differenti sulla stessa funzione
+       se hanno dominio o codominio differenti
+    4. accetta di avere morfismi differenti sulla stessa funzione e con
+       lo stesso dominio e codominio, scegliendo a caso quello da usare
+       (proof irrelevance)
+   #5. quando un morfismo viene definito, se la scelta del dominio o del
+       codominio e' ambigua l'utente puo' esplicitamente disambiguare
+       la scelta fornendo esplicitamente il "tipo" del morfismo
+   #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
+       l'utente puo' esplicitamente disambiguare la scelta globale fornendo
+       esplicitamente la scelta per alcune occorrenze di una funzione.
+    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
+       (fino a trovare il termine da riscrivere) non sia formato esclusivamente
+       da morfismi il cui dominio e codominio sia un setoide.
+       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).
+       L'implementazione di fatto alterna passi di setoid_replace a passi
+       di replace (per gestire i due casi)
+  ?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?
+*)
+
+Axiom S1 : Set.
+Axiom eqS1 : S1 -> S1 -> Prop.
\ No newline at end of file