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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
|
;; default abbrev table
; This is for coq V8, you should test coq version before loading
;#s are replaced by holes by holes-abbrev-complete
(if (boundp 'holes-abbrev-complete)
()
(define-abbrev-table 'coq-mode-abbrev-table
'(
("a" "auto" holes-abbrev-complete 4)
("ar" "autorewrite with @{db,db...} using @{tac}" holes-abbrev-complete 1)
("ab" "absurd " holes-abbrev-complete 0)
("abs" "absurd " holes-abbrev-complete 0)
("ap" "apply " holes-abbrev-complete 16)
("as" "assumption" holes-abbrev-complete 4)
("ass" "assert ( # : # )" holes-abbrev-complete 4)
("au" "auto" holes-abbrev-complete 1)
("aw" "auto with " holes-abbrev-complete 1)
("awa" "auto with arith" holes-abbrev-complete 4)
("c" "cases " holes-abbrev-complete 1)
("ch" "change " holes-abbrev-complete 1)
("chi" "change # in #" holes-abbrev-complete 1)
("chwi" "change # with # in #" holes-abbrev-complete 1)
("con" "constructor" holes-abbrev-complete 3)
("cong" "congruence" holes-abbrev-complete 3)
("dec" "decompose [#] @{hyp}" holes-abbrev-complete 3)
("def" "Definition #:# := #." holes-abbrev-complete 5)
("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5)
("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
("deg" "decide equality" holes-abbrev-complete 3)
("des" "destruct " holes-abbrev-complete 0)
("desu" "destruct # using #" holes-abbrev-complete 0)
("desa" "destruct # as #" holes-abbrev-complete 0)
("dis" "discriminate" holes-abbrev-complete 0)
("dm" "Declare Module # : # := #." holes-abbrev-complete 0)
("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0)
("dmi" "Declare Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
("dmi2" "Declare Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
("e" "elim #" holes-abbrev-complete 1)
("ea" "eauto" holes-abbrev-complete 0)
("eap" "eapply #" holes-abbrev-complete 0)
("eaw" "eauto with @{db}" holes-abbrev-complete 0)
("eawa" "eauto with arith" holes-abbrev-complete 0)
("el" "elim #" holes-abbrev-complete 0)
("elu" "elim # using #" holes-abbrev-complete 0)
("ex" "exists #" holes-abbrev-complete 0)
("f" "fun # => #" holes-abbrev-complete 0)
("f1" "fun #:# => #" holes-abbrev-complete 0)
("f2" "fun (#:#) (#:#) => #" holes-abbrev-complete 0)
("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
("fi" "functional induction @{f} @{args}" holes-abbrev-complete 0)
("fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." holes-abbrev-complete 3)
("fo" "forall #,#" holes-abbrev-complete 0)
("fo1" "forall #:#,#" holes-abbrev-complete 0)
("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0)
("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
("fs" "Functional Scheme @{name} := Induction for @{fun}." holes-abbrev-complete 0)
("fsto" "firstorder" holes-abbrev-complete 0)
("fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." holes-abbrev-complete 0)
("g" "generalize #" holes-abbrev-complete 0)
("ge" "generalize #" holes-abbrev-complete 0)
("gen" "generalize #" holes-abbrev-complete 0)
("hc" "Hint Constructors # : #." holes-abbrev-complete 0)
("he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." holes-abbrev-complete 0)
("hi" "Hint Immediate # : @{db}." holes-abbrev-complete 0)
("hr" "Hint Resolve # : @{db}." holes-abbrev-complete 0)
("hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." holes-abbrev-complete 0)
("hs" "Hints # : #." holes-abbrev-complete 0)
("hu" "Hint Unfold # : #." holes-abbrev-complete 0)
("i" "intro " holes-abbrev-complete 10)
("if" "if # then # else #" holes-abbrev-complete 1)
("in" "intro" holes-abbrev-complete 1)
("inf" "infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1)
("ind" "induction #" holes-abbrev-complete 2)
("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
("indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
("indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
("indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
("inj" "injection #" holes-abbrev-complete 2)
("inv" "inversion #" holes-abbrev-complete 9)
("intu" "intuition #" holes-abbrev-complete 9)
("is" "intros #" holes-abbrev-complete 11)
("ite" "if # then # else #" holes-abbrev-complete 1)
("l" "Lemma # : #." holes-abbrev-complete 4)
("li" "let # := # in #" holes-abbrev-complete 1)
("m" "match # with\n| # => #\nend" holes-abbrev-complete 1)
("m2" "match # with\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
("m3" "match # with\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
("m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
("m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
("mt" "Module Type # := #." holes-abbrev-complete 0)
("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0)
("mo" "Module # : # := #." holes-abbrev-complete 0)
("mo2" "Module # <: # := #." holes-abbrev-complete 0)
("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
("nota" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0)
("notas" "Notation \"#\" := # (at level #, # associativity)." holes-abbrev-complete 0)
("notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." holes-abbrev-complete 0)
("notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." holes-abbrev-complete 0)
("o" "omega" holes-abbrev-complete 0)
("om" "omega" holes-abbrev-complete 0)
("p" "Print #" holes-abbrev-complete 3)
("po" "pose ( # := # )" nil 0)
("pr" "print #" holes-abbrev-complete 2)
("rep" "replace # with #" holes-abbrev-complete 19)
("r" "rewrite #" holes-abbrev-complete 19)
("r<" "rewrite <- #" holes-abbrev-complete 0)
("rl" "rewrite <- #" holes-abbrev-complete 0)
("refl" "reflexivity #" holes-abbrev-complete 0)
("ri" "rewrite # in #" holes-abbrev-complete 19)
("ril" "rewrite <- # in #" holes-abbrev-complete 0)
("ri<" "rewrite <- # in #" holes-abbrev-complete 0)
("re" "rewrite #" holes-abbrev-complete 0)
("re<" "rewrite <- #" holes-abbrev-complete 0)
("ring" "ring #" holes-abbrev-complete 19)
("s" "simpl" holes-abbrev-complete 23)
("set" "set ( # := #)" holes-abbrev-complete 23)
("seth" "set ( # := #) in * |-" holes-abbrev-complete 23)
("setg" "set ( # := #) in |-*" holes-abbrev-complete 23)
("seti" "set ( # := #) in #" holes-abbrev-complete 23)
("su" "subst #" holes-abbrev-complete 23)
("sc" "Scheme @{name} := Induction for # Sort #." nil 0)
("si" "simpl" holes-abbrev-complete 0)
("sp" "Split" holes-abbrev-complete 1)
("sy" "symmetry" holes-abbrev-complete 0)
("sym" "symmetry" holes-abbrev-complete 0)
("t" "trivial" holes-abbrev-complete 1)
("tr" "trivial" holes-abbrev-complete 1)
("trans" "transitivity #" holes-abbrev-complete 1)
("ta" "tauto" holes-abbrev-complete 1)
("u" "unfold #" holes-abbrev-complete 1)
("un" "unfold #" holes-abbrev-complete 7)
("v" "Variable # : #." holes-abbrev-complete 7)
("vs" "Variables # : #." holes-abbrev-complete 7)
)
)
)
;TODO: build the command submenu automatically from abbrev table
(defpgdefault menu-entries
'(
("Insert Command"
"COMMAND ABBREVIATION"
["Definition def<C-BS>" (insert-and-expand "def") t]
["Fixpoint fix<C-BS>" (insert-and-expand "fix") t]
["Lemma l<C-BS>" (insert-and-expand "l") t]
""
["Inductive indv<C-BS>" (insert-and-expand "indv") t]
["Inductive1 indv1<C-BS>" (insert-and-expand "indv1") t]
["Inductive2 indv2<C-BS>" (insert-and-expand "indv2") t]
["Inductive3 indv3<C-BS>" (insert-and-expand "indv3") t]
["Inductive4 indv4<C-BS>" (insert-and-expand "indv4") t]
""
["Section..." coq-insert-section t]
""
("Modules"
"COMMAND ABBREVIATION"
["Module (interactive)... " coq-insert-module t]
["Module mo<C-BS>" (insert-and-expand "mo") t]
["Module (<:) mo2<C-BS>" (insert-and-expand "mo") t]
; ["Module (interactive) moi<C-BS>" (insert-and-expand "moi") t]
; ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
["Module Type mt<C-BS>" (insert-and-expand "mt") t]
; ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
; ""
["Declare Module dm<C-BS>" (insert-and-expand "dm") t]
["Declare Module (<:) dm2<C-BS>" (insert-and-expand "dm") t]
; ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
; ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
)
("Hints"
"COMMAND ABBREVIATION"
["Hint Constructors hc<C-BS>" (insert-and-expand "hc") t]
["Hint Immediate hi<C-BS>" (insert-and-expand "hi") t]
["Hint Resolve hr<C-BS>" (insert-and-expand "hr") t]
["Hint Rewrite hrw<C-BS>" (insert-and-expand "hrw") t]
["Hint Extern he<C-BS>" (insert-and-expand "he") t]
)
("Schemes"
"COMMAND ABBREVIATION"
["Scheme sc<C-BS>" (insert-and-expand "sc") t]
["Functional Scheme fs<C-BS>" (insert-and-expand "fs") t]
["Functional Scheme with fsw<C-BS>" (insert-and-expand "fsw") t]
)
("Notations"
"COMMAND ABBREVIATION"
["infix inf<C-BS>" (insert-and-expand "inf") t]
["Notation (no assoc) nota<C-BS>" (insert-and-expand "nota") t]
["Notation (assoc) notas<C-BS>" (insert-and-expand "notas") t]
["Notation (no assoc, scope) notasc<C-BS>" (insert-and-expand "notasc") t]
["Notation (assoc, scope) notassc<C-BS>" (insert-and-expand "notassc") t]
)
)
("Insert term"
"FORM ABBREVIATION"
["forall fo<C-BS>" (insert-and-expand "fo") t]
["forall1 fo1<C-BS>" (insert-and-expand "fo1") t]
["forall2 fo2<C-BS>" (insert-and-expand "fo2") t]
["forall3 fo3<C-BS>" (insert-and-expand "fo3") t]
["forall4 fo4<C-BS>" (insert-and-expand "fo4") t]
""
["fun f<ctrl-bacspace>" (insert-and-expand "f") t]
["fun1 f1<ctrl-bacspace>" (insert-and-expand "f1") t]
["fun2 f2<C-BS>" (insert-and-expand "f2") t]
["fun3 f3<C-BS>" (insert-and-expand "f3") t]
["fun4 f4<C-BS>" (insert-and-expand "f4") t]
""
["if then else if<C-BS>" (insert-and-expand "li") t]
["let in li<C-BS>" (insert-and-expand "li") t]
""
["match m<C-BS>" (insert-and-expand "m") t]
["match2 m2<C-BS>" (insert-and-expand "m2") t]
["match3 m3<C-BS>" (insert-and-expand "m3") t]
["match4 m4<C-BS>" (insert-and-expand "m4") t]
)
("Insert tactic (a-f)"
"TACTIC ABBREVIATION"
["absurd abs<C-BS>" (insert-and-expand "abs") t]
["assumption as<C-BS>" (insert-and-expand "as") t]
["assert ass<C-BS>" (insert-and-expand "ass") t]
["auto a<C-BS>" (insert-and-expand "a") t]
["auto with aw<C-BS>" (insert-and-expand "aw") t]
["auto with arith awa<C-BS>" (insert-and-expand "awa") t]
["autorewrite ar<C-BS>" (insert-and-expand "ar") t]
["cases c<C-BS>" (insert-and-expand "c") t]
["change ch<C-BS>" (insert-and-expand "ch") t]
["change in chi<C-BS>" (insert-and-expand "chi") t]
["change with in chwi<C-BS>" (insert-and-expand "chwi") t]
["constructor con<C-BS>" (insert-and-expand "con") t]
["congruence cong<C-BS>" (insert-and-expand "cong") t]
["decompose dec<C-BS>" (insert-and-expand "dec") t]
["decide equality deg<C-BS>" (insert-and-expand "deg") t]
["destruct des<C-BS>" (insert-and-expand "des") t]
["destruct using desu<C-BS>" (insert-and-expand "desu") t]
["destruct as desa<C-BS>" (insert-and-expand "desa") t]
["discriminate dis<C-BS>" (insert-and-expand "dis") t]
["eauto ea<C-BS>" (insert-and-expand "ea") t]
["eauto with eaw<C-BS>" (insert-and-expand "dec") t]
["elim e<C-BS>" (insert-and-expand "e") t]
["elim using elu<C-BS>" (insert-and-expand "elu") t]
["exists ex<C-BS>" (insert-and-expand "ex") t]
["field fld<C-BS>" (insert-and-expand "fld") t]
["firstorder fsto<C-BS>" (insert-and-expand "fsto") t]
["fourier fou<C-BS>" (insert-and-expand "fou") t]
["functional induction fi<C-BS>" (insert-and-expand "fi") t]
)
("Insert tactic (g-z)"
"TACTIC ABBREVIATION"
["generalize g<C-BS>" (insert-and-expand "g") t]
["induction ind<C-BS>" (insert-and-expand "ind") t]
["injection inj<C-BS>" (insert-and-expand "inj") t]
["intro i<C-BS>" (insert-and-expand "i") t]
["intros is<C-BS>" (insert-and-expand "is") t]
["intuition intu<C-BS>" (insert-and-expand "intu") t]
["inversion inv<C-BS>" (insert-and-expand "inv") t]
["omega om<C-BS>" (insert-and-expand "om") t]
["pose po<C-BS>" (insert-and-expand "om") t]
["reflexivity refl<C-BS>" (insert-and-expand "refl") t]
["replace rep<C-BS>" (insert-and-expand "rep") t]
["rewrite r<C-BS>" (insert-and-expand "r") t]
["rewrite in ri<C-BS>" (insert-and-expand "ri") t]
["rewrite <- r<<C-BS>" (insert-and-expand "rl") t]
["rewrite <- in ri<<C-BS>" (insert-and-expand "ril") t]
["set set<C-BS>" (insert-and-expand "set") t]
["set in hyp seth<C-BS>" (insert-and-expand "seth") t]
["set in goal setg<C-BS>" (insert-and-expand "setg") t]
["set in seti<C-BS>" (insert-and-expand "seti") t]
["simpl s<C-BS>" (insert-and-expand "s") t]
["simpl si<C-BS>" (insert-and-expand "si") t]
["split sp<C-BS>" (insert-and-expand "sp") t]
["subst su<C-BS>" (insert-and-expand "su") t]
["symmetry sym<C-BS>" (insert-and-expand "sym") t]
["transitivity trans<C-BS>" (insert-and-expand "trans") t]
["trivial t<C-BS>" (insert-and-expand "t") t]
["tauto ta<C-BS>" (insert-and-expand "ta") t]
["unfold u<C-BS>" (insert-and-expand "u") t]
)
["What are those highlighted chars??" (holes-short-doc) t]
("holes"
"make a hole active click on it"
"disable a hole click on it (button 2)"
"destroy a hole click on it (button 3)"
"make a hole with mouse C-M-select"
["make a hole at point C-M-h" (set-make-active-hole) t]
["make selection a hole C-M-h" (set-make-active-hole) t]
["replace active hole by selection C-M-y" (replace-update-active-hole) t]
"replace active hole with mouse C-M-Shift select"
["jump to active hole M-return" (set-point-next-hole-destroy) t]
["forget all holes in this buffer" (clear-all-buffer-holes) t]
["What are those holes?" (holes-short-doc) t]
)
["expand abbrev at point" expand-abbrev t]
["list abbrevs" list-abbrevs t]
["Print..." coq-Print t]
["Check..." coq-Check t]
["Hints" coq-PrintHint t]
["Show ith goal..." coq-Show t]
["Search isos/pattern..." coq-SearchIsos t]
["3 buffers view" coq-three-b t]
["Compile" coq-Compile t] ))
(provide 'coq-abbrev)
|
