## Stream: new members

### Topic: if then else

#### Victor Porton (Apr 02 2022 at 01:17):

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 (Apr 02 2022 at 01:22):

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 (Apr 02 2022 at 01:25):

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

#### Alex J. Best (Apr 02 2022 at 01:26):

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

#### Arthur Paulino (Apr 02 2022 at 01:26):

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 (Apr 02 2022 at 01:27):

@Alex J. Best unknown identifier 'open_locale'

#### Alex J. Best (Apr 02 2022 at 01:28):

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 (Apr 02 2022 at 01:29):

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

#### Arthur Paulino (Apr 02 2022 at 01:30):

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 (Apr 02 2022 at 01:32):

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

#### Arthur Paulino (Apr 02 2022 at 01:37):

The docs say

Execute all commands in the given locale

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

#### Victor Porton (Apr 02 2022 at 01:38):

@Arthur Paulino What is a locale?

#### Victor Porton (Apr 02 2022 at 01:39):

open_locale implies open? How to close open_locale?

#### Kyle Miller (Apr 02 2022 at 01:40):

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

#### Kyle Miller (Apr 02 2022 at 01:41):

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

#### Bryan Gin-ge Chen (Apr 02 2022 at 01:43):

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 (Apr 02 2022 at 01:46):

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

Last updated: Dec 20 2023 at 11:08 UTC