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

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

笔记; 使用的等价关系定义如下：

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函数也很有用，这是它的类型（C-c C-d P.subst在 Emacs 中）：

{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标准库中。

Answer 2