-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of ListSize is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

module ListSize where

open import Data.List
open import Data.Nat

lsize :  {a} {A : Set a}  List A  
lsize [] = 0
lsize (x  l) = suc (lsize l)

open import Relation.Binary.PropositionalEquality

sl₀+sl₁≡sl₀++l₁ :  {a} {A : Set a} {l₀ l₁ : List A}  lsize l₀ + lsize l₁  lsize (l₀ ++ l₁)
sl₀+sl₁≡sl₀++l₁ {l₀ = []} = refl
sl₀+sl₁≡sl₀++l₁ {l₀ = x  l₀} = cong suc (sl₀+sl₁≡sl₀++l₁ {l₀ = l₀})

_×_ :  {a} {A : Set a}    List A  List A
zero × l = []
suc n × l = l ++ (n × l)

sn×l≡n*sl :  {a} {A : Set a} {l : List A} {n}  lsize (n × l)  n * (lsize l)
sn×l≡n*sl {n = zero} = refl
sn×l≡n*sl {l = l} {suc n} = trans (sym (sl₀+sl₁≡sl₀++l₁ {l₀ = l} {l₁ = n × l})) (cong  x  lsize l + x) (sn×l≡n*sl {n = n}))