@@ -17,7 +17,7 @@ import Data.List.Properties as List
1717open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_;
1818 s≤s⁻¹; z≤n)
1919open import Data.Nat.Properties
20- using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc)
20+ using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc; +-identityʳ )
2121open import Data.Product.Base as Product
2222 using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
2323open import Data.Sum.Base using ([_,_]′)
@@ -38,6 +38,10 @@ open import Relation.Nullary.Decidable.Core using (Dec; does; yes; _×-dec_; map
3838open import Relation.Nullary.Negation.Core using (contradiction)
3939import Data.Nat.GeneralisedArithmetic as ℕ
4040
41+ private
42+ m+n+o≡n+[m+o] : ∀ m n o → m + n + o ≡ n + (m + o)
43+ m+n+o≡n+[m+o] m n o = trans (cong (_+ o) (+-comm m n)) (+-assoc n m o)
44+
4145private
4246 variable
4347 a b c d p : Level
@@ -479,14 +483,14 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
479483++-injective ws xs eq =
480484 (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
481485
482- ++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) ( xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
483- cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
484- ++-assoc eq [] ys zs = cast-is-id eq (ys ++ zs)
485- ++-assoc eq (x ∷ xs) ys zs = cong (x ∷_) (++-assoc (cong pred eq) xs ys zs)
486+ ++-assoc-eqFree : ∀ ( xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
487+ cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
488+ ++-assoc-eqFree [] ys zs = cast-is-id refl (ys ++ zs)
489+ ++-assoc-eqFree (x ∷ xs) ys zs = cong (x ∷_) (++-assoc-eqFree xs ys zs)
486490
487- ++-identityʳ : ∀ .(eq : n + zero ≡ n) ( xs : Vec A n) → cast eq (xs ++ []) ≡ xs
488- ++-identityʳ eq [] = refl
489- ++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)
491+ ++-identityʳ-eqFree : ∀ ( xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
492+ ++-identityʳ-eqFree [] = refl
493+ ++-identityʳ-eqFree (x ∷ xs) = cong (x ∷_) (++-identityʳ-eqFree xs)
490494
491495cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
492496 cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
@@ -880,9 +884,9 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
880884
881885-- snoc is snoc
882886
883- unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1 ) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
884- unfold-∷ʳ eq x [] = refl
885- unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs)
887+ unfold-∷ʳ-eqFree : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
888+ unfold-∷ʳ-eqFree x [] = refl
889+ unfold-∷ʳ-eqFree x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ-eqFree x xs)
886890
887891∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
888892∷ʳ-injective [] [] refl = (refl , refl)
@@ -930,16 +934,16 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
930934
931935-- _++_ and _∷ʳ_
932936
933- ++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
934- cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
935- ++-∷ʳ {m = zero} eq z [] [] = refl
936- ++-∷ʳ {m = zero} eq z [] (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
937- ++-∷ʳ {m = suc m} eq z (x ∷ xs) ys = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
937+ ++-∷ʳ-eqFree : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
938+ cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
939+ ++-∷ʳ-eqFree {m = zero} z [] [] = refl
940+ ++-∷ʳ-eqFree {m = zero} z [] (y ∷ ys) = cong (y ∷_) (++-∷ʳ-eqFree z [] ys)
941+ ++-∷ʳ-eqFree {m = suc m} z (x ∷ xs) ys = cong (x ∷_) (++-∷ʳ-eqFree z xs ys)
938942
939- ∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
940- cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
941- ∷ʳ-++ eq a [] {ys} = cong (a ∷_) (cast-is-id (cong pred eq) ys)
942- ∷ʳ-++ eq a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++ (cong pred eq) a xs)
943+ ∷ʳ-++-eqFree : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
944+ cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
945+ ∷ʳ-++-eqFree a [] {ys} = cong (a ∷_) (cast-is-id refl ys)
946+ ∷ʳ-++-eqFree a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++-eqFree a xs)
943947
944948------------------------------------------------------------------------
945949-- reverse
@@ -1025,14 +1029,14 @@ map-reverse f (x ∷ xs) = begin
10251029
10261030-- append and reverse
10271031
1028- reverse-++ : ∀ .(eq : m + n ≡ n + m) ( xs : Vec A m) (ys : Vec A n) →
1029- cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
1030- reverse-++ {m = zero} {n = n} eq [] ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
1031- reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
1032+ reverse-++-eqFree : ∀ ( xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
1033+ cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
1034+ reverse-++-eqFree {m = zero} {n = n} [] ys = ≈-sym (++-identityʳ-eqFree (reverse ys))
1035+ reverse-++-eqFree {m = suc m} {n = n} (x ∷ xs) ys = begin
10321036 reverse (x ∷ xs ++ ys) ≂⟨ reverse-∷ x (xs ++ ys) ⟩
10331037 reverse (xs ++ ys) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
1034- (reverse-++ _ xs ys) ⟩
1035- (reverse ys ++ reverse xs) ∷ʳ x ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
1038+ (reverse-++-eqFree xs ys) ⟩
1039+ (reverse ys ++ reverse xs) ∷ʳ x ≈⟨ ++-∷ʳ-eqFree x (reverse ys) (reverse xs) ⟩
10361040 reverse ys ++ (reverse xs ∷ʳ x) ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
10371041 reverse ys ++ (reverse (x ∷ xs)) ∎
10381042 where open CastReasoning
@@ -1076,37 +1080,37 @@ map-ʳ++ {ys = ys} f xs = begin
10761080 map f xs ʳ++ map f ys ∎
10771081 where open ≡-Reasoning
10781082
1079- ∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
1080- cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
1081- ∷-ʳ++ eq a xs {ys} = begin
1083+ ∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
1084+ cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
1085+ ∷-ʳ++-eqFree a xs {ys} = begin
10821086 (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
10831087 reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
1084- (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
1088+ (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩
10851089 reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
10861090 xs ʳ++ (a ∷ ys) ∎
10871091 where open CastReasoning
10881092
1089- ++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) ( xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
1090- cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
1091- ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
1093+ ++-ʳ++-eqFree : ∀ ( xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
1094+ cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
1095+ ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
10921096 ((xs ++ ys) ʳ++ zs) ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
10931097 reverse (xs ++ ys) ++ zs ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys)))
1094- (reverse-++ (+-comm m n) xs ys) ⟩
1095- (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
1098+ (reverse-++-eqFree xs ys) ⟩
1099+ (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) (reverse xs) zs ⟩
10961100 reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
10971101 reverse ys ++ (xs ʳ++ zs) ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
10981102 ys ʳ++ (xs ʳ++ zs) ∎
10991103 where open CastReasoning
11001104
1101- ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) ( xs : Vec A m) {ys : Vec A n} {zs} →
1102- cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
1103- ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
1105+ ʳ++-ʳ++-eqFree : ∀ ( xs : Vec A m) {ys : Vec A n} {zs : Vec A o } → let eq = m+n+o≡n+[m+o] m n o in
1106+ cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
1107+ ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
11041108 (xs ʳ++ ys) ʳ++ zs ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
11051109 (reverse xs ++ ys) ʳ++ zs ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
11061110 reverse (reverse xs ++ ys) ++ zs ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys)))
1107- (reverse-++ (+-comm m n) (reverse xs) ys) ⟩
1111+ (reverse-++-eqFree (reverse xs) ys) ⟩
11081112 (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
1109- (reverse ys ++ xs) ++ zs ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
1113+ (reverse ys ++ xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) xs zs ⟩
11101114 reverse ys ++ (xs ++ zs) ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
11111115 ys ʳ++ (xs ++ zs) ∎
11121116 where open CastReasoning
@@ -1333,14 +1337,91 @@ fromList-reverse List.[] = refl
13331337fromList-reverse (x List.∷ xs) = begin
13341338 fromList (List.reverse (x List.∷ xs)) ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩
13351339 fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
1336- fromList (List.reverse xs) ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨
1340+ fromList (List.reverse xs) ++ [ x ] ≈⟨ unfold-∷ʳ-eqFree x (fromList (List.reverse xs)) ⟨
13371341 fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
13381342 (fromList-reverse xs) ⟩
13391343 reverse (fromList xs) ∷ʳ x ≂⟨ reverse-∷ x (fromList xs) ⟨
13401344 reverse (x ∷ fromList xs) ≈⟨⟩
13411345 reverse (fromList (x List.∷ xs)) ∎
13421346 where open CastReasoning
13431347
1348+ ------------------------------------------------------------------------
1349+ -- TRANSITION TO EQ-FREE LEMMA
1350+ ------------------------------------------------------------------------
1351+ -- Please use the new proofs, which do not require an `eq` parameter.
1352+ -- In v3, `name` will be changed to be the same lemma as `name-eqFree`,
1353+ -- and `name-eqFree` will be deprecated.
1354+
1355+ ++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
1356+ cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
1357+ ++-assoc _ = ++-assoc-eqFree
1358+ {-# WARNING_ON_USAGE ++-assoc
1359+ "Warning: ++-assoc was deprecated in v2.2.
1360+ Please use ++-assoc-eqFree instead, which does not take eq."
1361+ #-}
1362+
1363+ ++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
1364+ ++-identityʳ _ = ++-identityʳ-eqFree
1365+ {-# WARNING_ON_USAGE ++-identityʳ
1366+ "Warning: ++-identityʳ was deprecated in v2.2.
1367+ Please use ++-identityʳ-eqFree instead, which does not take eq."
1368+ #-}
1369+
1370+ unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1 ) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
1371+ unfold-∷ʳ _ = unfold-∷ʳ-eqFree
1372+ {-# WARNING_ON_USAGE unfold-∷ʳ
1373+ "Warning: unfold-∷ʳ was deprecated in v2.2.
1374+ Please use unfold-∷ʳ-eqFree instead, which does not take eq."
1375+ #-}
1376+
1377+ ++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
1378+ cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
1379+ ++-∷ʳ _ = ++-∷ʳ-eqFree
1380+ {-# WARNING_ON_USAGE ++-∷ʳ
1381+ "Warning: ++-∷ʳ was deprecated in v2.2.
1382+ Please use ++-∷ʳ-eqFree instead, which does not take eq."
1383+ #-}
1384+
1385+ ∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
1386+ cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
1387+ ∷ʳ-++ _ = ∷ʳ-++-eqFree
1388+ {-# WARNING_ON_USAGE ∷ʳ-++
1389+ "Warning: ∷ʳ-++ was deprecated in v2.2.
1390+ Please use ∷ʳ-++-eqFree instead, which does not take eq."
1391+ #-}
1392+
1393+ reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
1394+ cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
1395+ reverse-++ _ = reverse-++-eqFree
1396+ {-# WARNING_ON_USAGE reverse-++
1397+ "Warning: reverse-++ was deprecated in v2.2.
1398+ Please use reverse-++-eqFree instead, which does not take eq."
1399+ #-}
1400+
1401+ ∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
1402+ cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
1403+ ∷-ʳ++ _ = ∷-ʳ++-eqFree
1404+ {-# WARNING_ON_USAGE ∷-ʳ++
1405+ "Warning: ∷-ʳ++ was deprecated in v2.2.
1406+ Please use ∷-ʳ++-eqFree instead, which does not take eq."
1407+ #-}
1408+
1409+ ++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
1410+ cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
1411+ ++-ʳ++ _ = ++-ʳ++-eqFree
1412+ {-# WARNING_ON_USAGE ++-ʳ++
1413+ "Warning: ++-ʳ++ was deprecated in v2.2.
1414+ Please use ++-ʳ++-eqFree instead, which does not take eq."
1415+ #-}
1416+
1417+ ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
1418+ cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
1419+ ʳ++-ʳ++ _ = ʳ++-ʳ++-eqFree
1420+ {-# WARNING_ON_USAGE ʳ++-ʳ++
1421+ "Warning: ʳ++-ʳ++ was deprecated in v2.2.
1422+ Please use ʳ++-ʳ++-eqFree instead, which does not take eq."
1423+ #-}
1424+
13441425------------------------------------------------------------------------
13451426-- DEPRECATED NAMES
13461427------------------------------------------------------------------------
0 commit comments