------------------------------------------------------------------------
-- The Agda standard library
--
-- An equational reasoning library for propositional equality over
-- vectors of different indices using cast.
--
-- See README.Data.Vec.Relation.Binary.Equality.Cast for
-- documentation and examples.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Relation.Binary.Equality.Cast where

open import Level using (Level)
open import Function.Base using (_∘_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Nat.Properties using (suc-injective)
open import Data.Vec.Base
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions using (Sym; Trans)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; trans; sym; cong)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)

private
  variable
    a b : Level
    A B : Set a
    l m n o : ℕ
    xs ys zs : Vec A n


cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
cast-is-id eq []       = refl
cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)

cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
             cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
  cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)


infix  _≈[_]_

_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set _
xs ≈[ eq ] ys = cast eq xs ≡ ys

------------------------------------------------------------------------
-- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’

≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {A = A} {n} xs refl ys)
≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq

≈-sym : .{m≡n : m ≡ n} → Sym {A = Vec A m} _≈[ m≡n ]_ _≈[ sym m≡n ]_
≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
  cast (sym m≡n) ys             ≡⟨ cong (cast (sym m≡n)) xs≈ys ⟨
  cast (sym m≡n) (cast m≡n xs)  ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
  cast (trans m≡n (sym m≡n)) xs ≡⟨ cast-is-id (trans m≡n (sym m≡n)) xs ⟩
  xs                            ∎
  where open ≡-Reasoning

≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} →
          Trans {A = Vec A m} _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
  cast (trans m≡n n≡o) xs ≡⟨ cast-trans m≡n n≡o xs ⟨
  cast n≡o (cast m≡n xs)  ≡⟨ cong (cast n≡o) xs≈ys ⟩
  cast n≡o ys             ≡⟨ ys≈zs ⟩
  zs                      ∎
  where open ≡-Reasoning

≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n))
          {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys →
          f xs ≈[ cong f-len eq ] f ys
≈-cong′ f {m = zero}  {n = zero}  {xs = []}     {ys = []}     refl = cast-is-id refl (f [])
≈-cong′ f {m = suc m} {n = suc n} {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl

------------------------------------------------------------------------
-- Reasoning combinators

module CastReasoning where

  open ≡-Reasoning public
    renaming (begin_ to begin-≡_; _∎ to _≡-∎)

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

  _∎ : (xs : Vec A n) → cast refl xs ≡ xs
  _∎ xs = ≈-reflexive refl

  _≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] ys
  xs ≈⟨⟩ xs≈ys = xs≈ys

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

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

  -- composition of the equality type on the right-hand side of _≈[_]_,
  -- or escaping to ordinary _≡_
  step-≃-⟩ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs
  step-≃-⟩ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)

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

  -- composition of the equality type on the left-hand side of _≈[_]_
  step-≂-⟩ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs
  step-≂-⟩ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs

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

  -- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
  -- operation
  ≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
           xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs
  ≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs)

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

  infix  begin_
  infixr  step-≃-⟩ step-≃-⟨ step-≂-⟩ step-≂-⟨ step-≈-⟩ step-≈-⟨ _≈⟨⟩_ ≈-cong
  infix  _∎

  syntax step-≃-⟩ 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 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