Email Gateway (Aug 19 2022 at 13:05): Email Gateway (Aug 19 2022 at 13:05):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi guys'n gals,
I feel ashamed now, while I feel it's so funny as much as useful enough to
be narrated, I'm telling the story here.
Say I had a local with “assumes A and B”. The most important stuff was in
A, so I was mainly busy proving theorems derived from A. One of those was
hard to me (I'm not a guru, and I'm as slow as a snail), and I multiple
times requested the help of Try/Sledgehammer and others. I was never happy
with the produced Isar proof, and to make it more clear, I wanted to
understand one I picked, expecting to make it more readable.
I was astonished to noticed one of the intermediate goal generated by
Sledgehammer, should have been impossible to prove according to my intents
and interpretations of A and B. I forked my investigations toward this new
case, and discovered I could both prove this goal and disprove it. Yes, I
could prove P and ¬ P! You guess I was rather frightened, while not
willing to believe in an Isabelle bug.
I finally understood: you could only prove ¬ P if you used A and B from
the locale's premisses and you could only prove P if you used only A and
don't bother about B; and as you could either bother or not about B, you
could prove both P and ¬ P one next to the other. So I changed the
locale's premisses into “assumes B and B ⟹ A” instead of “assumes A and
B”. I also have to add “using B” in most proofs about A targeting that
locale.
I was doing as if B was implicitly there everywhere; but it's not.
Moral of the story: don't forget the premisses, it's not enough to have it
in the locale's “assumes”, it probably also have to be there at the left
of an ⟹, in some propositions of the “assumes” section.
By the way, a question aside: is there a way to refer to a proposition
from another proposition? I mean so that I would not have to copy/paste
the premiss of “(text of B) ⟹ (text of A)” and just refer to B, as “B ⟹
(text of A)” instead of the latter.
Email Gateway (Aug 19 2022 at 13:05):From: Peter Lammich <lammich@in.tum.de>
Hi.
Already years ago, I got used to always provide some model for any
locale that contains "final results" of my formalization, just to make
sure that I have not introduced inconsistent assumptions by mistake. And
this is, unfortunately, easier than one may think. E.g., a simple typo
is already enough:
definition P :: "nat => bool" [...]
locale foo = assumes A: "j>0 ==> p j" (* <-- note the lower-case typo
here, p is actually a free variable! *)
inside the locale, you can prove everything you expect with A (and much
more ;) ). Only when interpreting the locale you will realize the
mistake.
Best,
Peter
Email Gateway (Aug 19 2022 at 13:05):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hello Johannes,
I already tried this one. It seems to be allowed by Isar‑Ref, but Isabelle
reject it with this message: “Illegal term bindings in context element”.
Email Gateway (Aug 19 2022 at 13:06):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
That's what I would like to avoid, as I would like to be able to predict
such issues. I'm still investigating the case, as the problem finally
remains unsolved: adding the premiss directly in the proposition did not
solve everything.
Some sanity theorems may help (successful in one case at least), but I
don't know any kind of general theorem which could assert there is no
possible contradictions. I guess this is feasible, as that must be
something close people do when they check a logic is sound and claim they
proved it.
Email Gateway (Aug 19 2022 at 13:06):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I was wrong, Isar‑Ref disallows it. Printed page 89 it says:
“Note that "(is p 1 . . . p n )" patterns given in the syntax of
assumes and defines above are illegal in locale definitions.”
Last updated: Nov 21 2024 at 12:39 UTC