set ℕ and being decidable

Stream: new members

[Bjørn Kjos-Hanssen]

I want to be able to say "either x is in K or not, so we split up into cases".
Here's a MWE of the obstacle:

axiom mwe (K: set ℕ) : ∃f:ℕ →ℕ , ∀ x:ℕ, f x =
(em (x ∈ K)).by_cases
(λ h: x ∈ K,  (0:ℕ))( λ h: x ∉ K,  (0:ℕ))

The error is

failed to synthesize type class instance for K : set ℕ, f : ℕ → ℕ, x : ℕ
⊢ decidable (x ∉ K)

[Kyle Miller]

Depending on what you're doing, you can have it take an additional argument [decidable_pred (∈ K)].

[Kyle Miller]

If this is inside a proof and you don't care about decidability, you can use tactic#classical to introduce the instances that come from the axiom of choice

[Bjørn Kjos-Hanssen]

Thanks @Kyle Miller I got the first suggestion to work. Any more detail on the second suggestion?

[Kyle Miller]

If you're in a tactic proof, you can do

begin
  classical,
  -- now every proposition has a `decidable` instance
  rest-of-proof
end

[Bjørn Kjos-Hanssen]

Is there a way when I'm not in tactic mode as well? :grinning:

[Kyle Miller]

I suppose you can jump in and out of tactic mode with by classical; exact ...expression...

[Kyle Miller]

Though there are other things you can do here, too. docs#classical.by_cases might be useful, though written as @classical.by_cases (x \in K) _ (case1) (case2)

[Kyle Miller]

You don't need the @ if you give each argument to each case a type, like you do in your MWE

[Bjørn Kjos-Hanssen]

Ah... does the @ do something special here?

[Kyle Miller]

It causes the two implicit arguments to become explicit

[Kyle Miller]

Oh, sorry, I didn't notice classical.by_cases was only for Prop-valued things.

[Kyle Miller]

@Bjørn Kjos-Hanssen Maybe this is duplicating something in the library and I didn't need to write it, but here:

noncomputable
def classical.by_cases' (p : Prop) {α : Sort*} (h1 : p → α) (h2 : ¬p → α) : α :=
by classical; exact if h : p then h1 h else h2 h

[Kyle Miller]

import tactic

noncomputable
def classical.by_cases' (p : Prop) {α : Sort*} (h1 : p → α) (h2 : ¬p → α) : α :=
by classical; exact if h : p then h1 h else h2 h

axiom mwe (K: set ℕ) : ∃f:ℕ →ℕ , ∀ x:ℕ, f x =
classical.by_cases' (x ∈ K)
(λ h: x ∈ K,  (0:ℕ))( λ h: x ∉ K,  (0:ℕ))

[Kyle Miller]

And this is what that looks like when p is implicit, too:

import tactic

noncomputable
def classical.by_cases' {p : Prop} {α : Sort*} (h1 : p → α) (h2 : ¬p → α) : α :=
by classical; exact if h : p then h1 h else h2 h

axiom mwe (K: set ℕ) : ∃f:ℕ →ℕ , ∀ x:ℕ, f x =
classical.by_cases'
(λ h: x ∈ K,  (0:ℕ))( λ h: x ∉ K,  (0:ℕ))

[Patrick Johnson]

You may also want to try open_locale classical

[Patrick Johnson]

And you probably want to use if instead of (em (x ∈ K)).by_cases

axiom mwe {K : set ℕ} :
∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = (if x ∈ K then 0 else 0)

[Bjørn Kjos-Hanssen]

Thanks both, for the thorough answers :working_on_it:

[Bjørn Kjos-Hanssen]

This is probably obvious but if I use exists.elim to get my hands on such an f, how would I now derive f y = 0 if I have a proof of y \in K available?

[Yakov Pechersky]

Say "if h : y in K ... then _ else _"

[Yakov Pechersky]

Which is nice syntax for the underlying dependent if then else called docs#dite

[Yakov Pechersky]

Ah, I misunderstood. exists.elim isn't dependent, you lose that property. You retain it if you use exists.some though, with exists.some_spec holding the property

[Bjørn Kjos-Hanssen]

I think I'm just forgetting some basic: if we have (in pseudocode)

def f(x)= if p x then y else z

and we also have a proof h:p a then how do we prove that f a = y?

[Yakov Pechersky]

by rw [if_pos h]

[Yakov Pechersky]

You're also implying that at some point you got an a. So:

lemma blah (h : p a) : f a = y :=
begin
  rw [f, ite_apply, if_pos h]
end

[Yakov Pechersky]

Probably, term mode if_pos h will work, since it will be definitionally true

[Bjørn Kjos-Hanssen]

Sorry, actually it's more like I need

def f (x) := if h: p x then y h else z h

in other words the output of f depends on what the proof h is... and then want to use h to prove f a = y h.

[Reid Barton]

docs#dif_pos

[Bjørn Kjos-Hanssen]

Fantastic... although dif_pos seems like a highly unintuitive name here :yum:

[Yakov Pechersky]

ite -> if_pos, dite -> dif_pos

[Yakov Pechersky]

where d is for dependent