refl in agda:解释同余属性

Question

通过以下等式定义,我们将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

我不确定我能解析这里到底发生了什么.我认为我们是隐藏参数的模式匹配refl:如果我们用refl替换第一个出现的另一个标识符,我们得到一个类型错误.在模式匹配之后,我想通过refl的定义m和n是相同的.然后魔术发生(应用关系功能的定义？还是内置？)

有关于发生了什么的直观描述？

Answer 1

是的,花括号{}中的参数是隐式的,只有在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,那么任何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在定义-不这样做, ,阿格达不会看到什么类型的是指refl中\_ ? refl)