Re: [isabelle] Non-idempotence of datatype constructors



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



On 2 May 2020, at 18:04, Manuel Eberl <eberlm at in.tum.de<mailto:eberlm at 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>



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