Email Gateway (Aug 23 2022 at 08:13): Email Gateway (Aug 23 2022 at 08:13):From: Thomas Sewell <sewell@chalmers.se>
Mark seems to have said similar things, here's my version:
The short answer is, "try" can't prove some of the goals you've stated because they aren't true.
The script you've attached contains a bunch of confusion about how Isar proof syntax works. Let me point out three cases:
You begin your proof with "cases l", and the first case with "case (A2Ordinary s1 b1)". This automatically fixes variables s1 and b1 and assumes that "l = A2Ordinary s1 b1". The assumption is initially named A2Ordinary (the name of the case), and also "this". You've fixed new copies of s1 and b1 and assumed the assumption again. I'm not sure if that's a problem but it is a possible source of confusion.
You then assume "P = A2Point x0 y0" which is definitely a problem. You're in danger of the "fails to refine any pending goal" error. The assume gadget is just for restating existing assumptions, and this isn't an existing assumption.
Finally, having proven "∃b2. m = A2Ordinary s1 b2", you attempt to show "y0 = s1*x0 + b2". The misunderstanding here is that the exists syntax is a binder, and the syntactic name b2 is meaningful only within the scope of the exists. Mark pointed this out.
Isar forces you to be intentional about these things. You can prove that "∃x. ..." with some property, and it won't try to unpack that x. If it did, you might get confusion between different instances of x. You need to tell it you want x to be a new name for a thing. As Mark said, the right thing in this case is "obtain", which was also the right way to handle "P = A2Point x0 y0". You want to obtain x0/y0/b2 at the proof scope with these properties.
To clarify:
obtain x0 y0 where P: "P = A2Point x0 y0"
by (cases P; simp)
Or, the short form of all this, it's easy to think that the problem is proving true statements in a formal system. Actually the first challenge is to state a true statement.
Cheers,
Thomas.
Last updated: Apr 20 2024 at 12:26 UTC