Email Gateway (Aug 18 2022 at 10:03): Email Gateway (Aug 18 2022 at 10:03):From: Michael Norrish <michael.norrish@nicta.com.au>
It looks to me as if someI2 should successfully eliminate any
occurrence of SOME within a term, but the following doesn't work:
lemma
"(SOME f::nat => nat. f 2 = 3) 2 = 3"
apply (rule someI2)
The resulting proof state is
goal (lemma, 2 subgoals):
1. ?P ?a
2. !!x. ?P x ==> (SOME f. f 2 = 3) 2 = 3
(This is even an instance of someI_ex or someI, but neither of these
work.)
Is there something wrong with unification that it doesn't see the match?
In the mean-time, what can I do to deal with an analogous situation? I
have a term of the form (SOME f. ...) and I want to prove properties
of it.
Michael.
Email Gateway (Aug 18 2022 at 10:03):From: Tobias Nipkow <nipkow@in.tum.de>
Michael,
You are the victim of an intensional incompleteness of my implementation
of polymorphic higher-order unification: in some situations, where
there are infinitely many possible instantiations of a type variable,
only the simplest one is chosen and the others are ignored. See
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ctrs90.html for
details. The solution is to instatiate the type variable by hand:
apply (rule someI2[where 'a = "nat => nat"])
Tobias
Michael Norrish wrote:
Last updated: May 03 2024 at 04:19 UTC