Naso (Jun 09 2023 at 14:01): Naso (Jun 09 2023 at 14:01):After applying a frule, the proof state has an 'anonymous type conversion' that looks like (?A18::'a ⇒ 'A ) a in the consequent of the goal, which makes it look like i have to prove something impossible (it would be a type error). What could this mean?
Mathias Fleury (Jun 12 2023 at 05:03):it is a variable that you have to instantiate. From your comment, I assume that you wand the identity here?
Manuel Eberl (Jun 13 2023 at 09:49):If this is a goal that you think is "wrong" but you are confident that your statement is correct and the rules you are applying are also correct then one possibility is also simply that your application of frule picked a different unifier from the one you had in mind. Proof methods like rule, frule, etc. perform higher order unification, and sometimes there are many different unifiers and it can be hard to predict which one will be picked.
You can backtrack through the other unifiers by putting one or more invocations of back after your frule application. But note that use of back is considered appropriate for experiments/debugging only because it is quite brittle. Also, in general, I would say that using something as low-level as frule in proofs is somewhat unusual these days. For exploration (i.e. "why does this proof not go through?", "how can I proceed here?") it's fine, but it is not rarely part of a finished proof. Of course, I don't know what your use case is and it might be perfectly appropriate for what you are doing – that's for you to judge. :smile:
Manuel Eberl (Jun 13 2023 at 09:53):Also, it is my impression that working explicitly on goals with schematic variables in them is generally something people don't do much anymore these days. The automation sometimes interacts with them in unpredictable ways, it is often not nice to deal with them in an Isar proof, and there is also no easy way to instantiate them manually; you always have to do it implicitly using unification.
Again, I'm sure some people will disagree with me and say that they do that sort of thing all the time, and I'm sure that there are circumstances where it makes sense. But since this is the "Beginner Questions" section I just wanted to point out to any beginners reading this that in my opinion, this is not really the mode in which most people use Isabelle these days.
Manuel Eberl (Jun 13 2023 at 09:54):As for your concrete problem, it would be much easier to give you a concrete answer that actually helps you if you could provide more context on what you are doing. For example: a minimum working example that we can "play around with".
Last updated: Apr 28 2024 at 08:19 UTC