How to prove unbound_prop

Stream: maths

[李拯先]

such as (∀ x, p x ∨ r) → (∀ x, p x) ∨ r, can someone give me some idea or solution

[Yury G. Kudryashov]

You need classical.by_cases r here.

[李拯先]

[Quoting…]
How to prove when r is wrong here

[Yury G. Kudryashov]

example {α : Type*} {p : α → Prop} {r : Prop} : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
λ H, classical.by_cases or.inr (λ hr, or.inl (λ x, (H x).elim id (λ hr', absurd hr' hr)))

[李拯先]

example {α : Type*} {p : α → Prop} {r : Prop} : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
λ H, classical.by_cases or.inr (λ hr, or.inl $ λ x, (H x).elim id (λ hr', absurd hr' hr))

I'm so sorry but i want to ask what is $ means here, and i know id meaning but i don't understand what its'meaning here, can you give me a explain？ thanks

[Yury G. Kudryashov]

Removed the dollar sign. f $ x is f x, f $ g x is f (g x) etc.

[Bryan Gin-ge Chen]

(f $ x y z) means the same thing as (f (x y z)). It lets you write function application with fewer parentheses.

i know id meaning but i don't understand what its'meaning here

Let's start by investigating λ x, (H x).elim id (λ hr', absurd hr' hr). If you replace that entire term with an underscore, Lean will report an error which will tell you what the type is:

example {α : Type*} {p : α → Prop} {r : Prop} : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
λ H, classical.by_cases or.inr (λ hr, or.inl $ _)
/-
don't know how to synthesize placeholder
context:
α : Type ?,
p : α → Prop,
r : Prop,
H : ∀ (x : α), p x ∨ r,
hr : ¬r
⊢ ∀ (x : α), p x
-/

This tells us that λ x, (H x).elim id (λ hr', absurd hr' hr) : ∀ (x : α), p x and hence (H x).elim id (λ hr', absurd hr' hr) : p x.

Next, you should be able to see that (H x) has type p x ∨ r (try putting your cursor over H and x in your editor). What may be less familiar is that (H x).elim is short for or.elim (H x) (this uses Lean's "dot notation", see the text after "Lean provides another useful syntactic gadget" in 3.1 of Theorem Proving in Lean).

or.elim has type ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c, so (H x).elim has type: (p x → p x) → (r → p x) → p x. The type of the first argument is (p x → p x), which matches the type of id : Π {α : Sort u_1}, α → α. You could also replace id with the equivalent term, λ hpx, hpx.

Informally, the last paragraph above could be stated this way: we've shown p x ∨ r and we want to prove p x. We have two cases, and the first one is to show p x from p x. This trivial implication is id.

[李拯先]

Thank you very much, your explanation help me a lot.

[Kevin Buzzard]

import tactic

example : 1 + 1 = 2 := rfl

open_locale classical

example (X : Type) (p : X → Prop) (r : Prop) :
(∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
begin
  intro h,
  by_cases hr : r,
  { -- r is true
    right,
    assumption
  },
  { -- r is false
    left,
    intro x,
    cases h x,
    { assumption},
    { contradiction}
  }
end