proof - 如何证明类型在 Agda 中有效？

Question

我正在尝试对依赖函数进行证明，但遇到了障碍。

假设我们有一个定理 f-equal

f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl

我试图证明一个更一般的概念，即在依赖函数上保持平等，但遇到了障碍。即类型

Π-equal : ∀ {A} {B : A → Set} {f : {a : A} → B a} {x y : A} →
            x ≡ y → f x ≡ f y

使编译器不高兴，因为它无法确定 f x 和 f y 属于同一类型。这似乎应该是一个可以解决的问题。是吗？

注意;使用的等价关系定义如下:

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

Answer 1

你可以显式改变f x的类型:

Π-equal : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> P.subst B p (f x) ≡ f y
Π-equal refl = refl

或者

Π-equal'T : ∀ {α β} {A : Set α} {B : A -> Set β} -> ((x : A) -> B x) -> (x y : A) -> x ≡ y -> Set β
Π-equal'T f x y p with f x | f y
...| fx | fy rewrite p = fx ≡ fy

Π-equal' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> Π-equal'T f x y p
Π-equal' refl = refl

或者你可以使用异构相等:

Π-equal'' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
          -> x ≡ y -> f x ≅ f y
Π-equal'' refl = refl

subst 函数也很有用，这里是它的类型(Emacs 中的C-c C-d P.subst):

{a p : .Agda.Primitive.Level} {A : Set a} (P : A → Set p)
      {x y : A} →
      x ≡ y → P x → P y

使用的进口:

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H

顺便说一句，您的 f-equal 在标准库中是 cong。