Stuck on a simple equality proof

Question

I'm trying to implement some matrix operations and proofs around them in Agda. The code involve the something near the following definitions:

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

I defined a data type for matrices using vectors and define null matrix and the matrix addition. My desire is to prove that null is the left identity of matrix addition:

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

I've tried to define it by induction on matrix indices, as follows:

 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 = {!!}

but, in all holes, the function null isn't expanded. Since null is defined using replicate and it uses recursion on natural numbers, I was expecting that matching on matrix indices would trigger reduction on null definition.

Just to mention, I've also tried to define such proof by induction over matrix structure (by recursion on xss). Again, the null definition isn't expanded in holes.

Am I doing something silly ?

EDIT: I'm using Agda 2.5.1.1 and standard library version 0.12.

Answer 1

I guess you're inspecting holes with C-c C-, and C-c C-. which don't perform full normalization. Try C-u C-u C-c C-, and C-u C-u C-c C-. instead.

Induction on xss almost works:

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)

But your equality is _≈_ — not _≡_, so you can't prove 0# + x ≡ x. You should use equality from the Data.Vec.Equality module, but this is way more verbose:

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.