Where does hq come from in this proof?

Stream: lean4

[Ulisse Mini]

Why does this work? we're passing a function into Or.inr but we aren't passing an argument for hq, where does hq come from?

open Classical
example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Or.elim (em p)
    (fun hp : p => Or.inr (fun hq : q => absurd (And.intro hp hq) h)) -- where does hq come from?
    (fun hp : ¬p => Or.inl hp)

This is a modified version of the last proof on https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html (which also doesn't make sense, how is hq : q being extracted automatically from hp : p and h : ¬(p ∧ q)?)

[Ruben Van de Velde]

not q is defined as q → false

[Ruben Van de Velde]

So to prove not q, you create a function that takes the assumption hq : q and prove false

[Kevin Buzzard]

hq comes from fun hq : q -> .... Your goal at that point is ¬q which by definition is q -> False so you are assuming a proof of q and returning a proof of False from what you have.

[Kevin Buzzard]

PS you say it "doesn't make sense", but I think what you mean is that it doesn't make sense to you.

[Kevin Buzzard]

Maybe read the section on Negation and Falsity on that link?

[Kevin Buzzard]

if it didn't make sense, that would be a problem, because the whole point of Lean is that it's checking that everything makes sense :-)

[Ulisse Mini]

I did read the section on contradictions & I understand the argument, I just thought hq was a different type then q, and I was wondering where we "create" hq. basically I don't understand where "assume for contradiction that hq is true" is written, it seems very implicit to me.

[Ulisse Mini]

Ruben Van de Velde said:

not q is defined as q → false

Ohh I think I understand now, thanks!

[Kevin Buzzard]

q : Prop and hq : q. So q is the statement and hq is the proof. If you want another resource then you could try the logic notes I wrote for my (mathematician) undergraduates a couple of weeks ago here.

[Ulisse Mini]

Kevin Buzzard said:

q : Prop and hq : q. So q is the statement and hq is the proof. If you want another resource then you could try the logic notes I wrote for my (mathematician) undergraduates a couple of weeks ago here.

Thanks! I'll take a look at those

[Kevin Buzzard]

Basically if you have a CS background then theorem proving in Lean might be the place to start, and if you have a maths background (e.g. you don't have a clue what a type or a term is, like my undergrads) then my more tactic based approach might be more suitable for you.