33--
44-- An equational reasoning library for propositional equality over
55-- vectors of different indices using cast.
6+ --
7+ -- To see example usages of this library, scroll to the `Combinators`
8+ -- section.
69------------------------------------------------------------------------
710
811{-# OPTIONS --cubical-compatible --safe #-}
912
1013module README.Data.Vec.Relation.Binary.Equality.Cast where
1114
1215open import Agda.Primitive
13- open import Data.List.Base as L using (List)
14- import Data.List.Properties as Lₚ
16+ open import Data.List.Base as List using (List)
17+ import Data.List.Properties as List
1518open import Data.Nat.Base
1619open import Data.Nat.Properties
1720open import Data.Vec.Base
1821open import Data.Vec.Properties
1922open import Data.Vec.Relation.Binary.Equality.Cast
2023open import Relation.Binary.PropositionalEquality
21- using (_≡_; refl; trans; sym; cong; subst ; module ≡-Reasoning )
24+ using (_≡_; refl; sym; cong; module ≡-Reasoning )
2225
2326private variable
2427 a : Level
@@ -27,10 +30,6 @@ private variable
2730 xs ys zs ws : Vec A n
2831
2932
30- -- To see example usages of this library, scroll to the combinators
31- -- section.
32-
33-
3433------------------------------------------------------------------------
3534-- Motivation
3635--
@@ -60,20 +59,20 @@ private variable
6059-- Although `cast` makes it possible to prove vector identities by ind-
6160-- uction, the explicit type-casting nature poses a significant barrier
6261-- to code reuse in larger proofs. For example, consider the identity
63- -- ‘fromList (xs L .∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `L ._∷ʳ_` is the
62+ -- ‘fromList (xs List .∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `List ._∷ʳ_` is the
6463-- snoc function of lists. We have
6564--
66- -- fromList (xs L .∷ʳ x) : Vec A (L .length (xs L .∷ʳ x))
65+ -- fromList (xs List .∷ʳ x) : Vec A (List .length (xs List .∷ʳ x))
6766-- = {- by definition -}
68- -- fromList (xs L .++ L .[ x ]) : Vec A (L .length (xs L .++ L .[ x ]))
67+ -- fromList (xs List .++ List .[ x ]) : Vec A (List .length (xs List .++ List .[ x ]))
6968-- = {- by fromList-++ -}
70- -- fromList xs ++ fromList L .[ x ] : Vec A (L .length xs + L .length [ x ])
69+ -- fromList xs ++ fromList List .[ x ] : Vec A (List .length xs + List .length [ x ])
7170-- = {- by definition -}
72- -- fromList xs ++ [ x ] : Vec A (L .length xs + 1)
71+ -- fromList xs ++ [ x ] : Vec A (List .length xs + 1)
7372-- = {- by unfold-∷ʳ -}
74- -- fromList xs ∷ʳ x : Vec A (suc (L .length xs))
73+ -- fromList xs ∷ʳ x : Vec A (suc (List .length xs))
7574-- where
76- -- fromList-++ : cast _ (fromList (xs L .++ ys)) ≡ fromList xs ++ fromList ys
75+ -- fromList-++ : cast _ (fromList (xs List .++ ys)) ≡ fromList xs ++ fromList ys
7776-- unfold-∷ʳ : cast _ (xs ∷ʳ x) ≡ xs ++ [ x ]
7877--
7978-- Although the identity itself is simple, the reasoning process changes
@@ -82,31 +81,42 @@ private variable
8281-- rearrange (the Agda version of) the identity into one with two
8382-- `cast`s, resulting in lots of boilerplate code as demonstrated by
8483-- `example1a-fromList-∷ʳ`.
85- example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
86- cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
84+ example1a-fromList-∷ʳ : ∀ (x : A) xs →
85+ .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) →
86+ cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x
8787example1a-fromList-∷ʳ x xs eq = begin
88- cast eq (fromList (xs L.∷ʳ x)) ≡⟨⟩
89- cast eq (fromList (xs L.++ L.[ x ])) ≡⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟨
90- cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
91- cast eq₂ (fromList xs ++ [ x ]) ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
92- fromList xs ∷ʳ x ∎
88+ cast eq (fromList (xs List.∷ʳ x))
89+ ≡⟨⟩
90+ cast eq (fromList (xs List.++ List.[ x ]))
91+ ≡⟨ cast-trans eq₁ eq₂ (fromList (xs List.++ List.[ x ])) ⟨
92+ cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ])))
93+ ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
94+ cast eq₂ (fromList xs ++ [ x ])
95+ ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
96+ fromList xs ∷ʳ x
97+ ∎
9398 where
9499 open ≡-Reasoning
95- eq₁ = Lₚ .length-++ xs {L .[ x ]}
96- eq₂ = +-comm (L .length xs) 1
100+ eq₁ = List .length-++ xs {List .[ x ]}
101+ eq₂ = +-comm (List .length xs) 1
97102
98103-- The `cast`s are irrelevant to core of the proof. At the same time,
99104-- they can be inferred from the lemmas used during the reasoning steps
100105-- (e.g. `fromList-++` and `unfold-∷ʳ`). To eliminate the boilerplate,
101106-- this library provides a set of equational reasoning combinators for
102107-- equality of the form `cast eq xs ≡ ys`.
103- example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
104- cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
108+ example1b-fromList-∷ʳ : ∀ (x : A) xs →
109+ .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) →
110+ cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x
105111example1b-fromList-∷ʳ x xs eq = begin
106- fromList (xs L.∷ʳ x) ≈⟨⟩
107- fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩
108- fromList xs ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟨
109- fromList xs ∷ʳ x ∎
112+ fromList (xs List.∷ʳ x)
113+ ≈⟨⟩
114+ fromList (xs List.++ List.[ x ])
115+ ≈⟨ fromList-++ xs ⟩
116+ fromList xs ++ [ x ]
117+ ≈⟨ unfold-∷ʳ (+-comm 1 (List.length xs)) x (fromList xs) ⟨
118+ fromList xs ∷ʳ x
119+ ∎
110120 where open CastReasoning
111121
112122
@@ -149,7 +159,7 @@ example2b eq xs a ys = begin
149159 (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ -- index: suc m + n
150160 reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ -- index: suc m + n
151161 (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
152- reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n
162+ reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n
153163 xs ʳ++ (a ∷ ys) ∎ -- index: m + suc n
154164 where open CastReasoning
155165
@@ -169,29 +179,35 @@ example2b eq xs a ys = begin
169179-- Note. Technically, `A` and `B` should be vectors of different length
170180-- and that `ys`, `zs` are vectors of non-definitionally equal index.
171181example3a-fromList-++-++ : {xs ys zs : List A} →
172- .(eq : L .length (xs L .++ ys L .++ zs) ≡
173- L .length xs + (L .length ys + L .length zs)) →
174- cast eq (fromList (xs L .++ ys L .++ zs)) ≡
182+ .(eq : List .length (xs List .++ ys List .++ zs) ≡
183+ List .length xs + (List .length ys + List .length zs)) →
184+ cast eq (fromList (xs List .++ ys List .++ zs)) ≡
175185 fromList xs ++ fromList ys ++ fromList zs
176186example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
177- fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
178- fromList xs ++ fromList (ys L.++ zs) ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (Lₚ.length-++ ys) (fromList xs))
179- (fromList-++ ys) ⟩
180- fromList xs ++ fromList ys ++ fromList zs ∎
187+ fromList (xs List.++ ys List.++ zs)
188+ ≈⟨ fromList-++ xs ⟩
189+ fromList xs ++ fromList (ys List.++ zs)
190+ ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩
191+ fromList xs ++ fromList ys ++ fromList zs
192+ ∎
181193 where open CastReasoning
182194
183195-- As an alternative, one can manually apply `cast-++ʳ` to expose `cast`
184196-- in the subterm. However, this unavoidably duplicates the proof term.
185197example3b-fromList-++-++′ : {xs ys zs : List A} →
186- .(eq : L .length (xs L .++ ys L .++ zs) ≡
187- L .length xs + (L .length ys + L .length zs)) →
188- cast eq (fromList (xs L .++ ys L .++ zs)) ≡
198+ .(eq : List .length (xs List .++ ys List .++ zs) ≡
199+ List .length xs + (List .length ys + List .length zs)) →
200+ cast eq (fromList (xs List .++ ys List .++ zs)) ≡
189201 fromList xs ++ fromList ys ++ fromList zs
190202example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
191- fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
192- fromList xs ++ fromList (ys L.++ zs) ≈⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
193- fromList xs ++ cast _ (fromList (ys L.++ zs)) ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
194- fromList xs ++ fromList ys ++ fromList zs ∎
203+ fromList (xs List.++ ys List.++ zs)
204+ ≈⟨ fromList-++ xs ⟩
205+ fromList xs ++ fromList (ys List.++ zs)
206+ ≈⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩
207+ fromList xs ++ cast _ (fromList (ys List.++ zs))
208+ ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
209+ fromList xs ++ fromList ys ++ fromList zs
210+ ∎
195211 where open CastReasoning
196212
197213-- `≈-cong` can be chained together much like how `cong` can be nested.
@@ -201,12 +217,16 @@ example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
201217example4-cong² : ∀ .(eq : (m + 1 ) + n ≡ n + suc m) a (xs : Vec A m) ys →
202218 cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
203219example4-cong² {m = m} {n} eq a xs ys = begin
204- reverse ((xs ++ [ a ]) ++ ys) ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
220+ reverse ((xs ++ [ a ]) ++ ys)
221+ ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
205222 (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
206223 (unfold-∷ʳ _ a xs)) ⟨
207- reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
208- reverse ys ++ reverse (xs ∷ʳ a) ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
209- ys ʳ++ reverse (xs ∷ʳ a) ∎
224+ reverse ((xs ∷ʳ a) ++ ys)
225+ ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
226+ reverse ys ++ reverse (xs ∷ʳ a)
227+ ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
228+ ys ʳ++ reverse (xs ∷ʳ a)
229+ ∎
210230 where open CastReasoning
211231
212232------------------------------------------------------------------------
@@ -222,25 +242,33 @@ example4-cong² {m = m} {n} eq a xs ys = begin
222242-- reasoning system of `_≈[_]_` and switches back to the reasoning
223243-- system of `_≡_`.
224244example5-fromList-++-++′ : {xs ys zs : List A} →
225- .(eq : L .length (xs L .++ ys L .++ zs) ≡
226- L .length xs + (L .length ys + L .length zs)) →
227- cast eq (fromList (xs L .++ ys L .++ zs)) ≡
245+ .(eq : List .length (xs List .++ ys List .++ zs) ≡
246+ List .length xs + (List .length ys + List .length zs)) →
247+ cast eq (fromList (xs List .++ ys List .++ zs)) ≡
228248 fromList xs ++ fromList ys ++ fromList zs
229249example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
230- fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩
231- fromList xs ++ fromList (ys L.++ zs) ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
232- fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
233- fromList xs ++ fromList ys ++ fromList zs ≡-∎
250+ fromList (xs List.++ ys List.++ zs)
251+ ≈⟨ fromList-++ xs ⟩
252+ fromList xs ++ fromList (ys List.++ zs)
253+ ≃⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩
254+ fromList xs ++ cast _ (fromList (ys List.++ zs))
255+ ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
256+ fromList xs ++ fromList ys ++ fromList zs
257+ ≡-∎
234258 where open CastReasoning
235259
236260-- Of course, it is possible to start with the reasoning system of `_≡_`
237261-- and then switch to the reasoning system of `_≈[_]_`.
238262example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
239263example6a-reverse-∷ʳ {n = n} x xs = begin-≡
240- reverse (xs ∷ʳ x) ≡⟨ ≈-reflexive refl ⟨
241- reverse (xs ∷ʳ x) ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
242- reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1 ) xs [ x ] ⟩
243- x ∷ reverse xs ∎
264+ reverse (xs ∷ʳ x)
265+ ≡⟨ ≈-reflexive refl ⟨
266+ reverse (xs ∷ʳ x)
267+ ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
268+ reverse (xs ++ [ x ])
269+ ≈⟨ reverse-++ (+-comm n 1 ) xs [ x ] ⟩
270+ x ∷ reverse xs
271+ ∎
244272 where open CastReasoning
245273
246274example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
0 commit comments