1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
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
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
+13. testare *veramente* setoid_replace (ora testato solamente il caso
di fallback su replace)
Incompatibilita':
1. full_trivial in setoid_replace
2. ipotesi permutate in lemma di "Add Morphism"
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.
### Dichiarazione dentro a un module type e a una sezione: ???
### Relazioni universalmente quantificate: ???
### Implementare zucchero sintattico per partial setoids.
### Nota: il parsing e pretty printing delle relazioni non e' in synch!
eq contro (ty,eq). Uniformare
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:
1. 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).
?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.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1.
Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'.
Add Setoid S1 eqS1' SetoidS1'.
Add Setoid S1 eqS1' SetoidS1'_bis.
Axiom S2: Set.
Axiom eqS2: S2 -> S2 -> Prop.
Axiom SetoidS2 : Setoid_Theory S2 eqS2.
Add Setoid S2 eqS2 SetoidS2.
Axiom f : S1 -> nat -> S2.
Add Morphism f : f_compat. Admitted.
Add Morphism f : f_compat2. Admitted.
Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
intros.
rewrite H.
apply (Seq_refl _ _ SetoidS2).
Qed.
Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
intros.
setoid_replace x with y.
apply (Seq_refl _ _ SetoidS2).
assumption.
Qed.
Axiom g : S1 -> S2 -> nat.
Add Morphism g : g_compat. Admitted.
Axiom P : nat -> Prop.
Theorem test2:
forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (P (g x' y')) -> (P (g x y)).
intros.
rewrite H.
rewrite H0.
assumption.
Qed.
Theorem test3:
forall x x' y y',
(eqS1 x x') -> (eqS2 y y') -> (P (S (g x' y'))) -> (P (S (g x y))).
intros.
rewrite H.
rewrite H0.
assumption.
Qed.
Theorem test4:
forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (S (g x y)) = (S (g x' y')).
intros.
rewrite H.
rewrite H0.
reflexivity.
Qed.
Theorem test5:
forall x x' y y', (eqS1 x x') -> (eqS2 y y') -> (S (g x y)) = (S (g x' y')).
intros.
setoid_replace (g x y) with (g x' y').
reflexivity.
rewrite <- H0.
rewrite H.
reflexivity.
Qed.
Axiom f_test6 : S2 -> Prop.
Add Morphism f_test6 : f_test6_compat. Admitted.
Axiom g_test6 : bool -> S2.
Add Morphism g_test6 : g_test6_compat. Admitted.
Axiom h_test6 : S1 -> bool.
Add Morphism h_test6 : h_test6_compat. Admitted.
Theorem test6:
forall E1 E2, (eqS1 E1 E2) -> (f_test6 (g_test6 (h_test6 E2))) ->
(f_test6 (g_test6 (h_test6 E1))).
intros.
rewrite H.
assumption.
Qed.
Theorem test7:
forall E1 E2 y y', (eqS1 E1 E2) -> (eqS2 y y') ->
(f_test6 (g_test6 (h_test6 E2))) ->
(f_test6 (g_test6 (h_test6 E1))) /\ (S (g E1 y')) = (S (g E2 y')).
intros.
rewrite H.
split; [assumption | reflexivity].
Qed.
Axiom S1_test8: Set.
Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
Add Setoid S1_test8 eqS1_test8 SetoidS1_test8.
Axiom f_test8 : S2 -> S1_test8.
Add Morphism f_test8 : f_compat_test8. Admitted.
Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'.
Add Setoid S1_test8 eqS1_test8' SetoidS1_test8'.
(*CSC: for test8 to be significant I want to choose the setoid
(S1_test8, eqS1_test8'). However this does not happen and
there is still no syntax for it ;-( *)
Axiom g_test8 : S1_test8 -> S2.
Add Morphism g_test8 : g_compat_test8. Admitted.
Theorem test8:
forall x x': S2, (eqS2 x x') ->
(eqS2 (g_test8 (f_test8 x)) (g_test8 (f_test8 x'))).
intros.
rewrite H.
Abort.
(*Print Setoids.*)
|
