坚持一个简单的平等证明

Question

我正在尝试在 Agda 中实现一些矩阵运算和围绕它们的证明。该代码涉及以下定义附近的内容：

open import Algebra     
open import Data.Nat hiding (_+_ ; _*_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality

module Teste {l l'}(cr : CommutativeSemiring l l') where

   open CommutativeSemiring cr hiding (refl)

   _×_ : ℕ → ℕ → Set l
   n × m = Vec (Vec Carrier m) n

   null : {n m : ℕ} → n × m
   null = replicate (replicate 0#)

   infixl 7 _∔_

   _∔_ : {n m : ℕ} → n × m → n × m → n × m
   [] ∔ [] = []
   (xs ∷ xss) ∔ (ys ∷ yss) = zipWith _+_ xs ys ∷ xss ∔ yss

我使用向量为矩阵定义了一个数据类型，并定义了 null 矩阵和矩阵加法。我的愿望是证明 null 是左恒等式矩阵加法：

 null-left-id-∔ : ∀ {n m : ℕ} → (xss : n × m) → (null {n} {m}) ∔ xss ≡ xss

我尝试通过对矩阵索引进行归纳来定义它，如下所示：

 null-left-id-∔ : ∀ {n m : ℕ} → (xss : n × m) → (null {n} {m}) ∔ xss ≡ xss
 null-left-id-∔ {zero} {zero} [] = refl
 null-left-id-∔ {zero} {suc m} xss = {!!}
 null-left-id-∔ {suc n} {zero} xss = {!!}
 null-left-id-∔ {suc n} {suc m} xss = {!!}

但是，在所有漏洞中，函数 null 都没有展开。由于 null 是使用 replicate 定义的，并且它对自然数使用递归，所以我期待匹配矩阵索引会触发 null 定义的缩减。

顺便提一下，我还尝试通过对矩阵结构的归纳来定义此类证明（通过 xss 上的递归）。同样，null 定义没有在空洞中展开。

我是不是在做傻事？

编辑：我使用的是 Agda 2.5.1.1 和标准库版本 0.12。

Answer 1

我猜你是在用 C-c C-, 和 C-c C-. 检查漏洞，它们没有执行完全规范化。请尝试 C-u C-u C-c C-, 和 C-u C-u C-c C-.。

xss 上的归纳几乎有效：

zipWith-+-replicate-0# : ∀ {n} → (xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≡ xs
zipWith-+-replicate-0#  []      = refl
zipWith-+-replicate-0# (x ∷ xs) = cong₂ _∷_ {!!} (zipWith-+-replicate-0# xs)

null-left-id-∔ : ∀ {n m} → (xss : n × m) → null ∔ xss ≡ xss
null-left-id-∔  []        = refl
null-left-id-∔ (xs ∷ xss) = cong₂ _∷_ (zipWith-+-replicate-0# xs) (null-left-id-∔ xss)

但是你的等式是 _≈_ — 而不是 _≡_，所以你无法证明 0# + x ≡ x。您应该使用 Data.Vec.Equality 模块中的相等性，但这更冗长：

open Equality
    (record { Carrier = Carrier
            ; _≈_ = _≈_
            ; isEquivalence = isEquivalence
            })
  renaming (_≈_ to _≈ᵥ_)

zipWith-+-replicate-0# : ∀ {n} → (xs : Vec Carrier n) → zipWith _+_ (replicate 0#) xs ≈ᵥ xs
zipWith-+-replicate-0#  []      = []-cong
zipWith-+-replicate-0# (x ∷ xs) = IsCommutativeMonoid.identityˡ +-isCommutativeMonoid _
                           ∷-cong zipWith-+-replicate-0# xs

private open module Dummy {m} = Equality
            (record { Carrier = Vec Carrier m
                    ; _≈_ = λ xs ys -> xs ≈ᵥ ys
                    ; isEquivalence = record
                        { refl  = refl _
                        ; sym   = Equality.sym _
                        ; trans = Equality.trans _
                        }
                    })
          renaming (_≈_ to _≈ᵥᵥ_)

null-left-id-∔ : ∀ {n m} → (xss : n × m) → null ∔ xss ≈ᵥᵥ xss
null-left-id-∔  []        = Equality.[]-cong
null-left-id-∔ (xs ∷ xss) = zipWith-+-replicate-0# xs Equality.∷-cong null-left-id-∔ xss

A full snippet.

坚持一个简单的平等证明

Stuck on a simple equality proof

agda

dependent-type