embeddings and subtypes

Stream: general

[Peter Nelson]

Given an embedding emb : α ↪ β, I am trying to use the natural correspondence between α and the subtype of β induced by set.range emb. I am also in a context where I want to do this with the subtype coming from another set E that is propeq but not defeq to set.range emb.

My first concern is whether this is just plain unidiomatic; doing this seems to be 'fighting' mathlib in the sense that I can't see how to use it directly. My second is more specific: the following code is an attempt to convert a function defined on subsets of α to one on subsets of the range of emb; and I get a strange error.

import tactic

noncomputable theory
open_locale classical

/-- Given an embedding from α to β and a set E equal to its range, gives an equivalence between α and the subtype of β corresponding to E -/
def subtype_inv_inj {α β: Type}(emb : α ↪ β){E : set β}(hE : E = set.range emb) : E ≃ α :=
let h : Π (y : E), (∃ x : α, emb x = y) :=
  by {rintros ⟨y,hy⟩, rw [hE, set.mem_range] at hy, cases hy with x hx, from ⟨x, by simp [hx]⟩},
 desc : Π (y : E), {x : α  // emb x = y} :=
  λ y, classical.indefinite_description _ (h y) in
{
  to_fun    := λ y, (desc y).val,
  inv_fun   := λ x, ⟨emb x, by {rw [hE, set.mem_range], from ⟨x, rfl⟩} ⟩,
  left_inv  := λ y, by {simp_rw (desc y).property, simp},
  right_inv := λ x, by {cases emb with f h_inj, from h_inj (desc ⟨f x,_⟩).property},
}

/-- given a function f on the subsets of α, and an embedding f from α to β, returns the corresponding function on subsets of the range of the embedding  -/
def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
  let pb_emb := subtype_inv_inj emb rfl in
    λ X, f (pb_emb '' X)

The second function gives the error message: failed to generate bytecode for 'pullback_r' code generation failed, VM does not have code for 'classical.indefinite_description'

Any advice on either a more principled way to do this, or a way to fix this specific error, would be appreciated.

[Mario Carneiro]

The error is easy enough to fix: write noncomputable def

[Yakov Pechersky]

Do you know if α β are finite? Then you could in theory have a computable one

[Peter Nelson]

I've tried that with no success

[Yakov Pechersky]

noncomputable def pullback_r doesn't work?

[Peter Nelson]

that's right

[Peter Nelson]

I do happen to know they're finite, but suppose I didnt? I don't have a constructivist bone in my body and would rather not do extra work to make things constructive.

[Yakov Pechersky]

My relevant PRs on this are #5872 and #5875

[Mario Carneiro]

I got it working with noncomputable def subtype_inv_inj and theorem pullback_r

[Peter Nelson]

Thanks - do you mind explaining your thought process? It feels odd to put theorem in front of a function definition.

[Mario Carneiro]

It has to do with the way lean interprets the keywords def vs theorem; specifically the latter does not get codegen

[Mario Carneiro]

this can cause a problem for downstream definitions, which is why we have the rule that data should be def

[Mario Carneiro]

but classical.indefinite_description is a theorem

[Mario Carneiro]

and that causes the error you are seeing

[Mario Carneiro]

I'm not saying this is a proper solution to the problem, indeed I think it will cause problems for the next definition using pullback_r

[Mario Carneiro]

Oh, inlining the let works

noncomputable def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
  λ X, f (subtype_inv_inj emb rfl '' X)

[Peter Nelson]

Mario Carneiro said:

Oh, inlining the let works

noncomputable def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
  λ X, f (subtype_inv_inj emb rfl '' X)

Well, I never would have guessed that!

[Mario Carneiro]

It's because subtype_inv_inj emb rfl '' X is computationally irrelevant. In fact it's probably not even noncomputable

[Mario Carneiro]

yep, noncomputable def subtype_inv_inj and def pullback_r works, even without the noncomputable theory at the top

[Mario Carneiro]

But when you hoist the subtype function to the top level, it means that it has to be evaluated. I suspect that the reason for the weird error is because it is not inlined for the noncomputable check but inlined later and lean gets confused about whether it's computable or not

[Peter Nelson]

Thanks!

[Yury G. Kudryashov]

BTW, you can use docs#equiv.set.range together with docs#equiv.set.of_eq to get the desired equiv.

[Yury G. Kudryashov]

Something like (equiv.set.range emb emb.injective).trans (equiv.set.of_eq hE)