forall basic question

Stream: lean4

[James Sully]

Hi I'm working through Theorem Proving in Lean 4.

I have a proof of commutivity of OR:

example : p ∨ q ↔ q ∨ p := Iff.intro
  (λ | Or.inl a => Or.inr a
     | Or.inr b => Or.inl b )
  (λ | Or.inl a => Or.inr a
     | Or.inr b => Or.inl b )

I wanted to simplify the repeated lambda by extracting a theorem:

theorem flipOr : p ∨ q → q ∨ p
  | Or.inl a => Or.inr a
  | Or.inr b => Or.inl b

example : p ∨ q ↔ q ∨ p := Iff.intro flipOr flipOr

however this gives a type error:

application type mismatch
  Iff.intro flipOr
argument
  flipOr
has type
  ∀ (p q : Prop), p ∨ q → q ∨ p : Prop
but is expected to have type
  p ∨ q → q ∨ p : Prop

if it's true for all p q, it must be true for the specific bound p and q in the example, right? How do I fix this?

[James Sully]

Nevermind, got it

example : p ∨ q ↔ q ∨ p := Iff.intro (flipOr p q) (flipOr q p)

[James Gallicchio]

You may want to look into implicit binders -- if you bind p and q in flipOr using implicit binders, the values will automatically be filled in by unification at the use-site:

theorem flipOr {p q} : p ∨ q → q ∨ p
...

[James Sully]

nice, thank you

[James Gallicchio]

I was sort of confused at first, because Lean will automatically introduce implicit bindings for any variables you use without binding them, so in a fresh file if you write

theorem flipOr : p ∨ q → q ∨ p
...

Lean will add the {p q : Prop} automatically. But I assume you declared variables (p q : Prop) above, which overrides the auto-implicit behavior.

[James Sully]

That is in fact exactly what my confusion was. It was because I didn't didn't write

variable (p q r : Prop)

myself, I copied the exercises from the book

[James Sully]

thanks very much!

[James Sully]

so when I add {p q} to a theorem in a context where I've already introduced p and q as variables, am I just shadowing them?

[James Gallicchio]

roughly, yeah. my impression is that all variables bindings are added at the start of each declaration before elaboration, and then any unused bindings are removed after elaboration. (someone correct me if that's wrong)

[James Sully]

ok, cool