Re: [Hol-info] proof replay?
When I try it in HOL Light on my machine it takes about 0.074 seconds, which is around 250 million CPU cycles according to the clock speed from "lscpu". This is the same order of magnitude that Dan was seeing. On the whole, the procedures like INT_ARITH are mostly fast enough for everyday interactive proofs, but may not be suited for cases where efficiency really matters. There are certain fundamental limitations on how fast one can get, subject to the need to produce a formal proof (particularly given that HOL Light requires arithmetic calculation to be done by inference). Nevertheless one can usually do a lot better than the everyday tactics, with a bit of effort. One place to look would be the work Alexey Solovyev did for the Flyspeck inequalities, which is in the HOL Light directory: Formal_ineqs/ That is often capable of proving large real linear inequalities amazingly quickly. But there may also be some more specific optimizations that would apply to Dan's problems or might suit them better, particularly if it is "small easy inequalities solved huge numbers of times". And yes, parsing and typechecking is usually even slower, so you would definitely want to avoid that in the inner loop if possible. John. On Thu, Jan 28, 2021 at 5:05 PM Konrad Slind wrote: > Just for clarification: the HOL4 term parser handled the supplied term > without alteration, and > intLib.ARITH_CONV is the HOL4 analog of INT_ARITH. > > > > > On Thu, Jan 28, 2021 at 6:59 PM Konrad Slind > wrote: > >> Also, there seems to be some inefficiency: the posted formula gets proved >> quite quickly in HOL4: >> >> Count.apply ARITH_CONV tm; >> runtime: 1.2s,gctime: 0.77200s, systime: 0.0s. >> Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 493764; Total: 493764 >> val it = >>⊢ 193650890589077504 * (2 * y + 1) ≤ >> 47942158315484610560 * (2 * x + 1) + 135203236847161865141 ∧ >> 0 ≤ >> 2655641718416121605914624 * (2 * x + 1) + >> 2208414543647439060992 * (2 * y + 1) + 6004289407548407186399935 ⇒ >> 0 ≤ >> 13137886070707932161376256 * (2 * x + 1) + >> 17509226798704706453504 * (x + y + 1) + 36152178747194683600721967 ⇔ >> T: >>thm >> >> On Thu, Jan 28, 2021 at 6:57 PM Konrad Slind >> wrote: >> >>> HOL4 has a notion of persistent theory, so you could spawn many >>> parallel sessions, each delivering a theory with one result, then >>> create a single descendant theory, import all the parent >>> theories, and chain your implications or inequalities there. >>> >>> It also provides integer decision procedures, so the calls to >>> INT_ARITH might possibly be directly substitute-able. >>> >>> Konrad. >>> >>> >>> On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein >>> wrote: >>> Thanks for the references and suggestions. As a scaled-down example of part of the time consumption, this takes 400 million CPU cycles: INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1) <= &47942158315484610560 * (&2 * (x:int) + &1) + &135203236847161865141 /\ &0 <= &2655641718416121605914624 * (&2 * x + &1) + &2208414543647439060992 * (&2 * y + &1) + &6004289407548407186399935 ==> &0 <= &13137886070707932161376256 * (&2 * x + &1) + &17509226798704706453504 * (x + y + &1) + &36152178747194683600721967`;; Hand proof: take 653244900095080313091/700376017867732114912 and 26794012414555294513937/5603008142941856919296 times the first and second inequalities, add, and observe that you now have a stronger version of the conclusion, offset by 1581608968911709059178093879/256. Changing INT_ARITH to g still takes around 100 million CPU cycles, which makes me wonder whether there's some bottleneck in parsing or printing. The code that I wrote to do a bunch of searching to find and print the whole sequence of relevant presumed theorems is, with no optimization effort, thousands of times faster than this. Of course that code doesn't have to bother with the symbolic aspects of proof manipulation. ---Dan ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info >>> ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] permutations of {0,1,...,n-1}
Hi Dan,
| Newbie question: In HOL Light (or in another variant of HOL if that has
| an easier answer), how should I define permutations of {0,1,...,n-1}?
There are a couple of HOL Light library files defining notions of
permutation, the first giving permutations on sets:
Library/permutations.ml
and the second giving permutations on lists
Permutations/*.ml
In your application I think the set one may be more relevant. This
tries to get a somewhat natural and well-behaved notion while sticking
to total functions (exactly the problematic issue you noted). This
is done by specifying that the function be the identity outside the
"domain". Thus, the main notion is "p permutes s", defined as:
p permutes s <=> (!x. ~(x IN s) ==> p(x) = x) /\ (!y. ?!x. p x = y)
For example, you could say in your setting
p permutes {i:num | i < n}
or if you don't mind offsetting the indices:
p permutes (1..n)
Alas "p permutes (0..n-1)" doesn't quite mean what one might hope
in the case n=0 since subtraction over N gives 0-1=0. One could use
Z instead as the indexing type but this looks uglier and has less
pre-proved machinery about number segments. Or maybe you never
want n-0 anyway, in which case it's fine.
John.
On Wed, Sep 9, 2020 at 3:10 AM D. J. Bernstein wrote:
> Newbie question: In HOL Light (or in another variant of HOL if that has
> an easier answer), how should I define permutations of {0,1,...,n-1}?
>
> The context I'm starting from is that a "Benes network" is a particular
> map from fixed-length bit sequences to permutations of {0,1,...,n-1}
> when n is a power of 2. It starts with conditionally swapping 0<->1,
> 2<->3, etc., then 0<->2 etc., continuing up and then down powers of 2.
> I've written detailed proofs for a fast parallel algorithm that computes
> suitable bits given a permutation. I'm trying to figure out how easily
> these proofs can be computer-verified with current tools.
>
> The definition of a Benes network is most easily expressed in terms of
> {0,1,...,n-1}. The algorithm has special roles for the even and odd
> elements of {0,1,...,n-1}, and uses comparisons to compute the minimum
> element of each cycle of a permutation, and then in the recursion
> divides indices by 2, so it seems pointless to generalize beyond
> {0,1,...,n-1}; the numbers have useful roles here.
>
> So far the four answers I've found that seem to be local minima in the
> "how complicated is the theorem statement" metric are the following:
>
>* Follow the usual mathematical definition, where a permutation of X
> is a function from X to X having an inverse. My understanding is
> that HOL variants generally don't support dependent types such as
> {0,1,...,n-1} depending on n; ergo, set-theoretically build these
> functions as subsets of num^2 satisfying certain conditions, define
> compositions of such functions, and define inverses.
>
>* Reformulate the theorems as being about permutations of any set X
> that has a specified bijection to {0,...,n-1}. I see that there's
> machinery _sort of_ handling this, the arbitrary $ bijection from
> {1,...,dimindex(:X)} to X when X is finite, and it's not a big deal
> to shift the indices by 1; but an arbitrary bijection is not a
> specified bijection, so matching this up to (say) software would
> then require another step to invert the arbitrary bijection. More
> to the point, whether it's specified or arbitrary, the bijection is
> making the theorem statement conceptually more complicated.
>
>* Describe permutations as lists satisfying certain conditions, as in
> Permutation/permutation.ml. This is a good match to the simplest
> software representation of a permutation as a list of its values,
> but again it seems to require separately defining composition etc.
> In set theory I'd expect the list (pi(0),pi(1),...,pi(n-1)) to be
> defined as the function x|->pi(x), which is exactly pi, and I don't
> terribly mind setting this up as a correspondence instead of an
> identity, but again the function wants the type {0,1,...,n-1}.
>
>* The applications I have in mind actually need only specific values
> of n such as n=8192. I understand that for each specific n I can
> build an explicit type with n elements, and then unroll the
> recursion across n. This would require the basic features of
> integers to be replicated across each of the explicit types.
>
> My objective here is high assurance, so I like what HOL Light and HOL
> Zero say about small kernels increasing the assurance level for the
> proofs, but I also want high assurance that the theorem statements are
> what's desired. Even a complete chain of
>
>* verifying that an algorithm computes b |-> Benes(b),
>* verifying that software implements this algorithm,
>* verifying that an algorithm computes pi |-> Bits(pi),
>* verifying that software implements
Re: [Hol-info] Using @ for multiple selections in HOL Light
Yes, here's one explicit HOL Light realization of Konrad's solution: let POLYNOMIAL_DEGREE_COEFFS = let th = prove (`?m c. !p. polynomial_function p ==> !x. p x = sum(0..m p) (\i. c p i * x pow i)`, REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[polynomial_function]) in REWRITE_RULE[RIGHT_IMP_FORALL_THM] (new_specification ["polynomial_degree"; "polynomial_coeffs"] th);; This gives you the following theorem val POLYNOMIAL_DEGREE_COEFFS : thm = |- !p x. polynomial_function p ==> p x = sum (0..polynomial_degree p) (\i. polynomial_coeffs p i * x pow i) Instead of this direct Skolemization you could instead choose to define these concepts in a more refined way with minimal degree and coefficients having a zero tail, something like this: let polynomial_deg = new_definition `polynomial_deg p = minimal m. ?c. !x. p x = sum(0..m) (\i. c i * x pow i)`;; let polynomial_cfs = new_definition `polynomial_cfs p = \i. if i <= polynomial_deg p then (@c. !x. p x = sum(0..polynomial_deg p) (\i. c i * x pow i)) i else &0`;; let POLYNOMIAL_DEG_CFS = prove (`!p x. polynomial_function p ==> p x = sum (0..polynomial_deg p) (\i. polynomial_cfs p i * x pow i)`, REPEAT GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN GEN_REWRITE_TAC LAND_CONV [MINIMAL] THEN REWRITE_TAC[GSYM polynomial_deg] THEN DISCH_THEN(MP_TAC o SELECT_RULE o CONJUNCT1) THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN SIMP_TAC[polynomial_cfs]);; But the main point is again that once you've got this and maybe a few other lemmas, you probably don't need much if any manual handling of select-terms at all. John. On Tue, Feb 18, 2020 at 5:09 PM Konrad Slind wrote: > If you have |- !p. ?m c. ... as a theorem, then you are set up to use > constant specification. Just have to apply SKOLEM_THM to move the > existentials out to the top level . > > Konrad. > > > On Tue, Feb 18, 2020 at 4:33 PM Norrish, Michael (Data61, Acton) < > michael.norr...@data61.csiro.au> wrote: > >> Maybe use the choice function to select a pair. I.e., write >> >> @(m,c). . >> >> ? >> >> Michael >> >> On 19 Feb 2020, at 09:30, "jpe...@student.bham.ac.uk" < >> jpe...@student.bham.ac.uk> wrote: >> >> >> Hi >> >> This is a question about using the select operator @ to return multiple >> values which depend on each other in HOL Light. >> >> For example when working with polynomial_function defined as >> polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i) >> it might be useful to be able to use the @ operator to return the >> upper bound m and the coefficient function c, however as the choice of m >> depends on c and visa versa you cannot use 2 separate select statements. >> (e.g. if m > degree(p) then c(n) must be 0 for degree(p)> >> What is the best way to approach this? Is there a way to return both of >> the values or would they have to be "combined together" inside the select >> statement? >> >> Thanks >> >> James >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
