在agda中进行反射：解释同余属性 [英] refl in agda : explaining congruence property

问题描述

在以下等式定义下，我们将refl作为构造函数

With the following definition of equality, we have refl as constructor

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

并且我们可以证明函数在相等性上是一致的

and we can prove that function are congruent on equality

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

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

I am not sure I can parse what is going on exactly here. I think we are pattern matching refl on hidden parameters : if we replace the first occurence by refl by another identifier, we get a type error. after pattern matching, I imagine that m and n are the same by the definition of refl. then magic occurs (a definition of functionality of a relation is applied ? or is it build in ?)

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

Is there an intuitive description on what is going on ?

推荐答案

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

Yes, the arguments in curly braces {} are implicit and they only need to be supplied or matched if agda cannot figure them out. It is necessary to specify them, since dependent types needs to refer to the values they depend on, but dragging them around all the time would make the code rather clunky.

表达式 cong f refl = refl 匹配显式参数（ A→B ）和（ m ≡n ）。如果要匹配隐式参数，则需要将匹配的表达式放在 {} 中，但是这里不需要这样做。然后在右侧确实是使用 refl 的（ fm≡fn ）的构造，它的工作原理是通过魔术。阿格达（Agda）具有内置公理，证明了这是事实。该公理与 J -公理类似（但要强于此）-归纳公理：如果某事物 C：（xy：A）→（x y ）→Set 对于 C xx refl 是正确的，那么对于任何 xy：A 和 p：x y 。

The expression cong f refl = refl matches the explicit arguments (A → B) and (m ≡ n). If you wanted to match the implicit arguments, you'd need to put the matching expression in {}, but here there is no need for that. Then on the right hand side it is indeed the construction of (f m ≡ f n) using refl, and it works "by magic". Agda has a built-in axiom that proves this to be true. That axiom is similar (but stronger than) J-axiom - the induction axiom: if something C : (x y : A) → (x ≡ y) → Set is true for C x x refl, then it is also true for any x y : A and 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 意味着什么类型$ c>）

(In this last line we: match explicit arguments f and p, and also the implicit arguments m=x and n=y. Then we pass to J one implicit argument, but it is not the first positional implicit, so we tell agda that it is C in the definition - without doing that, Agda won't see what type is meant by refl in \_ → refl)

这篇关于在agda中进行反射：解释同余属性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！