manual method for forall-elimination · Beginner Questions

Stream: Beginner Questions

Topic: manual method for forall-elimination

Qiyuan Xu (Jun 04 2021 at 07:17):

Hi, for a goal like \<And> x. P x, which method could refine it to P ?x, by eliminating the \<And>?

Mathias Fleury (Jun 04 2021 at 07:36):

The idea of Isar is to not do that...

Mathias Fleury (Jun 04 2021 at 07:41):

(assuming by that that you intend to instantiate a variable from a premise)

Manuel Eberl (Jun 04 2021 at 08:03):

Having a goal of P ?x would mean that you can solve the goal by plugging in whatever you want for ?x. Thus, you can refine the goal $\exists x.\ P\ x$ to P ?x, but certainly not the goal $\bigwedge x.\ P\ x$ .

Manuel Eberl (Jun 04 2021 at 08:05):

If your goal is $\bigwedge x.\ P\ x$ , the usual way to handle that in Isar is to fix a new variable (‘let x be arbitrary but fixed’) and then show that P x holds. That is done like this:

proof -
  fix x
  show "P x"

If none of this answers your question, you might have to provide some more context to make it easier for us to understand what it is that you are struggling with.

Mathias Fleury (Jun 04 2021 at 08:25):

My understanding was that the goal is (\<And> x. P x) ==> Q, but the question is not so clear...

Qiyuan Xu (Jun 04 2021 at 09:04):

Thank you. I'm just learning this and interested in all cases you mentioned.
BTW, another trivial case just for learning,

lemma "⋀ x. P x"
proof -
  fix x
  have "P x" by sorry
  thus "⋀ x. P x" by (* what method? *)
qed

which method could prove it here? Both the auto and sledgehammer fail here.

Another question: I also found the schematic variable ?thesis in this proof context is P rather than ⋀ x. P x, which is also confusing.

lemma "⋀ x. P x"
proof -
  term ?thesis (* P rather than ⋀ x. P x *)
qed

Qiyuan Xu (Jun 04 2021 at 09:14):

Just for learning, I'm also interested in which tactic in the apply form or which rule could eliminate the \<And> in the goal of lemma "\<And> x. P x" (if it was a worthy question

Mathias Fleury (Jun 04 2021 at 10:01):

You are missing some blocks for the first question:

lemma "⋀ x. P x"
proof -
  {
    fix x
    have "P x" sorry
  }
  thus "⋀ x. P x"
    by fast
qed

Mathias Fleury (Jun 04 2021 at 10:02):

Without it, it cannot work because ‹P x ⟹ (⋀x. P x)› does not hold ;-)

Mathias Fleury (Jun 04 2021 at 10:04):

For the ?thesis: you should not write lemma "⋀ x. P x" anyaway...

Mathias Fleury (Jun 04 2021 at 10:06):

Qiyuan Xu said:

Just for learning, I'm also interested in which tactic in the apply form or which rule could eliminate the \<And> in the goal of lemma "\<And> x. P x" (if it was a worthy question

A good approximation while learning Isabelle: it is not possible.

Qiyuan Xu (Jun 04 2021 at 10:18):

Mathias Fleury said:

You are missing some blocks for the first question:
lemma "⋀ x. P x"
proof -
  {
    fix x
    have "P x" sorry
  }
  thus "⋀ x. P x"
    by fast
qed

Right! I got it. It's clear in my mind now. Thank you.

Manuel Eberl (Jun 04 2021 at 10:23):

You could shorten this to just

lemma "⋀ x. P x"
proof -
  fix x
  show "P x" sorry
qed

That is by far the more idiomatic way. Plus, in a top-level goal statement like lemma or theorem, there is nor eason to include a ⋀ in front of the goal anyway. You can just leave it out because free variables in the goal are become schematic after you finished proving it anyway, just the same as if you had written it with a ⋀.

Qiyuan Xu (Jun 04 2021 at 10:31):

Manuel Eberl said:

You could shorten this to just
lemma "⋀ x. P x"
proof -
  fix x
  show "P x" sorry
qed
That is by far the more idiomatic way. Plus, in a top-level goal statement like lemma or theorem, there is nor eason to include a ⋀ in front of the goal anyway. You can just leave it out because free variables in the goal are become schematic after you finished proving it anyway, just the same as if you had written it with a ⋀.

Yes I know it, involving ⋀ in the outmost is just asking for trouble. I just tried to figure out the background mechanism, and really thank u :-)

Manuel Eberl (Jun 04 2021 at 10:36):

Basically, what you need to know is that $\bigwedge$ and $\Longrightarrow$ are special in the sense that Isar knows what they mean and they are integrated into the reasoning structure of Isar. When you have a $\bigwedge$ in a goal, it means that you have to do a fix x in order to prove it, and if you have a $P \Longrightarrow Q$ in a goal, it means that you have to do assume P in order to prove it.

Other logical connectives, such as the $\forall$ , $\exists$ , $\longrightarrow$ of HOL are not integrated with Isar directly. They are essentially opaque functions like any other function.

Manuel Eberl (Jun 04 2021 at 10:36):

It is very uncommon to have something like have "⋀x. P x" in an Isar proof. Certainly not a show "⋀x. P x".

Jakub Kądziołka (Jun 04 2021 at 10:56):

You might want to write have "P x" for x, though. One example is the equivalent of informal reasoning's WLoG:

assume comm: "P x y <--> P y x"
moreover have "P x y" if "x <= y" for x y
proof -
  ...
qed
ultimately have "P x y" by auto (* or perhaps blast with the lemma that x <= y \/ y <= x *)

Qiyuan Xu (Jun 04 2021 at 11:01):

Manuel Eberl said:

Basically, what you need to know is that $\bigwedge$ and $\Longrightarrow$ are special in the sense that Isar knows what they mean and they are integrated into the reasoning structure of Isar. When you have a $\bigwedge$ in a goal, it means that you have to do a fix x in order to prove it, and if you have a $P \Longrightarrow Q$ in a goal, it means that you have to do assume P in order to prove it.

I see. Then it's the reason why it's better to use the structural notation

lemma
  assumes asm: "P"
  shows "Q"

and we don't need to assume asm in proof body again.

Qiyuan Xu (Jun 04 2021 at 11:03):

Yes, the keyword for is elegant here.

Manuel Eberl (Jun 04 2021 at 11:11):

If you mention for, you should also know about if. You can write

have "P x" if "Q x" for x :: nat
proof -
  from that show "P x" sorry
qed

The that is the name that is given to the thing you assume with if. You can also give it another name, of course. I use this a lot.

Qiyuan Xu (Jun 04 2021 at 11:27):

yeah, it's clear and good. thanks.

Last updated: Dec 21 2024 at 16:20 UTC