# Zulip Chat Archive

## Stream: new members

### Topic: Finding where property holds

#### Dan Piponi (Dec 22 2021 at 20:17):

I want to write a function that given a proof that a property holds somewhere, returns a value where it holds.

Knowing I can write

```
constant P : ℕ → Prop
example : (∃ (n : ℕ), P n) → (∃ (n : ℕ), P n) :=
assume h,
match h with ⟨x, y⟩ := ⟨x, y⟩
end
```

I thought I'd be able to write

```
def find : (∃ (n : ℕ), P n) → ℕ :=
assume h,
match h with ⟨x, y⟩ := x
end
```

But I get `recursor 'Exists.dcases_on' can only eliminate into Prop`

.

Is there a way to implement what I want?

#### Stuart Presnell (Dec 22 2021 at 20:21):

Is docs#Exists.some what you're looking for?

#### Rob Lewis (Dec 22 2021 at 20:24):

There's also docs#nat.find . In general you can't do this computably, in which case `Exists.some`

(=`classical.some`

) is the right move. But in the `nat`

case you can compute a result.

#### Dan Piponi (Dec 22 2021 at 20:45):

I'm working in a classical context so thanks for the pointers to Exists.some which is what I need.

What's the mechanism by which the compiler accepts my first example but not the second?

#### Johan Commelin (Dec 22 2021 at 20:47):

@Dan Piponi The difference is the type of your goal. In the first case you're trying to prove a `Prop`

, so Lean knows it doesn't need to care about computational content. In the second case you're constructing data, which it refuses.

#### Johan Commelin (Dec 22 2021 at 20:47):

I guess that it would make sense that if you "switch on" classical mode, that the `match`

should also work in the second case. But everybody just uses `Exists.some`

instead.

#### Mauricio Collares (Dec 22 2021 at 20:53):

https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/ is relevant here, maybe

#### Kyle Miller (Dec 22 2021 at 21:23):

Dan Piponi said:

What's the mechanism by which the compiler accepts my first example but not the second?

Related to what Johan said, I think about it in terms of proof irrelevance. Since all proofs of a proposition are considered to be equal, you're not allowed to use any internal details of a proof unless you're doing so in a context where those details don't matter (like when proving another proposition).

With this example you give, it takes a proof of `∃ (n : ℕ), P n`

and matches it against `Exists.intro x y`

. What would it mean to return `x`

?

```
def find : (∃ (n : ℕ), P n) → ℕ :=
assume h,
match h with ⟨x, y⟩ := x
end
```

Suppose `Exists.intro x y`

and `Exists.intro x' y'`

were two proofs of `∃ (n : ℕ), P n`

. By proof irrelevance, `Exists.intro x y = Exists.intro x' y'`

, and then by applying `congr_arg find`

to this equality, the obvious interpretation would give you `x = x'`

. This can easily be a contradiction if `P`

is true for more than one input.

#### Kyle Miller (Dec 22 2021 at 21:25):

The docs#nat.find function gets around this by always returning the least natural number that satisfies `P`

, and the docs#Exists.some function gets around this by always returning the fixed value chosen by the choice function docs#classical.choice (via docs#classical.some)

#### Dan Piponi (Dec 22 2021 at 21:29):

Up to now I've been ignoring the mentions of sorts and universes in the list of type rules (eg. listed here https://leanprover.github.io/reference/expressions.html) Is it a rule about universes that causes the compiler to reject my code?

#### Kyle Miller (Dec 22 2021 at 21:30):

So, ignoring everything about computability, there's still the underlying issue of making sure you have something that's well-defined. Proof irrelevance is sort of like a quotient, and you're required to make sure a function from a `Prop`

is well-defined by avoiding certain things (like using `match`

on a proof if the goal is not a `Prop`

).

#### Kyle Miller (Dec 22 2021 at 21:32):

@Dan Piponi Yeah, the `Prop = Sort 0`

universe is special. It has proof irrelevance and `propext`

.

#### Dan Piponi (Dec 22 2021 at 21:37):

Thanks Kyle. Though I'm a mathematician by training I'm trying to understand this with my programmer hat on trying to figure out the rules for writing code that doesn't produce type errors.

#### Kyle Miller (Dec 22 2021 at 21:44):

We can check how `Exists`

works by seeing what Lean generates from its definition:

```
inductive Exists' {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists'
set_option pp.proofs true
#print prefix Exists'
/-
Exists' : Π {α : Sort u}, (α → Prop) → Prop
Exists'.cases_on : ∀ {α : Sort u} {p : α → Prop} {motive : Prop}, Exists' p → (∀ (w : α), p w → motive) → motive
Exists'.dcases_on : ∀ {α : Sort u} {p : α → Prop} {motive : Exists' p → Prop} (n : Exists' p),
(∀ (w : α) (h : p w), motive (Exists'.intro w h)) → motive n
Exists'.drec : ∀ {α : Sort u} {p : α → Prop} {motive : Exists' p → Prop},
(∀ (w : α) (h : p w), motive (Exists'.intro w h)) → ∀ (n : Exists' p), motive n
Exists'.drec_on : ∀ {α : Sort u} {p : α → Prop} {motive : Exists' p → Prop} (n : Exists' p),
(∀ (w : α) (h : p w), motive (Exists'.intro w h)) → motive n
Exists'.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists' p
Exists'.rec : ∀ {α : Sort u} {p : α → Prop} {motive : Prop}, (∀ (w : α), p w → motive) → Exists' p → motive
Exists'.rec_on : ∀ {α : Sort u} {p : α → Prop} {motive : Prop}, Exists' p → (∀ (w : α), p w → motive) → motive
-/
```

The key argument that determines what you can do with an inductive type is the "motive". For example, here's the one Lean was complaining about in your example:

```
Exists'.dcases_on : ∀ {α : Sort u} {p : α → Prop} {motive : Exists' p → Prop} (n : Exists' p),
(∀ (w : α) (h : p w), motive (Exists'.intro w h)) → motive n
```

The `∀ (w : α) (h : p w), motive (Exists'.intro w h)`

argument is what implements the idea of splitting up a proof into `w`

and `p w`

. Since the motive is only `Prop`

-valued, this `dcases_on`

is only allowed to prove some `Prop`

given specific values that are able prove `Exists' p`

.

#### Kyle Miller (Dec 22 2021 at 21:48):

Here's the non-`Prop`

inductive type version of `Exists`

:

```
inductive sigma' {α : Sort u} (p : α → Prop)
| intro (w : α) (h : p w) : sigma'
```

It actually remembers the `w`

, in contrast to `Exists`

. It's got a `cases_on`

with a motive that can take values in universes beyond `Prop`

:

```
sigma'.cases_on : Π {α : Sort u} {p : α → Prop} {motive : sigma' p → Sort l} (n : sigma' p),
(Π (w : α) (h : p w), motive (sigma'.intro w h)) → motive n
```

This is reflected in the fact that you are allowed to destruct the values and actually make use of them:

```
def find {P : ℕ → Prop} : (Σ' (n : ℕ), P n) → ℕ :=
assume h,
match h with ⟨x, y⟩ := x
end
```

#### Kyle Miller (Dec 22 2021 at 21:50):

@Dan Piponi I found these types to be rather hard to read early on, and I apologize for not really explaining them, since they are rather complicated dependent types. (I'd found it useful just knowing that this `motive`

argument was an underlying difference, and that Lean's equation compiler relies on these generated definitions for inductive types when you write `match`

expressions.)

#### Dan Piponi (Dec 22 2021 at 23:46):

Thanks @Kyle Miller! Up until you pointed out the `motive`

thing it was looking to me like there were special rules in the language for differentiating `Prop`

from `Type`

but now I (think I) can see that it's the definition of `Exists'`

that's special.

#### Mario Carneiro (Dec 22 2021 at 23:52):

specifically, it is the type of `Exists'.rec`

, as compared to `sigma'.rec`

#### Mario Carneiro (Dec 22 2021 at 23:53):

And the reason for this difference *is* built in to lean, this is called "small elimination" of inductive types and it is specific to inductive types in `Prop`

#### Dan Piponi (Dec 23 2021 at 01:38):

@Mario Carneiro Ah. "Small elimination" is a useful term I can google . Thanks!

Last updated: Dec 20 2023 at 11:08 UTC