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},