Zulip Chat Archive

Stream: lean4

Topic: universal quantification elimination


Yasu Watanabe (Feb 28 2022 at 22:34):

I'm learning lean4 with Theorem Proving in Lean 4 and I'm stuck in proving

example : ( x, p x  r)  ( x, p x)  r := sorry

I think to prove this, taking arbitrary a into hypothesis is needed but I don't know how to express this. I'd like to prove this with tactic since it provides me proof object too.

Mario Carneiro (Feb 28 2022 at 22:57):

Hint: use by_cases hr : r to consider the cases where r is true or false. In either case the problem simplifies to something you can prove

Mario Carneiro (Feb 28 2022 at 22:57):

Hint 2: you don't need a (you will for a later exercise though)

Yasu Watanabe (Mar 01 2022 at 03:16):

Ah, I see. I completely missed the text below.

Try proving these (one direction of the second of these requires classical logic):
I'll try it based on your hints. Thanks.


Last updated: Dec 20 2023 at 11:08 UTC