簡単な平等証明にぶつかって

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の定義は穴で拡張されていません。

私は何か愚かなことをしていますか？

EDIT：私は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-.を試してください。

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を証明することはできませんので、ない_≡_：xss上

誘導がほとんど機能します。あなたは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。