John Hughes (Mar 09 2024 at 23:46): John Hughes (Mar 09 2024 at 23:46):I'm in the middle of a more complex proof where my state looked like this:
proof (state)
goal (4 subgoals):
1. ⋀P Q. P ≠ Q ⟹
P ∈ A4Points ⟹
Q ∈ A4Points ⟹
A4join P Q ∈ A4Lines ∧
A4meets P (A4join P Q) ∧
A4meets Q (A4join P Q)
2. ⋀P Q m.
P ≠ Q ⟹
P ∈ A4Points ⟹
Q ∈ A4Points ⟹
A4meets P m ⟹
A4meets Q m ⟹ m = A4join P Q
3. ⋀P l. ¬ A4meets P l ⟹
P ∈ A4Points ⟹
l ∈ A4Lines ⟹
A4find_parallel l P
∈ A4Lines ∧
affine_plane_data.parallel
A4Points A4Lines A4meets
(A4find_parallel l P) l ∧
A4meets P
(A4find_parallel l P)
4. ∃P Q R.
P ∈ A4Points ∧
Q ∈ A4Points ∧
R ∈ A4Points ∧
P ≠ Q ∧
P ≠ R ∧
Q ≠ R ∧
¬ affine_plane_data.collinear
A4Points A4Lines A4meets P Q
R
and because the 4th subgoal looked simple enough, I thought I'd try to prove that. It wasn't simple, and I tried proving something simpler, namely just the assertion that there's a P in A4Points. I couldn't even do that, so I set about finding the smallest thing that I couldn't prove using a theorem-proof kind of approach (i.e., not the one-liner kind of proof you get with theorem "stuff" by simp).
Here's what I got to:
theory Affine1confusion
imports Complex_Main
begin
datatype a4pt = Pa | Qa | Ra | Sa
definition "A4Points = {Pa, Qa, Ra, Sa}"
theorem test_case: "Pa ∈ A4Points"
If I use try right after this, I find that by (simp add: A4Points_def) will work. But if I try to do a more Isar-like proof (one suitable for my 4-part goal above, so it starts with proof) then try suggests apply blast; when I paste that in, I get the dreaded "Illegal application of proof command in "state" mode" error.
Recalling that I'm supposed to offer up an approach to the proof, I tried proof -:
theorem test_case: "Pa ∈ A4Points"
proof -
try
bit that results in "tried in vain".
Any suggestions?
Mathias Fleury (Mar 10 2024 at 07:00):Here try does nothing, because there is no goal at that point:
theorem test_case: "Pa ∈ A4Points"
proof -
try
Try this instead:
theorem test_case: "Pa ∈ A4Points"
proof -
show ?thesis
try
Or this, without the proof to have a goal:
theorem test_case: "Pa ∈ A4Points"
try
Thanks. But I'm puzzled by your "there is no goal" assertion. Here's what the interface shows:
image.png
Over on the right, I can clearly see a "goal" in the Output panel.
I suspect that this has something to do with the "proof (state)" and "proof (prove)" distinction, which I have never managed to understand. In "proof (state)", is the word "state" a noun, as in "I'm showing you the current state of the proof", or an imperative verb, as in "we're doing a proof, and now it's time for you to state something"?
In general the keywords in Isar seems to have this peculiar characteristic that they're similar to things mathematicians write during proofs, but actually mean something a little different; I'm trying to gradually grasp the subtle differences. At the very most basic, after I write a theorem and then the word "Proof: ", I usually set about proving the thing claimed by the theorem. But in Isar, I have to start using these imperative verb like "show" or "obtain", as if I were directing some other person/entity to do the proving. This constantly trips me up.
Mathias Fleury (Mar 10 2024 at 14:28):I was never careful enough to realize that state and proof are different…
Mathias Fleury (Mar 10 2024 at 14:29):Anyhow, I think of proof of theorems like as either by some obvious arguments or Proof. First step1. Then step2. Finally the theorem holds
Mathias Fleury (Mar 10 2024 at 14:31):If you look at this for example https://en.wikipedia.org/wiki/Square_root_of_2#Proof_by_unique_factorization, every sentence is one intermediate step.
Mathias Fleury (Mar 10 2024 at 14:36):And remark that Isabelle is an ITP, so you are directing Isabelle to do the proof for you…
Mathias Fleury (Mar 10 2024 at 14:38):The proof state are the goals which are still open
Mathias Fleury (Mar 10 2024 at 14:39):lemma
shows ‹P ∧ (R ⟶ Q)›
proof (intro allI conjI impI) ―‹I sometimes uses (intro allI conjI impI)›
(*
proof (state)
goal (2 subgoals):
1. P
2. R ⟹ Q
*)
show P
sorry
(*
proof (state)
this:
P
goal (1 subgoal):
1. R ⟹ Q
*)
next (*actually optional*)
(*
proof (state)
goal (1 subgoal):
1. R ⟹ Q
*)
assume R
show Q
sorry
(*proof (state)
this:
Q
goal:
No subgoals!*)
qed
(this is the last fact the proof chain)
John Hughes (Mar 10 2024 at 15:47):Mathias Fleury said:
And remark that Isabelle is an ITP, so you are directing Isabelle to do the proof for you…
I confess that after my initial foray into using Isabelle, I tended to think of it as a "proof obstructor" rather than "assistant." I kept getting to situations where I had shown some statement P, and my goal was P, and I couldn't get Isabelle to say "OK, you're done." That made it just about the worst "assistant" imaginable. :)
Your example, and the annotation of it, are really helpful, and I've played around with a bunch of variations on it to better understand what's going on by seeing what results various things produced.
Returning to the example:
lemma
shows ‹P ∧ (R ⟶ Q)›
proof (intro allI conjI impI) ―‹I sometimes uses (intro allI conjI impI)›
(*
proof (state)
goal (2 subgoals):
1. P
2. R ⟹ Q
*)
show P
sorry
(*
proof (state)
this:
P
goal (1 subgoal):
1. R ⟹ Q
*)
I have a range of questions from the trivial to higher level.
You did some mumbo-jumbo with the intro allI conjI impI at the start, and I can see what that achieves, but it feels a lot like a apply-script. Is that common in Isar proofs, that there's a little bit of shuffling like this at the start to put the goals into a state that you like?
When it came to show P in your proof, could you have instead chosen to show something else that you might need later? Am I right in thinking that if I want to do that, I should say "have" rather than "show"? That is to say, I can use have (with names perhaps) to marshal a bunch of facts that I'll use later, doing something like have sillyFact:"True" by simp. Is that right?
In your proof, you could have chosen to show the other goal, right? I did that with
lemma
shows ‹P ∧ (R ⟶ Q)›
proof (intro allI conjI impI) ―‹I sometimes uses (intro allI conjI impI)›
show "R ⟹ Q"
sorry
and ended up with $P$ as my only remaining goal. But I had to put double-quotes around R ⟹ Q. I take it that there's a 'single names don't need quotes' 'rule here or something. Would it be weird to write
show "P"
i.e., to always use double-quotes around the thing I want to show?
shows item in the theorem? No amount of proving that we've already done changes its value? It doesn't, for instance, become the current goal after we've done a few steps, right?lemma
shows ‹P ∧(R ⟶ Q)›
proof -
have factP: P
sorry
also have factQ: "R ⟶ Q"
sorry
show ?thesis (by factP factQ)
qed
``
where that last `show` line isn't even syntactically correct...maybe I need `using` or something. It certainly feels as if knowing factP and factQ should be enough to allow me to conclude their conjunction. Is there a way to do this proof using the general structure I've outlined here?
5. (the trivial!) (a) In your lemma-statement, the thesis is shown between "<" and ">" signs, but not the standard ones; I think these are what are called cartouches. What ASCII key-combo produces these? (b) just after `proof`, there's a comment introduced by something that looks like an en-dash followed by a cartouche; what ASCII key-combo produces that?
6. Regarding `proof(prove)` vs `proof (state)` ... I'm still not certain about the noun/verb distinction. And I assume that when you talk about a goal being "open", operationally you mean "it appears in the list of goals/subgoal in the output panel". Is that right?
7. I'm still confused by the "there is no goal" claim vs. my screenshot.
You did some mumbo-jumbo with the intro allI conjI impI at the start, and I can see what that achieves, but it feels a lot like a apply-script. Is that common in Isar proofs, that there's a little bit of shuffling like this at the start to put the goals into a state that you like?
This usually arises in definitions with HOL.forall quantifiers intead of Pure.forall quantifiers (because you want a bool instead of prop). And even then, rarely.
Mathias Fleury (Mar 10 2024 at 16:32):When it came to show P in your proof, could you have instead chosen to show something else that you might need later? Am I right in thinking that if I want to do that, I should say "have" rather than "show"? That is to say, I can use have (with names perhaps) to marshal a bunch of facts that I'll use later, doing something like have sillyFact:"True" by simp. Is that right?
Exactly
Mathias Fleury (Mar 10 2024 at 16:35):[Double quotes]
I prefer cartouches over quotes, but there are more annoying to type. So I tend to skip them, because I am too lazy. But it does not matter
Mathias Fleury (Mar 10 2024 at 16:37):Am I right that "?thesis" always refers to the shows item in the theorem? No amount of proving that we've already done changes its value? It doesn't, for instance, become the current goal after we've done a few steps, right?
It refers to the last fact before a proof keyword.
lemma
shows P
proof -
term ?thesis (*P*)
have "A = 1" for A
proof -
term ?thesis (*A = 1*)
have "A = A"
proof -
term ?thesis (*A = A*)
Returning to item 1 above, my own approach to proving something like your lemma is one that's failed me repeatedly, although I've never really understood why. It looks something like this:
Your (by factP factQ) is not valid isabelle. This is a working proof:
lemma
shows ‹P ∧(R ⟶ Q) ∧ S›
proof -
have factP: P
sorry
moreover have "R ⟶ Q"
sorry
moreover have "S"
sorry
ultimately show ?thesis by (intro conjI)
qed
conjI decomposes P ∧(R ⟶ Q)∧ S into P and R ⟶ Q and S which are then picked from the context (the ultimately adds all those facts to the context)
Mathias Fleury (Mar 10 2024 at 16:43):Cartouche
Isabelle/jedit should give the cartouche as completion for " (it just takes a while)
Mathias Fleury (Mar 10 2024 at 16:44):The other is \<comment>
Mathias Fleury (Mar 10 2024 at 16:45):Isabelle is optimistic, if you write a show, it will assume that it worked and will produce a No subgoals!, even if it obviously does not:
lemma
shows ‹False›
proof -
show ?thesis by (intro conjI)
qed
This is necessary for the multi-threaded model
Mathias Fleury (Mar 10 2024 at 16:48):LOok at the figure https://cca.informatik.uni-freiburg.de/fleury/tutorial-wien23/06-Isar.pdf on page 8 (I have taken it from the Isabelle documentation, although I do not refind it currently), maybe this helps for the prove/state stuff
John Hughes (Mar 10 2024 at 17:12):Thanks. I think that answers about 90% of my questions....which means I'll be back with others soon. :)
Last updated: Apr 27 2024 at 20:14 UTC