Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Non-idempotence of datatype constructors


view this post on Zulip Email Gateway (Aug 23 2022 at 09:00):

From: Manuel Eberl <eberlm@in.tum.de>
This is one for our datatype experts:

I just noticed that theorems like

Cons x xs ≠ xs

are not automatically provided by the datatype package although they
should clearly hold for any datatype. To be more precise, I am talking
about theorems of the form

C x1 … xn ≠ x1

C x1 … xn ≠ xn

for any n-ary datatype constructor C (and of course also the flipped
variant).

I'm not sure how useful something like this is in practice and it's
fairly easy to prove these by hand when needed. I just ran into a
situation where I had an assumption of the form "C a b ≠ b" and was
surprised that the simplifier didn't take care of it automatically.

I realise that the datatype package already provides an absurd number of
theorems and one should be careful to blow it up even more, but seeing
as the number of theorems to be generated is linear in the number of
constructors and they're probably very easy to prove, one could consider
it. Or perhaps at least as an optional plugin or standalone tool.

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:02):

From: Tobias Nipkow <nipkow@in.tum.de>
I do think such rules are useful, esp if they are there by default. I suggest
they are best handled by a simproc that is triggered by any "(=)" but that
checks immediately if the two argumenst are of the appropriate type and form.
That can be done very quickly (there are similar simprocs already). The simproc
should work for any datatype and any degree of nesting of the constructors.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Manuel Eberl <eberlm@in.tum.de>
That sounds like a good idea.

However, if such a simproc is to work for any nesting of
constructors,having pre-proven theorems for every constructor will not
be enough.Instead, I suppose one would have to introduce a
"proper-subexpression"relation for datatypes (e.g. xs < Cons x xs) along
with a proof thatthis relation has the obvious properties (irreflexive,
asymmetric,transitive).

I guess that is something that only a datatype package plugin similar
tothe one for the "size" function could provide. Having looked at the
codebriefly, I think only the people who wrote the BNF package could (or
atleast should) implement that.

Alternatively, one could just use the size function (as someone
alreadysuggested in this thread) to get pretty much the same thing,
except thatit won't work for all datatypes (e.g. infinitely branching ones).

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Tobias Nipkow <nipkow@in.tum.de>
A first version which only deals with depth 1 would already cover most of the
practical cases.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Manuel Eberl <eberlm@in.tum.de>
True, but after your suggestion, I realised that the solution with the
"proper subexpression" relation (or, alternatively, the size function)
combined with a simproc that produces these theorems on the spot is
actually the superior approach in every respect. It's simpler, more
general, and probably more performant.

I can try to come up with a proof-of-concept implementation using the
size function approach, since that needs no additional new features from
the BNF package.

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Manuel Eberl <eberlm@in.tum.de>
I attached a proof of concept (works with Isabelle 2020) using the
simple size-based approach, including some example applications.

It works well, although I'm not sure what the proper way to get the
datatype information is (e.g. the list of all the constructors of the
datatype and the associated other datatypes in case of mutual recursion).

Is the ML interface of the BNF package documented anywhere (in
particular this aspect)?

Manuel
Foo.thy

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Manuel Eberl <eberlm@in.tum.de>
Unfortunately, the simproc breaks a few things in the AFP.

One of them is the proof of viewL_correct in Finger-Trees.FingerTree,
where a call to "auto" loops (it also loops when changing it to "simp").

It's not an implementation problem of my simproc either. When I disable
the simproc and add the theorems

"Node3 a b c d ≠ b" "Node3 a b c d ≠ c" "Node3 a b c d ≠ d"

to the simpset instead, it also loops.

These rules look perfectly harmless to me, so my suspicion would be that
the simpset in this theory was fragile all this time and these new rules
simply exposed that. However, I couldn't find any problematic-looking
simp rules either, so perhaps it's some premise that the simplifier adds
to the simpset itself.

After inspecting the trace, it seems that the simplifier tries to apply
the following rule over and over again:

[1]Adding rewrite rule "??.unknown":
nodeToList nd2 = [] ∧ nodeToList nd3 = [] ⟹
False ⟹
undefined = n_unwrap nd1 ⟹
is_leveln_node 0 nd1 ⟹ is_measured_node nd1 ⟹ nodeToList nd1 ≡ [undefined]

(plus a few other variants of this with other permutations of nd1, nd2,
nd3, so I guess it loops when trying to rewrite the first premise)

I find this a bit odd. Why does the simplifier add something that has
"False" in its premises to the simpset in the first place? Shouldn't
this entire thing get rewritten to "True" and discarded before that happens?

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:04):

From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Manuel,

while your code works for the examples you show, it does not seem to handle nested recursion. See code below, with your simproc enabled. Also I would register it only for types that belong to the size class, i.e.,

simproc_setup datatype_no_proper_subterm ("(x :: 'a :: size) = y") = ‹K datatype_no_proper_subterm_simproc›

Your retrieval of mutual types looks reasonable to me. As usual with Isabelle/ML, the most reliable documentation is the code.

I am sympathetic to the proposal of having a 'proper subexpression' ordering defined for all datatypes (e.g., via a plugin similarly to size). Its usefulness goes beyond the acyclicity rules which this thread is about. In particular, the 'proper subexpression' ordering can be used for 'strong induction' or to prove termination of functions in cases when size does not exists. (Provided that we also have the fact that this ordering is wellfounded proved.) Something along the following lines:

class subexp =
fixes subexp :: "'a ⇒ 'a ⇒ bool" (infixl "⊏" 65)
assumes wf: "wfP subexp"

declare [[typedef_overloaded]]

bnf_axiomatization 'a F [wits: "'a F"]

datatype x = Ctor "x F"

instantiation x :: subexp begin

definition subexp_x :: "x ⇒ x ⇒ bool" where
"subexp_x = tranclp (λx y. case y of Ctor f ⇒ x ∈ set_F f)"

instance
apply intro_classes
apply (unfold subexp_x_def)
apply (rule wfP_trancl)
apply (rule wfPUNIVI)
subgoal premises prems for P x
apply (induct x)
apply (rule prems[rule_format])
apply (simp only: x.case)
done
done

end

But one would like to have some reasonable simp rules for subexp_x (which may be as hard as the original problem that you are trying to solve). In particular, if F is itself a datatype that belongs to the subexp type class, its notion of subexp should be linked to the one of x.

Dmitriy

datatype 'a rtree = Leaf | Node 'a "'a rtree list"

lemma "Node x (a # xs) ≠ a"
apply simp? ―‹no_change›
apply (rule size_neq_size_imp_neq)
apply simp
done

lemma "Node x [c,a,b] ≠ a"
apply simp? ―‹no_change›
apply (rule size_neq_size_imp_neq)
apply simp
done

view this post on Zulip Email Gateway (Aug 23 2022 at 09:04):

From: Manuel Eberl <eberlm@in.tum.de>
Hello,

we're talking about Isabelle datatypes here, which are always finite
(final algebras is the categorial interpretation). The Haskell
interpretation is actually a codatatype (the final coalgebra) and
calling them "datatypes" is, in my opinion, actually a bit non-standard.
But it makes sense given the lazy semantics of Haskell.

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:04):

From: Manuel Eberl <eberlm@in.tum.de>
On 03/05/2020 11:46, Traytel Dmitriy wrote:

while your code works for the examples you show, it does not seem to handle nested recursion.

Yes, I am aware of that. Nested datatypes make things considerably more
complicated, so I'd rather not support that for now. I'd have to

  1. somehow figure out /all/ the other datatypes involved in the
    definition of my datatype and

  2. figure out a robust way to expand their size functions.

I have no idea how to do 1 with the information provided by the BNF
package (other than inspecting the types of the constructors to figure
out the nesting).

I also have no idea how to do 2 properly – the "size" plugin provides
some information with BNF_LFP_Size.size_of, but oddly enough it only
provides the equations for the "regular" size function "size", but not
for the generalised one (e.g. "size_list"), which appear in the size
functions of nested datatypes.

Note that I really do want to do 2, because relying on the simplifier
itself to solve the precondition "size lhs ≠ size rhs" is fragile and
breaks at least in some cases in the AFP.

I am sympathetic to the proposal of having a 'proper
subexpression' ordering defined for
all datatypes (e.g., via a plugin similarly to size).
Its usefulness goes beyond the
acyclicity rules which this thread is about.

Absolutely! It's probably no surprise to you when I say that I won't
implement this. But if you (or one of our other datatype experts) ever
does it, do let me know!

But one would like to have some reasonable simp rules for subexp_x
(which may be as hard as the original problem that you are trying to solve).
In particular, if F is itself a datatype that belongs to the subexp type class,
its notion of subexp should be linked to the one of x.

Already for mutual and nested datatypes, you would probably need an
entire family of relations for each combination of types (e.g. if you
have mutually recursive datatypes A and B, you would probably need
subexpr_A_A, subexpr_A_B, subexpr_B_A, subexpr_B_B).

I guess everything gets complicated once you involve nested datatypes…

Manuel

See code below, with your simproc enabled. Also I would register it
only for types that belong to the size class, i.e.,

simproc_setup datatype_no_proper_subterm ("(x :: 'a :: size) = y") = ‹K datatype_no_proper_subterm_simproc›

Your retrieval of mutual types looks reasonable to me. As usual with Isabelle/ML, the most reliable documentation is the code.

I am sympathetic to the proposal of having a 'proper subexpression' ordering defined for all datatypes (e.g., via a plugin similarly to size). Its usefulness goes beyond the acyclicity rules which this thread is about. In particular, the 'proper subexpression' ordering can be used for 'strong induction' or to prove termination of functions in cases when size does not exists. (Provided that we also have the fact that this ordering is wellfounded proved.) Something along the following lines:

class subexp =
fixes subexp :: "'a ⇒ 'a ⇒ bool" (infixl "⊏" 65)
assumes wf: "wfP subexp"

declare [[typedef_overloaded]]

bnf_axiomatization 'a F [wits: "'a F"]

datatype x = Ctor "x F"

instantiation x :: subexp begin

definition subexp_x :: "x ⇒ x ⇒ bool" where
"subexp_x = tranclp (λx y. case y of Ctor f ⇒ x ∈ set_F f)"

instance
apply intro_classes
apply (unfold subexp_x_def)
apply (rule wfP_trancl)
apply (rule wfPUNIVI)
subgoal premises prems for P x
apply (induct x)
apply (rule prems[rule_format])
apply (simp only: x.case)
done
done

end

But one would like to have some reasonable simp rules for subexp_x (which may be as hard as the original problem that you are trying to solve). In particular, if F is itself a datatype that belongs to the subexp type class, its notion of subexp should be linked to the one of x.

Dmitriy

datatype 'a rtree = Leaf | Node 'a "'a rtree list"

lemma "Node x (a # xs) ≠ a"
apply simp? ―‹no_change›
apply (rule size_neq_size_imp_neq)
apply simp
done

lemma "Node x [c,a,b] ≠ a"
apply simp? ―‹no_change›
apply (rule size_neq_size_imp_neq)
apply simp
done

On 2 May 2020, at 18:04, Manuel Eberl <eberlm@in.tum.de<mailto:eberlm@in.tum.de>> wrote:

I attached a proof of concept (works with Isabelle 2020) using the
simple size-based approach, including some example applications.

It works well, although I'm not sure what the proper way to get the
datatype information is (e.g. the list of all the constructors of the
datatype and the associated other datatypes in case of mutual recursion).

Is the ML interface of the BNF package documented anywhere (in
particular this aspect)?

Manuel

On 02/05/2020 16:19, Manuel Eberl wrote:
True, but after your suggestion, I realised that the solution with the
"proper subexpression" relation (or, alternatively, the size function)
combined with a simproc that produces these theorems on the spot is
actually the superior approach in every respect. It's simpler, more
general, and probably more performant.

I can try to come up with a proof-of-concept implementation using the
size function approach, since that needs no additional new features from
the BNF package.

Manuel

On 02/05/2020 16:16, Tobias Nipkow wrote:
A first version which only deals with depth 1 would already cover most
of the practical cases.

Tobias

On 02/05/2020 15:50, Manuel Eberl wrote:
That sounds like a good idea.

However, if such a simproc is to work for any nesting of
constructors,having pre-proven theorems for every constructor will not
be enough.Instead, I suppose one would have to introduce a
"proper-subexpression"relation for datatypes (e.g. xs < Cons x xs) along
with a proof thatthis relation has the obvious properties (irreflexive,
asymmetric,transitive).

I guess that is something that only a datatype package plugin similar
tothe one for the "size" function could provide. Having looked at the
codebriefly, I think only the people who wrote the BNF package could (or
atleast should) implement that.

Alternatively, one could just use the size function (as someone
alreadysuggested in this thread) to get pretty much the same thing,
except thatit won't work for all datatypes (e.g. infinitely branching
ones).

Manuel

On 02/05/2020 15:36, Tobias Nipkow wrote:
I do think such rules are useful, esp if they are there by default. I
suggest they are best handled by a simproc that is triggered by any
"(=)" but that checks immediately if the two argumenst are of the
appropriate type and form. That can be done very quickly (there are
similar simprocs already). The simproc should work for any datatype and
any degree of nesting of the constructors.

Tobias

On 01/05/2020 22:51, Manuel Eberl wrote:
Firstly, I don't think these theorem is especially useful. You might
have planned to add this to the simplifier, but its term net
doesn't do
any magic here. It will end up checking every term that matches
"Cons x
xs = ys" for whether "xs" can match "ys". I'm not sure if that
matching
is equality, alpha-equivalent or unifiable.

I honestly never think /that/ much about the performance
implications of
simp rules (as long as they're unconditional). At least for lists, by
the way, this is already a simp rule by default though, and lists are
probably by far the most prevalent data type in the Isabelle universe.

But you're certainly right that it would make sense to keep a look at
this performance impact if one wanted to add these to the simp set for
all datatypes by default, and I agree that the rules are probably not
helpful /that/ often. Still, it might be nice to have them available
nonetheless.

Secondly, you can prove these theorems by using this handy trivial
theorem : "size x ~= size y ==> x ~= y". Apparently that theorem
has the
name Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer
uses it to prove such inequalities.

It's even easier to prove it by induction. Plus, in fact, the "size"
thing only works if the data type even has a sensible size function.
That is not always the case, e.g. when you nest the datatype through a
function.

My main point however is that when you have a datatype with a dozen
binary constructors, there's quite a bit of copying & pasting involved
before you've proven all those theorems. Since it can (probably) be
automated very easily, why not do that? Whether or not these should be
simp lemmas by default is another question.

Manuel

<Foo.thy>

view this post on Zulip Email Gateway (Aug 23 2022 at 09:04):

From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Manuel,

On 4 May 2020, at 17:06, Manuel Eberl <eberlm@in.tum.de> wrote:

On 03/05/2020 11:46, Traytel Dmitriy wrote:

while your code works for the examples you show, it does not seem to handle nested recursion.

Yes, I am aware of that. Nested datatypes make things considerably more
complicated, so I'd rather not support that for now. I'd have to
1. somehow figure out /all/ the other datatypes involved in the
definition of my datatype and
2. figure out a robust way to expand their size functions.

I have no idea how to do 1 with the information provided by the BNF
package (other than inspecting the types of the constructors to figure
out the nesting).

We store the BNFs that nest recursive occurrences in fp_nesting_bnfs (in fp_sugar). There is also the live_nesting_bnfs for BNFs that nest an occurrence of one of the datatype's (live) type variables. See the following examples:

datatype 'a tree = Node 'a "'a tree list"
datatype ('a, 'b) tree2 = Node "'b ⇒ 'a option" "(('a, 'b) tree2 list × 'a) tree"
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list} |> the |> #fp_nesting_bnfs›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree} |> the |> #fp_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree} |> the |> #live_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree2} |> the |> #fp_nesting_bnfs |> map BNF_Def.name_of_bnf›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree2} |> the |> #live_nesting_bnfs |> map BNF_Def.name_of_bnf›

I'm not 100% sure whether you only need the fp_nesting_bnfs or the union of the two. And of course you will need the associated fp_sugars rather than just BNFs (for those types that are in fact datatypes), but these are easy to get once you have the names.

I also have no idea how to do 2 properly – the "size" plugin provides
some information with BNF_LFP_Size.size_of, but oddly enough it only
provides the equations for the "regular" size function "size", but not
for the generalised one (e.g. "size_list"), which appear in the size
functions of nested datatypes.

Jasmin can say more but it is probably due to the fact that the old interface didn't provide the generalized equations either. You could access the equations by name (cf. "List.list.size"), but this is of course a bit fragile. The correct way would be to extend BNF_LFP_Size's interface. The equations should be available internally.

Note that I really do want to do 2, because relying on the simplifier
itself to solve the precondition "size lhs ≠ size rhs" is fragile and
breaks at least in some cases in the AFP.

Makes sense.

I am sympathetic to the proposal of having a 'proper
subexpression' ordering defined for
all datatypes (e.g., via a plugin similarly to size).
Its usefulness goes beyond the
acyclicity rules which this thread is about.

Absolutely! It's probably no surprise to you when I say that I won't
implement this. But if you (or one of our other datatype experts) ever
does it, do let me know!

I won't promise anything, but will keep this in mind for students looking for theses. :)

But one would like to have some reasonable simp rules for subexp_x
(which may be as hard as the original problem that you are trying to solve).
In particular, if F is itself a datatype that belongs to the subexp type class,
its notion of subexp should be linked to the one of x.

Already for mutual and nested datatypes, you would probably need an
entire family of relations for each combination of types (e.g. if you
have mutually recursive datatypes A and B, you would probably need
subexpr_A_A, subexpr_A_B, subexpr_B_A, subexpr_B_B).

Right, or just one subexpr_(A+B)_(A+B) which is reminiscent of what function does for mutual recursion.

I guess everything gets complicated once you involve nested datatypes…

Actually, no. Because nesting is handled by the virtue of BNFs (more precisely their set function) in this case. See my example, where the recursive occurrence of x was nested in F.

Dmitriy

view this post on Zulip Email Gateway (Aug 23 2022 at 09:05):

From: Thomas Sewell <sewell@chalmers.se>
Two quick comments on this.

Firstly, I don't think these theorem is especially useful. You might have planned to add this to the simplifier, but its term net doesn't do any magic here. It will end up checking every term that matches "Cons x xs = ys" for whether "xs" can match "ys". I'm not sure if that matching is equality, alpha-equivalent or unifiable.

Secondly, you can prove these theorems by using this handy trivial theorem : "size x ~= size y ==> x ~= y". Apparently that theorem has the name Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer uses it to prove such inequalities.

Best regards,

Thomas.

view this post on Zulip Email Gateway (Aug 23 2022 at 09:05):

From: Manuel Eberl <eberlm@in.tum.de>
I cleaned up and optimised my simproc a little bit more [1] and ran some
tests [2]. In particular, I realised that it makes no sense for it to
work on lists since other simprocs already handle the problem there.

Both tests on my machine and on the Testboard seem to indicate that, on
average, the simproc leads to about 0.7% to 1.0% slowdown (both elapsed
time and CPU time).

Tobias and I think the simproc is interesting enough to switch on by
default (it makes trivial and obvious proof obligations go away).

Dmitriy and Jasmin were concerned that it might not be worth the
slowdown and that it should be discussed on the list. Jasmin thinks it
might not be useful often enough to justify a 1% slowdown and should
therefore not be enabled by default.

I on the other hand think that any simproc that is not enabled by
default will simply never be used in practice so that if we don't enable
it by default, we might as well not have it in the first place.

Feel free to weigh in on this, everyone!

Manuel

[1]: http://isabelle.in.tum.de/repos/testboard/rev/f13520ad9b93
[2]: https://ci.isabelle.systems/jenkins/job/testboard/320/

view this post on Zulip Email Gateway (Aug 23 2022 at 09:06):

From: Manuel Eberl <eberlm@in.tum.de>

Firstly, I don't think these theorem is especially useful. You might
have planned to add this to the simplifier, but its term net doesn't do
any magic here. It will end up checking every term that matches "Cons x
xs = ys" for whether "xs" can match "ys". I'm not sure if that matching
is equality, alpha-equivalent or unifiable.

I honestly never think /that/ much about the performance implications of
simp rules (as long as they're unconditional). At least for lists, by
the way, this is already a simp rule by default though, and lists are
probably by far the most prevalent data type in the Isabelle universe.

But you're certainly right that it would make sense to keep a look at
this performance impact if one wanted to add these to the simp set for
all datatypes by default, and I agree that the rules are probably not
helpful /that/ often. Still, it might be nice to have them available
nonetheless.

Secondly, you can prove these theorems by using this handy trivial
theorem : "size x ~= size y ==> x ~= y". Apparently that theorem has the
name Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer
uses it to prove such inequalities.

It's even easier to prove it by induction. Plus, in fact, the "size"
thing only works if the data type even has a sensible size function.
That is not always the case, e.g. when you nest the datatype through a
function.

My main point however is that when you have a datatype with a dozen
binary constructors, there's quite a bit of copying & pasting involved
before you've proven all those theorems. Since it can (probably) be
automated very easily, why not do that? Whether or not these should be
simp lemmas by default is another question.

Manuel


Last updated: Mar 28 2024 at 16:17 UTC