functional-programming - 定义共域子集的函数

Question

我正在尝试定义函数的图像限制
f : A → B 为 f': A → f[A]，其中 f'(a) = f(a) 。但是，我不确定如何在精益中定义它。
在我看来，最直观的定义方式是:

def fun_to_image {A B: Type*} (f: A → B): A → image f set.univ :=
        λ a, f a

但是，这会被拒绝，因为 (f a) 是 B 类型而不是 (image f set.univ)。

我什至尝试证明 f(a) ∈ (image f univ) 。这没有帮助:

def fun_to_image (f : A → B) : A → image f univ := 
    λ a , 
    have h : f a ∈ image f univ := 
        exists.intro a 
            (and.intro trivial (eq.refl (f a))),
    f a

错误信息是:

type mismatch, term
  λ (a : A), f a
has type
  A → B
but is expected to have type
  A → ↥(f '' univ)

set.univ和image在data.set中定义如下

def univ : set α :=
λ a, true

def image (f : α → β) (s : set α) : set β :=
{b | ∃ a, a ∈ s ∧ f a = b}

知道如何做到这一点吗？

Answer 1

你就快到了 (-;

错误消息中有一个小“警告标志”。

but is expected to have type
  A → ↥(f '' univ)

你可以看到令人毛骨悚然的向上箭头↥ 。让我解释一下这意味着什么:

正如您所记得的，image f set.univ被定义为子集。由于您将其视为一种类型，因此它会自动强制转换为所谓的子类型: if s : set X ，则对应subtype s具有 ⟨x, h⟩ 形式的条款(在 VScode 中输入 \< 和 \>)，其中 x : X和h : x ∈ s .

这种“强制类型”由 ↥ 表示.

因此，要完成定义，您必须编写 ⟨f a, h⟩ ，而不是 f a .

---

请注意，在 main library 中还有range的定义( here ) 旨在代替 image _ set.univ 。 它已经附带了 ( L1167 )

def range_factorization (f : ι → β) : ι → range f :=
λ i, ⟨f i, mem_range_self i⟩