I want to explain GEN_REWRITE_TAC, which I just understood (partly because of
Rob and Michael's advice here about is_comb etc), and to argue that
1) HOL programmers are very good at the pure math skill of adjoint functor, and
2) getting mathematicians to use HOL may require an interface that hides the
adjoint functor, as mathematicians are not used to using adjoint functor in
this way.
I suspect these points 1 & 2 hold for most proof assistants, e.g. Coq, which I
was surprised to learn is based on LCF and ocaml/camlp, just like HOL Light.
Currying is the simplest example of using adjoint functors, which basically
means the `exponential law', the bijection between sets of functions
C^(A x B) and (C^B)^A.
Here's an example of the HOL adjoint functor skill that I had to work very hard
to understand a while back. Let's take as an example this
Multivariate/topology.ml tactic
FIRST_ASSUM(MP_TAC o SPEC `&1 / &2`)
To understand this, we need to think about the adjoint functors involved here:
type goal = (string * thm) list * term;;
type goalstate = (term list * instantiation) * goal list * justification;;
type tactic = goal -> goalstate;;
type thm_tactic = thm -> tactic
FIRST_ASSUM : thm_tactic -> tactic
MP_TAC : thm_tactic
SPEC : term -> thm -> thm
(I this of a goalstate as a list of goals, although I guess that's just the
middle coordinate.)
So SPEC `&1 / &2` has type thm -> thm,
MP_TAC o SPEC `&1 / &2` has type thm -> tactic = thm_tactic, and
FIRST_ASSUM(MP_TAC o SPEC `&1 / &2`) is the tactic obtained by applying this
thm_tactic to the goal ([A1; ...; An], g) and producing the goalstate which
replaces the last goal with
([A1; ...; An], t ==> g), where t = SPEC `&1 / &2` An.
Understanding that just takes good adjoint functor skills, and eventually I was
able to work this exercise, but mathematicians don't expect to have to their
adjoint functor skills here.
John hid the adjoint functors involved in FIRST_ASSUM with "so" in the HOL
Light tutorial section 12.1 "Towards more readable proofs", while Freek in
miz3.ml used "-", as I did in my derivative readable.ml.
GEN_REWRITE_TAC gives a great exercise in adjoint functor, and I'll use as an
example my port of the page 90 tutorial theorem BINOMIAL_THEOREM in
RichterHilbertAxiomGeometry/readable.ml. A conversion (conv), has type
term -> thm. A conversional, like RAND_CONV, has type
conv -> conv, and the ref manual says
RAND_CONV c `t1 t2` applies c to the operand of the application `t1 t2` to
produce an theorem equation
|- t1 t2 = t1 t2'. Such equations are good for rewriting. Now
REWR_CONV : thm -> term -> thm
and for thm th which is an equation l = r,
REWR_CONV th is the conversion which takes a term tm and tries to match it with
l and return |- tm = tm', where tm' is a version of r. Note that if we had a
conversional cnvl, we can produce a new conversion
cnvl (REWR_CONV th). Now
GEN_REWRITE_TAC : (conv -> conv) -> thm list -> tactic
and I believe that GEN_REWRITE_TAC cnvl [th1,...,thn]
applies the conversion cnvl (REWR_CONV thi) to the goal, for i = 1,...,n.
I hope I got that right. I can't understand the ref manual's description of
GEN_REWRITE_TAC, but simp.ml defines
let GEN_REWRITE_TAC cnvl thl = CONV_TAC(GEN_REWRITE_CONV cnvl thl);;
and
CONV_TAC : conv -> tactic, and CONV_TAC c is a tactic that applies c to the
goal.
Let's step through my proof of BINOMIAL_THEOREM:
needs "RichterHilbertAxiomGeometry/readable.ml";;
interactive_goal `;
∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
`;;
interactive_proof `;
∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))
[Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
MATCH_MP_TAC num_INDUCTION;
simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
intro_TAC ∀n, nThm;
rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL
ADD_ASSOC;
rewriteR ADD_SYM;
`;;
The last step used rewriteR = GEN_REWRITE_TAC (RAND_CONV)
which I'll pass over as being to easy and go on to the next step which uses a
more complicated GEN_REWRITE_TAC. To motivate the next step, look at the
left-hand argument of binary operator + in the rand (i.e. RHS of the equation)
of the goal:
(fst o (dest_binop `(+):num->num->num`) o rand)
`nsum (0..n) (\x'. x * binom (n,x') * x EXP x' * y EXP (n - x')) +
nsum (0..n) (\x'. y * binom (n,x') * x EXP x' * y EXP (n - x')) =
nsum (0..n) (\i. binom (n,i) * x EXP SUC i * y EXP (SUC n - SUC i)) +
1 * x EXP 0 * y EXP (SUC n - 0) +
nsum (0..n) (\i. binom (n,SUC i) * x EXP SUC i * y EXP (SUC n - SUC i))`;;
`nsum (0..n) (\i. binom (n,i) * x EXP SUC i * y EXP (SUC n - SUC i))`
I want to rewrite this with SUB_SUC and EXP, and we can do that using
rewriteRLDepth = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o DEPTH_CONV) and
LAND_CONV : conv -> conv
which applies a conversion to left-hand argument of binary operator. Evaluate
interactive_proof `;
rewriteRLDepth SUB_SUC EXP;
`;;
and the goal is now
`nsum (0..n) (\x'. x * binom (n,x') * x EXP x' * y EXP (n - x')) +
nsum (0..n) (\x'. y * binom (n,x') * x EXP x' * y EXP (n - x')) =
nsum (0..n) (\i. binom (n,i) * (x * x EXP i) * y EXP (n - i)) +
1 * x EXP 0 * y EXP (SUC n - 0) +
nsum (0..n) (\i. binom (n,SUC i) * x EXP SUC i * y EXP (SUC n - SUC i))`
I got my selective rewrite, and here's the rest of the proof:
interactive_proof `;
rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM
Nsum0SUC;
simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n ∧ 0 <= SUC n] LT
BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
simplify ARITH_RULE [k <= n ⇒ SUC n - k = SUC(n - k)] EXP MULT_AC;
`;;
let BINOMIAL_THEOREM = top_thm();;
val BINOMIAL_THEOREM : thm =
|- !n. (x + y) EXP n =
nsum (0..n) (\k. binom (n,k) * x EXP k * y EXP (n - k))
I want to explain this GEN_REWRITE_TAC command, as it looks backwards to me.
How did
fst o (dest_binop `(+):num->num->num`) o rand
turn into
RAND_CONV o LAND_CONV o DEPTH_CONV ?
The conversion
(RAND_CONV o LAND_CONV o DEPTH_CONV) c
applies the conversion
(LAND_CONV o DEPTH_CONV) c to the rand above, and this applies the conversion
DEPTH_CONV c
to the left-hand argument
`(nsum (0..n) (\i. binom (n,i) * x EXP SUC i * y EXP (SUC n - SUC i)))`
of binary operator +.
I'm not real clear on DEPTH_CONV, which applies a conversion repeatedly to all
the sub-terms of a term, in bottom-up order, but John used it the tutorial, and
it works here.
That was really hard work for me, and I think I'm a good mathematician. The
point is that we can read off what we wanted from the name rewriteRLDepth going
left to right:
take the operand, and take the left-hand argument of binary operator + of that,
and do a Depth rewriting on that.
For an exercise, let's redo the above GEN_REWRITE_TAC for practice, and get rid
of the DEPTH_CONV. First note that we can get the part we want to rewrite with
SUB_SUC and EXP with
(rand o rand o rand o snd o dest_abs o rand o fst o (dest_binop
`(+):num->num->num`) o rand)
`nsum (0..n) (\x'. x * binom (n,x') * x EXP x' * y EXP (n - x')) +
nsum (0..n) (\x'. y * binom (n,x') * x EXP x' * y EXP (n - x')) =
nsum (0..n) (\i. binom (n,i) * x EXP SUC i * y EXP (SUC n - SUC i)) +
1 * x EXP 0 * y EXP (SUC n - 0) +
nsum (0..n) (\i. binom (n,SUC i) * x EXP SUC i * y EXP (SUC n - SUC i))`;;
`SUC n - SUC i`
(fst o (dest_binop `(*):num->num->num`) o rand o snd o dest_abs o rand o fst o
(dest_binop `(+):num->num->num`) o rand)
`nsum (0..n) (\x'. x * binom (n,x') * x EXP x' * y EXP (n - x')) +
nsum (0..n) (\x'. y * binom (n,x') * x EXP x' * y EXP (n - x')) =
nsum (0..n) (\i. binom (n,i) * x EXP SUC i * y EXP (SUC n - SUC i)) +
1 * x EXP 0 * y EXP (SUC n - 0) +
nsum (0..n) (\i. binom (n,SUC i) * x EXP SUC i * y EXP (SUC n - SUC i))`;;
`x EXP SUC i`
So we need two new GEN_REWRITE_TAC commands and tactics:
let rewriteRLRARRR = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o
ABS_CONV o RAND_CONV o RAND_CONV o RAND_CONV);;
let rewriteRLRARL = GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o
ABS_CONV o RAND_CONV o LAND_CONV);;
rewriteRLRARRR SUB_SUC;
rewriteRLRARL EXP;
Here's the finished proof:
let BINOMIAL_THEOREM = theorem `;
∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
proof
∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))
[Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
MATCH_MP_TAC num_INDUCTION;
simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
intro_TAC ∀n, nThm;
rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL
ADD_ASSOC;
rewriteR ADD_SYM;
rewriteRLRARRR SUB_SUC;
rewriteRLRARL EXP;
rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM
Nsum0SUC;
simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n ∧ 0 <= SUC n] LT
BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
simplify ARITH_RULE [k <= n ⇒ SUC n - k = SUC(n - k)] EXP MULT_AC;
qed;
`;;
val BINOMIAL_THEOREM : thm =
|- !n. (x + y) EXP n =
nsum (0..n) (\k. binom (n,k) * x EXP k * y EXP (n - k))
--
Best,
Bill
------------------------------------------------------------------------------
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments & Everything In Between.
Get a Quote or Start a Free Trial Today.
http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
