From 9c18223daae4e4b25001d5c9e818a8fde8ef4c9a Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 14 Sep 2019 15:33:36 +0200 Subject: [PATCH 1/4] =?UTF-8?q?[=20Data.List=20]=20function=20reverse-appe?= =?UTF-8?q?nd=20=5F=CA=B3++=5F,=20simplify=20proofs=20about=20reverse?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The properties are much easier to prove for the generalization of reverse to reverse-append. --- src/Data/List/Base.agda | 7 + src/Data/List/Properties.agda | 202 ++++++++++++------ .../List/Relation/Binary/Equality/Setoid.agda | 7 +- src/Data/List/Relation/Binary/Pointwise.agda | 8 + .../Sublist/Heterogeneous/Properties.agda | 8 + .../Binary/Sublist/Setoid/Properties.agda | 8 + .../Ternary/Interleaving/Properties.agda | 14 +- 7 files changed, 184 insertions(+), 70 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index f4d9272909..8c89a890bf 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -314,6 +314,13 @@ reverseAcc = foldl (flip _∷_) reverse : List A → List A reverse = reverseAcc [] +-- "Reverse append" xs ʳ++ ys = reverse xs ++ ys + +infixr 5 _ʳ++_ + +_ʳ++_ : List A → List A → List A +_ʳ++_ = flip reverseAcc + -- Snoc. infixl 5 _∷ʳ_ diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 1203939b71..a6b1d03f92 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -764,84 +764,152 @@ module _ {P : A → Set p} (P? : Decidable P) where ... | no ¬Px = P.cong (Prod.map id (x ∷_)) (partition-defn xs) ------------------------------------------------------------------------ --- reverse +-- reverse is an involution in the list monoid module _ {a} {A : Set a} where open FunctionProperties {A = List A} _≡_ + open P.≡-Reasoning - unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x - unfold-reverse x xs = helper [ x ] xs - where - open P.≡-Reasoning - helper : (xs ys : List A) → foldl (flip _∷_) xs ys ≡ reverse ys ++ xs - helper xs [] = refl - helper xs (y ∷ ys) = begin - foldl (flip _∷_) (y ∷ xs) ys ≡⟨ helper (y ∷ xs) ys ⟩ - reverse ys ++ y ∷ xs ≡⟨ P.sym (++-assoc (reverse ys) _ _) ⟩ - (reverse ys ∷ʳ y) ++ xs ≡⟨ P.sym $ P.cong (_++ xs) (unfold-reverse y ys) ⟩ - reverse (y ∷ ys) ++ xs ∎ + -- Defining property of reverse-append _ʳ++_. - reverse-++-commute : (xs ys : List A) → - reverse (xs ++ ys) ≡ reverse ys ++ reverse xs - reverse-++-commute [] ys = P.sym (++-identityʳ _) - reverse-++-commute (x ∷ xs) ys = begin - reverse (x ∷ xs ++ ys) ≡⟨ unfold-reverse x (xs ++ ys) ⟩ - reverse (xs ++ ys) ++ [ x ] ≡⟨ P.cong (_++ [ x ]) (reverse-++-commute xs ys) ⟩ - (reverse ys ++ reverse xs) ++ [ x ] ≡⟨ ++-assoc (reverse ys) _ _ ⟩ - reverse ys ++ (reverse xs ++ [ x ]) ≡⟨ P.sym $ P.cong (reverse ys ++_) (unfold-reverse x xs) ⟩ - reverse ys ++ reverse (x ∷ xs) ∎ - where open P.≡-Reasoning + ʳ++=reverse++ : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys + ʳ++=reverse++ [] = refl + ʳ++=reverse++ (x ∷ xs) {ys} = begin + (x ∷ xs) ʳ++ ys ≡⟨⟩ + xs ʳ++ x ∷ ys ≡⟨⟩ + xs ʳ++ [ x ] ++ ys ≡⟨ ʳ++=reverse++ xs ⟩ + reverse xs ++ [ x ] ++ ys ≡⟨ P.sym (++-assoc (reverse xs) _ _) ⟩ + (reverse xs ++ [ x ]) ++ ys ≡⟨ P.cong (_++ ys) (P.sym (ʳ++=reverse++ xs)) ⟩ + (xs ʳ++ [ x ]) ++ ys ≡⟨⟩ + reverse (x ∷ xs) ++ ys ∎ - reverse-involutive : Involutive reverse - reverse-involutive [] = refl - reverse-involutive (x ∷ xs) = begin - reverse (reverse (x ∷ xs)) ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩ - reverse (reverse xs ∷ʳ x) ≡⟨ reverse-++-commute (reverse xs) ([ x ]) ⟩ - x ∷ reverse (reverse (xs)) ≡⟨ P.cong (x ∷_) $ reverse-involutive xs ⟩ - x ∷ xs ∎ - where open P.≡-Reasoning + -- Corollary: reverse of cons is snoc of reverse. - length-reverse : (xs : List A) → length (reverse xs) ≡ length xs - length-reverse [] = refl - length-reverse (x ∷ xs) = begin - length (reverse (x ∷ xs)) ≡⟨ P.cong length $ unfold-reverse x xs ⟩ - length (reverse xs ∷ʳ x) ≡⟨ length-++ (reverse xs) ⟩ - length (reverse xs) + 1 ≡⟨ P.cong (_+ 1) (length-reverse xs) ⟩ - length xs + 1 ≡⟨ +-comm _ 1 ⟩ - suc (length xs) ∎ - where open P.≡-Reasoning + unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x + unfold-reverse x xs = ʳ++=reverse++ xs -reverse-map-commute : (f : A → B) (xs : List A) → - map f (reverse xs) ≡ reverse (map f xs) -reverse-map-commute f [] = refl -reverse-map-commute f (x ∷ xs) = begin - map f (reverse (x ∷ xs)) ≡⟨ P.cong (map f) $ unfold-reverse x xs ⟩ - map f (reverse xs ∷ʳ x) ≡⟨ map-++-commute f (reverse xs) ([ x ]) ⟩ - map f (reverse xs) ∷ʳ f x ≡⟨ P.cong (_∷ʳ f x) $ reverse-map-commute f xs ⟩ - reverse (map f xs) ∷ʳ f x ≡⟨ P.sym $ unfold-reverse (f x) (map f xs) ⟩ - reverse (map f (x ∷ xs)) ∎ - where open P.≡-Reasoning + -- Reverse-append of append is reverse-append after reverse-append. + -- Simple inductive proof. -reverse-foldr : ∀ (f : A → B → B) x ys → - foldr f x (reverse ys) ≡ foldl (flip f) x ys -reverse-foldr f x [] = refl -reverse-foldr f x (y ∷ ys) = begin - foldr f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldr f x) (unfold-reverse y ys) ⟩ - foldr f x ((reverse ys) ∷ʳ y) ≡⟨ foldr-∷ʳ f x y (reverse ys) ⟩ - foldr f (f y x) (reverse ys) ≡⟨ reverse-foldr f (f y x) ys ⟩ - foldl (flip f) (f y x) ys ∎ - where open P.≡-Reasoning + ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs + ʳ++-++ [] = refl + ʳ++-++ (x ∷ xs) {ys} {zs} = begin + (x ∷ xs ++ ys) ʳ++ zs ≡⟨⟩ + (xs ++ ys) ʳ++ x ∷ zs ≡⟨ ʳ++-++ xs ⟩ + ys ʳ++ xs ʳ++ x ∷ zs ≡⟨⟩ + ys ʳ++ (x ∷ xs) ʳ++ zs ∎ -reverse-foldl : ∀ (f : A → B → A) x ys → - foldl f x (reverse ys) ≡ foldr (flip f) x ys -reverse-foldl f x [] = refl -reverse-foldl f x (y ∷ ys) = begin - foldl f x (reverse (y ∷ ys)) ≡⟨ P.cong (foldl f x) (unfold-reverse y ys) ⟩ - foldl f x ((reverse ys) ∷ʳ y) ≡⟨ foldl-∷ʳ f x y (reverse ys) ⟩ - f (foldl f x (reverse ys)) y ≡⟨ P.cong (flip f y) (reverse-foldl f x ys) ⟩ - f (foldr (flip f) x ys) y ∎ - where open P.≡-Reasoning + -- Corollary: reverse is an involution with respect to append. + + reverse-++-commute : (xs ys : List A) → + reverse (xs ++ ys) ≡ reverse ys ++ reverse xs + reverse-++-commute xs ys = begin + reverse (xs ++ ys) ≡⟨⟩ + (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩ + ys ʳ++ xs ʳ++ [] ≡⟨⟩ + ys ʳ++ reverse xs ≡⟨ ʳ++=reverse++ ys ⟩ + reverse ys ++ reverse xs ∎ + + -- Reverse-append of reverse-append is commuted reverse-append after append. + -- Simple inductive proof. + + ʳ++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ʳ++ ys) ʳ++ zs ≡ ys ʳ++ xs ++ zs + ʳ++-ʳ++ [] = refl + ʳ++-ʳ++ (x ∷ xs) {ys} {zs} = begin + ((x ∷ xs) ʳ++ ys) ʳ++ zs ≡⟨⟩ + (xs ʳ++ x ∷ ys) ʳ++ zs ≡⟨ ʳ++-ʳ++ xs ⟩ + (x ∷ ys) ʳ++ xs ++ zs ≡⟨⟩ + ys ʳ++ (x ∷ xs) ++ zs ∎ + + -- Corollary: reverse is involutive. + + reverse-involutive : Involutive reverse + reverse-involutive xs = begin + reverse (reverse xs) ≡⟨⟩ + (xs ʳ++ []) ʳ++ [] ≡⟨ ʳ++-ʳ++ xs ⟩ + [] ʳ++ xs ++ [] ≡⟨⟩ + xs ++ [] ≡⟨ ++-identityʳ xs ⟩ + xs ∎ + + -- length of reverse-append + + length-ʳ++ : ∀ (xs {ys} : List A) → length (xs ʳ++ ys) ≡ length xs + length ys + length-ʳ++ [] = refl + length-ʳ++ (x ∷ xs) {ys} = begin + length ((x ∷ xs) ʳ++ ys) ≡⟨⟩ + length (xs ʳ++ x ∷ ys) ≡⟨ length-ʳ++ xs ⟩ + length xs + length (x ∷ ys) ≡⟨ +-suc _ _ ⟩ + length (x ∷ xs) + length ys ∎ + + -- Corollary: reverse preserves the length. + + length-reverse : length ∘ reverse ≗ length + length-reverse xs = begin + length (reverse xs) ≡⟨⟩ + length (xs ʳ++ []) ≡⟨ length-ʳ++ xs ⟩ + length xs + 0 ≡⟨ +-identityʳ _ ⟩ + length xs ∎ + + -- map distributes over reverse-append. + + map-ʳ++ : (f : A → B) (xs {ys} : List A) → + map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys + map-ʳ++ f [] = refl + map-ʳ++ f (x ∷ xs) {ys} = begin + map f ((x ∷ xs) ʳ++ ys) ≡⟨⟩ + map f (xs ʳ++ x ∷ ys) ≡⟨ map-ʳ++ f xs ⟩ + map f xs ʳ++ map f (x ∷ ys) ≡⟨⟩ + map f xs ʳ++ f x ∷ map f ys ≡⟨⟩ + (f x ∷ map f xs) ʳ++ map f ys ≡⟨⟩ + map f (x ∷ xs) ʳ++ map f ys ∎ + + -- Instance of map-ʳ++: map commutes with reverse. + + reverse-map-commute : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f + reverse-map-commute f xs = begin + map f (reverse xs) ≡⟨⟩ + map f (xs ʳ++ []) ≡⟨ map-ʳ++ f xs ⟩ + map f xs ʳ++ [] ≡⟨⟩ + reverse (map f xs) ∎ + + -- A foldr after a reverse is a foldl. + -- Simple inductive proof. + + foldr-ʳ++ : ∀ (f : A → B → B) b xs {ys} → + foldr f b (xs ʳ++ ys) ≡ foldl (flip f) (foldr f b ys) xs + foldr-ʳ++ f b [] = refl + foldr-ʳ++ f b (x ∷ xs) {ys} = begin + foldr f b ((x ∷ xs) ʳ++ ys) ≡⟨⟩ + foldr f b (xs ʳ++ x ∷ ys) ≡⟨ foldr-ʳ++ f b xs ⟩ + foldl (flip f) (foldr f b (x ∷ ys)) xs ≡⟨⟩ + foldl (flip f) (f x (foldr f b ys)) xs ≡⟨⟩ + foldl (flip f) (foldr f b ys) (x ∷ xs) ∎ + + -- Instantiation to reverse. + + reverse-foldr : ∀ (f : A → B → B) b → + foldr f b ∘ reverse ≗ foldl (flip f) b + reverse-foldr f b xs = foldr-ʳ++ f b xs + + -- A foldl after a reverse is a foldr. + -- Simple inductive proof. + + foldl-ʳ++ : ∀ (f : B → A → B) b xs {ys} → + foldl f b (xs ʳ++ ys) ≡ foldl f (foldr (flip f) b xs) ys + foldl-ʳ++ f b [] = refl + foldl-ʳ++ f b (x ∷ xs) {ys} = begin + foldl f b ((x ∷ xs) ʳ++ ys) ≡⟨⟩ + foldl f b (xs ʳ++ x ∷ ys) ≡⟨ foldl-ʳ++ f b xs ⟩ + foldl f (foldr (flip f) b xs) (x ∷ ys) ≡⟨⟩ + foldl f (f (foldr (flip f) b xs) x) ys ≡⟨⟩ + foldl f (foldr (flip f) b (x ∷ xs)) ys ∎ + + -- Instantiation to reverse. + + reverse-foldl : ∀ (f : B → A → B) b xs → + foldl f b (reverse xs) ≡ foldr (flip f) b xs + reverse-foldl f b xs = foldl-ʳ++ f b xs ------------------------------------------------------------------------ -- _∷ʳ_ diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index 5973b96a77..266ae99127 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -121,7 +121,12 @@ module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys ------------------------------------------------------------------------ --- filter +-- reverse + +infixr 5 _ʳ++⁺_ + +_ʳ++⁺_ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ +_ʳ++⁺_ = PW._ʳ++⁺_ reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys reverse⁺ = PW.reverse⁺ diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index 84cca6b82f..7b7a202293 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -243,6 +243,14 @@ module _ {R : REL A B ℓ} where reverseAcc⁺ rs′ [] = rs′ reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs + infixr 5 _ʳ++⁺_ + + _ʳ++⁺_ : ∀ {as bs as′ bs′} → + Pointwise R as bs → + Pointwise R as′ bs′ → + Pointwise R (as ʳ++ as′) (bs ʳ++ bs′) + rs ʳ++⁺ rs′ = reverseAcc⁺ rs′ rs + reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs) reverse⁺ = reverseAcc⁺ [] diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index 97125a9b12..f1312c65f4 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -292,6 +292,14 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds) reverseAcc⁺ (r ∷ abs) cds = reverseAcc⁺ abs (r ∷ cds) + infixr 5 _ʳ++⁺_ + + _ʳ++⁺_ : ∀ {as bs cs ds} → + Sublist R as bs → + Sublist R cs ds → + Sublist R (as ʳ++ cs) (bs ʳ++ ds) + _ʳ++⁺_ = reverseAcc⁺ + reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs) reverse⁺ rs = reverseAcc⁺ rs [] diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index c317c7e70d..ee595d8635 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -195,6 +195,14 @@ module _ {as bs : List A} where reverseAcc cs as ⊆ reverseAcc ds bs reverseAcc⁺ = HeteroProperties.reverseAcc⁺ + infixr 5 _ʳ++⁺_ + + _ʳ++⁺_ : ∀ {cs ds} → + as ⊆ bs → + cs ⊆ ds → + as ʳ++ cs ⊆ bs ʳ++ ds + _ʳ++⁺_ = reverseAcc⁺ + reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs reverse⁺ = HeteroProperties.reverse⁺ diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda index e8029ca130..cbcd697653 100644 --- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda +++ b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda @@ -38,14 +38,16 @@ module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c} -- _++_ ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → - Interleaving L R as₁ l₁ r₁ → Interleaving L R as₂ l₂ r₂ → + Interleaving L R as₁ l₁ r₁ → + Interleaving L R as₂ l₂ r₂ → Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂) ++⁺ [] sp₂ = sp₂ ++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂) ++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂) ++-disjoint : ∀ {as₁ as₂ l₁ r₂} → - Interleaving L R l₁ [] as₁ → Interleaving L R [] r₂ as₂ → + Interleaving L R l₁ [] as₁ → + Interleaving L R [] r₂ as₂ → Interleaving L R l₁ r₂ (as₁ ++ as₂) ++-disjoint [] sp₂ = sp₂ ++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂ @@ -91,6 +93,14 @@ module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c} reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂ reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂ + infixr 5 _ʳ++⁺_ + + _ʳ++⁺_ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → + Interleaving L R l₁ r₁ as₁ → + Interleaving L R l₂ r₂ as₂ → + Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂) + sp₁ ʳ++⁺ sp₂ = reverseAcc⁺ sp₂ sp₁ + reverse⁺ : ∀ {as l r} → Interleaving L R l r as → Interleaving L R (reverse l) (reverse r) (reverse as) reverse⁺ = reverseAcc⁺ [] From 416cca68082a0d8f8a75a99c55b743693fdd104c Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Mon, 16 Sep 2019 17:44:40 +0200 Subject: [PATCH 2/4] =?UTF-8?q?[=20List.reverse=20]=20new=20name:=20=CA=B3?= =?UTF-8?q?++-defn?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/List/Properties.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index a6b1d03f92..af2c63173d 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -773,21 +773,21 @@ module _ {a} {A : Set a} where -- Defining property of reverse-append _ʳ++_. - ʳ++=reverse++ : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys - ʳ++=reverse++ [] = refl - ʳ++=reverse++ (x ∷ xs) {ys} = begin + ʳ++-defn : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys + ʳ++-defn [] = refl + ʳ++-defn (x ∷ xs) {ys} = begin (x ∷ xs) ʳ++ ys ≡⟨⟩ xs ʳ++ x ∷ ys ≡⟨⟩ - xs ʳ++ [ x ] ++ ys ≡⟨ ʳ++=reverse++ xs ⟩ + xs ʳ++ [ x ] ++ ys ≡⟨ ʳ++-defn xs ⟩ reverse xs ++ [ x ] ++ ys ≡⟨ P.sym (++-assoc (reverse xs) _ _) ⟩ - (reverse xs ++ [ x ]) ++ ys ≡⟨ P.cong (_++ ys) (P.sym (ʳ++=reverse++ xs)) ⟩ + (reverse xs ++ [ x ]) ++ ys ≡⟨ P.cong (_++ ys) (P.sym (ʳ++-defn xs)) ⟩ (xs ʳ++ [ x ]) ++ ys ≡⟨⟩ reverse (x ∷ xs) ++ ys ∎ -- Corollary: reverse of cons is snoc of reverse. unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x - unfold-reverse x xs = ʳ++=reverse++ xs + unfold-reverse x xs = ʳ++-defn xs -- Reverse-append of append is reverse-append after reverse-append. -- Simple inductive proof. @@ -808,7 +808,7 @@ module _ {a} {A : Set a} where reverse (xs ++ ys) ≡⟨⟩ (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩ ys ʳ++ xs ʳ++ [] ≡⟨⟩ - ys ʳ++ reverse xs ≡⟨ ʳ++=reverse++ ys ⟩ + ys ʳ++ reverse xs ≡⟨ ʳ++-defn ys ⟩ reverse ys ++ reverse xs ∎ -- Reverse-append of reverse-append is commuted reverse-append after append. From e23ebe9d24824500a11ddf1ab4c0b1e159f46c9c Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 17 Sep 2019 10:20:55 +0200 Subject: [PATCH 3/4] [ List.reverse ] CHANGELOG [ci skip] --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e656b701b0..d0aa1164f2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -193,6 +193,10 @@ Other minor additions *-suc : m * sucℤ n ≡ m + m * n ``` +* Added to `Data.List` the reverse-append function `_ʳ++_` + which is `reverseAcc` with the intuitive argument order. + Generalized the properties of `reverse` to `_ʳ++_`. + * Added new definitions to `Data.List.Relation.Unary.All`: ```agda Null = All (λ _ → ⊥) From 3e9cdeb996324836dced413456f5b024c440ba44 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Thu, 19 Sep 2019 13:38:42 +0200 Subject: [PATCH 4/4] =?UTF-8?q?[=20List.reverse=20]=20=5F=CA=B3++=E2=81=BA?= =?UTF-8?q?=5F=20to=20=CA=B3++=E2=81=BA.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This patch should be undone along with making ++⁺ infix. In general, the predicate/relation-lifiting of an infix operator should be again an infix operator (arguments permitting). --- src/Data/List/Relation/Binary/Equality/Setoid.agda | 6 ++---- src/Data/List/Relation/Binary/Pointwise.agda | 6 ++---- .../Binary/Sublist/Heterogeneous/Properties.agda | 12 +++++------- .../Relation/Binary/Sublist/Setoid/Properties.agda | 12 +++++------- .../Relation/Ternary/Interleaving/Properties.agda | 12 +++++------- 5 files changed, 19 insertions(+), 29 deletions(-) diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index 266ae99127..f97463a3b8 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -123,10 +123,8 @@ module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) ------------------------------------------------------------------------ -- reverse -infixr 5 _ʳ++⁺_ - -_ʳ++⁺_ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ -_ʳ++⁺_ = PW._ʳ++⁺_ +ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ +ʳ++⁺ = PW.ʳ++⁺ reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys reverse⁺ = PW.reverse⁺ diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index 7b7a202293..31378e17c3 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -243,13 +243,11 @@ module _ {R : REL A B ℓ} where reverseAcc⁺ rs′ [] = rs′ reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs - infixr 5 _ʳ++⁺_ - - _ʳ++⁺_ : ∀ {as bs as′ bs′} → + ʳ++⁺ : ∀ {as bs as′ bs′} → Pointwise R as bs → Pointwise R as′ bs′ → Pointwise R (as ʳ++ as′) (bs ʳ++ bs′) - rs ʳ++⁺ rs′ = reverseAcc⁺ rs′ rs + ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs) reverse⁺ = reverseAcc⁺ [] diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index f1312c65f4..08de7bcd83 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -292,13 +292,11 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds) reverseAcc⁺ (r ∷ abs) cds = reverseAcc⁺ abs (r ∷ cds) - infixr 5 _ʳ++⁺_ - - _ʳ++⁺_ : ∀ {as bs cs ds} → - Sublist R as bs → - Sublist R cs ds → - Sublist R (as ʳ++ cs) (bs ʳ++ ds) - _ʳ++⁺_ = reverseAcc⁺ + ʳ++⁺ : ∀ {as bs cs ds} → + Sublist R as bs → + Sublist R cs ds → + Sublist R (as ʳ++ cs) (bs ʳ++ ds) + ʳ++⁺ = reverseAcc⁺ reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs) reverse⁺ rs = reverseAcc⁺ rs [] diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index ee595d8635..9180d50fa6 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -195,13 +195,11 @@ module _ {as bs : List A} where reverseAcc cs as ⊆ reverseAcc ds bs reverseAcc⁺ = HeteroProperties.reverseAcc⁺ - infixr 5 _ʳ++⁺_ - - _ʳ++⁺_ : ∀ {cs ds} → - as ⊆ bs → - cs ⊆ ds → - as ʳ++ cs ⊆ bs ʳ++ ds - _ʳ++⁺_ = reverseAcc⁺ + ʳ++⁺ : ∀ {cs ds} → + as ⊆ bs → + cs ⊆ ds → + as ʳ++ cs ⊆ bs ʳ++ ds + ʳ++⁺ = reverseAcc⁺ reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs reverse⁺ = HeteroProperties.reverse⁺ diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda index cbcd697653..5bb149a5a9 100644 --- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda +++ b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda @@ -93,13 +93,11 @@ module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c} reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂ reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂ - infixr 5 _ʳ++⁺_ - - _ʳ++⁺_ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → - Interleaving L R l₁ r₁ as₁ → - Interleaving L R l₂ r₂ as₂ → - Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂) - sp₁ ʳ++⁺ sp₂ = reverseAcc⁺ sp₂ sp₁ + ʳ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} → + Interleaving L R l₁ r₁ as₁ → + Interleaving L R l₂ r₂ as₂ → + Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂) + ʳ++⁺ sp₁ sp₂ = reverseAcc⁺ sp₂ sp₁ reverse⁺ : ∀ {as l r} → Interleaving L R l r as → Interleaving L R (reverse l) (reverse r) (reverse as)