------------------------------------------------------------------------
-- The Agda standard library
--
-- An equational reasoning library for propositional equality over
-- vectors of different indices using cast.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module README.Data.Vec.Relation.Binary.Equality.Cast where
open import Agda.Primitive
open import Data.List.Base as L using (List)
import Data.List.Properties as Lₚ
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Vec.Base
open import Data.Vec.Properties
open import Data.Vec.Relation.Binary.Equality.Cast
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; trans; sym; cong; subst; module ≡-Reasoning)
private variable
a : Level
A : Set a
l m n o : ℕ
xs ys zs ws : Vec A n
-- To see example usages of this library, scroll to the combinators
-- section.
------------------------------------------------------------------------
-- Motivation
--
-- The `cast` function is the computational variant of `subst` for
-- vectors. Since `cast` computes under vector constructors, it
-- enables reasoning about vectors with non-definitionally equal indices
-- by induction. See, e.g., Jacques Carette's comment in issue #1668.
-- <https://github.com/agda/agda-stdlib/pull/1668#issuecomment-1003449509>
--
-- Suppose we want to prove that ‘xs ++ [] ≡ xs’. Because `xs ++ []`
-- has type `Vec A (n + 0)` while `xs` has type `Vec A n`, they cannot
-- be directly related by homogeneous equality.
-- To resolve the issue, `++-right-identity` uses `cast` to recast
-- `xs ++ []` as a vector in `Vec A n`.
--
++-right-identity : ∀ .(eq : n + 0 ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
++-right-identity eq [] = refl
++-right-identity eq (x ∷ xs) = cong (x ∷_) (++-right-identity (cong pred eq) xs)
--
-- When the input is `x ∷ xs`, because `cast eq (x ∷ _)` equals
-- `x ∷ cast (cong pred eq) _`, the proof obligation
-- cast eq (x ∷ xs ++ []) ≡ x ∷ xs
-- simplifies to
-- x :: cast (cong pred eq) (xs ++ []) ≡ x ∷ xs
-- Although `cast` makes it possible to prove vector identities by ind-
-- uction, the explicit type-casting nature poses a significant barrier
-- to code reuse in larger proofs. For example, consider the identity
-- ‘fromList (xs L.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `L._∷ʳ_` is the
-- snoc function of lists. We have
--
-- fromList (xs L.∷ʳ x) : Vec A (L.length (xs L.∷ʳ x))
-- = {- by definition -}
-- fromList (xs L.++ L.[ x ]) : Vec A (L.length (xs L.++ L.[ x ]))
-- = {- by fromList-++ -}
-- fromList xs ++ fromList L.[ x ] : Vec A (L.length xs + L.length [ x ])
-- = {- by definition -}
-- fromList xs ++ [ x ] : Vec A (L.length xs + 1)
-- = {- by unfold-∷ʳ -}
-- fromList xs ∷ʳ x : Vec A (suc (L.length xs))
-- where
-- fromList-++ : cast _ (fromList (xs L.++ ys)) ≡ fromList xs ++ fromList ys
-- unfold-∷ʳ : cast _ (xs ∷ʳ x) ≡ xs ++ [ x ]
--
-- Although the identity itself is simple, the reasoning process changes
-- the index in the type twice. Consequently, its Agda translation must
-- insert two `cast`s in the proof. Moreover, the proof first has to
-- rearrange (the Agda version of) the identity into one with two
-- `cast`s, resulting in lots of boilerplate code as demonstrated by
-- `example1a-fromList-∷ʳ`.
example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
example1a-fromList-∷ʳ x xs eq = begin
cast eq (fromList (xs L.∷ʳ x)) ≡⟨⟩
cast eq (fromList (xs L.++ L.[ x ])) ≡˘⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟩
cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
cast eq₂ (fromList xs ++ [ x ]) ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
fromList xs ∷ʳ x ∎
where
open ≡-Reasoning
eq₁ = Lₚ.length-++ xs {L.[ x ]}
eq₂ = +-comm (L.length xs) 1
-- The `cast`s are irrelevant to core of the proof. At the same time,
-- they can be inferred from the lemmas used during the reasoning steps
-- (e.g. `fromList-++` and `unfold-∷ʳ`). To eliminate the boilerplate,
-- this library provides a set of equational reasoning combinators for
-- equality of the form `cast eq xs ≡ ys`.
example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
example1b-fromList-∷ʳ x xs eq = begin
fromList (xs L.∷ʳ x) ≈⟨⟩
fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩
fromList xs ++ [ x ] ≈˘⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟩
fromList xs ∷ʳ x ∎
where open CastReasoning
------------------------------------------------------------------------
-- Combinators
--
-- Let `xs ≈[ m≡n ] ys` denote `cast m≡n xs ≡ ys`. We have reflexivity,
-- symmetry and transitivity:
-- ≈-reflexive : xs ≈[ refl ] xs
-- ≈-sym : xs ≈[ m≡n ] ys → ys ≈[ sym m≡n ] xs
-- ≈-trans : xs ≈[ m≡n ] ys → ys ≈[ n≡o ] zs → xs ≈[ trans m≡n n≡o ] zs
-- Accordingly, `_≈[_]_` admits the standard set of equational reasoning
-- combinators. Suppose `≈-eqn : xs ≈[ m≡n ] ys`,
-- xs ≈⟨ ≈-eqn ⟩ -- `_≈⟨_⟩_` takes a `_≈[_]_` step, adjusting
-- ys -- the index at the same time
--
-- ys ≈˘⟨ ≈-eqn ⟩ -- `_≈˘⟨_⟩_` takes a symmetric `_≈[_]_` step
-- xs
example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
example2a eq xs a ys = begin
(reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
reverse xs ++ (a ∷ ys) ∎ -- index: m + suc n
where open CastReasoning
-- To interoperate with `_≡_`, this library provides `_≂⟨_⟩_` (\-~) for
-- taking a `_≡_` step during equational reasoning.
-- Let `≡-eqn : xs ≡ ys`, then
-- xs ≂⟨ ≡-eqn ⟩ -- Takes a `_≡_` step; no change to the index
-- ys
--
-- ys ≂˘⟨ ≡-eqn ⟩ -- Takes a symmetric `_≡_` step
-- xs
-- Equivalently, `≈-reflexive` injects `_≡_` into `_≈[_]_`. That is,
-- `xs ≂⟨ ≡-eqn ⟩ ys` is the same as `xs ≈⟨ ≈-reflexive ≡-eqn ⟩ ys`.
-- Extending `example2a`, we have:
example2b : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
example2b eq xs a ys = begin
(a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ -- index: suc m + n
reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ -- index: suc m + n
(reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
reverse xs ++ (a ∷ ys) ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩ -- index: m + suc n
xs ʳ++ (a ∷ ys) ∎ -- index: m + suc n
where open CastReasoning
-- Oftentimes index-changing identities apply to only part of the proof
-- term. When reasoning about `_≡_`, `cong` shifts the focus to the
-- subterm of interest. In this library, `≈-cong` does a similar job.
-- Suppose `f : A → B`, `xs : B`, `ys zs : A`, `ys≈zs : ys ≈[ _ ] zs`
-- and `xs≈f⟨c·ys⟩ : xs ≈[ _ ] f (cast _ ys)`, we have
-- xs ≈⟨ ≈-cong f xs≈f⟨c·ys⟩ ys≈zs ⟩
-- f zs
-- The reason for having the extra argument `xs≈f⟨c·ys⟩` is to expose
-- `cast` in the subterm in order to apply the step `ys≈zs`. When using
-- ordinary `cong` the proof has to explicitly push `cast` inside:
-- xs ≈⟨ xs≈f⟨c·ys⟩ ⟩
-- f (cast _ ys) ≂⟨ cong f ys≈zs ⟩
-- f zs
-- Note. Technically, `A` and `B` should be vectors of different length
-- and that `ys`, `zs` are vectors of non-definitionally equal index.
example3a-fromList-++-++ : {xs ys zs : List A} →
.(eq : L.length (xs L.++ ys L.++ zs) ≡
L.length xs + (L.length ys + L.length zs)) →
cast eq (fromList (xs L.++ ys L.++ zs)) ≡
fromList xs ++ fromList ys ++ fromList zs
example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
fromList xs ++ fromList (ys L.++ zs) ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (Lₚ.length-++ ys) (fromList xs))
(fromList-++ ys) ⟩
fromList xs ++ fromList ys ++ fromList zs ∎
where open CastReasoning
-- As an alternative, one can manually apply `cast-++ʳ` to expose `cast`
-- in the subterm. However, this unavoidably duplicates the proof term.
example3b-fromList-++-++′ : {xs ys zs : List A} →
.(eq : L.length (xs L.++ ys L.++ zs) ≡
L.length xs + (L.length ys + L.length zs)) →
cast eq (fromList (xs L.++ ys L.++ zs)) ≡
fromList xs ++ fromList ys ++ fromList zs
example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
fromList xs ++ fromList (ys L.++ zs) ≈⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
fromList xs ++ cast _ (fromList (ys L.++ zs)) ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
fromList xs ++ fromList ys ++ fromList zs ∎
where open CastReasoning
-- `≈-cong` can be chained together much like how `cong` can be nested.
-- In this example, `unfold-∷ʳ` is applied to the term `xs ++ [ a ]`
-- in `(_++ ys)` inside of `reverse`. Thus the proof employs two
-- `≈-cong`.
example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
example4-cong² {m = m} {n} eq a xs ys = begin
reverse ((xs ++ [ a ]) ++ ys) ≈˘⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
(≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
(unfold-∷ʳ _ a xs)) ⟩
reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
reverse ys ++ reverse (xs ∷ʳ a) ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩
ys ʳ++ reverse (xs ∷ʳ a) ∎
where open CastReasoning
------------------------------------------------------------------------
-- Interoperation between `_≈[_]_` and `_≡_`
--
-- This library is designed to interoperate with `_≡_`. Examples in the
-- combinators section showed how to apply `_≂⟨_⟩_` to take an `_≡_`
-- step during equational reasoning about `_≈[_]_`. Recall that
-- `xs ≈[ m≡n ] ys` is a shorthand for `cast m≡n xs ≡ ys`, the
-- combinator is essentially the composition of `_≡_` on the left-hand
-- side of `_≈[_]_`. Dually, the combinator `_≃⟨_⟩_` composes `_≡_` on
-- the right-hand side of `_≈[_]_`. Thus `_≃⟨_⟩_` intuitively ends the
-- reasoning system of `_≈[_]_` and switches back to the reasoning
-- system of `_≡_`.
example5-fromList-++-++′ : {xs ys zs : List A} →
.(eq : L.length (xs L.++ ys L.++ zs) ≡
L.length xs + (L.length ys + L.length zs)) →
cast eq (fromList (xs L.++ ys L.++ zs)) ≡
fromList xs ++ fromList ys ++ fromList zs
example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
fromList xs ++ fromList (ys L.++ zs) ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
fromList xs ++ fromList ys ++ fromList zs ≡-∎
where open CastReasoning
-- Of course, it is possible to start with the reasoning system of `_≡_`
-- and then switch to the reasoning system of `_≈[_]_`.
example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
example6a-reverse-∷ʳ {n = n} x xs = begin-≡
reverse (xs ∷ʳ x) ≡˘⟨ ≈-reflexive refl ⟩
reverse (xs ∷ʳ x) ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
x ∷ reverse xs ∎
where open CastReasoning
example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
example6b-reverse-∷ʳ-by-induction x [] = refl
example6b-reverse-∷ʳ-by-induction x (y ∷ xs) = begin
reverse (y ∷ (xs ∷ʳ x)) ≡⟨ reverse-∷ y (xs ∷ʳ x) ⟩
reverse (xs ∷ʳ x) ∷ʳ y ≡⟨ cong (_∷ʳ y) (example6b-reverse-∷ʳ-by-induction x xs) ⟩
(x ∷ reverse xs) ∷ʳ y ≡⟨⟩
x ∷ (reverse xs ∷ʳ y) ≡˘⟨ cong (x ∷_) (reverse-∷ y xs) ⟩
x ∷ reverse (y ∷ xs) ∎
where open ≡-Reasoning