if then else

Stream: new members

[Victor Porton]

How to use if then else with an undecidable predicate (in classic logic)? The following fails:

open classical
def subfunc_to_option {α β: Type} {c: set α} --[decidable_pred c]
(f: {x:α // c x} → β) : α → option β :=
λ y:α, if h: c y then option.some (f ⟨y, h⟩) else none

[Arthur Paulino]

In tactic mode you can use tactic#by_cases to split your logic like that
#xy:

def subfunc_to_option {α β: Type} {c: set α} --[decidable_pred c]
(f: {x:α // c x} → β) : α → option β := λ _ : α, none

[Victor Porton]

@Arthur Paulino Doesn't your code return a function that always returns none? It is not what I need.

[Alex J. Best]

Maybe you want open_locale classical instead of just open classical? This will add classical decidable instances to you environment

[Arthur Paulino]

Victor Porton said:

Arthur Paulino Doesn't your code return a function that always returns none? It is not what I need.

Sorry about that! I didn't notice the def

[Victor Porton]

@Alex J. Best unknown identifier 'open_locale'

[Alex J. Best]

It's part of mathlib indeed. Is mathlib a dependency of your project? Or are you working on a local copy of mathlib? This will add a lot of functionality for you

[Victor Porton]

@Alex J. Best do use mathlib (I asked how to install it about 1/2h ago.)

[Arthur Paulino]

import tactic

open_locale classical

noncomputable def subfunc_to_option {α β: Type} {c: set α}
(f: {x:α // c x} → β) : α → option β :=
λ y:α, if h: c y then option.some (f ⟨y, h⟩) else none

[Victor Porton]

@Arthur Paulino That works. But what does open_locale do?

[Arthur Paulino]

The docs say

Execute all commands in the given locale

If you're interested, this is where it's defined

[Victor Porton]

@Arthur Paulino What is a locale?

[Victor Porton]

open_locale implies open? How to close open_locale?

[Kyle Miller]

open_locale doesn't do open. It just runs whatever commands people put in the "locale"

[Kyle Miller]

I think every command that's in a locale is a command to define notation and add typeclass instances

[Bryan Gin-ge Chen]

These docs explain locales a bit more, and also give commands that let you check what gets run when you open a locale.

edit: I guess these docs don't actually define "locale", but I think it's just the name that was chosen for a tag like classical that these "localized" commands are attached to.

[Kyle Miller]

Like I was saying in another thread, when you're using sets you need to make sure to be consistent with how you interact with them -- in the code below, I switched it all to use ∈, which if you switch any one of them back to c x you'll get some errors.

While open_locale classical can be nice, there are problems you might run into if you don't let the caller choose the decidability instance:

def subfunc_to_option {α β: Type} {c: set α} [decidable_pred (∈ c)]
  (f: {x:α // x ∈ c} → β) : α → option β :=
λ y:α, if h: y ∈ c then option.some (f ⟨y, h⟩) else none

This doesn't actually require the predicate to be decidable, since a caller can use the classical decidability instances (which open_locale classical makes available to you).