module Bug where

open import Data.List using (List; []; _∷_; [_]; reverse)
open import Data.List.Properties using (unfold-reverse)
open import Data.List.Relation.Unary.All as AllM using (All; []; _∷_)
open import Data.List.Relation.Unary.All.Properties using (++⁺) 
open import Data.Nat using (ℕ; suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl; ≤-step)
open import Relation.Binary.PropositionalEquality using (sym; subst)


module _ {α} {A : Set α}
  where
  all-reverse :  ∀ {p} {P : A → Set p} {xs : List A} → All P xs →  
                                                         All P (reverse xs)       
  all-reverse {_} {_} {[]}      _            =  []                                
  all-reverse {_} {P} {x ∷ xs} (Px ∷ P-xs) =                                      
                                subst (All P) [rev-xs]:x≡rev-xxs P-[rev-xs]:x     
                      where                                                       
                      P-rev-xs            = all-reverse P-xs                      
                      P-[rev-xs]:x        = ++⁺ P-rev-xs (Px ∷ [])                
                      [rev-xs]:x≡rev-xxs = sym (unfold-reverse x xs)              
 

upFrom : ℕ → ℕ → List ℕ    -- \m c → [m .. m+c]    
upFrom m 0         =  [ m ]                                                       
upFrom m (suc cnt) =  m ∷ (upFrom (suc m) cnt)                                    

upTo : ℕ → List ℕ   
upTo = upFrom 0  

downFrom : ℕ → List ℕ
downFrom 0       =  [ 0 ]
downFrom (suc n) =  (suc n) ∷ (downFrom n)

downFrom-n-≤n : ∀ n → All (_≤ n) (downFrom n)
downFrom-n-≤n 0       =  z≤n ∷ []
downFrom-n-≤n (suc n) =  ≤-refl ∷ (AllM.map ≤-step (downFrom-n-≤n n))

xs≤⇒rev-xs≤ :  ∀ n → {xs : List ℕ} → All (_≤ n) xs → All (_≤ n) (reverse xs)
xs≤⇒rev-xs≤ n =  all-reverse {P = (_≤ n)}

upTo-n≤n :  ∀ n → All (_≤ n) (upTo n)
upTo-n≤n n =  xs≤⇒rev-xs≤ n (downFrom-n-≤n n)