Email Gateway (Aug 19 2022 at 09:15): Email Gateway (Aug 19 2022 at 09:15):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I recently had to check some very large proof using the code that was generated by Isabelle.
Unfortunately we have not been able to parse the proof within reasonable time.
Therefore, we started to profile our parser (which is written as an Isabelle function)
and we stumbled upon a strange hotspot: nat!
In Code_Integer we have the following code-equation:
lemma nat_code [code]:
"nat k = (if k ≤ 0 then 0 else
let
(l, j) = divmod_int k 2;
n = nat l;
l' = n + n
in if j = 0 then l' else Suc l')"
proof -
have "2 = nat 2" by simp
show ?thesis
apply (subst mult_2 [symmetric])
apply (auto simp add: Let_def divmod_int_mod_div not_le
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
apply (unfold 2 = nat 2)
apply (subst nat_mod_distrib [symmetric])
apply simp_all
done
qed
Is there any reason why this is so complex? I would imagine a much simpler equation where
the proof is also simple.
lemma [code]: "nat k = (if k ≤ 0 then 0 else Suc (nat (k - 1)))"
proof (cases k)
case (nonneg n)
show ?thesis unfolding nonneg
by (induct n, auto)
qed simp
Best regards,
René
Email Gateway (Aug 19 2022 at 09:15):From: René Neumann <rene.neumann@in.tum.de>
Why not something tail-recursive, which, under the assumption that the
compiler cannot optimize the above into something tail-recursive, should
perform even better (probably except for Haskell):
fun nat' :: "int ⇒ nat ⇒ nat" where
"nat' k accu = (if k ≤ 0 then accu else nat' (k - 1) (Suc accu))"
lemma nat'_correct:
"nat' k l = nat k + l"
proof (cases k)
case (nonneg n)
show ?thesis unfolding nonneg
by (induct n arbitrary: l) simp_all
qed simp
lemma [code]: "nat k = nat' k 0"
unfolding nat'_correct by simp
Email Gateway (Aug 19 2022 at 09:15):From: René Neumann <rene.neumann@in.tum.de>
Just for the fun, a simple test:
fun nat' :: "int ⇒ nat ⇒ nat" where
"nat' k accu = (if k ≤ 0 then accu else nat' (k - 1) (Suc accu))"
fun nat_th :: "int ⇒ nat" where
"nat_th k = (if k ≤ 0 then 0 else Suc (nat_th (k - 1)))"
ML {*
val y : IntInf.int = 70000000;
(* Tail-recursive approach *)
val t = Time.now ();
val _ = @{code nat'} y (@{code nat} 0);
val nat_tail = Time.- (Time.now (), t);
(* René Thiemann's approach *)
val t = Time.now ();
val _ = @{code nat_th} y;
val nat_th = Time.- (Time.now() , t);
(* approach from Code_Integer *)
val t = Time.now ();
val _ = @{code nat} y;
val nat = Time.- (Time.now(), t);
*}
Results:
val nat_tail = 9.403: Time.time
val nat_th = 28.333: Time.time
val nat = 9.594: Time.time
Here the difference between nat_tail and nat is neglegible. When running
the above multiple times, sometimes 'nat_tail' is a little better, other
times 'nat' is.
Email Gateway (Aug 19 2022 at 09:15):From: Brian Huffman <huffman@in.tum.de>
Note that if you import HOL/Library/Code_Nat.thy, which declares a
binary code representation for type nat, then the implementation of
function nat from Code_Integer is much faster than either nat' or
nat_th.
Email Gateway (Aug 19 2022 at 09:16):From: René Thiemann <rene.thiemann@uibk.ac.at>
Since my use-case is a more complex program in Haskell, I prefer my version,
but indeed for eager languages the tail-recursive variant is more plausible.
with nat (from library)
3.32 seconds
with my version of nat:
2.61 seconds
with your tail-rec. version of nat:
2.76 seconds
Best regards,
René
Email Gateway (Aug 19 2022 at 09:16):From: René Thiemann <rene.thiemann@uibk.ac.at>
Perhaps, then one can load this more complex nat-function only in "HOL/Library/Code_Nat.thy"?
Email Gateway (Aug 19 2022 at 09:25):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Brian,
Unfortunately, HOL/Library/Code_Nat.thy does not fully work in my case.
The following short example shows the problem:
theory Test
imports "~~/src/HOL/Library/Code_Nat"
begin
fun foo where
"foo xs 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"
export_code foo in Haskell file -
complains about
"Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
foo [] (Suc ?uu) ≡ False
Of course, I can drop the pattern matching on Suc, but I do not want to do that
manually for all my functions.
Cheers,
René
PS: The problem also occurs in the development version of Isabelle where
I imported Code_Binary_Nat instead of Code_Nat (changeset ad52ddd35c3a)
Email Gateway (Aug 19 2022 at 09:26):From: Brian Huffman <huffman@in.tum.de>
Hi René,
The ML setup in Code_Nat.thy is intended to automatically translate
away patterns involving Suc, so that you don't have to do it yourself.
Unfortunately the translation is kind of picky; it only works if for
each rule with a "Suc n" pattern, there is a matching rule with a "0"
pattern in its place. E.g. the following modification works with
Code_Nat.thy in Isabelle2012:
fun foo where
"foo [] 0 = True"
| "foo (x # xs) 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"
But instead of changing your code, please try out the attached version
of Code_Nat.thy, where I have modified the code preprocessor.
Florian: Perhaps you could look at my code and see whether it would be
suitable to check in to the development repo. It might still contain
some bugs; I haven't tested it on nested patterns like "Suc (Suc n)"
for example.
Email Gateway (Aug 19 2022 at 09:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Brian,
I will put this in my queue which at the moment is near denial of
service :-(. But note that the code originally is from Stefan.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:26):From: René Thiemann <rene.thiemann@uibk.ac.at>
fun foo where
"foo xs 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"export_code foo in Haskell file -
complains about
"Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
foo [] (Suc ?uu) ≡ FalseThe ML setup in Code_Nat.thy is intended to automatically translate
away patterns involving Suc, so that you don't have to do it yourself.
Unfortunately the translation is kind of picky; it only works if for
each rule with a "Suc n" pattern, there is a matching rule with a "0"
pattern in its place.
I understand.
E.g. the following modification works with
Code_Nat.thy in Isabelle2012:fun foo where
"foo [] 0 = True"
| "foo (x # xs) 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"But instead of changing your code, please try out the attached version
of Code_Nat.thy, where I have modified the code preprocessor.
Thanks Brian, for the new version of Code_Nat. Unfortunately, it works for foo,
but not for other functions. A minimized example that fails is as follows:
fun double :: "nat ⇒ nat" where
"double 0 = 0"
| "double n = n + n"
export_code double in Haskell file -
Constructor as head in equation:
nat_of_num ?n ≡ plus_nat_inst.plus_nat (pred_numeral ?n) (nat_of_num num.One)
René
Email Gateway (Aug 19 2022 at 09:27):From: Brian Huffman <huffman@in.tum.de>
This took me a minute to figure out! In this example double.simps
actually contains the rule "double (Suc n) = Suc n + Suc n". Since the
RHS mentions "Suc" we must also generate code for "Suc" as well, which
is where the problem starts.
In the code equation for Suc, "Suc n = n + 1", my code preprocessor
incorrectly translates away the Suc on the LHS. I attach an updated
version that fixes this.
However, after some more thought I don't think that my general
approach will work at all for patterns like "Suc (Suc n)"; in the long
run we'll probably have to stay with a code preprocessor like the
current one, which can combine multiple equations into single ones
that use if-then-else or case.
Email Gateway (Aug 19 2022 at 09:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
the observation made by Brian has indeed been the primary motiviation
for this »representation-ignorant binary digit scanning« equation.
There is a high chance that this could be changed in a similar way you
suggest. However, there is a reform of all that code generation
arithmetic stuff ongoing, and this particular issue cannot be dealt in
isolation with within the distribution. So, I would recommend to
declare this code equation in your particular application until this
reform shows up in a release (it is very likely that this will not be
the upcoming release).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:28):From: Makarius <makarius@sketis.net>
Just some side-remarks about the Isabelle/ML that is quoted above:
* Type int is always the normal mathematical one, i.e. IntInf and Int
coincide. (There are some special tricks to make the different SML
implementations underlying Isabelle/ML agree on this.)
* Structure Timing provides some tools for timing, notably the classic
timeit and timeap combinators. Since timing on multicore hardware
is difficult to get right, it currently prints elapsed / CPU / GC time
to give some starting points for further guessing. (In any case it is
the standard library entry for that, so when better timing mechanisms
become available they will be integrated here.)
Makarius
Email Gateway (Aug 19 2022 at 09:29):From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Florian,
This is perfectly fine for me. I can easily install my code-equation
and will also wait on other changes in arithmetic. Anyway, my main
motivation for posting my observation was that if one does not know
about Code_Nat one obtains strange-looking code for "nat".
Cheers,
René
Email Gateway (Aug 19 2022 at 10:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
Thanks Brian, for the new version of Code_Nat.
see now http://isabelle.in.tum.de/repos/isabelle/rev/0a2371e7ced3
It is now possible, in theory Code_Binary_Nat, to drop the dependency on
the venerable preprocessor by Stefan Berghofer (theory
Code_Abstract_Nat) and install this specific preprocessor instead.
However, after some more thought I don't think that my general
approach will work at all for patterns like "Suc (Suc n)"; in the long
run we'll probably have to stay with a code preprocessor like the
current one, which can combine multiple equations into single ones
that use if-then-else or case.
Also the preprocessor from Code_Abstract_Nat cannot compile away all
patterns: it always needs 0/Suc twins to proceed.
Cheers,
Florian
signature.asc
Last updated: Apr 19 2024 at 04:17 UTC