Using the function-wrapping concepts in Mark's Tactician and some of that
code, I am now able to execute HOL Light tactic proofs and present them as
rather traditional-style forward proofs. (Mark in turn credits Roland
Zumkeller in the Tactician code.) At the bottom of this email are two of
Mark's Tactician example proofs shown as forward proofs.
Thanks Mark and also John for a synopsis of the history of HOL proof
recording systems. My main interest is in converting proofs to more
human-readable form rather than porting, but clearly these are related
subjects.
Many of the steps in my recorded forward proofs use higher-level inference
rules. The higher-level rules (as in drule.ml) are wrapped and the
high-level steps are recorded, so they can be presented. The proofs are
still longer than I would prefer. I think some of this can be remedied by
by a little more intelligence in the presentation code, but there are a
couple of more substantial issues. If anyone has suggestions in these areas
I am interested in hearing about them.
1. Some higher-level forward inference rules seem to exist without being
bound to global names. This means I cannot wrap them, so the recording and
presentation fall back to the primitive rules. The primitive inference
rules are wrapped after loading of fusion.ml, so uses of them from code
loaded later invokes the proof recording. Higher-level inference rules are
wrapped after loading of drule.ml, so code loaded after that refers to
wrapped versions when using any of the global names. At least that is my
theory about the origin of many of the occurrences of primitive inference
rules in the proofs below.
2. I can wrap functions (inference rules) that take conversions as
arguments. This might be useful if I could present those conversions in a
human-friendly way. Conversions are functions so presenting them is not as
easy as presenting a term or theorem. In fact I'm not sure what might be
practical to achieve here. I have tried using functions as keys in a
Hashtbl, but this does not seem to function reliably. Perhaps it fails when
key collisions occur.
3. Furthermore the forward proofs don't match up very neatly with the
original tactic proof. See "next steps" below for more on this.
About this "wrapping" concept --
This "wrapping" of functions in essence is loading OCaml functions
definitions that have a structure (taking REFL as an example) like:
let REFL tm =
let result = REFL tm in
(* Records information about the arguments and result here. *)
result;;
The name REFL in the function body refers to a pre-existing REFL function,
but references to REFL in code loaded after this refer to the new version
that does recording.
This approach is attractive in that it does not require modifying the HOL
Light source code to add the recording functionality, but recording proof
information "on the side" makes it a bit less straightforward to
reconstruct the forward proof.
Next steps --
For next steps I think it may be quite helpful to record the activities of
tactics and their kin in working with goals and subgoals. This hopefully
would help me generate a presentation that is at a higher level, and should
also make it easier to match the presentation with an original tactic
proof. Tactician already records quite a bit of this sort of information,
so perhaps it would be good to do this as an extension of Tactician. Mark,
I'll contact you about this.
Cheers,
Cris
Here are a couple of examples generated with my current experimental code.
The forward-style proofs are not exactly in two-column style. The actual
style aims to coexist peacefully with the existing code for displaying
theorems with hypotheses, and it also tries to use a presentation style
that doesn't make too many very wide lines.
Here is Mark's example 1 for Tactician. The original tactic proof is:
# g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
# e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
and I am getting this forward proof from it:
1 REFL of `x`:
|- x = x
2 REFL of `y`:
|- y = y
3 REFL of `z`:
|- z = z
4 GEN of `z`, 3:
|- !z. z = z
5 GEN_ALPHA_CONV of `z`, `!z. z = z`:
|- (!z. z = z) <=> (!z. z = z)
6 EQ_MP of 5, 4:
|- !z. z = z
7 GEN of `y`, 2:
|- !y. y = y
8 GEN_ALPHA_CONV of `y`, `!y. y = y`:
|- (!y. y = y) <=> (!y. y = y)
9 EQ_MP of 8, 7:
|- !y. y = y
10 GEN of `x`, 1:
|- !x. x = x
11 GEN_ALPHA_CONV of `x`, `!x. x = x`:
|- (!x. x = x) <=> (!x. x = x)
12 EQ_MP of 11, 10:
|- !x. x = x
13 CONJ of 9, 6:
|- (!y. y = y) /\ (!z. z = z)
14 CONJ of 12, 13:
|- (!x. x = x) /\ (!y. y = y) /\ (!z. z = z)
This is Mark's example 3, which starts with a "packaged" tactic proof:
# let REAL_MUL_LINV_UNIQ = prove
(`!x y. (x * y = &1) ==> (inv(y) = x)`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `y = &0` THEN
ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_OF_NUM_EQ; ARITH_EQ] THEN
FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV) THEN
ASM_REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
DISCH_THEN(ACCEPT_TAC o SYM));;
I am currently getting a forward proof like this:
1 SPEC of `y = &0`, EXCLUDED_MIDDLE:
|- y = &0 \/ ~(y = &0)
2 ASSUME of `y = &0`:
y = &0
|- y = &0
3 ASSUME of `~(y = &0)`:
~(y = &0)
|- ~(y = &0)
4 CONJUNCT2 of ARITH_EQ:
|- (_0 = _0 <=> T) /\
(!n. BIT0 n = _0 <=> n = _0) /\
(!n. BIT1 n = _0 <=> F) /\
(!n. _0 = BIT0 n <=> _0 = n) /\
(!n. _0 = BIT1 n <=> F) /\
(!m n. BIT0 m = BIT0 n <=> m = n) /\
(!m n. BIT0 m = BIT1 n <=> F) /\
(!m n. BIT1 m = BIT0 n <=> F) /\
(!m n. BIT1 m = BIT1 n <=> m = n)
5 CONJUNCT2 of 4:
|- (!n. BIT0 n = _0 <=> n = _0) /\
(!n. BIT1 n = _0 <=> F) /\
(!n. _0 = BIT0 n <=> _0 = n) /\
(!n. _0 = BIT1 n <=> F) /\
(!m n. BIT0 m = BIT0 n <=> m = n) /\
(!m n. BIT0 m = BIT1 n <=> F) /\
(!m n. BIT1 m = BIT0 n <=> F) /\
(!m n. BIT1 m = BIT1 n <=> m = n)
6 CONJUNCT2 of 5:
|- (!n. BIT1 n = _0 <=> F) /\
(!n. _0 = BIT0 n <=> _0 = n) /\
(!n. _0 = BIT1 n <=> F) /\
(!m n. BIT0 m = BIT0 n <=> m = n) /\
(!m n. BIT0 m = BIT1 n <=> F) /\
(!m n. BIT1 m = BIT0 n <=> F) /\
(!m n. BIT1 m = BIT1 n <=> m = n)
7 CONJUNCT2 of 6:
|- (!n. _0 = BIT0 n <=> _0 = n) /\
(!n. _0 = BIT1 n <=> F) /\
(!m n. BIT0 m = BIT0 n <=> m = n) /\
(!m n. BIT0 m = BIT1 n <=> F) /\
(!m n. BIT1 m = BIT0 n <=> F) /\
(!m n. BIT1 m = BIT1 n <=> m = n)
8 CONJUNCT2 of 7:
|- (!n. _0 = BIT1 n <=> F) /\
(!m n. BIT0 m = BIT0 n <=> m = n) /\
(!m n. BIT0 m = BIT1 n <=> F) /\
(!m n. BIT1 m = BIT0 n <=> F) /\
(!m n. BIT1 m = BIT1 n <=> m = n)
9 CONJUNCT1 of 8:
|- !n. _0 = BIT1 n <=> F
10 SPEC_ALL of 9:
|- _0 = BIT1 n <=> F
11 CONJUNCT1 of ARITH_EQ:
|- !m n. NUMERAL m = NUMERAL n <=> m = n
12 SPEC_ALL of 11:
|- NUMERAL m = NUMERAL n <=> m = n
13 SPEC_ALL of REAL_OF_NUM_EQ:
|- &m = &n <=> m = n
14 SPEC_ALL of REAL_MUL_RZERO:
|- x * &0 = &0
15 REFL of `y = &0`:
|- y = &0 <=> y = &0
16 REFL of `y = &0`:
|- y = &0 <=> y = &0
17 TRANS of 16, 15:
|- y = &0 <=> y = &0
18 EQ_MP of 17, 2:
y = &0
|- y = &0
19 REFL of `(*) x`:
|- (*) x = (*) x
20 MK_COMB of 19, 18:
y = &0
|- x * y = x * &0
21 REFL of `x * &0 = &0`:
|- x * &0 = &0 <=> x * &0 = &0
22 REFL of `x * &0 = &0`:
|- x * &0 = &0 <=> x * &0 = &0
23 TRANS of 22, 21:
|- x * &0 = &0 <=> x * &0 = &0
24 EQ_MP of 23, 14:
|- x * &0 = &0
25 TRANS of 20, 24:
y = &0
|- x * y = &0
26 REFL of `(=)`:
|- (=) = (=)
27 MK_COMB of 26, 25:
y = &0
|- (=) (x * y) = (=) (&0)
28 REFL of `&1`:
|- &1 = &1
29 MK_COMB of 27, 28:
y = &0
|- x * y = &1 <=> &0 = &1
30 REFL of `&m = &n <=> m = n`:
|- (&m = &n <=> m = n) <=> &m = &n <=> m = n
31 REFL of `&m = &n <=> m = n`:
|- (&m = &n <=> m = n) <=> &m = &n <=> m = n
32 TRANS of 31, 30:
|- (&m = &n <=> m = n) <=> &m = &n <=> m = n
33 EQ_MP of 32, 13:
|- &m = &n <=> m = n
34 INST of `1`, `n`, `0`, `m`, 33:
|- &0 = &1 <=> 0 = 1
35 REFL of `NUMERAL m = NUMERAL n <=> m = n`:
|- (NUMERAL m = NUMERAL n <=> m = n) <=> NUMERAL m = NUMERAL n <=> m = n
36 REFL of `NUMERAL m = NUMERAL n <=> m = n`:
|- (NUMERAL m = NUMERAL n <=> m = n) <=> NUMERAL m = NUMERAL n <=> m = n
37 TRANS of 36, 35:
|- (NUMERAL m = NUMERAL n <=> m = n) <=> NUMERAL m = NUMERAL n <=> m = n
38 EQ_MP of 37, 12:
|- NUMERAL m = NUMERAL n <=> m = n
39 INST of `BIT1 _0`, `n`, `_0`, `m`, 38:
|- 0 = 1 <=> _0 = BIT1 _0
40 REFL of `_0 = BIT1 n <=> F`:
|- (_0 = BIT1 n <=> F) <=> _0 = BIT1 n <=> F
41 REFL of `_0 = BIT1 n <=> F`:
|- (_0 = BIT1 n <=> F) <=> _0 = BIT1 n <=> F
42 TRANS of 41, 40:
|- (_0 = BIT1 n <=> F) <=> _0 = BIT1 n <=> F
43 EQ_MP of 42, 10:
|- _0 = BIT1 n <=> F
44 INST of `_0`, `n`, 43:
|- _0 = BIT1 _0 <=> F
45 TRANS of 39, 44:
|- 0 = 1 <=> F
46 TRANS of 34, 45:
|- &0 = &1 <=> F
47 TRANS of 29, 46:
y = &0
|- x * y = &1 <=> F
48 REFL of `(==>)`:
|- (==>) = (==>)
49 MK_COMB of 48, 47:
y = &0
|- (==>) (x * y = &1) = (==>) F
50 REFL of `y = &0`:
|- y = &0 <=> y = &0
51 REFL of `y = &0`:
|- y = &0 <=> y = &0
52 TRANS of 51, 50:
|- y = &0 <=> y = &0
53 EQ_MP of 52, 2:
y = &0
|- y = &0
54 REFL of `inv`:
|- inv = inv
55 MK_COMB of 54, 53:
y = &0
|- inv y = inv (&0)
56 REFL of `(=)`:
|- (=) = (=)
57 MK_COMB of 56, 55:
y = &0
|- (=) (inv y) = (=) (inv (&0))
58 REFL of `x`:
|- x = x
59 MK_COMB of 57, 58:
y = &0
|- inv y = x <=> inv (&0) = x
60 MK_COMB of 49, 59:
y = &0
|- x * y = &1 ==> inv y = x <=> F ==> inv (&0) = x
61 REFL of `F ==> t <=> T`:
|- (F ==> t <=> T) <=> F ==> t <=> T
62 REFL of `F ==> t <=> T`:
|- (F ==> t <=> T) <=> F ==> t <=> T
63 TRANS of 62, 61:
|- (F ==> t <=> T) <=> F ==> t <=> T
64 EQ_MP of 63,
`|- F ==> t <=> T`:
|- F ==> t <=> T
65 INST of `inv (&0) = x`, `t`, 64:
|- F ==> inv (&0) = x <=> T
66 TRANS of 60, 65:
y = &0
|- x * y = &1 ==> inv y = x <=> T
67 EQT_ELIM of 66:
y = &0
|- x * y = &1 ==> inv y = x
68 REFL of `x * y = &1 ==> inv y = x`:
|- x * y = &1 ==> inv y = x <=> x * y = &1 ==> inv y = x
69 SYM of 68:
|- x * y = &1 ==> inv y = x <=> x * y = &1 ==> inv y = x
70 MATCH_MP of REAL_MUL_LINV, 3:
~(y = &0)
|- inv y * y = &1
71 SYM of 70:
~(y = &0)
|- &1 = inv y * y
72 SUBS_CONV of 71, `x * y = &1 ==> inv y = x`:
~(y = &0)
|- x * y = &1 ==> inv y = x <=> x * y = inv y * y ==> inv y = x
73 SYM of 72:
~(y = &0)
|- x * y = inv y * y ==> inv y = x <=> x * y = &1 ==> inv y = x
74 SPEC_ALL of REAL_EQ_MUL_RCANCEL:
|- x * z = y * z <=> x = y \/ z = &0
75 EQF_INTRO of 3:
~(y = &0)
|- y = &0 <=> F
76 REFL of `x * z = y * z <=> x = y \/ z = &0`:
|- (x * z = y * z <=> x = y \/ z = &0) <=> x * z = y * z <=> x = y \/ z = &0
77 REFL of `x * z = y * z <=> x = y \/ z = &0`:
|- (x * z = y * z <=> x = y \/ z = &0) <=> x * z = y * z <=> x = y \/ z = &0
78 TRANS of 77, 76:
|- (x * z = y * z <=> x = y \/ z = &0) <=> x * z = y * z <=> x = y \/ z = &0
79 EQ_MP of 78, 74:
|- x * z = y * z <=> x = y \/ z = &0
80 INST of `inv y`, `y`, `y`, `z`, 79:
|- x * y = inv y * y <=> x = inv y \/ y = &0
81 REFL of `y = &0 <=> F`:
|- (y = &0 <=> F) <=> y = &0 <=> F
82 REFL of `y = &0 <=> F`:
|- (y = &0 <=> F) <=> y = &0 <=> F
83 TRANS of 82, 81:
|- (y = &0 <=> F) <=> y = &0 <=> F
84 EQ_MP of 83, 75:
~(y = &0)
|- y = &0 <=> F
85 REFL of `(\/) (x = inv y)`:
|- (\/) (x = inv y) = (\/) (x = inv y)
86 MK_COMB of 85, 84:
~(y = &0)
|- x = inv y \/ y = &0 <=> x = inv y \/ F
87 REFL of `t \/ F <=> t`:
|- (t \/ F <=> t) <=> t \/ F <=> t
88 REFL of `t \/ F <=> t`:
|- (t \/ F <=> t) <=> t \/ F <=> t
89 TRANS of 88, 87:
|- (t \/ F <=> t) <=> t \/ F <=> t
90 EQ_MP of 89,
`|- t \/ F <=> t`:
|- t \/ F <=> t
91 INST of `x = inv y`, `t`, 90:
|- x = inv y \/ F <=> x = inv y
92 TRANS of 86, 91:
~(y = &0)
|- x = inv y \/ y = &0 <=> x = inv y
93 TRANS of 80, 92:
~(y = &0)
|- x * y = inv y * y <=> x = inv y
94 REFL of `(==>)`:
|- (==>) = (==>)
95 MK_COMB of 94, 93:
~(y = &0)
|- (==>) (x * y = inv y * y) = (==>) (x = inv y)
96 REFL of `inv y = x`:
|- inv y = x <=> inv y = x
97 MK_COMB of 95, 96:
~(y = &0)
|- x * y = inv y * y ==> inv y = x <=> x = inv y ==> inv y = x
98 SYM of 97:
~(y = &0)
|- x = inv y ==> inv y = x <=> x * y = inv y * y ==> inv y = x
99 ASSUME of `x = inv y`:
x = inv y
|- x = inv y
100 SYM of 99:
x = inv y
|- inv y = x
101 DISCH of `x = inv y`, 100:
|- x = inv y ==> inv y = x
102 EQ_MP of 98, 101:
~(y = &0)
|- x * y = inv y * y ==> inv y = x
103 EQ_MP of 73, 102:
~(y = &0)
|- x * y = &1 ==> inv y = x
104 EQ_MP of 69, 103:
~(y = &0)
|- x * y = &1 ==> inv y = x
105 DISJ_CASES of 1, 67, 104:
|- x * y = &1 ==> inv y = x
106 GEN of `y`, 105:
|- !y. x * y = &1 ==> inv y = x
107 GEN_ALPHA_CONV of `y`, `!y. x * y = &1 ==> inv y = x`:
|- (!y. x * y = &1 ==> inv y = x) <=> (!y. x * y = &1 ==> inv y = x)
108 EQ_MP of 107, 106:
|- !y. x * y = &1 ==> inv y = x
109 GEN of `x`, 108:
|- !x y. x * y = &1 ==> inv y = x
110 GEN_ALPHA_CONV of `x`, `!x y. x * y = &1 ==> inv y = x`:
|- (!x y. x * y = &1 ==> inv y = x) <=> (!x y. x * y = &1 ==> inv y = x)
111 EQ_MP of 110, 109:
|- !x y. x * y = &1 ==> inv y = x
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
