equality - 在agda中进行反射:解释同余属性

根据以下相等性定义，我们将refl作为构造函数

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

我们可以证明函数在等式上是一致的

cong : ∀ { a b} { A : Set a }  { B : Set b }
       (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f  refl  = refl

我不确定我是否可以解析这里到底发生了什么。
我认为我们正在对隐藏参数进行模式匹配反射:如果我们将反射的第一个匹配项替换为另一个标识符，则会出现类型错误。
在模式匹配之后，我想根据反射的定义，m和n是相同的。然后发生魔术(应用了关系功能的定义吗？或者它是内置的？)

是否对发生的事情有直观的描述？

最佳答案

是的，花括号{}中的参数是隐式的，只有在agda无法找出它们时才需要提供或匹配它们。必须指定它们，因为从属类型需要引用它们所依赖的值，但是一直拖拽它们会使代码相当笨拙。

表达式cong f refl = refl与显式参数(A → B)和(m ≡ n)匹配。如果要匹配隐式参数，则需要将匹配的表达式放在{}中，但是这里不需要这样做。然后在右侧确实是使用f m ≡ f n构造(refl)，并且它是“魔术般地”工作的。阿格达(Agda)具有内置的公理，证明了这是事实。该公理类似于J -axiom-归纳公理:如果C : (x y : A) → (x ≡ y) → Set中的C x x refl是true，则任何x y : A和p : x ≡ y也是如此。

J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
                     (c : ∀ x → C x x refl) →
                     (x y : A) → (p : x ≡ y) → C x y p
-- this really is an axiom, but in Agda there is a stronger built-in,
-- which can be used to prove this
J c x .x refl = c x -- this _looks_ to only mean x ≡ x
                    -- but Agda's built-in extends this proof to all cases
                    -- for which x ≡ y can be constructed - that's the point
                    -- of having induction

cong : ∀ { a b} { A : Set a }  { B : Set b }
       (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y} -- the type of equality
                                               -- of function results
                     (\_ → refl) -- f x ≡ f x is true indeed
                     x y p

(在最后一行中:我们匹配显式参数f和p，以及隐式参数m=x和n=y。然后，我们将一个隐式参数传递给J，但它不是第一个位置隐式参数，因此我们告诉agda它是C定义-如果不这样做，Agda将看不到refl中的\_ → refl意味着什么类型)