# Zulip Chat Archive

## Stream: maths

### Topic: How to prove unbound_prop

#### 李拯先 (Feb 01 2020 at 05:59):

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

#### Yury G. Kudryashov (Feb 01 2020 at 06:10):

You need `classical.by_cases r`

here.

#### 李拯先 (Feb 01 2020 at 07:11):

[Quoting…]

How to prove when r is wrong here

#### Yury G. Kudryashov (Feb 01 2020 at 07:16):

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)))

#### 李拯先 (Feb 01 2020 at 07:55):

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 (Feb 01 2020 at 08:09):

Removed the dollar sign. `f $ x`

is `f x`

, `f $ g x`

is `f (g x)`

etc.

#### Bryan Gin-ge Chen (Feb 01 2020 at 08:42):

`(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`

.

#### 李拯先 (Feb 01 2020 at 09:30):

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

#### Kevin Buzzard (Feb 01 2020 at 11:58):

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

Last updated: May 06 2021 at 18:20 UTC