Skip to content

Commit e8ca696

Browse files
konrad-slindkonrad-slind
committed
revised README, added example, added output of running examples
1 parent 9a925a5 commit e8ca696

File tree

4 files changed

+529
-9
lines changed

4 files changed

+529
-9
lines changed

‎examples/acl2/hol-to-acl2/README.md‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,29 @@
11
# HOL to ACL2 Translation
22

33
This directory provides an automated translation from a subset of HOL
4-
to ACL(zfc), a formalization of Set Theory in the ACL2 system. Details
4+
to ACL2(zfc), a formalization of Set Theory in the ACL2 system. Details
55
of ACL2(zfc) can be found at
66
```
7-
https://github.com/acl2/acl2/tree/master/books/projects/set-theory
7+
https://github.com/acl2/acl2/tree/master/books/projects/set-theory
88
```
99

1010
The modelling of the HOL logic in ACL2(zfc) is analogous to the
11-
"Pitts" semantics of the HOL4 Logic Manual. It can be found at
11+
"Pitts" semantics of the HOL4 Logic Manual. It can be found at the `acl2/`
12+
subdirectory of the HOL to ACL2 translation project in ACL2, here:
1213
```
13-
https://github.com/acl2/acl2/tree/master/books/projects/hol-in-acl2/acl2
14+
https://github.com/acl2/acl2/tree/master/books/projects/hol-in-acl2/
1415
```
16+
The `examples/` subdirectory located there should be kept in sync with
17+
the `examples/` directory located here.
1518

1619
The translator itself can be seen in action in the `examples` directory.
1720
Typing
1821
```
19-
<holdir>/bin/Holmake cleanAll
20-
<holdir>/bin/Holmake
22+
<holdir>/bin/Holmake cleanAll
23+
<holdir>/bin/Holmake
2124
```
2225
will create, for each `<x>Script.sml`, a corresponding file
23-
`<x>.defhol`, comprising a list of so-called `defhol forms` which can
24-
then be used in ACL2(zfc) to "recreate" the selected definitions,
25-
theorems, and goals coming from the `<x>` formalization in HOL4.
26+
`<x>.defhol`, comprising a list of so-called `defhol` forms which can
27+
then be used in ACL2(zfc) to create set theory translations of the
28+
selected definitions, theorems, and goals from the `<x>` formalization
29+
in HOL4.

‎examples/acl2/hol-to-acl2/examples/eval_poly.defhol‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
(defhol
2+
:fns ((cond (:arrow* :bool a a a)))
3+
:defs ((:forall ((x a) (y a))
4+
(equal (hap* (cond (typ (:arrow* :bool a a a))) (hp-true) x y) x))
5+
(:forall ((x a) (y a))
6+
(equal (hap* (cond (typ (:arrow* :bool a a a))) (hp-false) x y) y))))
7+
8+
(defhol
9+
:fns ((comma (:arrow* a b (:hash a b))))
10+
:defs ((:forall ((x a) (y b))
11+
(equal (hap* (comma (typ (:arrow* a b (:hash a b)))) x y)
12+
(hp-comma x y)))))
13+
14+
(defhol
15+
:fns ((fst (:arrow* (:hash a b) a)))
16+
:defs ((:forall ((x a) (y b))
17+
(equal (hap* (fst (typ (:arrow* (:hash a b) a))) (hp-comma x y)) x))))
18+
19+
(defhol
20+
:fns ((snd (:arrow* (:hash a b) b)))
21+
:defs ((:forall ((x a) (y b))
22+
(equal (hap* (snd (typ (:arrow* (:hash a b) b))) (hp-comma x y)) y))))
23+
24+
(defhol
25+
:fns ((suc (:arrow* :num :num)))
26+
:defs ((:forall ((m :num))
27+
(equal (hap* (suc (typ (:arrow* :num :num))) m) (hp+ (hp-num 1) m)))))
28+
29+
(defhol
30+
:fns ((<= (:arrow* :num :num :bool)))
31+
:defs ((:forall ((x :num) (y :num))
32+
(equal (hap* (<= (typ (:arrow* :num :num :bool))) x y)
33+
(hp-or (hp< x y) (hp= x y))))))
34+
35+
(defhol
36+
:fns ((hd (:arrow* (:list a) a)))
37+
:defs ((:forall ((h a) (t (:list a)))
38+
(equal (hap* (hd (typ (:arrow* (:list a) a))) (hp-cons h t)) h))))
39+
40+
(defhol
41+
:fns ((null (:arrow* (:list a) :bool)))
42+
:defs ((equal
43+
(hap* (null (typ (:arrow* (:list a) :bool))) (hp-nil (typ a)))
44+
(hp-true))
45+
(:forall ((h a) (t (:list a)))
46+
(equal (hap* (null (typ (:arrow* (:list a) :bool))) (hp-cons h t))
47+
(hp-false)))))
48+
49+
(defhol
50+
:fns ((exp (:arrow* :num :num :num)))
51+
:defs ((:forall ((m :num))
52+
(equal (hap* (exp (typ (:arrow* :num :num :num))) m (hp-num 0))
53+
(hp-num 1)))
54+
(:forall ((m :num) (n :num))
55+
(equal
56+
(hap* (exp (typ (:arrow* :num :num :num))) m
57+
(hap* (suc (typ (:arrow* :num :num))) n))
58+
(hp* m (hap* (exp (typ (:arrow* :num :num :num))) m n))))))
59+
60+
(defhol
61+
:fns ((polyp (:arrow* (:list (:hash :num :num)) :bool)))
62+
:defs ((equal
63+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
64+
(hp-nil (typ (:hash :num :num)))) (hp-true))
65+
(:forall ((e :num) (c :num))
66+
(equal
67+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
68+
(hp-cons (hp-comma c e) (hp-nil (typ (:hash :num :num)))))
69+
(hp-and (hp< (hp-num 0) c)
70+
(hap* (<= (typ (:arrow* :num :num :bool))) (hp-num 0) e))))
71+
(:forall
72+
((r (:list (:hash :num :num))) (e2 :num) (e1 :num) (c2 :num) (c1 :num))
73+
(equal
74+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
75+
(hp-cons (hp-comma c1 e1) (hp-cons (hp-comma c2 e2) r)))
76+
(hp-and (hp< (hp-num 0) c1)
77+
(hp-and (hap* (<= (typ (:arrow* :num :num :bool))) (hp-num 0) e1)
78+
(hp-and (hp< e2 e1)
79+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool)))
80+
(hp-cons (hp-comma c2 e2) r)))))))))
81+
82+
(defhol
83+
:fns ((eval_poly (:arrow* (:list (:hash :num :num)) :num :num)))
84+
:defs ((:forall ((v :num))
85+
(equal
86+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
87+
(hp-nil (typ (:hash :num :num))) v) (hp-num 0)))
88+
(:forall ((v :num) (r (:list (:hash :num :num))) (e :num) (c :num))
89+
(equal
90+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
91+
(hp-cons (hp-comma c e) r) v)
92+
(hp+ (hp* c (hap* (exp (typ (:arrow* :num :num :num))) v e))
93+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
94+
r v))))))
95+
96+
(defhol
97+
:fns ((sum_polys
98+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
99+
(:list (:hash :num :num)))))
100+
:defs ((equal
101+
(hap*
102+
(sum_polys
103+
(typ
104+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
105+
(:list (:hash :num :num))))) (hp-nil (typ (:hash :num :num)))
106+
(hp-nil (typ (:hash :num :num)))) (hp-nil (typ (:hash :num :num))))
107+
(:forall ((v7 (:list (:hash :num :num))) (v6 (:hash :num :num)))
108+
(equal
109+
(hap*
110+
(sum_polys
111+
(typ
112+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
113+
(:list (:hash :num :num))))) (hp-nil (typ (:hash :num :num)))
114+
(hp-cons v6 v7)) (hp-cons v6 v7)))
115+
(:forall ((v3 (:list (:hash :num :num))) (v2 (:hash :num :num)))
116+
(equal
117+
(hap*
118+
(sum_polys
119+
(typ
120+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
121+
(:list (:hash :num :num))))) (hp-cons v2 v3)
122+
(hp-nil (typ (:hash :num :num)))) (hp-cons v2 v3)))
123+
(:forall
124+
((r2 (:list (:hash :num :num))) (r1 (:list (:hash :num :num))) (e2 :num)
125+
(e1 :num) (c2 :num) (c1 :num))
126+
(equal
127+
(hap*
128+
(sum_polys
129+
(typ
130+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
131+
(:list (:hash :num :num))))) (hp-cons (hp-comma c1 e1) r1)
132+
(hp-cons (hp-comma c2 e2) r2))
133+
(hap*
134+
(cond
135+
(typ
136+
(:arrow* :bool (:list (:hash :num :num)) (:list (:hash :num :num))
137+
(:list (:hash :num :num))))) (hp= e1 e2)
138+
(hp-cons (hp-comma (hp+ c1 c2) e1)
139+
(hap*
140+
(sum_polys
141+
(typ
142+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
143+
(:list (:hash :num :num))))) r1 r2))
144+
(hap*
145+
(cond
146+
(typ
147+
(:arrow* :bool (:list (:hash :num :num)) (:list (:hash :num :num))
148+
(:list (:hash :num :num))))) (hp< e1 e2)
149+
(hp-cons (hp-comma c2 e2)
150+
(hap*
151+
(sum_polys
152+
(typ
153+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
154+
(:list (:hash :num :num))))) (hp-cons (hp-comma c1 e1) r1) r2))
155+
(hp-cons (hp-comma c1 e1)
156+
(hap*
157+
(sum_polys
158+
(typ
159+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
160+
(:list (:hash :num :num))))) r1 (hp-cons (hp-comma c2 e2) r2)))))))))
161+
162+
(defhol
163+
:name eval_sum_poly_distrib
164+
:goal (:forall
165+
((x (:list (:hash :num :num))) (y (:list (:hash :num :num))) (v :num))
166+
(hp-implies
167+
(hp-and (hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool))) x)
168+
(hap* (polyp (typ (:arrow* (:list (:hash :num :num)) :bool))) y))
169+
(hp=
170+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
171+
(hap*
172+
(sum_polys
173+
(typ
174+
(:arrow* (:list (:hash :num :num)) (:list (:hash :num :num))
175+
(:list (:hash :num :num))))) x y) v)
176+
(hp+
177+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
178+
x v)
179+
(hap* (eval_poly (typ (:arrow* (:list (:hash :num :num)) :num :num)))
180+
y v))))))

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

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
Theory eval_poly
2+
Ancestors
3+
arithmetic list
4+
Libs
5+
HOL_to_ACL2
6+
7+
(*---------------------------------------------------------------------------*)
8+
(* A polynomial is a list of pairs (constant, exponent), sorted by *)
9+
(* decreasing order of exponent. Example: *)
10+
(* *)
11+
(* [(3,2); (5,0)] stands for 3x^2 + 5x^0 = 3x^2 + 5 *)
12+
(*---------------------------------------------------------------------------*)
13+
14+
Definition polyp_def:
15+
polyp [] = T ∧
16+
polyp [(c,e)] = (0 < c /\ 0 <= e) ∧
17+
polyp ((c1,e1)::(c2,e2)::r) =
18+
(0 < c1 /\ 0 <= e1 /\ e2 < e1 /\ polyp ((c2,e2)::r))
19+
End
20+
21+
(*---------------------------------------------------------------------------*)
22+
(* Evaluate the polynomial for x having the value v. Example: *)
23+
(* *)
24+
(* ⊢ eval_poly [(3,2); (5,0)] 4 = 53: thm *)
25+
(* *)
26+
(*---------------------------------------------------------------------------*)
27+
28+
Definition eval_poly_def:
29+
eval_poly [] v = 0 ∧
30+
eval_poly ((c,e)::r) v = c * (v ** e) + eval_poly r v
31+
End
32+
33+
(*---------------------------------------------------------------------------*)
34+
(* Polynomial addition. Evaluating the sum of two polynomials is equal to *)
35+
(* the sum of evaluating the polynomials. *)
36+
(* *)
37+
(* Example: *)
38+
(* *)
39+
(* ⊢ sum_polys [(3,2); (5,0)] *)
40+
(* [(4,2); (3,1); (2,0)] = [(7,2); (3,1); (7,0)]: thm *)
41+
(* *)
42+
(* ⊢ eval_poly [(3,2); (5,0)] 4 = 53: thm *)
43+
(* ⊢ eval_poly [(4,2); (3,1); (2,0)] 4 = 78: thm *)
44+
(* *)
45+
(* ⊢ eval_poly *)
46+
(* (sum_polys [(3,2); (5,0)] [(4,2); (3,1); (2,0)]) 4 = 131: thm *)
47+
(* *)
48+
(*---------------------------------------------------------------------------*)
49+
50+
Definition sum_polys_def:
51+
sum_polys [] [] = [] ∧
52+
sum_polys [] p = p ∧
53+
sum_polys p [] = p ∧
54+
sum_polys ((c1,e1)::r1) ((c2,e2)::r2) =
55+
if e1 = e2 then
56+
(c1+c2,e1)::sum_polys r1 r2 else
57+
if e1 < e2 then
58+
(c2,e2)::sum_polys ((c1,e1)::r1) r2
59+
else
60+
(c1,e1)::sum_polys r1 ((c2,e2)::r2)
61+
End
62+
63+
(*---------------------------------------------------------------------------*)
64+
(* Distributive property *)
65+
(*---------------------------------------------------------------------------*)
66+
67+
Theorem eval_poly_sum_polys:
68+
∀x y v.
69+
polyp x ∧ polyp y
70+
⇒
71+
eval_poly (sum_polys x y) v
72+
=
73+
eval_poly x v + eval_poly y v
74+
Proof
75+
recInduct sum_polys_ind >> rw[] >>
76+
gvs [eval_poly_def,sum_polys_def] >>
77+
`polyp r1 /\ polyp r2` by
78+
(Cases_on ‘r1’ >> Cases_on ‘r2’ >>
79+
TRY(Cases_on ‘h’) >> TRY (Cases_on ‘h'’) >>
80+
gvs [polyp_def]) >>
81+
gvs[] >> rw[] >> gvs[eval_poly_def]
82+
QED
83+
84+
(*---------------------------------------------------------------------------*)
85+
(* Turns out the well-formedness condition isn't needed. *)
86+
(*---------------------------------------------------------------------------*)
87+
88+
Theorem eval_poly_sum_polys_again:
89+
∀x y v.
90+
eval_poly (sum_polys x y) v
91+
=
92+
eval_poly x v + eval_poly y v
93+
Proof
94+
recInduct sum_polys_ind >> rw[] >>
95+
gvs [eval_poly_def,sum_polys_def] >>
96+
rw[] >> gvs[eval_poly_def]
97+
QED
98+
99+
(*---------------------------------------------------------------------------*)
100+
(* Make defhol forms for sending to ACL2. We send the proved theorem as a *)
101+
(* goal to be proved in ACL2(zfc) *)
102+
(*---------------------------------------------------------------------------*)
103+
104+
val defs = basis_defs @ [EXP, polyp_def, eval_poly_def, sum_polys_def];
105+
106+
val goals =
107+
[mk_named_goal "eval_sum_poly_distrib" (concl eval_poly_sum_polys)]
108+
109+
val _ = print_defhols_to_file "eval_poly.defhol" (defs @ goals);

0 commit comments

Comments
 (0)