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
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
|
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
+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. goal con impl
+12. testare *veramente* setoid_replace (ora testato solamente il caso
di fallback su replace)
Incompatibilita':
1. full_trivial in setoid_replace
2. "as ..." per "Add Setoid"
3. ipotesi permutate in lemma di "Add Morphism"
4. iff invece di if in "Add Morphism" nel caso di predicati
5. setoid_replace poteva riscrivere sia c1 in c2 che c2 in c1
(???? o poteva farlo da destra a sinitra o viceversa? ????)
### 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)
### Nota: il parsing e pretty printing delle relazioni non e' in synch!
eq contro (ty,eq). Uniformare
### diminuire la taglia dei proof term
??? il messaggio di errore non e' assolutamente significativo quando
nessuna marcatura viene trovata
### fare in modo che uscendo da una sezione vengano quantificate le
relazioni e i morfismi. Hugo: paciugare nel discharge.ml
### implementare relazioni/morfismi quantificati con dei LetIn (che palle...)
decompose_prod da far diventare simile a un Reduction.dest_arity?
(ma senza riduzione??? e perche' li' c'e' riduzione?)
Soluzione da struzzo: fare zeta-conversione.
### fare in modo che impl sia espanso nel lemma di compatibilita' del
morfismo (richiesta di Marco per poter fare Add Hing)
??? snellire la sintassi omettendo "proved by" come proposto da Marco? ;-(
### non capisce piu' le riscritture con uguaglianze quantificate (almeno
nell'esempio di Marco)
### Bas Spitters: poter dichiarare che ogni variabile nel contesto di tipo
un setoid_function e' un morfismo
### unificare le varie check_...
### sostituire a Use_* una sola eccezione Optimize
Implementare:
-2. user-defined subrelations && user-proved subrelations
-1. trucco di Bruno
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 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.
Stessa cosa per la setoid_rewrite.
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. [setoid_]rewrite ... in ...
setoid_replace ... in ...
[setoid_]reflexivity
[setoid_]transitivity ...
[setoid_]symmetry
[setoid_]symmetry in ...
11. permette di dichiarare dei setoidi/relazioni/morfismi in un module
type
12. relazioni, morfismi e setoidi quantificati
*)
Axiom S1: Set.
Axiom eqS1: S1 -> S1 -> Prop.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1 as S1setoid.
Instance eqS1_default : DefaultRelation eqS1.
Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'.
Add Setoid S1 eqS1' SetoidS1' as S1setoid'.
Add Setoid S1 eqS1' SetoidS1'_bis as S1setoid''.
Axiom S2: Set.
Axiom eqS2: S2 -> S2 -> Prop.
Axiom SetoidS2 : Setoid_Theory S2 eqS2.
Add Setoid S2 eqS2 SetoidS2 as S2setoid.
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.
reflexivity.
Qed.
Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
intros.
setoid_replace x with y.
reflexivity.
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 as S1_test8setoid.
Instance eqS1_test8_default : DefaultRelation eqS1_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' as S1_test8setoid'.
(*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.*)
|
