Matthew Torrence (Dec 03 2021 at 12:43): Matthew Torrence (Dec 03 2021 at 12:43):I'm having trouble matching meta-universally quantified variables in my conclusion in Eisabach with the match command. Let's say I want to match an HOL \<forall> . I can do that as follows:
method mymethod =
(match conclusion in "∀x. A x" for A ⇒ blah)
And that works fine:
lemma "∀x::nat. x + x = 2*x"
apply(mymethod) (* matches, does blah *)
However, a similar looking method with an \<And> instead doesn't match:
method mymethod2 =
(match conclusion in "⋀x. A x" for A ⇒ blah)
lemma "⋀x::nat. x + x = 2*x"
apply(mymethod) (* fails *)
I can kind of see why, since:
method debugabit =
(match conclusion in A for A ⇒ ‹print_term A›)
lemma "⋀x::nat. x + x = 2*x"
apply(debugabit)
gives:
print_term: A: x + x = 2 * x
Which obviously doesn't have an explicit \<And>. What ways are there for dealing with this? One solution is that I can match very broadly:
method mymethod2 =
(match conclusion in "A x" for A x ⇒ blah)
But this is annoying, since it picks up x = a billion things other than the variable I'm interested in, and that was breaking some of my other methods. Are there any suggestions for matching this correctly, or getting a reference to the quantified variable?
Matthew Torrence (Dec 03 2021 at 13:23):(An email thread that may be relevant: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-October/msg00091.html)
Wolfgang Jeltsch (Dec 04 2021 at 01:08):Yes, interestingly, the application of match seems to fix the universally quantified variable.
When matching a pattern like A x, you need to make sure that x refers to the x in your conclusion. For this, I think, you need to manually fix the variable and then reference it inside your method application as follows (I’m using n instead of x):
lemma
fixes n :: nat
shows "n + n = 2 * n"
apply (match conclusion in "A n" for A ⇒ ‹print_term A›)
This correctly prints λa. a + a = 2 * a. Note that fixing the variable only affects the proof; from the outside, n appears as a schematic variable, like if you had explicitly universally quantified it.
Now the above example uses match directly inside apply. What if you wanted to have it in a separate, custom proof method? Then you would have to explicitly communicate the variable to be considered the argument of A to the method (it’s good you have to do that, because it ensures that your proof method is independent of the naming of the argument in the respective conclusion). Here’s how you could achieved that:
method print_predicate for n = (match conclusion in "A n" for A ⇒ ‹print_term A›)
lemma
fixes n :: nat
shows "n + n = 2 * n"
apply (print_predicate n)
I hope that helps. :smile:
Matthew Torrence (Dec 06 2021 at 12:48):This is helpful information, thanks. Unfortunately, there's still a slight problem with it, which is that I can't refer to the variable x when it's universally quantified in my goal. For instance, your example works well when we have
lemma
fixes n :: nat
shows "n + n = 2 * n"
but if we have
lemma
shows "!!n. n + n = 2 * n"
we're kind of out of luck, since we have no name to refer to n with. In this simple example, the solution is very obvious (just use fix n). However, I encounter this situation often where I'm in the middle of an apply-style proof, and my subgoals have all these "un-referable" variables, and I need to break out Isar to get anything done. I encountered the main problem here when trying to create methods to help deal with this
Matthew Torrence (Dec 06 2021 at 12:50):For instance, I encounter this type of situation when I apply(insert atheorem[of stuff]) where I haven't filled in all the unknowns in atheorem, or when I apply(induction) (in the inductive hypothesis)
Matthew Torrence (Dec 06 2021 at 13:01):It looks like apply(atomize) might be of some help: https://stackoverflow.com/questions/21430238/how-to-replace-%E2%8B%80-and-%E2%9F%B9-with-%E2%88%80-and-%E2%9F%B6-in-assumption, but I can't quite get it to work on the example I gave...
Matthew Torrence (Dec 06 2021 at 13:08):aha! What I was looking for was apply(atomize (full)) (https://stackoverflow.com/questions/53487024/pull-all-occurrences-of-the-induction-variable-into-the-conclusion-in-isabelle). To summarize, this takes meta quantifiers to HOL quantifiers, which (as we started with) might be easier to match over. I'll have to play around, because this feels fairly hack-y, but I'm glad to at least have a solution
Wolfgang Jeltsch (Dec 06 2021 at 23:23):Why are you using apply-style?
Personally, I find apply style great for experimenting in order to find concise proof method expressions to be used with by (for example, to come up with something like by transfer (auto simp del: shift_append simp add: shift_append [symmetric]). For the final code, I never use apply but exclusively Isar.
Matthew Torrence (Dec 07 2021 at 15:09):In this case, it's mostly so I can automate the reasoning with methods, but I also find it nicer for certain subgoals to work backwards rather than forwards (for example, when you're repeatedly applying rules, end up with lots of subgoals, and want to know which ones disappear by auto)
Matthew Torrence (Dec 07 2021 at 15:09):I guess dropping into a forward proof in these cases is by far the more maintainable option though
Matthew Torrence (Dec 07 2021 at 15:10):Another case is when I have a very complicated algebraic term, and I want to apply a lot of substitutions. In that case, my Isar proofs get very long very quickly, because I'm having to repeat myself. I find myself in this case a lot
Last updated: Apr 24 2024 at 12:33 UTC