[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Alexander Krauss]

On 08/20/2011 01:18 AM, Florian Haftmann wrote:

> A typical example for what I was alluding to can be found at:
>
> http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/6e3e9c6c5062#l1.37
>
>  Observe the following proof:
>
> lemma part_equivpI: "(\<exists>x. R x x) \<Longrightarrow>  symp R
> \<Longrightarrow>  transp R \<Longrightarrow>  part_equivp R" apply
> (simp add: part_equivp_def) -- {* (I) "sane" proof state *} apply
> auto -- {* (II) "insane" proof state *} apply (auto elim: sympE
> transpE) -- {* (III) does not even terminate; adding "simp add:
> mem_def" succeeds! *}
>
> The second »auto« imposes a »\<in>« on predicates, although mem_def,
> Collect_def or similar do not appear in the proof text (push to the
> »wrong world«).  Worse, the final auto does not even terminate, this
> is what I had in mind when referring to an enlarged search space.
> Here, the way the system is build forces me to use »simp add:
> mem_def«.

Thanks for clarifying. This is a very good example. In essence, it boils
down to this:

lemma "(A :: 'a => bool) = B"
apply (rule) (* subset_antisym, introduces set connectives *)

I have predicates in mind (and in the context, A and B may be used as
predicates), but this is not visible from the goal state, which contains
only equality. Then, the system will apply subset_antisym, which is
incorrect. subset_antisym is declared [intro!], so this happens with
auto, too. Then the user has no choice but unfold mem_def, to get back
into a sane state.

So I would say this is not so much about search space but about the fact
that automated tools actually need the proper type information to behave
correctly!

>>> * The logical identification of sets and predicates prevents
>>> some
>>>> reasonable simp rules on predicates: e.g. you cannot have (A
>>>> |inf| B) x = A x&  B x because then expressions like "set xs
>>>> |inter| set ys" behave strangely if the are eta-expanded (e.g.
>>>> due to induction).
>> This sounds more like a problem with the underlying infrastructure
>> that should be fixed, rather than working around the problem by
>> introducing new type constructors. Can you give an example of a
>> proof by induction, where eager eta expansion leads to an
>> unnecessarily complicated proof?
>
> theory Scratch imports Main "~~/src/HOL/Library/Lattice_Syntax"
> begin
>
> declare List.set_append [simp del]
>
> thm sup_apply declare sup_apply [simp]
>
> lemma set_append: "set (xs @ ys) = (set xs \<union>  set ys)" apply
> (induct xs) apply simp_all apply auto -- {* non-termination! *}
>

Nice example again.

Actually, there's a fundamental inconsistency in the current setup in
that some operations (like Un) are identified with the lattice
operations, where as other operations like membership or comprehension
are syntactically distinct. So whenever only connectives of the first
kind occur in the goal, the automation can apply rules of both types,
which possibly "specializes" the type to one of the two variants.

Looks pretty much that one cannot really do without the type
information... I wonder if similar effects can occur in other HOLs...

>>The current
>> implementation of subtyping allows to declare only one map function
>> for a type constructor. Thus, we can have either the contravariant
>> or the covariant map for the function type, but not both at the
>> same time. The introduction of set as an own datatype would resolve
>> this issue.

> This is an interesting oberservation which also applies to the
> instantiation of sets for type classes: in 'a =>  bool, you have to
> think about 'a in a contravariant fashion, whereas in 'a set it is
> covariant.

The situation in monotonicity checking (as part of Nitpick) is exactly 
this covariant vs. contravariant issue. We resolved it by re-inferring 
the whole thing.

So, from subtyping point of view, sets and predicates are really two 
different beasts...

Alex