Skip to content

Commit df9d13d

Browse files
konrad-slindkonrad-slind
committed
initial HOL--> ACL2 implementation
1 parent ec2580f commit df9d13d

File tree

7 files changed

+1036
-0
lines changed

7 files changed

+1036
-0
lines changed

‎examples/acl2/hol-to-acl2/examples/Holmakefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
INCLUDES = $(HOLDIR)/examples/acl2/hol-to-acl2/src

‎examples/acl2/hol-to-acl2/examples/eval-poly.sml‎

Lines changed: 328 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,328 @@
1+
(*---------------------------------------------------------------------------*)
2+
(* Simple polynomial evaluator example *)
3+
(*---------------------------------------------------------------------------*)
4+
5+
use "translator.sml";
6+
7+
open bossLib arithmeticTheory pairTheory combinTheory optionTheory listTheory;
8+
9+
Definition polyp_def:
10+
polyp [] = T /\
11+
polyp ((c,e)::r) =
12+
(polyp r /\ c <> 0 /\ 0 <= e /\
13+
(NULL r \/ SND(HD r) < e))
14+
End
15+
16+
Definition eval_poly_def:
17+
eval_poly [] v = 0 ∧
18+
eval_poly ((c,e)::r) v = c * (v ** e) + eval_poly r v
19+
End
20+
21+
Definition sum_polys_def:
22+
sum_polys [] [] = [] ∧
23+
sum_polys [] p = p ∧
24+
sum_polys p [] = p ∧
25+
sum_polys ((c1,e1)::r1) ((c2,e2)::r2) =
26+
if e1 = e2 then
27+
(c1+c2,e1) :: sum_polys r1 r2 else
28+
if e1 < e2 then
29+
(c2,e2)::sum_polys ((c1,e1)::r1) r2
30+
else
31+
(c1,e1)::sum_polys r1 ((c2,e2)::r2)
32+
End
33+
34+
Theorem cond_thm:
35+
(!x y:'a. (if T then x else y) = x) /\
36+
(!x y:'a. (if F then x else y) = y)
37+
Proof
38+
rw[]
39+
QED
40+
41+
Definition COMMA_def:
42+
COMMA x y = (x,y)
43+
End
44+
45+
Theorem null_thm:
46+
(NULL ([]:'a list) = T) /\ (!h t. NULL(h::t : 'a list) = F)
47+
Proof
48+
rw[]
49+
QED
50+
51+
Theorem suc_thm:
52+
∀m. SUC m = 1 + m
53+
Proof
54+
decide_tac
55+
QED
56+
57+
Theorem leq_thm:
58+
!x y. x <= y <=> x < y \/ x = y
59+
Proof
60+
rw[]
61+
QED
62+
63+
val basis_defs =
64+
[cond_thm, COMMA_def, HD, null_thm, suc_thm, leq_thm, FST, SND,
65+
EXP, polyp_def, eval_poly_def, sum_polys_def];
66+
67+
val goals =
68+
[mk_named_goal "eval_sum_poly_distrib"
69+
``∀x y v.
70+
polyp x ∧ polyp y ⇒
71+
eval_poly (sum_polys x y) v
72+
=
73+
eval_poly x v + eval_poly y v``];
74+
75+
val sexps = map hol_sexp (basis_defs @ goals);
76+
77+
(*
78+
val basis_defs =
79+
[⊢ (∀x y. (if T then x else y) = x) ∧ ∀x y. (if F then x else y) = y,
80+
⊢ ∀x y. COMMA x y = (x,y),
81+
⊢ ∀h t. HD (h::t) = h,
82+
⊢ (NULL [] ⇔ T) ∧ ∀h t. NULL (h::t) ⇔ F,
83+
⊢ ∀m. SUC m = 1 + m,
84+
⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y,
85+
⊢ ∀x y. FST (x,y) = x,
86+
⊢ ∀x y. SND (x,y) = y,
87+
⊢ (∀m. m ** 0 = 1) ∧ ∀m n. m ** SUC n = m * m ** n,
88+
⊢ (polyp [] ⇔ T) ∧
89+
∀r e c.
90+
polyp ((c,e)::r) ⇔
91+
polyp r ∧ c ≠ 0 ∧ 0 ≤ e ∧ (NULL r ∨ SND (HD r) < e),
92+
⊢ (∀v. eval_poly [] v = 0) ∧
93+
∀v r e c. eval_poly ((c,e)::r) v = c * v ** e + eval_poly r v,
94+
⊢ sum_polys [] [] = [] ∧ (∀v7 v6. sum_polys [] (v6::v7) = v6::v7) ∧
95+
(∀v3 v2. sum_polys (v2::v3) [] = v2::v3) ∧
96+
∀r2 r1 e2 e1 c2 c1.
97+
sum_polys ((c1,e1)::r1) ((c2,e2)::r2) =
98+
if e1 = e2 then (c1 + c2,e1)::sum_polys r1 r2
99+
else if e1 < e2 then (c2,e2)::sum_polys ((c1,e1)::r1) r2
100+
else (c1,e1)::sum_polys r1 ((c2,e2)::r2)]: thm list
101+
102+
val sexps =
103+
[("COND",
104+
(defhol
105+
:fns ((cond (:arrow* :bool a a a)))
106+
:defs ((:forall ((x a) (y a))
107+
(equal (hap* (cond (typ (:arrow* :bool a a a))) (hp-true) x y) x))
108+
(:forall ((x a) (y a))
109+
(equal (hap* (cond (typ (:arrow* :bool a a a))) (hp-false) x y) y))))),
110+
("COMMA",
111+
(defhol
112+
:fns ((comma (:arrow* a b (:hash a b))))
113+
:defs ((:forall ((x a) (y b))
114+
(equal (hap* (comma (typ (:arrow* a b (:hash a b)))) x y)
115+
(hp-comma x y)))))),
116+
("HD",
117+
(defhol
118+
:fns ((hd (:arrow* (:list a) a)))
119+
:defs ((:forall ((h a) (t (:list a)))
120+
(equal (hap* (hd (typ (:arrow* (:list a) a))) (hp-cons h t)) h))))),
121+
("NULL",
122+
(defhol
123+
:fns ((null (:arrow* (:list a) :bool)))
124+
:defs ((equal
125+
(hap* (null (typ (:arrow* (:list a) :bool))) (hp-nil (typ a)))
126+
(hp-true))
127+
(:forall ((h a) (t (:list a)))
128+
(equal (hap* (null (typ (:arrow* (:list a) :bool))) (hp-cons h t))
129+
(hp-false)))))),
130+
("SUC",
131+
(defhol
132+
:fns ((suc (:arrow* :num :num)))
133+
:defs ((:forall ((m :num))
134+
(equal (hap* (suc (typ (:arrow* :num :num))) m)
135+
(hp+ (hp-num 1) m)))))),
136+
("<=",
137+
(defhol
138+
:fns ((<= (:arrow* :num :num :bool)))
139+
:defs ((:forall ((x :num) (y :num))
140+
(equal (hap* (<= (typ (:arrow* :num :num :bool))) x y)
141+
(hp-or (hp< x y) (hp= x y))))))),
142+
("FST",
143+
(defhol
144+
:fns ((fst (:arrow* (:hash a b) a)))
145+
:defs ((:forall ((x a) (y b))
146+
(equal (hap* (fst (typ (:arrow* (:hash a b) a))) (hp-comma x y))
147+
x))))),
148+
("SND",
149+
(defhol
150+
:fns ((snd (:arrow* (:hash a b) b)))
151+
:defs ((:forall ((x a) (y b))
152+
(equal (hap* (snd (typ (:arrow* (:hash a b) b))) (hp-comma x y))
153+
y))))),
154+
("EXP",
155+
(defhol
156+
:fns ((exp (:arrow* :num :num :num)))
157+
:defs ((:forall ((m :num))
158+
(equal (hap* (exp (typ (:arrow* :num :num :num))) m (hp-num 0))
159+
(hp-num 1)))
160+
(:forall ((m :num) (n :num))
161+
(equal
162+
(hap* (exp (typ (:arrow* :num :num :num))) m
163+
(hap* (suc (typ (:arrow* :num :num))) n))
164+
(hp* m (hap* (exp (typ (:arrow* :num :num :num))) m n))))))),
165+
("polyp",
166+
(defhol
167+
:fns ((polyp (:arrow* (:list (:hash :num :num)) :bool)))
168+
:defs ((equal
169+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
170+
(hp-nil (typ (:hash :num :num)))) (hp-true))
171+
(:forall ((r (:list (:hash :num :num))) (e :num) (c :num))
172+
(equal
173+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
174+
(hp-cons (hp-comma c e) r))
175+
(hp-and
176+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool))) r)
177+
(hp-and (hp-not (hp= c (hp-num 0)))
178+
(hp-and
179+
(hap* (<= (typ (:arrow* :num :num :bool))) (hp-num 0) e)
180+
(hp-or
181+
(hap* (null (typ (:arrow* (:list (:hash :num :num)) :bool)))
182+
r)
183+
(hp<
184+
(hap* (snd (typ (:arrow* (:hash :num :num) :num)))
185+
(hap*
186+
(hd
187+
(typ
188+
(:arrow* (:list (:hash :num :num)) (:hash :num :num))))
189+
r)) e)))))))))),
190+
("eval_poly",
191+
(defhol
192+
:fns ((eval_poly (:arrow* (:list (:hash :num :num)) :num :num)))
193+
:defs ((:forall ((v :num))
194+
(equal
195+
(hap*
196+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
197+
(hp-nil (typ (:hash :num :num))) v) (hp-num 0)))
198+
(:forall ((v :num) (r (:list (:hash :num :num))) (e :num) (c :num))
199+
(equal
200+
(hap*
201+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
202+
(hp-cons (hp-comma c e) r) v)
203+
(hp+ (hp* c (hap* (exp (typ (:arrow* :num :num :num))) v e))
204+
(hap*
205+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
206+
r v))))))),
207+
("sum_polys",
208+
(defhol
209+
:fns ((sum_polys
210+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
211+
(:list (:hash :num :num)))))
212+
:defs ((equal
213+
(hap*
214+
(sum_polys
215+
(typ
216+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
217+
(:list (:hash :num :num))))) (hp-nil (typ (:hash :num :num)))
218+
(hp-nil (typ (:hash :num :num))))
219+
(hp-nil (typ (:hash :num :num))))
220+
(:forall ((v7 (:list (:hash :num :num))) (v6 (:hash :num :num)))
221+
(equal
222+
(hap*
223+
(sum_polys
224+
(typ
225+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
226+
(:list (:hash :num :num))))) (hp-nil (typ (:hash :num :num)))
227+
(hp-cons v6 v7)) (hp-cons v6 v7)))
228+
(:forall ((v3 (:list (:hash :num :num))) (v2 (:hash :num :num)))
229+
(equal
230+
(hap*
231+
(sum_polys
232+
(typ
233+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
234+
(:list (:hash :num :num))))) (hp-cons v2 v3)
235+
(hp-nil (typ (:hash :num :num)))) (hp-cons v2 v3)))
236+
(:forall
237+
((r2 (:list (:hash :num :num))) (r1 (:list (:hash :num :num)))
238+
(e2 :num) (e1 :num) (c2 :num) (c1 :num))
239+
(equal
240+
(hap*
241+
(sum_polys
242+
(typ
243+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
244+
(:list (:hash :num :num))))) (hp-cons (hp-comma c1 e1) r1)
245+
(hp-cons (hp-comma c2 e2) r2))
246+
(hap*
247+
(cond
248+
(typ
249+
(:arrow* :bool (:list (:hash :num :num))
250+
(:list (:hash :num :num)) (:list (:hash :num :num)))))
251+
(hp= e1 e2)
252+
(hp-cons (hp-comma (hp+ c1 c2) e1)
253+
(hap*
254+
(sum_polys
255+
(typ
256+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
257+
(:list (:hash :num :num))))) r1 r2))
258+
(hap*
259+
(cond
260+
(typ
261+
(:arrow* :bool (:list (:hash :num :num))
262+
(:list (:hash :num :num)) (:list (:hash :num :num)))))
263+
(hp< e1 e2)
264+
(hp-cons (hp-comma c2 e2)
265+
(hap*
266+
(sum_polys
267+
(typ
268+
(:arrow* (:list (:hash :num :num))
269+
(:list (:hash :num :num)) (:list (:hash :num :num)))))
270+
(hp-cons (hp-comma c1 e1) r1) r2))
271+
(hp-cons (hp-comma c1 e1)
272+
(hap*
273+
(sum_polys
274+
(typ
275+
(:arrow* (:list (:hash :num :num))
276+
(:list (:hash :num :num)) (:list (:hash :num :num))))) r1
277+
(hp-cons (hp-comma c2 e2) r2)))))))))),
278+
("eval_sum_poly_distrib",
279+
(defhol
280+
:name eval_sum_poly_distrib
281+
:goal (:forall
282+
((x (:list (:hash :num :num))) (y (:list (:hash :num :num)))
283+
(v :num))
284+
(hp-implies
285+
(hp-and
286+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool))) x)
287+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool))) y))
288+
(hp=
289+
(hap*
290+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
291+
(hap*
292+
(sum_polys
293+
(typ
294+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
295+
(:list (:hash :num :num))))) x y) v)
296+
(hp+
297+
(hap*
298+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
299+
x v)
300+
(hap*
301+
(eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
302+
y v)))))))]: (string * t) list
303+
*)
304+
305+
(* Another version, where polyp is defined with deeper pattern-matching
306+
Definition polyp_def:
307+
(polyp [] = T) /\
308+
(polyp [(c,e)] = (0 < c /\ 0 <= e)) /\
309+
(polyp ((c1,e1)::(c2,e2)::r) =
310+
(0 < c1 /\ 0 <= e1 /\ e2 < e1 /\ polyp ((c2,e2)::r)))
311+
End
312+
313+
Theorem eval_poly_sum_polys:
314+
∀x y v. polyp x ∧ polyp y ⇒
315+
eval_poly (sum_polys x y) v
316+
=
317+
eval_poly x v + eval_poly y v
318+
Proof
319+
recInduct sum_polys_ind >> rw[] >>
320+
gvs [eval_poly_def,sum_polys_def] >>
321+
subgoal `polyp r1 /\ polyp r2`
322+
>- (`(r1 = [] \/ (?c3 e3 t1. r1 = (c3,e3)::t1)) /\
323+
(r2 = [] \/ (?c4 e4 t2. r2 = (c4,e4)::t2))` by
324+
metis_tac [list_CASES, pair_CASES] >>
325+
gvs[polyp_def]) >>
326+
gvs[] >> rw[] >> gvs[] >> rw [eval_poly_def]
327+
QED
328+
*)

‎examples/acl2/hol-to-acl2/examples/ex1Script.sml‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
Theory ex1
2+
Ancestors
3+
combin pair option prim_rec arithmetic list hol_to_acl2
4+
Libs
5+
HOL_to_ACL2
6+
7+
Definition Even_Odd_def:
8+
Even 0 = T ∧
9+
Even (SUC n) = Odd n ∧
10+
Odd 0 = F ∧
11+
Odd (SUC n) = Even n
12+
End
13+
14+
Theorem DIVISION_FOR_ACL2[local] =
15+
DIVISION
16+
|> SIMP_RULE bool_ss [PULL_FORALL]
17+
|> SPEC_ALL
18+
|> EQT_INTRO
19+
|> GEN_ALL;
20+
21+
val defs = (* following ex1.lisp plus a few others *)
22+
[suc_thm,
23+
PRE,
24+
I_THM,
25+
C_THM,
26+
K_THM,
27+
o_THM,
28+
COMMA_def,
29+
FST,
30+
SND,
31+
UNCURRY_DEF,
32+
OPTION_BIND_def,
33+
OPTION_MAP_DEF,
34+
list_case_def,
35+
list_size_def,
36+
MAP,
37+
FOLDR,
38+
FOLDL,
39+
mk_spec [``(DIV)``, ``(MOD)``] DIVISION_FOR_ACL2,
40+
Even_Odd_def,
41+
EXP]
42+
43+
val thms =
44+
[mk_named_thm "MAP_ID_I" MAP_ID_I,
45+
mk_named_thm "MAP_o" MAP_o
46+
];
47+
48+
val goals =
49+
[mk_named_goal "FST-COMMA" (concl FST),
50+
mk_named_goal "BOOL_CASES_AX" (concl BOOL_CASES_AX),
51+
mk_named_goal "pair_fst_snd_eq" (concl (GSYM PAIR_FST_SND_EQ))];
52+
53+
val _ = print_defhols_to_file "ex1.defhol" (defs @ thms @ goals);

0 commit comments

Comments
 (0)