Email Gateway (Aug 22 2022 at 12:30): Email Gateway (Aug 22 2022 at 12:30):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am stumped. I have a proof block of the following form:
proof -
...a bunch of stuff that proves A "2" and "6"...
let ?X = "...a modestly sized expression..."
let ?Y = "...another expression of similar size..."
let ?Z = "...yet another expression similar to the first..."
have "?X = ?Y" using A by auto
also have "?Y = ?Z" using 2 6 by auto
finally show "?X = ?Z" by auto
qed
The proofs of "?X = ?Y" and "?Y = ?Z" succeed.
The proof of "?X = ?Z" does not (the final "auto" is underlined
with a red squiggle and the output window says "Failed to apply
initial proof method", though the "using this" and "goal"
expressions are identical).
I introduced the "lets" after encountering the original problem,
to make sure that there wasn't some subtle difference in the
expressions or that they were being interpreted in different ways
if they occurred multiple times.
The "show" is in blue, indicating that it matches the statement
to be proved in the current block. It doesn't matter if I change
"show" to "have", the proof still fails. It also doesn't matter
if I change "have ... also have ... finally" to
"have ... moreover have ... ultimately show".
I also tried rewriting it as:
have XY: "?X = ?Y" using A by auto
have YZ: "?Y = ?Z" using 2 6 by auto
thus "?X = ?Z" by (metis XY YZ)
and metis does not terminate.
Does anyone have any idea what could cause this? I can't really
distill the example better because it's embedded in thousands of
lines of context. As I indicated, I tried ways of rewriting it
that seemed to me like they might work around the problem, to no
avail.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:30):From: Ramana Kumar <rk436@cam.ac.uk>
Something to do with mismatching types or type classes I'd expect.
Email Gateway (Aug 22 2022 at 12:30):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eugene,
Another cause might be eta-expansion which happens occasionally during resolution and is
not shown in the proof state by default (attribute eta_contract). When this happens, the
simplifier can go into very different directions. Have you tried the following?
have "?X = ?Y" using A by auto
also have "?Y = ?Z" using 2 6 by auto
finally show "?X = ?Z" .
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:30):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Eugene,
another potential failure reason: is ?Y a subexpression of ?X ? Then it might be the case
that the „?Y = ?Z“ also modifies the ?X. To prevent this you can try
def X = ?X
def Z = ?Z
have „X = ?Y“ unfolding X_def using A by auto
also have „?Y = Z“ unfolding Z_def using 2 6 by auto
finally have „?X = ?Z“ unfolding X_def Z_def .
Cheers,
René
Email Gateway (Aug 22 2022 at 12:30):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Thanks for the suggestions. I've tried those, but they don't help.
Here is an abstracted version of the situation, which tries to get
rid of some of the simplifier issues by introducing definitions.
This one happens to succeed, but not in the way I would expect
(the proof shown was generated by sledgehammer). I don't really
understand why a trivial proof (not referencing X_def and Y_def)
is not possible. The types and the fact that the expressions don't
all have the same sets of free variables might be a clue. Perhaps it
is something to do with the way sum types are implemented in the system.
theory Barf
imports Main
begin
definition XXX :: "'a ⇒ 'b ⇒ 'a ⇒ 'b ⇒ 'a + 'b ⇒ 'c + 'b"
where "XXX f g x y = (λz :: 'a + 'b. Inr y)"
definition YYY :: "'a => 'b => 'a => 'a => 'b => 'b => 'a + 'b => 'a + 'b"
where "YYY f g x x' y y' = id"
definition ZZZ :: "'a ⇒ 'b ⇒ 'a ⇒ 'b ⇒ 'b ⇒ 'a + 'b ⇒ 'd + 'b"
where "ZZZ f g x y y' = (λz :: 'a + 'b. Inr y)"
lemma
assumes "XXX f g x y = YYY f g x x' y y'"
and "YYY f g x x' y y' = ZZZ f g x y y'"
shows "XXX f g x y = ZZZ f g x y y'"
proof -
have "XXX f g x y = id"
by (simp add: YYY_def assms(1))
then show ?thesis
using XXX_def id_apply sum.simps(4) by (metis (full_types))
qed
end
The same approach with definitions has not yet allowed me to prove
the original example, though, because as you can see, the proof that
does succeed is not a straight application of transitivity, but rather
uses special properties of the expressions involved. Amusingly, when
I do try that approach on the original example, rendered as shown:
have XY: "XXX f g x y = YYY f g x x' y y'"
using A by (auto simp add: XXX_def YYY_def)
moreover have YZ: "YYY f g x x' y y' = ZZZ f g x y y'"
using 2 6 by (auto simp add: YYY_def ZZZ_def)
ultimately have "XXX f g x y = ZZZ f g x y y'"
using HOL.trans [of "XXX f g x y" "YYY f g x x' y y'" "ZZZ f g x y y'"]
the proof state display shows:
proof (prove)
using this:
XXX f g x y = YYY f g x x' y y'
YYY f g x x' y y' = ZZZ f g x y y'
XXX f g x y = YYY f g x x' y y' ⟹
YYY f g x x' y y' = ZZZ f g x y y' ⟹ XXX f g x y = ZZZ f g x y y'
goal (1 subgoal):
Have I maybe missed some subtle point about HOL?
- Gene Stark
Email Gateway (Aug 22 2022 at 12:30):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gene,
In this example, polymorphism gets in the way. Type inference assigns different types to
the ZZZ instances. You can see this by hovering over the ZZZs in the theory file
(unfortunately, this does not work in the Output buffer) or with
using [[show_consts]]
apply -
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 12:31):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Ah, yes. Thank you, Andreas.
I completed the original proof by introducing type constraints to avoid the
unwanted polymorphism.
- Gene Stark
Last updated: Apr 19 2024 at 04:17 UTC