Flattened matrix vs 2D matrix lookup equivalence (proof) - 寻求更优雅

Question

我有一个（显而易见的）声明的证明，即在矩阵的扁平表示中查找元素作为 m * n 长度向量与向量的向量表示相同。但是我的证明感觉很笨拙。 [我不会在这里给出证明，因为这样做会使搜索产生偏差！]。为了使这个问题独立，下面我给出了一个独立的 Agda 模块，其中包含一些有用的引理。 [其中一些引理可能应该在标准库中，但不是。]

基本上，我正在寻找一种优雅的方法来填补底部的洞，lookup∘concat 的证明。如果你也能让我的引理更优雅，请随意！

module NNN where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties
open import Data.Vec
open import Data.Fin using (Fin; inject≤; fromℕ; toℕ)
open import Data.Fin.Properties using (bounded)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality

-- some useful lemmas
cong+r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i + k ≤ j + k
cong+r≤ {0}     {j}     z≤n       k = n≤m+n j k
cong+r≤ {suc i} {0}     ()        k -- absurd
cong+r≤ {suc i} {suc j} (s≤s i≤j) k = s≤s (cong+r≤ {i} {j} i≤j k)

cong+l≤ : ∀ {i j} → i ≤ j → (k : ℕ) → k + i ≤ k + j
cong+l≤ {i} {j} i≤j k =
  begin (k + i
           ≡⟨ +-comm k i ⟩ 
         i + k
           ≤⟨ cong+r≤ i≤j k ⟩ 
         j + k
           ≡⟨ +-comm j k ⟩ 
         k + j ∎)
  where open ≤-Reasoning

cong*r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i * k ≤ j * k
cong*r≤ {0}     {j}     z≤n       k = z≤n
cong*r≤ {suc i} {0}     ()        k -- absurd
cong*r≤ {suc i} {suc j} (s≤s i≤j) k = cong+l≤ (cong*r≤ i≤j k) k 

sinj≤ : ∀ {i j} → suc i ≤ suc j → i ≤ j
sinj≤ {0}     {j}     _        = z≤n
sinj≤ {suc i} {0}     (s≤s ()) -- absurd
sinj≤ {suc i} {suc j} (s≤s p)  = p

i*n+k≤m*n : ∀ {m n} → (i : Fin m) → (k : Fin n) → 
            (suc (toℕ i * n + toℕ k) ≤ m * n)
i*n+k≤m*n {0} {_} () _
i*n+k≤m*n {_} {0} _ ()
i*n+k≤m*n {suc m} {suc n} i k = 
  begin (suc (toℕ i * suc n + toℕ k) 
           ≡⟨  cong suc (+-comm (toℕ i * suc n) (toℕ k))  ⟩
         suc (toℕ k + toℕ i * suc n)
           ≡⟨ refl ⟩
         suc (toℕ k) + (toℕ i * suc n)
           ≤⟨ cong+r≤ (bounded k) (toℕ i * suc n) ⟩ 
         suc n + (toℕ i * suc n)
           ≤⟨ cong+l≤ (cong*r≤ (sinj≤ (bounded i)) (suc n)) (suc n) ⟩
         suc n + (m * suc n) 
           ≡⟨ refl ⟩
         suc m * suc n ∎)
  where open ≤-Reasoning

fwd : {m n : ℕ} → (Fin m × Fin n) → Fin (m * n)
fwd {m} {n} (i , k) = inject≤ (fromℕ (toℕ i * n + toℕ k)) (i*n+k≤m*n i k)

lookup∘concat : ∀ {m n} {A : Set} (i : Fin m) (j : Fin n) 
  (xss : Vec (Vec A n) m) → 
  lookup (fwd (i , j)) (concat xss) ≡ lookup j (lookup i xss)
lookup∘concat i j xss = {!!}

Answer 1

最好通过归纳来定义fwd，然后剩下的。

open import Data.Nat.Base
open import Data.Fin hiding (_+_)
open import Data.Vec
open import Data.Vec.Properties
open import Relation.Binary.PropositionalEquality

fwd : ∀ {m n} -> Fin m -> Fin n -> Fin (m * n)
fwd {suc m} {n}  zero   j = inject+ (m * n) j
fwd     {n = n} (suc i) j = raise n (fwd i j)

-- This should be in the standard library.
lookup-++-raise : ∀ {m n} {A : Set} (j : Fin n) (xs : Vec A m) (ys : Vec A n)
                -> lookup (raise m j) (xs ++ ys) ≡ lookup j ys
lookup-++-raise j  []      ys = refl
lookup-++-raise j (x ∷ xs) ys = lookup-++-raise j xs ys

lookup∘concat : ∀ {m n} {A : Set} i j (xss : Vec (Vec A n) m) 
              -> lookup (fwd i j) (concat xss) ≡ lookup j (lookup i xss)
lookup∘concat  zero   j (xs ∷ xss) = lookup-++-inject+ xs (concat xss) j
lookup∘concat (suc i) j (xs ∷ xss)
  rewrite lookup-++-raise (fwd i j) xs (concat xss) = lookup∘concat i j xss

fwd的可靠性证明：

module Soundness where
  open import Data.Nat.Properties.Simple
  open import Data.Fin.Properties

  soundness : ∀ {m n} (i : Fin m) (j : Fin n) -> toℕ (fwd i j) ≡ toℕ i * n + toℕ j
  soundness {suc m} {n}  zero   j = sym (inject+-lemma (m * n) j)
  soundness     {n = n} (suc i) j rewrite toℕ-raise n (fwd i j)
                                        | soundness i j
                                        = sym (+-assoc n (toℕ i * n) (toℕ j))

Flattened matrix vs 2D matrix lookup equivalence (proof) - 寻求更优雅

Flattened matrix vs 2D matrix lookup equivalence (proof) - seeking more elegance

proof

agda