Застрял на простом доказательстве равенства

Я пытаюсь реализовать некоторые матричные операции и доказательства вокруг них в 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.


dependent-type agda
person Rodrigo Ribeiro    schedule 03.09.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я предполагаю, что вы проверяете дыры с помощью 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

Полный фрагмент.

person user3237465    schedule 03.09.2016
comment
Спасибо за Ваш ответ! Меня всегда озадачивала система записей / модулей Agda. - person Rodrigo Ribeiro; 04.09.2016