useless assumptions in a proof

Stream: new members

[ebp]

Hi,

Suppose I want to prove an arbitrary statement; say for example p → (q → p) with p and q propositions. I was wondering why Lean doesn't allow me to make assumptions which are not at all helpful or useful for the proof. I.e., why do I get the "failed to unify" error when trying to assume hpq : p ∧ q. Is there another way of introducing statements like these in your proofs ?

Thanks!

[Eric Wieser]

assume isn't for "making assumptions", its for "giving names to the things you already stated as an assumption in your goal"

[ebp]

Ah, yes, that makes sense., thanks! Then I can rephrase my question to: "is there a way of making arbitrary assumptions, which do not necessarily have anything to do with my goal?"

[Reid Barton]

What does it mean to do that, in an ordinary pen-and-paper proof?

[Reid Barton]

Obviously if you can assume anything, like false, you can prove whatever you like

[Reid Barton]

So probably you are really doing something like either introducing and then proving an intermediate statement, or doing an analysis by cases

[ebp]

It does not really contribute anything in an ordinary pen-and-paper proof. It it just that in an ordinary pen-and-paper proof you can just assume anything you want, however, it wont bring you even the slightest closer to proving your goal.

[Reid Barton]

Right, so in that case the Lean equivalent is to simply not do it!

[Reid Barton]

Normally I would ask for an example of a proof where you want to do something like this, but it sounds like you already agree that it can never happen.

[ebp]

Hah, yes I figured that it is not helpful for writing an actual proof, but I was just wondering if it was possible at all. There is indeed not an example of a proof in which this is helpful.

[Mario Carneiro]

The lean equivalent depends on what you want to prove after you have made your assumption. If your goal is G and you want to assume A and prove G, then deduce not A, then it's by_cases. If you want to assume A and prove B in the course of a proof of G, then that's have : A -> B

[Mario Carneiro]

these moves are not completely useless, they introduce a fact to your context that you can then use in the proof of the goal (which you still have to get back to after you have proved your hypothetical)

[Arthur Paulino]

And if you want to give it a name, then say have hyp_name : A -> B

[ebp]

But it seems that in these cases the assumptions do have a direct use in your proof. I was more looking for something which really does not help anything in the final proof, like the example I gave in my opening post.

[Patrick Johnson]

ebp said:

It does not really contribute anything in an ordinary pen-and-paper proof. It it just that in an ordinary pen-and-paper proof you can just assume anything you want, however, it wont bring you even the slightest closer to proving your goal.

Sure, you can even write 0 = 1 on a paper. The paper won't complain.