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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
