Stream: Beginner Questions

Topic: Extract explicit value from Isabelle proof

jimmy (Apr 15 2024 at 20:52):

How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For example, in the following goal, I’m looking to extract a numerical value for ?solution, e.g. ?solution = 5:

schematic_goal test:
  assumes “x = 3” and “y = 2"
  shows “?solution = x + y”

The following proof works, but doesn’t provide a numerical value for ?solution. Isabelle seems content with ?solution = x + y without further simplification.

proof -
  show “x + y = x + y” using assms by auto
qed

I’ve also experimented with using existentials but didn’t seem to get anywhere with that either. Is this possible to achieve?

In the more general case, if I don’t know the exact form of the answer, how can I force a proof to provide a closed-form solution for an unknown target variable? (And is there an easy way to specify the “closed-form solution” requirement in Isabelle?)

Note that I’m not necessarily asking Isabelle to compute the answer, just enforcing that the proof won’t go through unless an explicit value is either provided or computed.

Lukas Stevens (Apr 16 2024 at 08:30):

First of all, I would recommend adding type annotation to x and y because numerals are very general and you can't prove much about them. Other than that, one can achieve what you want like this

schematic_goal
  assumes "x = 3" and "y = 2"
  shows "numeral ?solution = x + y"
  using assms
  by auto

jimmy (Apr 27 2024 at 21:03):

Thanks a bunch. What exactly is going on here / what references should I read to understand what "numeral" is?

Suppose I were to fix x and y to be rationals and modify the assumptions to be x = 2.1 and y = 2.2: how could I apply the same sort of restriction?

Last updated: Dec 21 2024 at 16:20 UTC