Email Gateway (Aug 18 2022 at 13:33): Email Gateway (Aug 18 2022 at 13:33):From: Tim McKenzie <tjm1983@gmail.com>
In the attached file, I define a locale called metric, and I prove
interpretation real_euclid: metric dist
I also define a locale (based on metric) called non_exact_metric, and I try to
begin proving
interpretation real_euclid: non_exact_metric "dist:: [real^2, real^2] => real"
Isabelle 2009 balks at the last show in the file, complaining "Local statement
will fail to refine any pending goal", even though I've specified that I only
want to prove the interpretation for the two-dimensional case of dist. If I
remove the bit that specifies that ?x is of type real^2, then Isabelle happily
processes the show command. I don't think I'd be able to finish the proof,
though, since one-dimensional Euclidean space doesn't satisfy non_exact.
Can someone explain to me what's going on here?
Tim
<><
Metric.thy
signature.asc
Email Gateway (Aug 18 2022 at 13:33):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Tim,
Running your proof script with "show sorts" enabled highlights exactly
what the problem is. In your first "show" statement, the goal you have
stated has a more general type than what you intended: "real^2" is
replaced with "real ^ 'a". Since the more general statement still
resolves with the original goal, Isar does not complain. Now Isabelle
is expecting you to prove this new, more general goal, which of course
is impossible. To fix the problem, just add a type annotation to the
"show" statement to force x y and z to have type "real^2".
interpretation real_euclid: non_exact_metric "dist :: [real^2, real^2] => real"
proof
(* the subgoal at this point is for type "real ^ 2" *)
show "EX x y z.
~ real_euclid.exact x y z &
~ real_euclid.exact y z x &
~ real_euclid.exact z x y"
(* the subgoal at this point is for type "real ^ 'a" *)
proof
let ?x = "0 :: real^2"
show "EX y z.
~ real_euclid.exact ?x y z &
~ real_euclid.exact y z ?x &
~ real_euclid.exact z ?x y"
I am actually surprised that no warning message is generated after the
first "show", since you are adding a new type variable "'a" to the
proof state that wasn't there before. I think there should be a
warning message in this case, because inventing a new type variable is
probably not what anyone would intend to do.
Email Gateway (Aug 18 2022 at 13:34):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Tim,
if you turn on "show types" in Isabelle, you see that the goal in your
interpretation proof for real_euclid : non_exact_metric after the first
"proof" command still contains the type "real ^ 2" for the existentially
quantified x y z.
Your show statement however replaces this type constraint with "real ^
'a" because this is the most general type that can be inferred for the
proposition to be shown. Since this type is more general than the typing
for the actual goal to be shown, Isabelle does not complain.
Hence, inside your second proof, the type for ?x should be "real ^ 'a"
with 'a being now fixed.
The solution is to include a type constraint already in the first show
statement:
interpretation real_euclid: non_exact_metric "dist :: [real2, real2]
\<Rightarrow> real"
proof
show "\<exists>x y z :: real ^ 2.
\<not> real_euclid.exact x y z \<and>
\<not> real_euclid.exact y z x \<and>
\<not> real_euclid.exact z x y"
Regards,
Andreas
Tim McKenzie schrieb:
Email Gateway (Aug 18 2022 at 13:34):From: Tim McKenzie <tjm1983@gmail.com>
Thanks Brian and Andreas for your excellent explanations. I think I
understand the problem now, and I've also found out how to turn on
"show types" and "show sorts" in Proof General, so I should be able to
diagnose similar problems in future.
Tim
<><
Last updated: May 03 2024 at 04:19 UTC