Finding where property holds

Stream: new members

[Dan Piponi]

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]

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

[Rob Lewis]

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]

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]

@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]

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]

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

[Kyle Miller]

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]

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]

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]

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]

@Dan Piponi Yeah, the Prop = Sort 0 universe is special. It has proof irrelevance and propext.

[Dan Piponi]

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]

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]

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]

@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]

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]

specifically, it is the type of Exists'.rec, as compared to sigma'.rec

[Mario Carneiro]

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]

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