List.pf

import Nat
import Option
import Set
import MultiSet
import Pair
import Maps

union List<T> {
  empty
  node(T, List<T>)
}

function length<E>(List<E>) -> Nat {
  length(empty) = 0
  length(node(n, next)) = 1 + length(next)
}

function operator ++ <E>(List<E>, List<E>) -> List<E> {
  operator ++(empty, ys) = ys
  operator ++(node(n, xs), ys) = node(n, xs ++ ys)
}

function reverse<E>(List<E>) -> List<E> {
  reverse(empty) = empty
  reverse(node(n, next)) = reverse(next) ++ node(n, empty)
}

function set_of<T>(List<T>) -> Set<T> {
  set_of(empty) = ∅
  set_of(node(x, xs)) = single(x) ∪ set_of(xs)
}

function mset_of<T>(List<T>) -> MultiSet<T> {
  mset_of(empty) = m_fun(λ{0})
  mset_of(node(x, xs)) = m_one(x) ⨄ mset_of(xs)
}

function map<T,U>(List<T>, fn T->U) -> List<U> {
  map(empty, f) = empty
  map(node(x, ls), f) = node(f(x), map(ls, f))
}

function foldr<T,U>(List<T>, U, fn T,U->U) -> U {
  foldr(empty, u, c) = u
  foldr(node(t, ls), u, c) = c(t, foldr(ls, u, c))
}

function foldl<T,U>(List<T>, U, fn U,T->U) -> U {
  foldl(empty, u, c) = u
  foldl(node(t, ls), u, c) = foldl(ls, c(u, t), c)
}

function down_from(Nat) -> List<Nat> {
  down_from(zero) = empty
  down_from(suc(n)) = node(n, down_from(n))
}

define up_to : fn Nat -> List<Nat> = λ n { reverse(down_from(n)) }

function range_aux(Nat, Nat, Nat) -> List<Nat> {
  range_aux(0, end, k) = map(up_to(end), (λ x { x + k }) : fn Nat->Nat)
  range_aux(suc(begin'), end, k) =
    switch end {
      case zero { empty } /* shouldn't happen */
      case suc(end') { range_aux(begin', end', suc(k)) }
    }
}

define range : fn Nat,Nat -> List<Nat> = λ b, e { range_aux(b, e, 0) }

function interval(Nat, Nat) -> List<Nat> {
  interval(zero, n) = empty
  interval(suc(k), n) = node(n, interval(k, suc(n)))
}

function zip<T,U>(List<T>, List<U>) -> List< Pair<T, U> > {
  zip(empty, ys) = empty
  zip(node(x, xs'), ys) =
    switch ys {
      case empty { empty }
      case node(y, ys') { node(pair(x,y), zip(xs', ys')) }
    }
}

function all_elements<T>(List<T>, fn (T) -> bool) -> bool {
  all_elements(empty, P) = true
  all_elements(node(x, xs'), P) = P(x) and all_elements(xs', P)
}

function filter<E>(List<E>, fn (E)->bool) -> List<E> {
  filter(empty, P) = empty
  filter(node(x, ls), P) =
    if P(x) then node(x, filter(ls, P))
    else filter(ls, P)
}

function remove<T>(List<T>, T) -> List<T> {
  remove(empty, y) = empty
  remove(node(x, xs'), y) =
    if x = y then
      xs'
    else
      node(x, remove(xs', y))
}

function remove_all<T>(List<T>, T) -> List<T> {
  remove_all(empty, y) = empty
  remove_all(node(x, xs'), y) =
    if x = y then
      remove_all(xs', y)
    else
      node(x, remove_all(xs', y))
}

function nth<T>(List<T>, T) -> (fn Nat -> T) {
  nth(empty, default) = λi{default}
  nth(node(x, xs), default) = λi{
    if i = 0 then
      x
    else
       nth(xs, default)(pred(i))
  }
}

function get<T>(List<T>) -> (fn Nat -> Option<T>) {
  get(empty) = λi{none}
  get(node(x, xs)) = λi{
    if i = 0 then
       just(x)
    else
       get(xs)(pred(i))
  }
}

function take<T>(Nat, List<T>) -> List<T> {
  take(0, xs) = empty
  take(suc(n), xs) =
    switch xs {
      case empty { empty }
      case node(x, xs') { node(x, take(n, xs')) }
    }
}

function drop<T>(Nat, List<T>) -> List<T> {
  drop(0, xs) = xs
  drop(suc(n), xs) =
    switch xs {
      case empty { empty }
      case node(x, xs') { drop(n, xs') }
    }
}

define flip : < T,U,V > fn (fn T,U->V) ->(fn U,T->V)
  = generic T,U,V { λf{ λx,y{ f(y,x) }}}

function rev_app<T>(List<T>, List<T>) -> List<T> {
  rev_app(empty, ys) = ys
  rev_app(node(x, xs), ys) = rev_app(xs, node(x, ys))
}

function head<T>(List<T>) -> Option<T> {
  head(empty) = none
  head(node(x, xs)) = just(x)
}

function tail<T>(List<T>) -> List<T> {
  tail(empty) = empty
  tail(node(x, xs)) = xs
}

/********************** Theorems *********************************/

theorem length_one_nat: all x:Nat. length(node(x, empty)) = 1
proof
  arbitrary x:Nat
  equations
  length(node(x, empty)) = 1 + 0  by definition {length, length}
                     ... = 1      by add_zero[1]
end

theorem length_one: all U :type. all x:U. length(node(x, empty)) = 1
proof
  arbitrary U:type
  arbitrary x:U
  equations
    length(node(x, empty)) = 1 + 0  by definition {length, length}
                       ... = 1      by add_zero[1]
end

theorem length_zero_empty: all T:type. all xs:List<T>.
  if length(xs) = 0
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty { . }
    case node(x, xs') {
      suppose len_z
      conclude false
          by apply not_one_add_zero[length(xs')] to
             definition length in len_z
    }
  }
end

theorem length_append: all U :type. all xs :List<U>. all ys :List<U>.
  length(xs ++ ys) = length(xs) + length(ys)
proof
  arbitrary U :type
  enable {length, operator++, operator +, operator +}
  induction List<U>
  case empty {
    arbitrary ys:List<U>
    conclude length(@empty<U> ++ ys) = length(@empty<U>) + length(ys)  by .
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>
    equations
      length(node(n,xs') ++ ys)
          = 1 + length(xs' ++ ys)              by .
      ... = 1 + (length(xs') + length(ys))     by rewrite IH[ys]
      ... = length(node(n,xs')) + length(ys)   by .
  }
end

theorem append_assoc: all U :type. all xs :List<U>. all ys :List<U>, zs:List<U>.
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
proof
  arbitrary U :type
  enable operator++
  induction List<U>
  case empty {
    arbitrary ys :List<U>, zs :List<U>
    conclude (@empty<U> ++ ys) ++ zs = empty ++ (ys ++ zs)  by .
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>, zs :List<U>
    equations
      (node(n,xs') ++ ys) ++ zs
          = node(n, (xs' ++ ys) ++ zs)  by .
      ... = node(n,xs') ++ (ys ++ zs)  by rewrite IH[ys,zs]
  }
end

theorem append_empty: all U :type. all xs :List<U>.
  xs ++ empty = xs
proof
  arbitrary U:type
  induction List<U>
  case empty {
    conclude (empty : List<U>) ++ empty = empty  by definition operator++
  }
  case node(n, xs') suppose IH: xs' ++ empty = xs' {
    equations
      node(n,xs') ++ empty
          = node(n, xs' ++ empty)    by definition operator++
      ... = node(n,xs')              by rewrite IH
  }
end

theorem length_reverse: all U :type. all xs :List<U>.
  length(reverse(xs)) = length(xs)
proof
  arbitrary U : type
  induction List<U>
  case empty {
    conclude length(reverse(@empty<U>)) = length(@empty<U>)
        by definition reverse
  }
  case node(n, xs') suppose IH {
    enable {length, reverse, operator +}
    equations
      length(reverse(node(n,xs')))
          = length(reverse(xs') ++ node(n,empty)) by .
      ... = length(reverse(xs')) + length(node(n,empty))
                    by rewrite length_append<U>[reverse(xs')][node(n,empty)]
      ... = length(xs') + 1        by rewrite IH
      ... = length(node(n,xs'))    by rewrite add_one[length(xs')]
  }
end


theorem length_map: all T:type. all f:fn T->T. all xs:List<T>.
  length(map(xs, f)) = length(xs)
proof
  arbitrary T:type
  arbitrary f:fn T->T
  induction List<T>
  case empty {
    definition map
  }
  case node(x, ls') suppose IH {
    equations
      length(map(node(x,ls'),f))
          = 1 + length(map(ls',f))  by definition {map, length}
      ... = 1 + length(ls')         by rewrite IH
      ... ={ length(node(x,ls')) }     by definition {length}
  }
end

theorem map_id: all T:type. all f:fn T->T. if (all x:T. f(x) = x) then
   all xs:List<T>. map(xs, f) = xs
proof
  arbitrary T:type
  arbitrary f:fn T->T
  suppose fxx: (all x:T. f(x) = x)
  induction List<T>
  case empty {
    conclude map(@empty<T>, f) = empty      by definition map
  }
  case node(x, ls) suppose IH {
    equations
      map(node(x,ls),f)
          = node(f(x), map(ls, f)) by definition map
      ... = node(x, map(ls, f))    by rewrite fxx[x]
      ... = node(x,ls)             by rewrite IH
  }
end

define id_nat : fn Nat -> Nat = λx{x}

theorem map_append: all T:type. all f: fn T->T, ys:List<T>. all xs:List<T>.
  map(xs ++ ys, f) = map(xs,f) ++ map(ys, f)
proof
  arbitrary T:type
  arbitrary f:fn T->T, ys:List<T>
  induction List<T>
  case empty {
    equations
      map(@empty<T> ++ ys, f)
          = map(ys, f)                  by definition operator++
      ... ={ @empty<T> ++ map(ys, f) }        by definition operator++
      ... ={ map(@empty<T>, f) ++ map(ys, f) }  by definition map
  }
  case node(x, xs')
    suppose IH: map(xs' ++ ys, f) = map(xs',f) ++ map(ys, f)
  {
    enable {map, operator++}
    equations
      map((node(x,xs') ++ ys), f)
          = node(f(x), map(xs' ++ ys, f))         by .
      ... = node(f(x), map(xs',f) ++ map(ys,f))   by rewrite IH
      ... = map(node(x,xs'),f) ++ map(ys,f)       by .
  }
end

theorem map_compose: all T:type, U:type, V:type. all f:fn T->U, g:fn U->V.
  all ls :List<T>. map(map(ls, f), g) = map(ls, g ∘ f)
proof
  arbitrary T:type, U:type, V:type
  arbitrary f:fn T->U, g:fn U->V
  induction List<T>
  case empty { definition map }
  case node(x, ls) suppose IH {
    enable {map, operator ∘}
    equations
      map(map(node(x,ls),f),g)
	  = node(g(f(x)), map(map(ls, f), g))  by .
      ... = node(g(f(x)), map(ls, g ∘ f))      by rewrite IH
      ... = map(node(x,ls), g [o] f)           by .
  }
end

theorem zip_id_right: all T:type, U:type. all xs:List<T>. @zip<T,U>(xs, empty) = empty
proof
  arbitrary T:type, U:type
  induction List<T>
  case empty { definition zip }
  case node(x, xs') { definition zip }
end

theorem zip_map: all T1:type, T2:type, U1:type, U2:type.
  all f : fn T1 -> T2, g : fn U1 -> U2.
  all xs:List<T1>. all ys:List<U1>.
  zip(map(xs, f), map(ys, g)) = map(zip(xs,ys), pairfun(f,g))
proof
  arbitrary T1:type, T2:type, U1:type, U2:type
  arbitrary f:fn T1 -> T2, g:fn U1 -> U2
  enable {map, zip}
  induction List<T1>
  case empty {
    arbitrary ys:List<U1>
    conclude zip(map(@empty<T1>, f), map(ys,g)) = map(zip(@empty<T1>,ys), pairfun(f,g))
        by .
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<U1>
    switch ys {
      case empty suppose EQ { . }
      case node(y, ys') {
	equations
	  zip(map(node(x,xs'),f),map(node(y,ys'),g))
	    = node(pair(f(x), g(y)), zip(map(xs',f), map(ys',g)))      by .
	... = node(pair(f(x), g(y)), map(zip(xs',ys'), pairfun(f,g)))
		by rewrite IH[ys']
        ... = node(pair(f(x), g(y)), map(zip(xs', ys'), λp{pair(f(first(p)), g(second(p)))}))
               by definition pairfun
	... ={ map(zip(node(x,xs'),node(y,ys')), pairfun(f,g)) }
		by definition {pairfun, first, second}
      }
    }
  }
end

theorem filter_all: all T:type. all P:fn (T)->bool. all xs:List<T>. 
  if all_elements(xs, P) then filter(xs, P) = xs
proof
  arbitrary T:type
  arbitrary P:fn (T)->bool
  induction List<T>
  case empty {
    suppose cond: all_elements(@empty<T>, P)
    conclude filter(@empty<T>, P) = empty by definition filter
  }
  case node(x, xs') suppose IH: if all_elements(xs',P) then filter(xs',P) = xs' {
    suppose Pxs: all_elements(node(x,xs'),P)
    have Px: P(x) by definition all_elements in Pxs
    suffices (if P(x) then node(x,filter(xs',P)) else filter(xs',P)) = node(x,xs')
        by definition filter
    suffices node(x,filter(xs',P)) = node(x,xs')
        by rewrite (apply eq_true to Px)
    have Pxs': all_elements(xs',P) by definition all_elements in Pxs
    have IH': filter(xs',P) = xs' by apply IH to Pxs'
    rewrite IH'
  }
end

theorem all_elements_implies_member: all T:type. all xs:List<T>.
  all P: fn T -> bool.
  if all_elements(xs,P)
  then (all x:T. if x ∈ set_of(xs) then P(x))
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary P:fn T -> bool
    suppose _
    arbitrary x:T
    suppose x_in_mt
    conclude false  by definition {set_of, operator ∈, rep} in x_in_mt
  }
  case node(x, xs') suppose IH {
    arbitrary P:fn T -> bool
    suppose P_xxs: all_elements(node(x,xs'),P)
    arbitrary y:T
    enable {set_of, operator ∈, rep, operator ∪, single, all_elements}
    suppose prem: x = y or rep(set_of(xs'))(y)
    cases prem
    case xy {
      conclude P(y)  by rewrite xy in P_xxs
    }
    case y_xs {
      have P_xs: all_elements(xs', P)  by P_xxs
      conclude P(y)  by apply (apply IH[P] to P_xs)[y] to y_xs
    }
  }
end

theorem member_implies_all_elements: all T:type. all xs:List<T>.
  all P: fn T -> bool.
  if (all x:T. if x ∈ set_of(xs) then P(x))
  then all_elements(xs,P)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary P: fn T -> bool
    suppose _
    definition all_elements
  }
  case node(x, xs') suppose IH {
    arbitrary P: fn T -> bool
    suppose prem
    suffices P(x) and all_elements(xs',P)   by definition all_elements
    enable {set_of,operator ∪, operator∈, rep, single}
    have Px: P(x)  by prem[x]
    have Pxs: all_elements(xs',P)
        by apply IH[P] to
           suffices all x:T. (if x ∈ set_of(xs') then P(x))  by .
           arbitrary z:T suppose z_xs
	   apply prem[z] to z_xs
    Px, Pxs
  }
end

theorem all_elements_eq_member: all T:type. all xs:List<T>, P: fn(T)->bool.
  all_elements(xs,P) = (all x:T. if x ∈ set_of(xs) then P(x))
proof
  arbitrary T:type
  arbitrary xs:List<T>, P: fn(T)->bool
  apply iff_equal[all_elements(xs,P), (all x:T. if x ∈ set_of(xs) then P(x))]
  to member_implies_all_elements<T>[xs][P],
     all_elements_implies_member<T>[xs][P]
end

theorem all_elements_implies: all T:type. all xs:List<T>.
  all P: fn T -> bool, Q: fn T -> bool.
  if all_elements(xs,P) and (all z:T. if P(z) then Q(z))
  then all_elements(xs,Q)
proof
  arbitrary T:type
  arbitrary xs:List<T>
  arbitrary P: fn T -> bool, Q: fn T -> bool
  suppose prem: all_elements(xs,P) and all z:T. (if P(z) then Q(z))
  have Pxs: (all x:T. if x ∈ set_of(xs) then P(x))
    by rewrite all_elements_eq_member<T>[xs,P] in (conjunct 0 of prem)
  _rewrite all_elements_eq_member<T>[xs,Q]
  arbitrary y:T
  suppose y_xs
  have Py: P(y) by apply Pxs[y] to y_xs
  conclude Q(y) by apply (conjunct 1 of prem)[y] to Py
end

theorem set_of_empty: all T:type. all xs:List<T>.
  if set_of(xs) = ∅
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty {
      .
    }
    case node(x, xs') {
      suppose prem
      have x_xxs: x ∈ (single(x) ∪ set_of(xs'))
        by apply in_left_union<T>[set_of(xs'), x, single(x)]
	   to single_member<T>[x]
      conclude false
        by apply empty_no_members<T>[x]
	   to (rewrite (definition set_of in prem) in x_xxs)
    }
  }
end

theorem mset_of_empty: all T:type. all xs:List<T>.
  if mset_of(xs) = m_fun(λx{0})
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty {
      .
    }
    case node(x, xs') {
      suppose prem
      have cnt_x_z: cnt(m_fun(λx{0} : fn T->Nat))(x) = 0
        by definition cnt
      have cnt_x_pos: 1 ≤ cnt(m_fun(λx{0} : fn T->Nat))(x)
        by suffices 1 ≤ cnt(mset_of(node(x,xs')))(x)
               by rewrite symmetric prem
           suffices 1 ≤ 1 + cnt(mset_of(xs'))(x)
               by definition {mset_of, operator ⨄, cnt, m_one}
	   less_equal_add[1][cnt(mset_of(xs'))(x)]
      conclude false
          by definition {cnt, operator ≤} in
	     cnt_x_pos
    }
  }
end

theorem som_mset_eq_set: all T:type. all xs:List<T>.
  set_of_mset(mset_of(xs)) = set_of(xs)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    suffices char_fun(λx{(if cnt(m_fun(λ{0}:fn T->Nat))(x) = 0
                          then false else true)} : fn T->bool)
           = char_fun(λ_{false})
        by definition {mset_of, set_of, set_of_mset}
    have eq:(λx{if cnt(m_fun(λx{0} : fn T->Nat))(x) = 0 then false else true}
             : fn T->bool)
            = λ_{false}
        by extensionality  arbitrary x:T  definition cnt
    rewrite eq
  }
  case node(x, xs') suppose IH {
    suffices set_of_mset(m_one(x) ⨄ mset_of(xs')) = single(x) ∪ set_of(xs')
        by definition {mset_of, set_of}
    suffices single(x) ∪ set_of_mset(mset_of(xs')) = single(x) ∪ set_of(xs')
        by rewrite som_union<T>[m_one(x), mset_of(xs')]
                 | som_one_single<T>[x]
    rewrite IH
  }
end

theorem remove_all_absent: all T:type. all xs:List<T>. all y:T.
  not (y ∈ set_of(remove_all(xs, y)))
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary y:T
    suffices (if y ∈ char_fun(λ_{false}) then false)
        by definition {remove_all, set_of}
    empty_no_members<T>[y]
  }
  case node(x, xs')
      suppose IH: all y:T. not (y ∈ set_of(remove_all(xs',y)))
  {
    arbitrary y:T
    switch x = y {
      case true suppose xy_true {
        have x_eq_y: x = y by rewrite xy_true
        suffices not (y ∈ set_of(remove_all(node(y,xs'),y)))
            by rewrite x_eq_y
        suffices not (y ∈ set_of(remove_all(xs',y)))
            by definition remove_all
        IH[y]
      }
      case false suppose xy_false {
        suffices not (y ∈ set_of(if x = y then remove_all(xs',y)
                                 else node(x,remove_all(xs',y))))
            by definition remove_all
	suppose y_in_sx_xsy
	have y_in_sx_or_xsy: y ∈ single(x) or y ∈ set_of(remove_all(xs',y))
	  by apply member_union<T>[y,single(x), set_of(remove_all(xs',y))]
	     to (definition set_of in rewrite xy_false in y_in_sx_xsy)
	cases y_in_sx_or_xsy
	case y_in_sx {
	  have xy: x = y by apply single_equal<T> to y_in_sx
	  conclude false by rewrite xy_false in xy
	}
	case y_in_xsy {
	  conclude false by apply IH[y] to y_in_xsy
	}
      }
    }
  }
end

theorem all_elements_member:
  all T:type. all ys: List<T>. all x:T, P: fn T->bool.
  if all_elements(ys, P) and x ∈ set_of(ys)
  then P(x)
proof
  arbitrary T:type arbitrary ys:List<T>
  arbitrary x:T, P:fn T->bool
  suppose prem
  apply (rewrite all_elements_eq_member<T>[ys, P] in conjunct 0 of prem)[x]
  to conjunct 1 of prem
end

theorem all_elements_set_of: all T:type. all xs:List<T>, ys:List<T>, P:fn T -> bool.
  if set_of(xs) = set_of(ys)
  then all_elements(xs, P) = all_elements(ys, P)
proof
  arbitrary T:type
  arbitrary xs:List<T>, ys:List<T>, P:fn T -> bool
  suppose xs_ys
  _rewrite all_elements_eq_member<T>[xs,P] | all_elements_eq_member<T>[ys,P]
  _rewrite xs_ys.
end

theorem set_of_append: all T:type. all xs:List<T>.
  all ys:List<T>.
  set_of(xs ++ ys) = set_of(xs) ∪ set_of(ys)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>
    suffices set_of(ys) = ∅ ∪ set_of(ys)
        by definition {operator++, set_of}
    rewrite empty_union<T>[set_of(ys)]
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>
    _definition {operator++, set_of}
    _rewrite IH[ys]
    _rewrite union_assoc<T>[single(x), set_of(xs'), set_of(ys)].
  }
end

theorem all_elements_append: all T:type. all xs:List<T>.
  all ys:List<T>, P:fn T -> bool.
  if all_elements(xs, P) and all_elements(ys, P)
  then all_elements(xs ++ ys, P)
proof
  arbitrary T:type arbitrary xs:List<T>
  arbitrary ys:List<T>, P:fn T -> bool
  suppose prem
  _rewrite all_elements_eq_member<T>[xs ++ ys, P]
  _rewrite set_of_append<T>[xs][ys]
  arbitrary x:T
  suppose x_xs_ys
  have x_xs_or_x_ys: x ∈ set_of(xs) or x ∈ set_of(ys)
    by apply member_union<T>[x,set_of(xs),set_of(ys)] to x_xs_ys
  cases x_xs_or_x_ys
  case x_xs {
    apply (rewrite all_elements_eq_member<T>[xs,P] in conjunct 0 of prem)[x]
    to x_xs
  }
  case x_ys {
    apply (rewrite all_elements_eq_member<T>[ys,P] in conjunct 1 of prem)[x]
    to x_ys
  }
end

theorem take_append: all E:type. all xs:List<E>. all ys:List<E>.
  take(length(xs), xs ++ ys) = xs
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary ys:List<E>
    _definition {length, operator++, take}.
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    _definition {length, operator++, operator+, take}
    _rewrite zero_add[length(xs')]
    _rewrite IH[ys].
  }
end

theorem nth_drop: all T:type. all n:Nat. all xs:List<T>, i:Nat, d:T.
  nth(drop(n, xs), d)(i) = nth(xs, d)(n + i)
proof
  arbitrary T:type
  induction Nat
  case zero {
    arbitrary xs:List<T>, i:Nat, d:T
    _definition {drop, operator+}.
  }
  case suc(n') suppose IH {
    arbitrary xs:List<T>, i:Nat, d:T
    _definition drop
    switch xs {
      case empty {
        _definition nth.
      }
      case node(x, xs') {
	_definition nth
	have nsz: not (suc(n') + i = 0) by
	  suppose sz conclude false by definition operator + in sz
	_rewrite (apply eq_false to nsz)
	_definition {operator +, pred}
	conclude nth(drop(n',xs'),d)(i) = nth(xs',d)(n' + i) by IH[xs',i,d]
      }
    }
  }
end

theorem nth_append_front: all T:type. all xs:List<T>. all ys:List<T>, i:Nat, d:T.
  if i < length(xs)
  then nth(xs ++ ys, d)(i) = nth(xs, d)(i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, i:Nat, d:T
    suppose i_z: i < length(@empty<T>)
    conclude false by definition {length, operator <, operator ≤} in i_z
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:Nat, d:T
    suppose i_xxs: i < length(node(x,xs))
    _definition operator++
    switch i {
      case zero {
        definition nth
      }
      case suc(i') suppose i_si {
        _definition {nth, pred}
	have i_xs: i' < length(xs) by
	    enable {operator <, operator ≤}
	    conclude i' < length(xs)
              by rewrite i_si in
                 definition {length, operator+,operator+} in i_xxs
	apply IH[ys, i', d] to i_xs
      }
    }
  }
end

theorem nth_append_back: all T:type. all xs:List<T>. all ys:List<T>, i:Nat, d:T.
  nth(xs ++ ys, d)(length(xs) + i) = nth(ys, d)(i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, i:Nat, d:T
    _definition {operator++, length, operator +}.
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:Nat, d:T
    _definition {operator++,length, nth}
    have X: not ((1 + length(xs)) + i = 0)
      by suppose eq_z enable operator + conclude false by eq_z
    _rewrite (apply eq_false to X)
    _definition {operator +, pred, operator+}
    IH[ys, i, d]
  }
end

lemma rev_app_reverse_append: all T:type. all xs:List<T>. all ys:List<T>.
  rev_app(xs, ys) = reverse(xs) ++ ys
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>
    definition {rev_app,reverse,operator++}
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>
    _definition {rev_app, reverse}
    equations
      rev_app(xs', node(x,ys))
          = reverse(xs') ++ node(x,ys) by IH[node(x,ys)]
      ... = reverse(xs') ++ { (node(x,empty) ++ ys) }
            by _definition {operator++,operator++}.
      ... = (reverse(xs') ++ node(x,empty)) ++ ys
            by symmetric append_assoc<T>[reverse(xs')][node(x,empty),ys]
  }
end

lemma foldr_rev_app_foldl:
  all T:type. all xs:List<T>. all ys:List<T>, b:T, f:fn T,T->T.
  foldr(rev_app(xs,ys), b, f) = foldl(xs, foldr(ys,b,f), flip(f))
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, b:T, f:fn T,T->T
    _definition {rev_app,foldl}.
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>, b:T, f:fn T,T->T
    _definition {rev_app}
    _rewrite IH[node(x,ys),b,f]
    _definition {foldl,flip,foldr}.
  }
end

theorem flip_flip:
  all T:type. all f:fn T,T->T. flip(flip(f)) = f
proof
  arbitrary T:type
  arbitrary f:fn T,T->T
  extensionality
  arbitrary x:T, y:T
  _definition flip.
end

theorem foldl_foldr:
  all T:type. all xs:List<T>, b:T, f:fn T,T->T.
  foldl(xs, b, f) = foldr(reverse(xs), b, flip(f))
proof
  arbitrary T:type
  arbitrary xs:List<T>, b:T, f:fn T,T->T
  equations
    foldl(xs, b, f)
        ={ foldl(xs,foldr(@empty<T>, b, flip(f)), flip(flip(f))) }
              by _definition foldr _rewrite flip_flip<T>[f].
    ... = foldr(rev_app(xs,empty),b,flip(f))
              by symmetric foldr_rev_app_foldl<T>[xs][empty,b,flip(f)]
    ... = foldr(reverse(xs) ++ empty, b, flip(f))
              by _rewrite rev_app_reverse_append<T>[xs][empty].
    ... = foldr(reverse(xs), b, flip(f)) 
             by _rewrite append_empty<T>[reverse(xs)].
end

theorem mset_equal_implies_set_equal: all T:type. all xs:List<T>, ys:List<T>.
  if mset_of(xs) = mset_of(ys)
  then set_of(xs) = set_of(ys)
proof
  arbitrary T:type
  arbitrary xs:List<T>, ys:List<T>
  suppose xs_ys
  equations
    set_of(xs) = set_of_mset(mset_of(xs))
               by symmetric som_mset_eq_set<T>[xs]
           ... = set_of_mset(mset_of(ys))
               by _rewrite xs_ys.
	   ... = set_of(ys)
               by som_mset_eq_set<T>[ys]
end

theorem head_append: all E:type. all L:List<E>. all R:List<E>.
  if 0 < length(L) 
  then head(L ++ R) = head(L)
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary R:List<E>
    suppose pos_len
    conclude false  by definition {length, operator <, operator ≤} in pos_len
  }
  case node(x, xs) suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    equations
          head(node(x,xs) ++ R)
        = just(x)                           by definition {operator++,head}
    ... ={ head(node(x,xs)) }            by definition head
  }
end

theorem tail_append: all E:type. all L:List<E>. all R:List<E>.
  if 0 < length(L) 
  then tail(L ++ R) = tail(L) ++ R
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary R:List<E>
    suppose pos_len
    conclude false
      by definition {length, operator <, operator≤} in pos_len
  }
  case node(x, xs') suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    definition {operator++,tail}
  }
end

union ListZipper<T> {
  mkZip(List<T>, List<T>)
}

function zip2list<T>(ListZipper<T>) -> List<T> {
  zip2list(mkZip(ctx, ls)) = rev_app(ctx, ls)
}

function zip_left<T>(ListZipper<T>) -> ListZipper<T> {
  zip_left(mkZip(ctx, ls)) =
	switch ctx {
	  case empty { mkZip(empty, ls) }
	  case node(x, ctx') { mkZip(ctx', node(x, ls)) }
	}
}

function zip_right<T>(ListZipper<T>) -> ListZipper<T> {
  zip_right(mkZip(ctx, ls)) =
	switch ls {
	  case empty {  mkZip(ctx, empty) }
	  case node(x, ls') { mkZip(node(x,ctx), ls') }
	}
}

theorem left_2list_identity: all T:type. all z:ListZipper<T>.
  zip2list(z) = zip2list(zip_left(z))
proof
  arbitrary T:type
  arbitrary z:ListZipper<T>
  switch z {
    case mkZip(ctx, ls) {
      _definition zip_left
      switch ctx {
        case empty { . }
	case node(x,ctx') {
	  _definition {zip2list, rev_app}.
	}
      }
    }
  }
end

theorem right_2list_identity: all T:type. all z:ListZipper<T>.
  zip2list(z) = zip2list(zip_right(z))
proof
  arbitrary T:type
  arbitrary z:ListZipper<T>
  switch z {
    case mkZip(ctx, ls) {
      _definition zip_right
      switch ls {
        case empty { . }
	case node(x,ls') {
	  _definition {zip2list, rev_app}.
	}
      }
    }
  }
end