John Hughes (Mar 06 2025 at 13:03): John Hughes (Mar 06 2025 at 13:03):I have a terrible feeling that I'm asking the same question a second time (see #Beginner Questions > Skolem confusion ) but here goes. I've distilled this down from a larger example, but that means that in and of itself, it makes little sense.
Anyhow, a locale of type "a1" consists of a set Items containing some nat-sets; to be an a1, the nat-sets must each have cardinality two.
theory LocaleMWE3
imports Main
begin
locale a1 =
fixes Items:: "nat set set"
assumes ax1: "⟦X ∈ Items⟧ ⟹ card X = 2" (* A *)
begin
end (* a1 *)
I believe that Axiom 1 (i.e. ax1) expresses this requirement.
I'd like to establish that a particular set of items constitutes an a1 using the locale predicate:
lemma a1example1:
fixes Items
assumes "Items = { {1::nat,4}, {2, 4}}"
shows "a1 Items"
To do so, I begin by saying that within this context, in which Items is associated with {{1 , 4}, {2, 4}}, axiom 1 holds true; that should suffice to prove that Items satisfies the predicate called a1:
proof -
have 0: "⟦X ∈ Items⟧ ⟹ (card X = 2)" using assms by fastforce (* AA *)
show ?thesis using a1_def assms by simp (* B but sledgehammer doesn't find a proof using 0 *)
qed
This proof doesn't work as expected. I've shown fact 0, which is exactly axiom 1, verbatim, but sledgehammer refuses to use it in proving the lemma. In an alternative version, I've put a ⋀ X . in front of the assertion that axiom 1 holds, and everything works fine:
lemma a1example2:
fixes Items
assumes "Items = { {1::nat,4}, {2, 5}}"
shows "a1 Items"
proof -
have 1: "⋀ X .⟦X ∈ Items⟧ ⟹ (card X = 2)" using assms by fastforce
show ?thesis using 1 a1_def by blast (* C *)
qed
I've also done a third proof, using ∀, and it works too, of course -- -I just did it to double-check:
lemma a1example3:
shows "a1 { {1::nat,3}, {2, 4}}"
proof -
have 0: "∀X. X ∈ {{1::nat, 3}, {2, 4}} ⟶ (card X = 2)" by simp
show ?thesis using 0 a1_def by blast
qed
So back in the first proof, can someone tell me what the line marked (* AA *) actually states? As in, "if you were writing this proof in natural language, what would this assertion say?" And can you contrast it with what like (* A *) expresses?
At a mechanical level, I'm fine -- I can continue my proofs by adding in the ⋀ X . stuff -- but I'd feel a lot better if I knew what that (apparently useless) fact 0 is saying, so that I can avoid this particular hurdle in the future.
Yong Kiam (Mar 06 2025 at 15:43):I think (as you figured out) (the mistake I made several times is the reverse situation, where there should be a ax1 doesn't say what you think it says ("forall X ..."). This is a mistake I've made several times (mentioning a variable in the locale assumptions which isn't fixed)... I think it ends up referring to whatever X is in the enclosing context, but the technical details of what exactly it means I'll leave for someone else to answerfixes of a variable, but I left it out and it got universally quantified)
wrong explanation, see Chelsea's below
Chelsea Edmonds (Mar 06 2025 at 15:53):Here's a few examples I hope will help. This links to your question before, which highlights the difference between working with an established theorem (or locale context assumption) and an ongoing proof, as well as understanding the importance of quantifiers in assumptions. Lets go back to your original question. Consider the below example:
lemma a1example2:
assumes a: "⟦X ∈ Items⟧ ⟹ (card X = 2)"
shows "a1 Items"
proof -
thm a
show ?thesis sorry
qed
thm a1example2
This lemma states "if for some x in Items, the cardinality of X is 2, Items satisfies the assumptions of locale a1". Which can't actually be proven as this assumption isn't strong enough (hence the sorry), but we'll assume for now it dows. Inspect the lemma using a1example2 as above. See how Isabelle has converted the free variable X into an unknown now we're outside the proof context? So if we now wanted to use this lemma, we would instantiate the x, which would mean we could give the theorem any set for X (including one that may not be in Items), and falsely show Items satisfies a1. E.g, the following example goes through, where Items contains one set of size 3.
lemma a1example3:
shows "a1 {{1::nat, 2, 3}}"
proof -
have "{} ∈ {{1, 2, 3}} ⟹ card {} = 2"
by fastforce
then show ?thesis using a1example2[of "{}"] by metis
qed
This is why assumptions on a set need the forall, which I think is more relevant to your last question. But its important to keep in mind when looking at your current problem. For facts in the Isar proof, such as AA, the free variables in fact 0 aren't even converted into unknowns (which is what your prog prove quote discussed for an actual theorem), so can't be instantiated to start with (compared to an actual theorem statement, such as lemma01 below - which can't be proven anyway). This is why we need to add the quantifier inline. E.g. see the difference in the two uses of thm in jedit with the below code.
lemma 01: "⟦X ∈ Items⟧ ⟹ (card X = 2)"
sorry
thm 01
lemma a1example1:
assumes "Items = { {1::nat,4}, {2, 4}}"
shows "a1 Items"
proof -
have 0: "⟦X ∈ Items⟧ ⟹ (card X = 2)"
sorry
thm 0
Locale assumptions actually work slightly differently. When you assume something in the format of A, Isabelle's mechanisms implicitly adds the quantification. You can see this by applying the unfold locales tactic (see example below) which changes your proof to have all the assumptions of a1 as your goals. See how in the unfolded goals, it adds in the quantification.
lemma a1example1:
assumes "Items = { {1::nat,4}, {2, 4}}"
shows "a1 Items"
proof (unfold_locales)
Of course you still need to be careful if you have an assumption in a locale which is an implication, which may in turn need to quantify over only part of that statement - this circles back around to the logical meaning discussed in the first examples. But in your case, your ax1 is perfectly fine.
Yong Kiam (Mar 06 2025 at 16:03):^ I deleted my answer which is incorrect
John Hughes (Mar 06 2025 at 17:06):Chelsea Edmonds said:
Thanks for your detailed answer, which I think probably addresses the essence of my confusion, but I can't quite piece it together yet.
lemma a1example2: assumes a: "⟦X ∈ Items⟧ ⟹ (card X = 2)" shows "a1 Items" proof - thm a show ?thesis sorry qed thm a1example2This lemma states "if for some x in Items, the cardinality of X is 2, Items satisfies the assumptions of locale a1".
I don't understand why it says that. I've always read P ==> Q as the metalogic version of "if P then Q"; in this case, that
becomes "if X is in Items, then its cardinality is 2." Can you explain why I should be reading it as something different? I understand that it's in an assumes, so I should really be reading the whole lemma statement as "Suppose we know that if X is in items, it's cardinality is 2. Then Items is an example of an a1 locale ".
But I still don't see where the "if for some x in Items..." comes from. Wouldn't that amount to an implicit existential quantifier?
I think that in my example 2,
thm a1example2
lemma a1example1:
fixes Items
assumes "Items = { {1::nat,4}, {2, 4}}"
shows "a1 Items"
proof -
have 0: "⟦X ∈ Items⟧ ⟹ (card X = 2)" using assms by fastforce
show ?thesis using a1_def assms by simp (* B but sledgehammer doesn't find a proof using 0 *)
qed
fact 0 really does mean the universal thing, because if I change the second set in Items in the assumptions to {2, 4, 5}, the fastforce proof suddenly fails. And yet there clearly still is some X in items (namely {1, 4}) for which the cardinality is 2.
Your later comment -- "Locale assumptions actually work slightly differently. When you assume something in the format of A, Isabelle's mechanisms implicitly adds the quantification" -- makes it clear that when I set about proving that some structure has the characteristics necessary to meet some locale-spec, I should prove not the stated "axioms" of the locale, but their quantified versions. (This does seem like a not-so-great design choice, but obviously I can't fix it.)
The remaining stuff you wrote --- about free vars becoming unknowns once the theorem's proved (but not before) --- I already understand (or at least I'm aware of it and am sort of used to it).
Which can't actually be proven as this assumption isn't strong enough (hence the sorry), but we'll assume for now it dows. Inspect the lemma using
a1example2as above. See how Isabelle has converted the free variable X into an unknown now we're outside the proof context? So if we now wanted to use this lemma, we would instantiate the x, which would mean we could give the theorem any set for X (including one that may not be in Items), and falsely show Items satisfies a1. E.g, the following example goes through, where Items contains one set of size 3.lemma a1example3: shows "a1 {{1::nat, 2, 3}}" proof - have "{} ∈ {{1, 2, 3}} ⟹ card {} = 2" by fastforce then show ?thesis using a1example2[of "{}"] by metis qed
This next bit, though -- I still can't quite get it. I'll keep re-reading and see whether it sinks in. But in the meantime, can you address my earlier question, namely, "At point AA in my initial proof, what is an english-language translation of of that line (up to but not including the "using assms..." part), and why?" I feel as if having that would really help me. It's a little upsetting to discover that I've proved something that doesn't, on reflection, even make sense to me!
This is why assumptions on a set need the forall, which I think is more relevant to your last question. But its important to keep in mind when looking at your current problem. For facts in the Isar proof, such as AA, the free variables in fact 0 aren't even converted into unknowns (which is what your prog prove quote discussed for an actual theorem), so can't be instantiated to start with (compared to an actual theorem statement, such as lemma01 below - which can't be proven anyway). This is why we need to add the quantifier inline. E.g. see the difference in the two uses of thm in jedit with the below code. [...]
Mathias Fleury (Mar 06 2025 at 19:13):John Hughes said:
Chelsea Edmonds said:
Thanks for your detailed answer, which I think probably addresses the essence of my confusion, but I can't quite piece it together yet.lemma a1example2: assumes a: "⟦X ∈ Items⟧ ⟹ (card X = 2)" shows "a1 Items" proof - thm a show ?thesis sorry qed thm a1example2This lemma states "if for some x in Items, the cardinality of X is 2, Items satisfies the assumptions of locale a1".
I don't understand why it says that. I've always read
P ==> Qas the metalogic version of "if P then Q"; in this case, that
becomes "if X is in Items, then its cardinality is 2." Can you explain why I should be reading it as something different? I understand that it's in anassumes, so I should really be reading the whole lemma statement as "Suppose we know that if X is in items, it's cardinality is 2. ThenItemsis an example of ana1locale ".
But I still don't see where the "if for some x in Items..." comes from. Wouldn't that amount to an implicit existential quantifier?
It isP ==> Q ==> R vs (P ==> Q) ==> R.
The lemma is the same as:
lemma a1example2:
"(⟦X ∈ Items⟧ ⟹ (card X = 2)) ⟹ a1 Items"
And given how implication work, it means that:
- either there is some X such that (⟦X ∈ Items⟧ ⟹ (card X = 2)) and then a1 items holds
- or there is not such X (False ==> everything)
Mathias Fleury (Mar 06 2025 at 19:17):fact 0 really does mean the universal thing, because if I change the second set in Items in the assumptions to {2, 4, 5}, the fastforce proof suddenly fails. And yet there clearly still is some X in items (namely {1, 4}) for which the cardinality is 2.
nearly, with a for X to have it forall-quantified it works:
have 0: "⟦X ∈ Items⟧ ⟹ (card X = 2)" for X using assms by fastforce
image.png
Without the for X jEdit is actually using the weird color, which means "something is wrong here, this variable is free. However, you are logically allowed to do that, so I let you shoot yourself in the foot".
Mathias Fleury (Mar 06 2025 at 19:21):This next bit, though -- I still can't quite get it. I'll keep re-reading and see whether it sinks in. But in the meantime, can you address my earlier question, namely, "At point AA in my initial proof, what is an english-language translation of of that line (up to but not including the "using assms..." part), and why?" I feel as if having that would really help me. It's a little upsetting to discover that I've proved something that doesn't, on reflection, even make sense to me!
The best way I think is to see it in action: try it out!
Add some thm X in various places (it works on the named haves too! And assumes!) and see what happens to the variables. Are they changed to ?a? are they kept?
John Hughes (Mar 06 2025 at 19:44):You say:
The lemma is the same as:
lemma a1example2: "(⟦X ∈ Items⟧ ⟹ (card X = 2)) ⟹ a1 Items"And given how implication work, it means that:
- either there is some X such that
(⟦X ∈ Items⟧ ⟹ (card X = 2))and thena1 itemsholds- or there is not such X (
False ==> everything)
Where does the "some" come from here? I don't see an existential quantifier anywhere!
I'm not doubting you -- what you say is obviously true -- but I'm not sure how I'm supposed to know that from "(⟦X ∈ Items⟧ ⟹ (card X = 2)) ⟹ a1 Items".
nearly, with a
for Xto have it forall-quantified it works:have 0: "⟦X ∈ Items⟧ ⟹ (card X = 2)" for X using assms by fastforceWithout the
for XjEdit is actually using the weird color, which means "something is wrong here, this variable is free. However, you are logically allowed to do that, so I let you shoot yourself in the foot".
Using the "for X" is the same as putting "⋀X . in front, right? So I already understand that this is one route to making things work.
And I see that the X is highlighted in jEdit at the point you mention, but I still don't know what the thing I proved means --- surely there's some meaning to it, or having "proved" it wouldn't make sense.
As for "try it out", I have done that for about 12 hours now. I can see what's happening --- I just don't understand what it means. I've obviously got some mistaken notions about fix-assume-show statements of theorems or something, and about the meaning of formulas with free variables in them, but I don't know what those mistaken notions are.
Mathias Fleury (Mar 06 2025 at 19:50):I think the fancy name is mini-scoping, but the argument is just how ∀ distributes over implication:
lemma ‹(∀X. (P X ⟶ Q)) ⟷ ((∃X. P X) ⟶ Q)›
by auto
Last updated: Mar 09 2025 at 12:28 UTC