Zulip Chat Archive

Stream: maths

Topic: How to prove unbound_prop


view this post on Zulip 李拯先 (Feb 01 2020 at 05:59):

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

view this post on Zulip Yury G. Kudryashov (Feb 01 2020 at 06:10):

You need classical.by_cases r here.

view this post on Zulip 李拯先 (Feb 01 2020 at 07:11):

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

view this post on Zulip 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)))

view this post on Zulip 李拯先 (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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 李拯先 (Feb 01 2020 at 09:30):

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

view this post on Zulip 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