Smaug/agda
1
2
3
4
5
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
{-# OPTIONS --safe --warning=error #-}

open import LogicalFormulae
open import Naturals -- for length

module Lists where
  data Vec {a} (A : Set a) : ℕ → Set a where
    [] : Vec A 0
    _::_ : {len : ℕ} (x : A) (xs : Vec A len) → Vec A (succ len)

  [_] : {a : _} → {A : Set a} → (a : A) → Vec A 1
  [ a ] = a :: []

  _++_ : {a : _} → {A : Set a} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m +N n)
  [] ++ m = m
  (x :: l) ++ m = x :: (l ++ m)

  appendEmptyList : {a : _} → {A : Set a} → {m : ℕ} → (l : Vec A m) → (l ++ [] ≡ l)
  appendEmptyList [] = refl
  appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)

  concatAssoc : {a : _} → {A : Set a} → {m n o : ℕ} → (x : Vec A m) → (y : Vec A n) → (z : Vec A o) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
  concatAssoc [] m n = refl
  concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)

  canMovePrepend : {a : _} → {A : Set a} → (l : A) → {m n : ℕ} → (x : Vec A m) (y : Vec A n) → ((l :: x) ++ y ≡ l :: (x ++ y))
  canMovePrepend l [] n = refl
  canMovePrepend l (x :: m) n = refl

  rev : {a : _} → {A : Set a} → {m : ℕ} → Vec A m → Vec A m
  rev [] = []
  rev (x :: l) = (rev l) ++ [ x ]

  revIsHom : {a : _} → {A : Set a} → {m n : ℕ} → (l1 : Vec A m) → (l2 : Vec A n) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
  revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
  revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
  ... | r = equalityCommutative (appendEmptyList r)
  revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
    where
      s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
      s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
      t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
      t' = revIsHom l1 (x :: l2)
      t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
      t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))

  revRevIsId : {a : _} → {A : Set a} → {m : ℕ} → (l : Vec A m) → (rev (rev l) ≡ l)
  revRevIsId [] = refl
  revRevIsId (x :: l) = t
    where
      s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
      s = revIsHom (rev l) [ x ]
      t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
      t = identityOfIndiscernablesRight (rev (rev l ++ (x :: []))) ([ x ] ++ rev (rev l)) ([ x ] ++ l) _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))

  map : {a : _} → {b : _} → {A : Set a} → {B : Set b} → {m : ℕ} → (f : A → B) → Vec A m → Vec B m
  map f [] = []
  map f (x :: list) = (f x) :: (map f list)