> I bet the information that p, q, and m have type num is stored somewhere.
> I know we can infer the type num from the assumptions, but that's not
always true.
> Can you tell me where this type information is stored?
Every occurrence of a variable in HOL includes the type of the variable.
You can
think of a variable v:ty as being a pair ("v",ty). There are only 4 classes
of terms
in HOL: variable, constant, application, and lambda. These may be
implemented
in any way one wants, but the interface to the abstract type of terms uses
only
mk_var, dest_var, is_var
mk_const, dest_const, is_const
mk_comb, dest_comb, is_comb
mk_abs, dest_abs, is_abs
Looking at the typing of dest_var
dest_var : term -> string * hol_type
tells you immediately that the types of variables are---from the point of
view of clients
of the abstract type of term---held at the occurrences.
Konrad.
On Sat, Apr 27, 2013 at 11:00 PM, Bill Richter <
rich...@math.northwestern.edu> wrote:
> Vince, I think you just explained to me that I've been misunderstanding
> HOL all along! What I'd been asking about environment and scope of
> variable sounds now like the simple fact that HOL allows free variables. I
> think that means that FOL is actually quite different than the way
> mathematicians think, even though it amounts to the same proofs.
>
> I still don't understand why you want to avoid preterms.
>
> Let me answer this question, and then explain my HOL misunderstanding, by
> going back to my earlier post about quotexpander. It's worth going through
> again to highlight John's related preterm code.
>
> You proposed a modification of quotexpander in system.ml using "." at the
> start indicate a preterm. I got a lot out of your proposal, and came up
> with my own modification, where "\"" at the start indicates a string:
>
> let quotexpander s =
> if s = "" then failwith "Empty quotation" else
> let c = String.sub s 0 1 in
> if c = "\"" then
> "\""^(String.escaped (String.sub s 1 (String.length s - 1)))^"\"" else
> if c = ":" then
> "parse_type \""^
> (String.escaped (String.sub s 1 (String.length s - 1)))^"\""
> else if c = ";" then "parse_qproof \""^(String.escaped s)^"\""
> else "parse_term \""^(String.escaped s)^"\"";;
>
> Modify quotexpander this way and then start a new HOL Light process by
> ocaml
> #use "hol.ml";;
> Then the code included below works. The definitions of consider and
> case_split there are quite simple.
>
> But I can also define case_split using preterms, with this code:
>
> let parse_qproof s = (fst o parse_preterm o lex o explode)
> (String.sub s 1 (String.length s - 1));;
>
> let case_split sDestruct pretermDisjlist tac =
> let disjthm = (term_of_preterm o (retypecheck [])) (end_itlist
> (fun pt1 pt2 -> (Combp (Combp (`;\/`, pt1), pt2))) pretermDisjlist) in
> SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
> (DESTRUCT_TAC sDestruct);;
>
> I think that's a lot more complicated than my string version below, and I
> could not define consider using preterms.
>
> However, I realized last night that John did more complicated preterm
> stunts in Examples/mizar.ml
>
> (*
> ------------------------------------------------------------------------- *)
> (* Some preterm operations we need.
> *)
> (*
> ------------------------------------------------------------------------- *)
>
> let rec split_ppair ptm =
> match ptm with
> Combp(Combp(Varp(",",dpty),ptm1),ptm2) -> ptm1::(split_ppair ptm2)
> | _ -> [ptm];;
>
> let pmk_conj(ptm1,ptm2) =
> Combp(Combp(Varp("/\\",dpty),ptm1),ptm2);;
>
> let pmk_exists(v,ptm) =
> Combp(Varp("?",dpty),Absp(v,ptm));;
>
> John's version of consider there is better than mine, but it's a lot more
> complicated. BTW let me say that John's mizar.ml predates Freek's
> Mizar-like code written, and it's only 682 lines long, and I counted 160 of
> those lines as defining John's Mizar-like by justification, and I don't
> want that. So that's only 522 of code that I have to understand. I can't
> believe it's that hard to understand?
>
> Maybe I don't get your question here, because it looks more complex
> than I thought.
>
> Maybe I've been misunderstanding HOL Light! I've been thinking that
> various occurences of the same variable had the same value, but maybe I had
> it all wrong. Let's go through the code below, which is my version of the
> tutorial proof of the irrationality of sqrt.
>
> After the first 3 lines, we have fixed the variables p & q (of type num),
> the goal is
>
> q = 0
>
> and we have two labeled assumptions
>
> 0 [`!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)`] (A)
> 1 [`p * p = 2 * q * q`] (B)
>
> Now a mathematicians would think this means that we have chosen arbitrary
> elements of the set that num denotes, and that the variables p and q will
> refer to these fixed, but arbitrary, elements from now on. But I think
> that's not what HOL is doing! I think HOL is just saying that the
> assumptions and the goals are now written in terms of the free variables p
> & q. And I guess HOL and FOL are designed this way because that's the way
> math works, but I never saw that before.
>
> The next SUBGOAL_TAC command uses assumption B and easily gives as a new
> assumption
>
> 2 [`EVEN (p * p) <=> EVEN (2 * q * q)`]
>
> The next SUBGOAL_TAC command uses this last assumption, theorems ARITH and
> EVEN_MULT to prove the new assumption
>
> 3 [`EVEN p`]
>
> I guess that's true for any free variables p & q of type num! The next
> consider command fixes the variable m of type num and gives us the labeled
> assumption
>
> 4 [`p = 2 * m`] (C)
>
> Basically MESON proved that such an m exists using theorem EVEN_EXISTS.
> So now we have three free variables p, q, and m which all have type num,
> and 5 assumptions about p, q, and m, but I think now that p, q, and m are
> just free variables. Now I have a question for you:
>
> I bet the information that p, q, and m have type num is stored somewhere.
> I know we can infer the type num from the assumptions, but that's not
> always true. Can you tell me where this type information is stored?
>
> Now I do
>
> e(case_split "qp | pq" [`"(q:num) < p`; `"p <= q`] [ARITH_TAC]);;
>
> This gives two cases, with labels qp and pq, and I can do this because
> ARITH_TAC proves that for all p & q of type num, either q < p or p <= q. I
> think now that there's no connection here between this p & q and the p & q
> above that I think are "fixed". Since my proof is interactive, I now work
> the first case, which has a new assumption
>
> 5 [`q < p`] (qp)
>
> The next SUBGOAL_TAC command gives us the new assumption
>
> 6 [`q * q = 2 * m * m ==> m = 0`]
>
> I think MESON's proof only needs the two free variables p and q and the
> assumptions qp and A. I think MESON just instantiates the !m. m < p of
> assumption A with m = q, which is true by assumption qp. Then the
> consequent of assumption A becomes, after an alpha conversion
>
> (!z. q * q = 2 * z * z ==> z = 0)
>
> and MESON can then instantiate z with m to get our assumption 6 above.
> Note that this entire argument has nothing to do with any "fact" that p, q
> and m denote fixed elements of the set denoted by the type num. It's just
> FOL using the free variables p, q & m, promoted to HOL by the typing, and
> assumptions qp and A. Wow. How could I have misunderstood this all along!
>
> Let's see how the next NUM_RING_thmTAC command proves the goal q = 0 using
> these 3 assumptions:
>
> 1 [`p * p = 2 * q * q`] (B)
> 4 [`p = 2 * m`] (C)
> 6 [`q * q = 2 * m * m ==> m = 0`]
>
> We have free variables p, q and m and these 3 statements. B and C give
> p^2 = 2q^2 and p = 2m, so
>
> 4 m^2 = 2 q^2
>
> q^2 = 2 m^2
>
> Assumption 6 then gives m = 0. By C, p = 0 and then by B,
>
> 2 q^2 = 0,
>
> so q = 0. NUM_RING can perform this sort of nonlinear deduction. Now
> we're working the other case
>
> 5 [`p <= q`] (pq)
>
> The next SUBGOAL_TAC command uses this last assumption and the theorem
> LE_MULT2 to prove
>
> 6 [`p * p <= q * q`]
>
> and surely this is true for any free variables p and q of type num.
> There's no reason to think that HOL Light is remembering that p and q
> denote fixed natural numbers that we've been using all along!
>
> The next SUBGOAL_TAC command deduces
>
> 7 [`q * q = 0`]
>
> from this last assumption and B:
>
> 1 [`p * p = 2 * q * q`] (B)
> 6 [`p * p <= q * q`]
>
> That is, ARITH_TAC can prove that for any free variables p & q, that if
>
> 2 q^2 <= q^2
>
> then q = 0. Nothing about HOL Light is remembering our fixed natural
> numbers p & q!
>
> Now NUM_RING proves the goal. But surely we believe that for any free
> variable q of type num that
> q = 0
> if q^2 = 0.
>
> --
> Best,
> Bill
>
> let consider vars_t prfs lab =
> let len = String.length vars_t in
> let rec findSuchThat = function
> n -> if String.sub vars_t n 9 = "such that" then n
> else findSuchThat (n + 1) in
> let n = findSuchThat 1 in
> let vars = String.sub vars_t 0 (n - 1) and
> t = String.sub vars_t (n + 9) (len - n - 9) in
> let tm = parse_term ("?" ^ vars ^ ". " ^ t) in
> match prfs with
> p::ps -> (warn (ps <> []) "Consider: additional subproofs ignored";
> SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
> THENL [p; ALL_TAC])
> | [] -> failwith "Consider: no subproof given";;
>
> let case_split sDestruct sDisjlist tac =
> let rec list_mk_string_disj = function
> [] -> ""
> | s::[] -> "(" ^ s ^ ")"
> | s::ls -> "(" ^ s ^ ") \\/ " ^ list_mk_string_disj ls in
> let disjthm = parse_term (list_mk_string_disj sDisjlist) in
> SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
> (DESTRUCT_TAC sDestruct);;
>
> let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;;
> let NUM_RING_thmTAC = TACtoThmTactic (CONV_TAC NUM_RING);;
> let ARITH_thmTAC = TACtoThmTactic ARITH_TAC;;
> let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;
>
> g `!p q. p * p = 2 * q * q ==> q = 0`;;
> e(MATCH_MP_TAC num_WF);;
> e(INTRO_TAC "!p; A; !q; B");;
> e(SUBGOAL_TAC "" `EVEN(p * p) <=> EVEN(2 * q * q)`
> [HYP MESON_TAC "B" []]);;
> e(SUBGOAL_TAC "" `EVEN(p)` [so (MESON_TAC [ARITH; EVEN_MULT])]);;
> e(consider `"m such that p = 2 * m`
> [so (MESON_TAC [EVEN_EXISTS])] "C");;
> e(case_split "qp | pq" [`"(q:num) < p`; `"p <= q`] [ARITH_TAC]);;
> e(SUBGOAL_TAC "" `q * q = 2 * m * m ==> m = 0` [HYP MESON_TAC "qp A" []]);;
> e(so (HYP NUM_RING_thmTAC "B C" []));;
> e(SUBGOAL_TAC "" `p * p <= (q:num) * q` [so (MESON_TAC [LE_MULT2 ])]);;
> e(SUBGOAL_TAC "" `q * q = 0` [so (HYP ARITH_thmTAC "B" [])]);;
> e(so (NUM_RING_thmTAC []));;
> let NSQRT_2 = top_thm();;
>
>
> ------------------------------------------------------------------------------
> Try New Relic Now & We'll Send You this Cool Shirt
> New Relic is the only SaaS-based application performance monitoring service
> that delivers powerful full stack analytics. Optimize and monitor your
> browser, app, & servers with just a few lines of code. Try New Relic
> and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
