PROOF-ListProp-appendAddLengths.agda 946 Bytes
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2 3 4
-- Agda program using the Iowa Agda library

open import bool

5
module PROOF-ListProp-appendAddLengths
Michael Hanus 's avatar
Michael Hanus committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

++ : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
++ [] x = x
++ (y :: z) u = y :: (++ z u)

append : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
append x y = ++ x y

---------------------------------------------------------------------------

appendAddLengths : {a : Set} → (x : 𝕃 a) → (y : 𝕃 a)
                 → ((length x) + (length y)) ≡ (length (append x y))
appendAddLengths [] y = refl
appendAddLengths (x :: xs) y rewrite appendAddLengths xs y = refl

---------------------------------------------------------------------------