REFL在AGDA：解释的一致性财产

有了平等的如下定义，我们REFL作为构造REFL在AGDA：解释的一致性财产

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的第一次发生，我们得到一个类型错误。模式匹配后，我想像m和n是由refl的定义相同。那么会发生魔法（关系的功能定义是否应用？或者是否内置？）

是否存在关于正在发生的事情的直观描述？

来源

2014-11-23 nicolas

您在'm≡n'上进行模式匹配。 'refl'是'_≡_'类型的唯一构造函数，它只匹配语法上相同的表达式，即两个表达式需要表示完全相同的语法树。由此可见，“f”的应用也产生相同的语法树。 – 2014-11-23 18:04:36

相同的语法树，它可以归一化到同一个语义？你可以添加这个答案，以便我可以将它标记为 – nicolas 2014-11-23 19:33:07

在'9：https://www.youtube.com/watch?v=eVTc0zaS_hk&index=3 – nicolas 2014-12-03 18:17:54

是，在大括号{}的论据是隐含的，他们只需要提供或匹配，如果AGDA琢磨不出来。有必要指定它们，因为依赖类型需要引用它们依赖的值，但是一直拖动它们会使代码非常笨重。

表达式cong f refl = refl与显式参数（A → B）和（m ≡ n）匹配。如果你想匹配隐含的参数，你需要把匹配表达式放在{}，但这里没有必要这样做。然后在右侧，确实是使用refl构建（f m ≡ f n），并且它“有魔力”。 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 - 如果不这样做，Agda将不会看到refl在\_ → refl中的含义

来源

2014-11-24 08:34:00

一些相关的解释多么丰富，正是我所需要的。谢谢！ – nicolas 2014-11-24 09:27:52

REFL在AGDA：解释的一致性财产

回答

相关问题