VecCastReason.agda

{-# OPTIONS --without-K --safe #-}

module VecCastReason where

open import Data.Nat.Base
open import Data.Nat.Properties using (+-comm; +-suc; +-assoc)
open import Data.List.Base as List using (List; []; _∷_)
import Data.List.Properties as Listₚ
open import Data.Vec.Base
open import Data.Vec.Properties hiding (reverse-++; cast-reverse)
open import Function.Base using (_∘_; id; flip)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.Definitions using (Sym; Trans)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≗_; refl; sym; trans; cong; subst; module ≡-Reasoning)

open ≡-Reasoning using (begin_; _∎; step-≡; step-≡˘; _≡⟨⟩_)

open Agda.Primitive using (Level)

variable
  a : Level
  A : Set a
  n m o : ℕ
  xs ys zs ws : Vec A n


≋-by : .(eq : n ≡ m) → REL (Vec A n) (Vec A m) _
≋-by eq xs ys = cast eq xs ≡ ys

infix 5 ≋-by
syntax ≋-by n≡m xs ys = xs ≋[ n≡m ] ys

----------------------------------------------------------------
-- ≋-by is ‘reflexive’, ‘symmetric’ and ‘transitive’

≋-refl : (xs : Vec A n) → xs ≋[ refl ] xs
≋-refl xs = cast-is-id refl xs

≋-sym : ∀ {a} {A : Set a} .{eq : n ≡ m} →
        Sym (≋-by {A = A} eq) (≋-by (sym eq))
≋-sym {eq = eq} {xs} {ys} xs≋ys = begin
  cast (sym eq) ys            ≡˘⟨ cong (cast (sym eq)) xs≋ys ⟩
  cast (sym eq) (cast eq xs)  ≡⟨ cast-trans eq (sym eq) xs ⟩
  cast (trans eq (sym eq)) xs ≡⟨ cast-is-id (trans eq (sym eq)) xs ⟩
  xs                          ∎

≋-trans : ∀ {a} {A : Set a} .{eq₁ : n ≡ m} .{eq₂ : m ≡ o} →
          Trans (≋-by {A = A} eq₁) (≋-by eq₂) (≋-by (trans eq₁ eq₂))
≋-trans {eq₁ = eq₁} {eq₂} {xs} {ys} {zs} xs≋ys ys≋zs = begin
  cast (trans eq₁ eq₂) xs ≡˘⟨ cast-trans eq₁ eq₂ xs ⟩
  cast eq₂ (cast eq₁ xs)  ≡⟨ cong (cast eq₂) xs≋ys ⟩
  cast eq₂ ys             ≡⟨ ys≋zs ⟩
  zs                      ∎

----------------------------------------------------------------
-- convenient syntax for ‘equational’ reasoning

infix 1 begin≋_
infixr 2 step-stop≡ step-≈ step-≈˘ step-≋ step-≋˘
infix 3 _≋∎

begin≋_ : ∀ .{n≡m : n ≡ m} {xs : Vec A n} {ys : Vec A m} →
          xs ≋[ n≡m ] ys →
          cast n≡m xs ≡ ys
begin≋ xs≋ys = xs≋ys

step-stop≡ : ∀ .{n≡m : n ≡ m} (xs : Vec A n) {ys zs : Vec A m} →
             ys ≡ zs →
             xs ≋[ n≡m ] ys →
             xs ≋[ n≡m ] zs
step-stop≡ xs ys≡zs xs≋ys = trans xs≋ys ys≡zs

_≋∎ : ∀ .{eq : n ≡ n} (xs : Vec A n) → cast eq xs ≡ xs
_≋∎ {eq = eq} xs = cast-is-id refl xs


step-≈ : ∀ .{n≡m : n ≡ m} (xs {ys} : Vec A n) {zs : Vec A m} →
         ys ≋[ n≡m ] zs →
         xs ≡ ys →
         xs ≋[ n≡m ] zs
step-≈ {n≡m = n≡m} xs ys≋zs xs≡ys = trans (cong (cast n≡m) xs≡ys) ys≋zs

step-≈˘ : ∀ .{n≡m : n ≡ m} (xs {ys} : Vec A n) {zs : Vec A m} →
          ys ≋[ n≡m ] zs →
          ys ≡ xs →
          xs ≋[ n≡m ] zs
step-≈˘ xs ys≋zs ys≡xs = step-≈ xs ys≋zs (sym ys≡xs)

step-≋ : ∀ .{n≡o : n ≡ o} .{n≡m : n ≡ m} (xs : Vec A n) {ys : Vec A m} {zs : Vec A o} →
         ys ≋[ trans (sym n≡m) n≡o ] zs →
         xs ≋[ n≡m ] ys →
         xs ≋[ n≡o ] zs
step-≋ xs ys≋zs xs≋ys = ≋-trans xs≋ys ys≋zs

step-≋˘ : ∀ .{n≡o : n ≡ o} .{m≡n : m ≡ n} (xs : Vec A n) {ys : Vec A m} {zs : Vec A o} →
          ys ≋[ trans m≡n n≡o ] zs →
          ys ≋[ m≡n ] xs →
          xs ≋[ n≡o ] zs
step-≋˘ xs ys≋zs ys≋xs = step-≋ xs ys≋zs (≋-sym ys≋xs)

syntax step-stop≡ xs ys≡zs xs≋ys = xs ≋⇒≡⟨ xs≋ys ⟩ ys≡zs
syntax step-≈  xs ys≋zs xs≡ys = xs  ≈⟨ xs≡ys ⟩ ys≋zs
syntax step-≈˘ xs ys≋zs ys≡xs = xs ≈˘⟨ ys≡xs ⟩ ys≋zs
syntax step-≋  xs ys≋zs xs≋ys = xs  ≋⟨ xs≋ys ⟩ ys≋zs
syntax step-≋˘ xs ys≋zs ys≋xs = xs ≋˘⟨ ys≋xs ⟩ ys≋zs

∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) x (xs : Vec A n) {ys} →
        cast eq ((xs ∷ʳ x) ++ ys) ≡ xs ++ (x ∷ ys)
∷ʳ-++ eq x []       {ys} = cong (x ∷_) (cast-is-id (cong pred eq) ys)
∷ʳ-++ eq x (y ∷ xs) {ys} = cong (y ∷_) (∷ʳ-++ (cong pred eq) x xs)

++-identityʳ : ∀ {n} .(eq : n ≡ n + zero) (xs : Vec A n) → cast eq xs ≡ xs ++ []
++-identityʳ eq []       = refl
++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)

cast-++ˡ : ∀ .(eq : n ≡ o) (xs : Vec A n) {ys : Vec A m} →
           cast (cong (_+ m) eq) (xs ++ ys) ≡ cast eq xs ++ ys
cast-++ˡ {o = zero}  eq []       {ys} = cast-is-id refl (cast eq [] ++ ys)
cast-++ˡ {o = suc o} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ˡ (cong pred eq) xs)

cast-++ʳ : ∀ .(eq : m ≡ o) (xs : Vec A n) {ys : Vec A m} →
           cast (cong (n +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys
cast-++ʳ {n = zero}  eq []       {ys} = refl
cast-++ʳ {n = suc n} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq xs)




fromList-reverse : (xs : List A) → cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
fromList-reverse List.[] = refl
fromList-reverse (x List.∷ xs) = begin≋
  fromList (List.reverse (x List.∷ xs))         ≋⟨ cast-fromList (Listₚ.ʳ++-defn xs {List.[ x ]}) ⟩
  fromList (List.reverse xs List.++ List.[ x ]) ≋⟨ fromList-++ (List.reverse xs) {List.[ x ]} ⟩
  fromList (List.reverse xs) ++ [ x ]           ≋⟨ unfold-∷ʳ (+-comm _ 1) x vec-of-rev-xs ⟩
  fromList (List.reverse xs) ∷ʳ x               ≋⇒≡⟨ cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) x vec-of-rev-xs ⟩
  cast _ (fromList (List.reverse xs)) ∷ʳ x      ≡⟨ cong (_∷ʳ x) (fromList-reverse xs) ⟩
  reverse (fromList xs) ∷ʳ x                    ≡˘⟨ reverse-∷ x (fromList xs) ⟩
  reverse (x ∷ fromList xs)                     ≡⟨⟩
  reverse (fromList (x List.∷ xs))              ∎
  where vec-of-rev-xs = fromList (List.reverse xs)


∷-ʳ++ : ∀ .(eq : (suc n) + m ≡ n + suc m) x (xs : Vec A n) {ys} →
        cast eq ((x ∷ xs) ʳ++ ys) ≡ xs ʳ++ (x ∷ ys)
∷-ʳ++ eq x xs {ys} = begin≋
  (x ∷ xs) ʳ++ ys         ≈⟨ unfold-ʳ++ (x ∷ xs) ys ⟩
  reverse (x ∷ xs) ++ ys  ≈⟨ cong (_++ ys) (reverse-∷ x xs) ⟩
  (reverse xs ∷ʳ x) ++ ys ≋⟨ ∷ʳ-++ eq x (reverse xs) ⟩
  reverse xs ++ (x ∷ ys)  ≈˘⟨ unfold-ʳ++ xs (x ∷ ys) ⟩
  xs ʳ++ (x ∷ ys)         ≋∎


ʳ++-++ : ∀ .(eq : n + m + o ≡ m + (n + o)) (xs : Vec A n) {ys : Vec A m} {zs : Vec A o} →
         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
ʳ++-++ {n = zero}  {m} {o} eq []       {ys} {zs} = cast-is-id eq (([] ++ ys) ʳ++ zs)
ʳ++-++ {n = suc n} {m} {o} eq (x ∷ xs) {ys} {zs} = begin≋
  (x ∷ xs ++ ys) ʳ++ zs                  ≋⟨ ∷-ʳ++ (sym (+-suc (n + m) o)) x (xs ++ ys) ⟩
  (xs ++ ys) ʳ++ (x ∷ zs)                ≋⟨ ʳ++-++ (eq-induction-step eq) xs ⟩
  ys ʳ++ (xs ʳ++ (x ∷ zs))               ≈⟨ unfold-ʳ++ ys (xs ʳ++ (x ∷ zs)) ⟩
  reverse ys ++ (xs ʳ++ (x ∷ zs))        ≋⇒≡⟨ cast-++ʳ (+-suc n o) (reverse ys) ⟩
  reverse ys ++ cast _ (xs ʳ++ (x ∷ zs)) ≡⟨ cong (reverse ys ++_) (≋-sym (∷-ʳ++ (sym (+-suc n o)) x xs)) ⟩
  reverse ys ++ ((x ∷ xs) ʳ++ zs)        ≡˘⟨ unfold-ʳ++ ys ((x ∷ xs) ʳ++ zs) ⟩
  ys ʳ++ ((x ∷ xs) ʳ++ zs)               ∎
  where
  eq-induction-step : (suc n + m + o ≡ m + (suc n + o)) → ((n + m) + suc o ≡ m + (n + suc o))
  eq-induction-step eq = begin
    n + m + suc o   ≡⟨ +-suc (n + m) o ⟩
    suc (n + m + o) ≡⟨ eq ⟩
    m + suc (n + o) ≡˘⟨ cong (m +_) (+-suc n o) ⟩
    m + (n + suc o) ∎

reverse-++-another : ∀ .(eq : n + m ≡ m + n) (xs : Vec A n) (ys : Vec A m) →
                     cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
reverse-++-another {n = n} {m} eq xs ys = begin≋
  reverse (xs ++ ys)                      ≋⟨ ++-identityʳ (+-comm 0 (n + m)) (reverse (xs ++ ys)) ⟩
  reverse (xs ++ ys) ++ []                ≈˘⟨ unfold-ʳ++ (xs ++ ys) [] ⟩
  (xs ++ ys) ʳ++ []                       ≋⟨ ʳ++-++ (trans (cong (_+ 0) (+-comm n m)) (+-assoc m n zero)) xs ⟩
  ys ʳ++ (xs ʳ++ [])                      ≈⟨ cong (ys ʳ++_) (unfold-ʳ++ xs []) ⟩
  ys ʳ++ (reverse xs ++ [])               ≈⟨ unfold-ʳ++ ys (reverse xs ++ []) ⟩
  reverse ys ++ (reverse xs ++ [])        ≋⇒≡⟨ cast-++ʳ (+-comm n 0) (reverse ys) ⟩
  reverse ys ++ cast _ (reverse xs ++ []) ≡˘⟨ unfold-ʳ++ ys (cast _ (reverse xs ++ [])) ⟩
  ys ʳ++ cast _ (reverse xs ++ [])        ≡⟨ cong (ys ʳ++_) (≋-sym (++-identityʳ (+-comm 0 n) (reverse xs))) ⟩
  ys ʳ++ reverse xs                       ≡⟨ unfold-ʳ++ ys (reverse xs) ⟩
  reverse ys ++ reverse xs                ∎


reverse-++ : ∀ .(eq : n + m ≡ m + n) (xs : Vec A n) (ys : Vec A m) →
             cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
reverse-++ {n = zero}  {m = m} eq []       ys = ++-identityʳ (+-comm zero m) (reverse ys)
reverse-++ {n = suc n} {m = m} eq (x ∷ xs) ys = begin≋
  reverse (x ∷ xs ++ ys)              ≈⟨ reverse-∷ x (xs ++ ys) ⟩
  reverse (xs ++ ys) ∷ʳ x             ≋⟨ cast-∷ʳ (cong suc (+-comm n m)) x (reverse (xs ++ ys)) ⟩
  (cast _ (reverse (xs ++ ys))) ∷ʳ x  ≈⟨ cong (_∷ʳ x) (reverse-++ _ xs ys) ⟩
  (reverse ys ++ reverse xs) ∷ʳ x     ≋⇒≡⟨ ++-∷ʳ _ x (reverse ys) (reverse xs) ⟩
  reverse ys ++ (reverse xs ∷ʳ x)     ≡˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
  reverse ys ++ (reverse (x ∷ xs))    ∎


ʳ++-ʳ++ : ∀ .(eq : (n + m) + o ≡ m + (n + o)) (xs : Vec A n) {ys : Vec A m} {zs} →
          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
ʳ++-ʳ++ {n = n} {m} {o} eq xs {ys} {zs} = begin≋
  (xs ʳ++ ys) ʳ++ zs                         ≈⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
  (reverse xs ++ ys) ʳ++ zs                  ≈⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
  reverse (reverse xs ++ ys) ++ zs           ≋⟨ eq-cong-rev-++ ⟩
  (reverse ys ++ reverse (reverse xs)) ++ zs ≈⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
  (reverse ys ++ xs) ++ zs                   ≋⟨ ++-assoc (trans eq₁ eq) (reverse ys) xs zs ⟩
  reverse ys ++ (xs ++ zs)                   ≈˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩
  ys ʳ++ (xs ++ zs)                          ≋∎
  where
  eq₁ = cong (_+ o) (+-comm m n)
  eq-cong-rev-++ = begin
    cast _ (reverse (reverse xs ++ ys) ++ zs)  ≡⟨ cast-++ˡ (+-comm n m) (reverse (reverse xs ++ ys)) ⟩
    cast _ (reverse (reverse xs ++ ys)) ++ zs  ≡⟨ cong (_++ zs) (reverse-++ (+-comm n m) (reverse xs) ys) ⟩
    (reverse ys ++ reverse (reverse xs)) ++ zs ∎


cast-reverse : ∀ .(eq : n ≡ m) (xs : Vec A n) → cast eq (reverse xs) ≡ reverse (cast eq xs)
cast-reverse {m = zero}  eq []       = refl
cast-reverse {m = suc m} eq (x ∷ xs) = begin≋
  reverse (x ∷ xs)           ≈⟨ reverse-∷ x xs ⟩
  reverse xs ∷ʳ x            ≋⇒≡⟨ cast-∷ʳ eq x (reverse xs) ⟩
  (cast _ (reverse xs)) ∷ʳ x ≡⟨ cong (_∷ʳ x) (cast-reverse _ xs) ⟩
  (reverse (cast _ xs)) ∷ʳ x ≡˘⟨ reverse-∷ x (cast _ xs) ⟩
  reverse (x ∷ cast _ xs)    ≡⟨⟩
  reverse (cast eq (x ∷ xs)) ∎