Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)



Hi Peter and Peter,

The termination proof methods (lexicographic_order and size_change) use the [measure_function] theorems to generate all candidate functions in a Prolog style. If this rule for size_prod is added globally, then these methods will try many more candidates for functions which use pairs. In detail, every tuple argument gets two changes, namely with "size" and with "size_prod ... ...". In case of nested tuples, this lead to quadratically many candidates. Accordingly, the matrix output by a failing lexicographic order may become harder to read because there are more columns and more failed goals.

My feeling would be that it would not make a big difference for most function definitions, but some could experience a significant slow-down. AFAIK, the size plugin of the datatype package does not generate these [measure_function] theorems for the size_F functions, either, probably for the same reason.

Andreas

On 15/08/17 17:56, Peter Lammich wrote:
On Di, 2017-08-15 at 12:14 +0200, Tobias Nipkow wrote:
I learned about

lemma [measure_function]: "is_measure f â is_measure g â is_measure
(size_prod f g)"
by (rule is_measure.intros)

from Peter Lammich who probably uses it more often. He may have some
insight as
to the dangers of using this by default.

I have not used this very often, too. Only for small isolated examples,
but not in the basis of some big developments.

Nevertheless, I would be curious what would happen if one adds this
lemma by default (e.g. to Main)


--
   Peter



Not that the recursive function need not be tupled for this to help
because
internally the arguments are tupled anyway.

It would indeed be nice if this were mention in the "function
manual". In case
somebody feel sufficiently au fait with this feature ...

Tobias

On 14/08/2017 18:05, Lars Hupel wrote:


Another question for you and Andreas: what is the substantive
difference in intent between Finite_Map and FinFun? I used
Finite_Map as I needed the BNF setup, but I reached for FinFun
first as I knew it was there. In the fullness of time, could they
perhaps be merged?
Here's a mailing list thread on that issue:
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September
/msg00015.html>.


And another, but perhaps more directly for the BNF people: Iâve
been tripped up on products uniformly having a constant size a
few times now. Hereâs a quick theorem search:

    Basic_BNF_LFPs.prod.size(2): size (?x1.0, ?x2.0) = Suc 0

Could it too be made more useful by returning the sum of the
sizes of its arguments?
There is such a function: "size_prod". However, you have to tell
the
function package about it.


(These arose in termination arguments, and the fun package seems
to avoid using size on products. I wonder if such a change would
impact it.)
Here's a contrived example:

fun contrived :: "('a list à 'a list) â ('a list à 'a list)" where
"contrived (xs, y1 # y2 # ys) = contrived (y1 # xs, ys)" |
"contrived (x1 # x2 # xs, ys) = contrived (xs, x1 # ys)" |
"contrived _ = ([], [])"

By default, the function package won't be able to derive a
termination
measure for this. But you can add the following before the
definition:

lemma [measure_function]: "is_measure (size_prod size size)"
by (rule is_measure.intros)

There's probably a good reason why this doesn't happen by default.
(Possibly time complexity of the termination prover.) If this thing
keeps happening to you (or you need nesting), try this:

lemma [measure_function]: "is_measure f â is_measure g â is_measure
(size_prod f g)"
by (rule is_measure.intros)

This might mess up things elsewhere though, so try it at your own
risk.

Cheers
Lars






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.