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：解釋的一致性財產

回答

相關問題