Zulip Chat Archive

Stream: lean4

Topic: need a little help : p ∨ false ↔ p

Gregor (Nov 29 2021 at 18:28):

Hey there, im currently trying to complete the current "Theorem Proving in Lean 4" guide and the exercises. but at the moment i am failing with the following hypothesis : p ∨ false ↔ p

ive came so far:

example : p ∨ false ↔ p :=
  Iff.intro
    (
      fun hpf : ( p ∨ false) =>
        hpf.elim
          (fun hp : p => hp)
          (
            sorry
          )
    )
    (fun hp : p =>
      Or.inl hp
    )

but i have no clue how to resolve the "false is true in my assumption" to an "absurd" or something like that.
can somebody help me?

Marcus Rossel (Nov 29 2021 at 18:30):

I don't have an answer yet, but check out #backticks.

Gregor (Nov 29 2021 at 18:32):

Marcus Rossel said:

I don't have an answer yet, but check out #backticks.

thx ^^, ive changed the post

Marcus Rossel (Nov 29 2021 at 18:32):

Does False.elim work?

Gregor (Nov 29 2021 at 18:32):

False.elim doesn't seem to exist

Marcus Rossel (Nov 29 2021 at 18:33):

Ahh, it might be called rec or cases at the moment

Gregor (Nov 29 2021 at 18:34):

so, how do i use it? something like

fun (hf : false) =>
              rec hf

doesnt work

Marcus Rossel (Nov 29 2021 at 18:34):

hmm, so for me False.elim does exist

Horatiu Cheval (Nov 29 2021 at 18:35):

False.elim should exist. Are you on stable or on nightly?

Gregor (Nov 29 2021 at 18:35):

latest nightly

Gregor (Nov 29 2021 at 18:36):

whats the new equivalent for False.elim now?

Marcus Rossel (Nov 29 2021 at 18:38):

Gregor said:

whats the new equivalent for False.elim now?

I'll have to check, but fun hf => False.rec (fun _ => p) hf should work for you (in the spot where the sorry is).

Gregor (Nov 29 2021 at 18:38):

or rather, how would I use False.elim here?

Horatiu Cheval (Nov 29 2021 at 18:39):

On 2021-11-24 #check @False.elim gives me False.elim : {C : Sort u_1} → False → C so it should still be there

Marcus Rossel (Nov 29 2021 at 18:40):

@Gregor are you spelling the False upper- or lowercase? It has to be uppercase.
The value false is a Bool.

Gregor (Nov 29 2021 at 18:41):

if im writing uppercase, lean gives me an error

Gregor (Nov 29 2021 at 18:41):

hm okay, if it works on your site its my fault

Gregor (Nov 29 2021 at 18:42):

im going to reset my lean setup, maybe that will do the trick

Gregor (Nov 29 2021 at 18:42):

thank you for your advices^^

Marcus Rossel (Nov 29 2021 at 18:43):

Gregor said:

im going to reset my lean setup, maybe that will do the trick

This works:

example : p ∨ False ↔ p :=
  Iff.intro
    (
      fun hpf : ( p ∨ False) =>
        hpf.elim
          (fun hp : p => hp)
          (fun hf : False => False.elim hf)
    )
    (fun hp : p => Or.inl hp)

Marcus Rossel (Nov 29 2021 at 18:43):

Note the uppercase False!

Horatiu Cheval (Nov 29 2021 at 18:43):

Just to be clear, if you type
#check False.elim
then you see something like
unknown constant 'False.elim in the infoview?

Marcus Rossel (Nov 29 2021 at 18:43):

Gregor said:

if im writing lowercase, lean gives me an error

Exactly. That's because it has to be uppercase.

Gregor (Nov 29 2021 at 18:43):

okay, ive booted a fresh and up-to-date docker environment

Gregor (Nov 29 2021 at 18:44):

so, lean still gives me an error when im trying to write False with an uppercase

Gregor (Nov 29 2021 at 18:45):

"expected term"

Horatiu Cheval (Nov 29 2021 at 18:46):

Can you post a full #mwe of your code? It's easier that way

Gregor (Nov 29 2021 at 18:55):

well, now lean4 wont start at all

Gregor (Nov 29 2021 at 18:59):

variable (p : Prop)
example : p ∨ False ↔ p :=
  Iff.intro
    (
      fun hpf : ( p ∨ False) =>
        hpf.elim
          (fun hp : p => hp)
          (fun hf : False => False.elim hf)
    )
    (fun hp : p => Or.inl hp)