Skip to content

Commit 32bb531

Browse files
garesgares
committed
[elpi] minimalistic integration
1 parent 0c56e85 commit 32bb531

File tree

120 files changed

+309129
-39
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

120 files changed

+309129
-39
lines changed

‎dune-workspace‎

Whitespace-only changes.

‎lambdap.elpi‎

Lines changed: 1298 additions & 0 deletions
Large diffs are not rendered by default.

‎lambdapi.opam‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ depends: [
6262
"cmdliner" {>= "1.1.0"}
6363
"stdlib-shims" {>= "0.1.0"}
6464
"odoc" {with-doc}
65-
"elpi" { >= "1.16.0" & < "1.17.0" }
65+
"elpi" { >= "1.16.6" & < "1.17.0" }
6666
]
6767
build: [
6868
["dune" "subst"] {dev}

‎out/Coq__Arith__Arith__base.dk‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(; This file was automatically generated by Coqine. ;)
2+
(; The encoding used was: "template_cic". ;)
3+
4+
(; End of translation. ;)

‎out/Coq__Arith__Between.dk‎

Lines changed: 2513 additions & 0 deletions
Large diffs are not rendered by default.

‎out/Coq__Arith__Compare__dec.dk‎

Lines changed: 5066 additions & 0 deletions
Large diffs are not rendered by default.

‎out/Coq__Arith__EqNat.dk‎

Lines changed: 2688 additions & 0 deletions
Large diffs are not rendered by default.

‎out/Coq__Arith__Factorial.dk‎

Lines changed: 342 additions & 0 deletions
Large diffs are not rendered by default.

‎out/Coq__Arith__Gt.dk‎

Lines changed: 1422 additions & 0 deletions
Large diffs are not rendered by default.

‎out/Coq__Arith__Le.dk‎

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
(; This file was automatically generated by Coqine. ;)
2+
(; The encoding used was: "template_cic". ;)
3+
4+
def let__H0 :
5+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
6+
H :
7+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n Coq__Init__Datatypes.O) ->
8+
n0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
9+
__ :
10+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n0 Coq__Init__Datatypes.O) ->
11+
cupicef.Term cupicef.prop
12+
(Coq__Init__Logic.eq
13+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
14+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
15+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
16+
cupicef.I)
17+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
18+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
19+
cupicef.I)
20+
cupicef.I Coq__Init__Datatypes.nat)
21+
n0 Coq__Init__Datatypes.O)
22+
23+
:= n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
24+
H :
25+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n Coq__Init__Datatypes.O) =>
26+
n0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
27+
Coq__Init__Logic.match____and cupicef.prop
28+
(cupicef.prod cupicef.prop cupicef.prop
29+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
30+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O)
31+
(__ :
32+
cupicef.Term cupicef.prop
33+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O) =>
34+
Coq__Init__Logic.eq
35+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
36+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
37+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
38+
cupicef.I)
39+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
40+
(cupicef.axiom
41+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
42+
cupicef.I)
43+
cupicef.I Coq__Init__Datatypes.nat)
44+
n0 Coq__Init__Datatypes.O))
45+
(cupicef.prod cupicef.prop cupicef.prop
46+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
47+
(Coq__Init__Logic.eq
48+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
49+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
50+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
51+
cupicef.I)
52+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
53+
(cupicef.axiom
54+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
55+
cupicef.I)
56+
cupicef.I Coq__Init__Datatypes.nat)
57+
n0 Coq__Init__Datatypes.O)
58+
(__ :
59+
cupicef.Term cupicef.prop
60+
(Coq__Init__Logic.eq
61+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
62+
(cupicef.axiom
63+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
64+
(cupicef.univ cupicef.set
65+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
66+
(cupicef.univ
67+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
68+
(cupicef.axiom
69+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
70+
cupicef.I)
71+
cupicef.I Coq__Init__Datatypes.nat)
72+
n0 Coq__Init__Datatypes.O) =>
73+
Coq__Init__Peano.le n0 Coq__Init__Datatypes.O))
74+
(__ :
75+
cupicef.Term cupicef.prop
76+
(Coq__Init__Logic.and
77+
(cupicef.prod cupicef.prop cupicef.prop
78+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
79+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O)
80+
(__ :
81+
cupicef.Term cupicef.prop
82+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O) =>
83+
Coq__Init__Logic.eq
84+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
85+
(cupicef.axiom
86+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
87+
(cupicef.univ cupicef.set
88+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
89+
(cupicef.univ
90+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
91+
(cupicef.axiom
92+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
93+
cupicef.I)
94+
cupicef.I Coq__Init__Datatypes.nat)
95+
n0 Coq__Init__Datatypes.O))
96+
(cupicef.prod cupicef.prop cupicef.prop
97+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
98+
(Coq__Init__Logic.eq
99+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
100+
(cupicef.axiom
101+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
102+
(cupicef.univ cupicef.set
103+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
104+
(cupicef.univ
105+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
106+
(cupicef.axiom
107+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
108+
cupicef.I)
109+
cupicef.I Coq__Init__Datatypes.nat)
110+
n0 Coq__Init__Datatypes.O)
111+
(__ :
112+
cupicef.Term cupicef.prop
113+
(Coq__Init__Logic.eq
114+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
115+
(cupicef.axiom
116+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
117+
(cupicef.univ cupicef.set
118+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
119+
(cupicef.univ
120+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
121+
(cupicef.axiom
122+
(cupicef.type
123+
(cupicef.s (cupicef.s cupicef.z))))
124+
cupicef.I)
125+
cupicef.I Coq__Init__Datatypes.nat)
126+
n0 Coq__Init__Datatypes.O) =>
127+
Coq__Init__Peano.le n0 Coq__Init__Datatypes.O))) =>
128+
cupicef.prod cupicef.prop cupicef.prop
129+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
130+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O)
131+
(__0 :
132+
cupicef.Term cupicef.prop
133+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O) =>
134+
Coq__Init__Logic.eq
135+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
136+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
137+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
138+
cupicef.I)
139+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
140+
(cupicef.axiom
141+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
142+
cupicef.I)
143+
cupicef.I Coq__Init__Datatypes.nat)
144+
n0 Coq__Init__Datatypes.O))
145+
(__ :
146+
(__ :
147+
cupicef.Term cupicef.prop
148+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O) ->
149+
cupicef.Term cupicef.prop
150+
(Coq__Init__Logic.eq
151+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
152+
(cupicef.axiom
153+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
154+
(cupicef.univ cupicef.set
155+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
156+
(cupicef.univ
157+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
158+
(cupicef.axiom
159+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
160+
cupicef.I)
161+
cupicef.I Coq__Init__Datatypes.nat)
162+
n0 Coq__Init__Datatypes.O)) =>
163+
__0 :
164+
(__0 :
165+
cupicef.Term cupicef.prop
166+
(Coq__Init__Logic.eq
167+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
168+
(cupicef.axiom
169+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
170+
(cupicef.univ cupicef.set
171+
(cupicef.type (cupicef.s cupicef.z)) cupicef.I)
172+
(cupicef.univ
173+
(cupicef.type (cupicef.s (cupicef.s cupicef.z)))
174+
(cupicef.axiom
175+
(cupicef.type (cupicef.s (cupicef.s cupicef.z))))
176+
cupicef.I)
177+
cupicef.I Coq__Init__Datatypes.nat)
178+
n0 Coq__Init__Datatypes.O) ->
179+
cupicef.Term cupicef.prop
180+
(Coq__Init__Peano.le n0 Coq__Init__Datatypes.O)) =>
181+
__)
182+
(Coq__Arith__PeanoNat.Nat__le__0__r n0).
183+
184+
thm le__n__0__eq :
185+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
186+
__ :
187+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n Coq__Init__Datatypes.O) ->
188+
cupicef.Term cupicef.prop
189+
(Coq__Init__Logic.eq
190+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
191+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
192+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
193+
cupicef.I)
194+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
195+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
196+
cupicef.I)
197+
cupicef.I Coq__Init__Datatypes.nat)
198+
Coq__Init__Datatypes.O n)
199+
200+
:= n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
201+
H :
202+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n Coq__Init__Datatypes.O) =>
203+
Coq__Init__Logic.eq__sym
204+
(cupicef.cast (cupicef.type (cupicef.s cupicef.z))
205+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
206+
(cupicef.univ cupicef.set (cupicef.type (cupicef.s cupicef.z))
207+
cupicef.I)
208+
(cupicef.univ (cupicef.type (cupicef.s (cupicef.s cupicef.z)))
209+
(cupicef.axiom (cupicef.type (cupicef.s (cupicef.s cupicef.z))))
210+
cupicef.I)
211+
cupicef.I Coq__Init__Datatypes.nat)
212+
n Coq__Init__Datatypes.O (let__H0 n H n H).
213+
214+
thm le__n__S :
215+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
216+
m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
217+
__ : cupicef.Term cupicef.prop (Coq__Init__Peano.le n m) ->
218+
cupicef.Term cupicef.prop
219+
(Coq__Init__Peano.le (Coq__Init__Datatypes.S n)
220+
(Coq__Init__Datatypes.S m))
221+
222+
:= Coq__Init__Peano.le__n__S.
223+
224+
thm le__S__n :
225+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
226+
m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
227+
__ :
228+
cupicef.Term cupicef.prop
229+
(Coq__Init__Peano.le (Coq__Init__Datatypes.S n)
230+
(Coq__Init__Datatypes.S m)) ->
231+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n m)
232+
233+
:= Coq__Init__Peano.le__S__n.
234+
235+
thm le__Sn__le :
236+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
237+
m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
238+
__ :
239+
cupicef.Term cupicef.prop
240+
(Coq__Init__Peano.le (Coq__Init__Datatypes.S n) m) ->
241+
cupicef.Term cupicef.prop (Coq__Init__Peano.le n m)
242+
243+
:= Coq__Arith__PeanoNat.Nat__lt__le__incl.
244+
245+
thm le__elim__rel :
246+
P :
247+
(__ : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
248+
__0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
249+
cupicef.Univ cupicef.prop) ->
250+
__ :
251+
(p : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
252+
cupicef.Term cupicef.prop (P Coq__Init__Datatypes.O p)) ->
253+
__0 :
254+
(p : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
255+
q : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
256+
__0 : cupicef.Term cupicef.prop (Coq__Init__Peano.le p q) ->
257+
__1 : cupicef.Term cupicef.prop (P p q) ->
258+
cupicef.Term cupicef.prop
259+
(P (Coq__Init__Datatypes.S p) (Coq__Init__Datatypes.S q))) ->
260+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
261+
m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
262+
__1 : cupicef.Term cupicef.prop (Coq__Init__Peano.le n m) ->
263+
cupicef.Term cupicef.prop (P n m)
264+
265+
:= P :
266+
(__ : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
267+
__0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
268+
cupicef.Univ cupicef.prop) =>
269+
H0 :
270+
(p : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
271+
cupicef.Term cupicef.prop (P Coq__Init__Datatypes.O p)) =>
272+
HS :
273+
(p : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
274+
q : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
275+
__ : cupicef.Term cupicef.prop (Coq__Init__Peano.le p q) ->
276+
__0 : cupicef.Term cupicef.prop (P p q) ->
277+
cupicef.Term cupicef.prop
278+
(P (Coq__Init__Datatypes.S p) (Coq__Init__Datatypes.S q))) =>
279+
n : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
280+
Coq__Init__Datatypes.nat__ind
281+
(n0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
282+
cupicef.prod cupicef.set (cupicef.rule cupicef.prop cupicef.prop)
283+
(cupicef.rule cupicef.set (cupicef.rule cupicef.prop cupicef.prop))
284+
cupicef.I Coq__Init__Datatypes.nat
285+
(m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
286+
cupicef.prod cupicef.prop cupicef.prop
287+
(cupicef.rule cupicef.prop cupicef.prop) cupicef.I
288+
(Coq__Init__Peano.le n0 m)
289+
(__ : cupicef.Term cupicef.prop (Coq__Init__Peano.le n0 m) =>
290+
P n0 m)))
291+
(m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
292+
H :
293+
cupicef.Term cupicef.prop
294+
(Coq__Init__Peano.le Coq__Init__Datatypes.O m) =>
295+
H0 m)
296+
(n0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
297+
IHn :
298+
(m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat ->
299+
__ : cupicef.Term cupicef.prop (Coq__Init__Peano.le n0 m) ->
300+
cupicef.Term cupicef.prop (P n0 m)) =>
301+
m : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
302+
Le :
303+
cupicef.Term cupicef.prop
304+
(Coq__Init__Peano.le (Coq__Init__Datatypes.S n0) m) =>
305+
Coq__Init__Peano.le__ind (Coq__Init__Datatypes.S n0)
306+
(m0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
307+
P (Coq__Init__Datatypes.S n0) m0)
308+
(HS n0 n0 (Coq__Init__Peano.le__n n0)
309+
(IHn n0 (Coq__Init__Peano.le__n n0)))
310+
(m0 : cupicef.Term cupicef.set Coq__Init__Datatypes.nat =>
311+
H :
312+
cupicef.Term cupicef.prop
313+
(Coq__Init__Peano.le (Coq__Init__Datatypes.S n0) m0) =>
314+
H1 : cupicef.Term cupicef.prop (P (Coq__Init__Datatypes.S n0) m0) =>
315+
HS n0 m0 (le__Sn__le n0 m0 H) (IHn m0 (le__Sn__le n0 m0 H)))
316+
m Le)
317+
n.
318+
319+
(; End of translation. ;)

0 commit comments

Comments
 (0)