open import Prelude open import Logic.Base open import Logic.Identity open import Logic.ChainReasoning open import Data.List open import ListProperties open import List+ module Derivation {Val : Set} (ø : Val) (_+_ : Val -> Val -> Val) (_↑_ : Val -> Val -> Val) (↑assoc : (a : Val) -> (b : Val) -> (c : Val) -> ((a ↑ b) ↑ c) ≡ (a ↑ (b ↑ c))) (+distr↑ : (a : Val) -> (b : Val) -> (c : Val) -> ((a + (b ↑ c)) ≡ ((a + b) ↑ (a + c)))) where module DChainR = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans) open DChainR -- Some more funcions on lists. til : {A : Set} -> A -> List⁺ (List A) -> List⁺ (List A) til a [ x ]⁺ = (a :: x) ::⁺ [ x ]⁺ til a (x ::⁺ xs) = (a :: x) ::⁺ x ::⁺ xs tails : {A : Set} -> List A -> List⁺ (List A) tails = foldr til [ [] ]⁺ ini : {A : Set} -> A -> List⁺ (List A) -> List⁺ (List A) ini a xs = [] ::⁺ map⁺ (_::_ a) xs inits : {A : Set} -> List A -> List⁺ (List A) inits = foldr ini [ [] ]⁺ -- scan data _∣_ (A : Set) (P : A -> Set) : Set where sub : (x : A) -> P x -> A ∣ P depfst : {A : Set} {P : A -> Set} -> (A ∣ P) -> A depfst (sub x p) = x depsnd : {A : Set} {P : A -> Set} -> (a : (A ∣ P)) -> P (depfst a) depsnd (sub x p) = p scanr-der : {A B : Set} -> (f : A -> B -> B) -> (e : B) -> ∀ (\x -> (List⁺ B ∣ \y -> (map⁺ (foldr f e) ∘ tails) x ≡ y)) scanr-der f e x = sub (foldr (sc f) ([ e ]⁺) x) (chain> (map⁺ (foldr f e) ∘ tails) x === foldr (sc f) ([ e ]⁺) x by foldr-fusion (map⁺ (foldr f e)) (map-til f) x) where sc : {A B : Set} -> (A -> B -> B) -> A -> List⁺ B -> List⁺ B sc f a [ b ]⁺ = f a b ::⁺ [ b ]⁺ sc f a (b ::⁺ x) = f a b ::⁺ b ::⁺ x map-til : {A B : Set} -> (f : A -> B -> B) -> {e : B} -> (a : A) -> (x : List⁺ (List A)) -> map⁺ (foldr f e) (til a x) ≡ sc f a (map⁺ (foldr f e) x) map-til {A} {B} f {e} a [ x ]⁺ = chain> map⁺ (foldr f e) (til a [ x ]⁺) === map⁺ (foldr f e) ((a :: x) ::⁺ [ x ]⁺) by refl === foldr f e (a :: x) ::⁺ map⁺ (foldr f e) [ x ]⁺ by refl === f a (foldr f e x) ::⁺ map⁺ (foldr f e) [ x ]⁺ by refl === sc f a (map⁺ (foldr f e) [ x ]⁺) by refl map-til {A} {B} f {e} a (x ::⁺ xs) = chain> map⁺ (foldr f e) (til a (x ::⁺ xs)) === map⁺ (foldr f e) ((a :: x) ::⁺ x ::⁺ xs) by refl === foldr f e (a :: x) ::⁺ foldr f e x ::⁺ map⁺ (foldr f e) xs by refl === f a (foldr f e x) ::⁺ foldr f e x ::⁺ map⁺ (foldr f e) xs by refl === sc f a (foldr f e x ::⁺ map⁺ (foldr f e) xs) by refl === sc f a (map⁺ (foldr f e) (x ::⁺ xs)) by refl scanr : {A B : Set} -> (A -> B -> B) -> B -> List A -> List⁺ B scanr f e x = depfst (scanr-der f e x) scanr-pf : {A B : Set} -> {f : A -> B -> B} -> {e : B} -> (x : List A) -> ((map⁺ (foldr f e) ∘ tails) x ≡ scanr f e x) scanr-pf {A} {B} {f} {e} x = depsnd (scanr-der f e x) -- Maximum max : List⁺ Val -> Val max = foldr⁺ _↑_ id sum : List Val -> Val sum = foldr _+_ ø max-cat : (x : List⁺ Val) -> (y : List⁺ Val) -> max (x ++⁺ y) ≡ (max x ↑ max y) max-cat x y = chain> max (x ++⁺ y) === foldr⁺ _↑_ (\a -> a ↑ max y) x by foldr⁺-fusion' max (\_ _ -> refl) x === max x ↑ max y by sym (foldr⁺-fusion' (\b -> b ↑ max y) (\a b -> ↑assoc a b (max y)) x) max-concat⁺ : (xs : List⁺ (List⁺ Val)) -> max (concat⁺ xs) ≡ max (map⁺ max xs) max-concat⁺ xs = chain> max (concat⁺ xs) === foldr⁺ (\x a -> max x ↑ a) max xs by foldr⁺-fusion' max (\x y -> max-cat x y) xs === max (foldr⁺ (\x y -> max x ::⁺ y) ([_]⁺ ∘ max) xs) by sym (foldr⁺-fusion' max (\_ _ -> refl) xs) === max (map⁺ max xs) by refl max-map+ : (a : Val) -> (x : List⁺ Val) -> max (map⁺ (_+_ a) x) ≡ (a + max x) max-map+ a x = chain> max (map⁺ (_+_ a) x) === max (foldr⁺ (\b y -> (a + b) ::⁺ y) (\b -> [ a + b ]⁺) x) by refl === foldr⁺ (\b c -> (a + b) ↑ c) (\b -> a + b) x by foldr⁺-fusion' max (\_ _ -> refl) x === a + max x by sym (foldr⁺-fusion' (_+_ a) (\b c -> +distr↑ a b c) x) -- Maximum segment sum segs : {A : Set} -> List A -> List⁺ (List A) segs = concat⁺ ∘ map⁺ inits ∘ tails mss-der : (x : List Val) -> (Val ∣ \m -> (max ∘ map⁺ sum ∘ segs) x ≡ m) mss-der x = sub ((max ∘ scanr _⊗_ ø) x) (chain> (max ∘ map⁺ sum ∘ segs) x === (max ∘ map⁺ sum ∘ concat⁺ ∘ map⁺ inits ∘ tails) x by refl === (max ∘ concat⁺ ∘ map⁺ (map⁺ sum) ∘ map⁺ inits ∘ tails) x by cong max (sym (concat⁺-map⁺ ((map⁺ inits ∘ tails) x))) === (max ∘ map⁺ max ∘ map⁺ (map⁺ sum) ∘ map⁺ inits ∘ tails) x by max-concat⁺ ((map⁺ (map⁺ sum) ∘ map⁺ inits ∘ tails) x) === (max ∘ map⁺ max ∘ map⁺ (map⁺ sum ∘ inits) ∘ tails) x by cong (\xs -> max (map⁺ max xs)) (sym (map⁺-compose (tails x))) === (max ∘ map⁺ (max ∘ map⁺ sum ∘ inits) ∘ tails) x by cong max (sym (map⁺-compose (tails x))) === (max ∘ map⁺ (foldr _⊗_ ø) ∘ tails) x by cong max (map⁺-eq max-sum-prefix (tails x)) === (max ∘ scanr _⊗_ ø) x by cong max (scanr-pf x) ) where _⊕_ : Val -> List⁺ Val -> List⁺ Val a ⊕ y = ø ::⁺ map⁺ (_+_ a) y _⊗_ : Val -> Val -> Val a ⊗ b = ø ↑ (a + b) max-sum-prefix : (x : List Val) -> max (map⁺ sum (inits x)) ≡ foldr _⊗_ ø x max-sum-prefix x = chain> max (map⁺ sum (inits x)) === max (foldr _⊕_ [ ø ]⁺ x) by cong max (foldr-fusion (map⁺ sum) lemma1 x) === foldr _⊗_ ø x by foldr-fusion max lemma2 x where lemma1 : (a : Val) -> (xs : List⁺ (List Val)) -> map⁺ sum (ini a xs) ≡ (a ⊕ (map⁺ sum xs)) lemma1 a xs = chain> map⁺ sum (ini a xs) === ø ::⁺ map⁺ sum (map⁺ (_::_ a) xs) by refl === ø ::⁺ map⁺ (_+_ a) (map⁺ sum xs) by cong (_::⁺_ ø) (chain> map⁺ sum (map⁺ (_::_ a) xs) === map⁺ (sum ∘ (_::_ a)) xs by sym (map⁺-compose xs) === map⁺ ((_+_ a) ∘ sum) xs by map⁺-eq (\x -> refl) xs === map⁺ (_+_ a) (map⁺ sum xs) by (map⁺-compose xs) ) === a ⊕ (map⁺ sum xs) by refl lemma2 : (a : Val) -> (x : List⁺ Val) -> max (a ⊕ x) ≡ (a ⊗ max x) lemma2 a x = chain> max (a ⊕ x) === max (ø ::⁺ map⁺ (_+_ a) x) by refl === ø ↑ max (map⁺ (_+_ a) x) by refl === ø ↑ (a + max x) by cong (\b -> ø ↑ b) (max-map+ a x) === a ⊗ max x by refl mss : List Val -> Val mss x = depfst (mss-der x)