John Hughes (Mar 02 2025 at 15:40): John Hughes (Mar 02 2025 at 15:40):In a larger document, I ran into something that surprised me, and I've reduced it to a minimal example.
theory SkolemMWE
imports Complex_Main
begin
lemma x:
assumes "h ∈ {A} ∧ k ∈ {B} ⟹ h ≠ k"
shows "True"
proof -
have 0: "h ∈ {A} ∧ k ∈ {B} ⟹ h ≠ k" using assms by auto
obtain h1 where 1:"h1 ∈ {A}" by auto
obtain k1 where 2:"k1 ∈ {B}" by auto
have 3: "h1 ≠ k1" using 0 1 2 by blast
end
Now obviously it's easy to show the conclusion, but the point I wanted to make is in have 3: in my (failed) proof.
I thought that fact 0 said "if you have an item h that's in this set, and an item k that in that set, then they are not equal", and that this was implicitly a "forall possible h and k and A and B". (It's also clearly false, as quickcheck notes: if A and B are equal, then the result isn't true.)
Regardless, facts 1 and 2 say that we've met the preconditions for fact 0, but Isabelle can't derive the conclusion of fact 0 from them.
I'm sorry this is such a contrived example -- but it does capture the main question which is "why doesn't fact 0 seem to match up with facts 1 and 2 to imply that h1 and k1 are distinct?"
Mathias Fleury (Mar 02 2025 at 15:50):John Hughes said:
I'm sorry this is such a contrived example -- but it does capture the main question which is "why doesn't fact 0 seem to match up with facts 1 and 2 to imply that
h1andk1are distinct?"
because fact 0 talks about the variable h and k (the ones you have fixed in the lemma), and you cannot decide that h=h1 and k=k1, you have prove it.
John Hughes (Mar 02 2025 at 17:00):I didn't think that I was "fixing" h and k, butI guess I was wrong. Perhaps I can ask the question differently:
Here's a silly theorem, stated in English: Suppose you have two sets, U and V, that they have the property that if h is in U and k is in V, then h and k are unequal. Then if you have h1 and h2 in U and k in V, we have that h1 != k and h2 != k.
Can you write this theorem in fix-assume-show form and use a proof that's at least somewhat similar to what I wrote, but avoids the "you said it was true for these fixed things, not for arbitrary things" problem? I'd really like to know how to express this sort of thing, and my attempt to do so clearly didn't meet my goal. (I understand that there's a trivial proof that does not follow my pattern, but that trivial proof won't work in the larger context in which I'm trying to use these ideas.)
terru (Mar 02 2025 at 18:04):you have to explicitly mark that your assumption should hold for any h and k (e.g. using ∀ or the meta-logic forall ⋀):
lemma x:
assumes "⋀h k. h ∈ {A} ∧ k ∈ {B} ⟹ h ≠ k"
shows "True"
proof -
have 0: "⋀h k. h ∈ {A} ∧ k ∈ {B} ⟹ h ≠ k" using assms by auto
obtain h1 where 1:"h1 ∈ {A}" by auto
obtain k1 where 2:"k1 ∈ {B}" by auto
have 3: "h1 ≠ k1" using 0 1 2 by blast
Thanks, @terru . From reading "Programming and Proving" I'd inferred that the "forall" was implicit in theorem statements. Here's a brief quotation from page 6, for example:
...
datatype nat = 0 | Suc nat
All values of type nat are generated by the constructors 0 and Suc. Thus the values of type nat are 0, Suc 0, Suc (Suc 0), etc. There are many predefined functions: +, ∗, 6, etc. Here is how you could define your own addition:
fun add :: "nat ⇒ nat ⇒ nat" where "add 0 n = n" |
"add (Suc m) n = Suc(add m n)"And here is a proof of the fact that add m 0 = m:
lemma add_02: "add m 0 = m" apply(induction m)
apply(auto)
done
...
As a result of that final done, Isabelle associates the lemma just proved with its name. You can now inspect the lemma with the commandthm add_02 which displays add ?m 0 = ?m
The free variable m has been replaced by the unknown ?m. There is no logical difference between the two but there is an operational one: unknowns can be instantiated, which is what you want after some lemma has been proved.
So at least in this form of theorem-statement, there's an implicit "forall" generated.
And even in a theorem like this one
lemma z:
assumes "x ≤ x + (y::nat)"
shows "x < x + (1::nat)"
sorry
the result ends up being
theorem z:
?x ≤ ?x + ?y ⟹ ?x < ?x + 1
which seems to indicate a generalization over all x and y, not just something about a particular x and y. So I guess I don't understand why the forall is needed in your version (although it clearly works, and I appreciate the insight on how to get past this particular bump in the road!).
terru (Mar 02 2025 at 18:39):you are correct! but the argument of the forall is important. Perhaps that's clearer when not using the assumes-syntax — then your original statement becomes ⋀h k. (h ∈ {?A} ∧ k ∈ {?B} ⟹ h ≠ k) ⟹ True, whereas in the version i gave it's (⋀h k. h ∈ {?A} ∧ k ∈ {?B} ⟹ h ≠ k) ⟹ True (notice that the ⋀ now "ends" earlier, which allows you to instantiate the names bound by it inside the proof; otherwise they're free variables, which I have attempted to show with the ⋀ extending all the way — although iirc this is not technically correct with how they're actually handled inside isabelle, but "true enough" to show the difference here)
John Hughes (Mar 02 2025 at 19:05):I'm not sure I completely understand, but I'm pretty sure that this is the thing I needed. (I'm particularly not sure why "in the version I gave you ...." ends with that "==> True"!) I have to go do other things right now, but I'm going to digest this later and see whether it all makes sense after that. Thanks!
Last updated: Mar 09 2025 at 12:28 UTC