Lists

This development is largely ported from the seq library of SSReflect. The names of several operations have been changed to use the standard Coq list definitions (e.g., seq => list, cat => app, size => length) and a few lemmas have been added.

Require Import Vbase Varith.
Require Coq.omega.Omega.

Set Implicit Arguments.

Open Scope bool_scope.
Open Scope list_scope.

List operations


Section Operations.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Type l : (list T).

Definition ohead l :=
  match l with
    | nilNone
    | x :: _Some x
  end.

Definition head l :=
  match l with
    | nilx0
    | x :: _x
  end.

Definition behead l :=
  match l with
    | nilnil
    | _ :: xx
  end.

Definition ncons n x := iter n (cons x).
Definition nlist n x := ncons n x nil.

Fixpoint snoc l z :=
  match l with
    | nilz :: nil
    | x :: lx :: snoc l z
  end.

Fixpoint last x l :=
  match l with
    | nilx
    | :: last
  end.

Fixpoint olast l :=
  match l with
    | nilNone
    | :: Some (last )
  end.

Fixpoint belast x l :=
  match l with
    | nilnil
    | :: x :: belast
  end.

Indexing

Fixpoint onth l n {struct n} :=
  match l, n with
    | nil, _None
    | x :: l, OSome x
    | x :: l, S nonth l n
  end.

Fixpoint oset_nth l n y {struct n} :=
  match l, n with
    | nil, _None
    | x :: l, OSome (y :: l)
    | x :: l, S nmatch oset_nth l n y with
                       | NoneNone
                       | Some Some (x :: )
                     end
  end.

Fixpoint nth l n {struct n} :=
  match l, n with
    | nil, _x0
    | x :: l, Ox
    | x :: l, S nnth l n
  end.

Fixpoint set_nth l n y {struct n} :=
  match l, n with
    | nil, _ncons n x0 (y :: nil)
    | x :: l, Oy :: l
    | x :: l, S nx :: set_nth l n y
  end.

Searching for elements

Fixpoint In x l :=
  match l with
    | nilFalse
    | y :: ly = x In x l
  end.

Fixpoint find f l :=
  match l with
    | nil ⇒ 0
    | x :: if (f x : bool) then 0 else S (find f )
  end.

Fixpoint filter f l :=
  match l with
    | nilnil
    | x :: if (f x : bool) then x :: filter f else filter f
  end.

Fixpoint count f l :=
  match l with
    | nil ⇒ 0
    | x :: if (f x : bool) then S (count f ) else count f
  end.

Fixpoint has f l :=
  match l with
    | nilfalse
    | x :: f x || has f
  end.

Fixpoint all f l :=
  match l with
    | niltrue
    | x :: f x && all f
  end.

Fixpoint sieve (m : list bool) (s : list T) {struct m} : list T :=
  match m, s with
  | b :: , x :: if b then x :: sieve else sieve
  | _, _nil
  end.

Surgery

Fixpoint drop n l {struct l} :=
  match l, n with
  | _ :: l, S drop l
  | _, _l
  end.

Fixpoint take n l {struct l} :=
  match l, n with
  | x :: l, S x :: take l
  | _, _nil
  end.

Definition rot n l := drop n l ++ take n l.

Definition rotr n l := rot (length l - n) l.

Fixpoint rev_append l1 l2 :=
  match l1 with
    | nill2
    | x :: l1rev_append l1 (x :: l2)
  end.

Index sequence: the list [m; m + 1; ... m + n].

Fixpoint iota (m n : nat) : list nat :=
  match n with
    | Onil
    | S nm :: iota (S m) n
  end.

End Operations.


Definition rev T s :=
  match tt with tt
    rev_append s (@nil T)
  end.

Basic properties


Section SequencesBasic.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Lemma length0nil : s, length s = 0 → s = nil.

Lemma length_behead : s, length (behead s) = (length s) - 1.

Lemma length_ncons : n x s, length (ncons n x s) = n + length s.

Lemma length_nlist : n x, length (nlist n x) = n.

Lemma length_app : s1 s2, length (s1 ++ s2) = length s1 + length s2.

Lemma app0l : s, nil ++ s = s.

Lemma app1l : x s, (x :: nil) ++ s = x :: s.

Lemma app_cons : x s1 s2, (x :: s1) ++ s2 = x :: s1 ++ s2.

Lemma app_ncons : n x s1 s2, ncons n x s1 ++ s2 = ncons n x (s1 ++ s2).

Lemma app_nlist : n x s, nlist n x ++ s = ncons n x s.

Lemma appl0 : s, s ++ nil = s.

Lemma appA : s1 s2 s3, (s1 ++ s2) ++ s3 = s1 ++ (s2 ++ s3).

Lemma nconsE : n x s, ncons n x s = nlist n x ++ s.

last, belast, rcons, and last induction.

Lemma snoc_cons : x s z, snoc (x :: s) z = x :: snoc s z.

Lemma appl1 : l x, l ++ (x :: nil) = snoc l x.

Lemma snocE : l x, snoc l x = l ++ (x :: nil).

Lemma lastI : x s, x :: s = snoc (belast x s) (last x s).

Lemma last_cons : x y s, last x (y :: s) = last y s.

Lemma length_snoc : s x, length (snoc s x) = S (length s).

Lemma length_belast : x s, length (belast x s) = length s.

Lemma last_app : x s1 s2, last x (s1 ++ s2) = last (last x s1) s2.

Lemma last_snoc : x s z, last x (snoc s z) = z.

Lemma belast_app : x s1 s2,
  belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.

Lemma belast_snoc : x s z, belast x (snoc s z) = x :: s.

Lemma app_snoc : x s1 s2, snoc s1 x ++ s2 = s1 ++ x :: s2.

Lemma snoc_app : x s1 s2,
  snoc (s1 ++ s2) x = s1 ++ snoc s2 x.

Inductive last_spec : list TType :=
  | LastNil : last_spec nil
  | LastRcons s x : last_spec (snoc s x).

Lemma lastP : s, last_spec s.

Lemma last_ind :
   P (Hnil: P nil) (Hlast: s x, P sP (snoc s x)) s, P s.

Inductive last_spec_eq (y : list T): Type :=
  | LastEqNil : y = nillast_spec_eq y
  | LastEqRcons s x : y = snoc s xlast_spec_eq y.

Lemma last_eqP : (s: list T), last_spec_eq s.

Sequence indexing.

Lemma nth0 : l, nth x0 l 0 = head x0 l.

Lemma nth_default : s n, length s nnth x0 s n = x0.

Lemma nth_nil : n, nth x0 nil n = x0.

Lemma last_nth : x s, last x s = nth x0 (x :: s) (length s).

Lemma nth_last : s, nth x0 s (length s - 1) = last x0 s.

Lemma nth_behead : s n, nth x0 (behead s) n = nth x0 s (S n).

Lemma nth_app : s1 s2 n,
 nth x0 (s1 ++ s2) n = if ltn n (length s1) then nth x0 s1 n else nth x0 s2 (n - length s1).

Lemma nth_snoc : s x n,
  nth x0 (snoc s x) n = (if n < length s then nth x0 s n else if n == length s then x else x0).

Lemma nth_ncons : m x s n,
  nth x0 (ncons m x s) n = (if ltn n m then x else nth x0 s (n - m)).

Lemma nth_nlist : m x n, nth x0 (nlist m x) n = (if ltn n m then x else x0).

Lemma eq_from_nth : s1 s2
  (EQlength: length s1 = length s2)
  (EQnth: i, i < length s1nth x0 s1 i = nth x0 s2 i),
  s1 = s2.

Lemma length_set_nth :
   s n y, length (set_nth x0 s n y) = (if ltn n (length s) then length s else S n).

Lemma set_nth_nil : n y, set_nth x0 nil n y = ncons n x0 (y :: nil).


Lemma onth0 : l, onth l 0 = ohead l.

Lemma onth_none : s n, length s nonth s n = None.

Lemma onth_nil : n, onth nil n = None (A:=T).

Lemma olast_nth : s, olast s = onth s (length s - 1).

Lemma onth_last : s, onth s (length s - 1) = olast s.

Lemma onth_behead : s n, onth (behead s) n = onth s (S n).

Lemma onth_app : s1 s2 n,
 onth (s1 ++ s2) n = if n < (length s1) then onth s1 n else onth s2 (n - length s1).

Lemma onth_snoc : s x n,
  onth (snoc s x) n = (if n < length s then onth s n else if n == length s then Some x else None).

Lemma onth_ncons : m x s n,
  onth (ncons m x s) n = (if n < m then Some x else onth s (n - m)).

Lemma onth_nlist : m x n, onth (nlist m x) n = (if n < m then Some x else None).

Lemma eq_from_onth : s1 s2
  (EQnth: i, onth s1 i = onth s2 i),
  s1 = s2.

Lemma length_oset_nth :
   s n y (EQ: oset_nth s n y = Some ), length = length s.

Lemma oset_nth_nil : n y, oset_nth nil n y = None.

End SequencesBasic.

Automation support

Properties of find, count, has, all


Section SeqFind.

Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Variable f : pred T.

Lemma count_filter : l, count f l = length (filter f l).

Lemma has_count : l, has f l = ltn 0 (count f l).

Lemma count_length : l, count f l length l.

Lemma all_count : l, all f l = (count f l == length l).

Lemma all_filterP : s, reflect (filter f s = s) (all f s).

Lemma has_find : l, has f l = ltn (find f l) (length l).

Lemma find_length : l, find f l length l.

Lemma find_app : s1 s2,
  find f (s1 ++ s2) = if has f s1 then find f s1 else length s1 + find f s2.

Lemma has_nil : has f nil = false.

Lemma has_list1 : x, has f (x :: nil) = f x.

Lemma all_nil : all f nil = true.

Lemma all_list1 : x, all f (x :: nil) = f x.

Lemma nth_find : s, has f sf (nth x0 s (find f s)).

Lemma before_find : s i, i < find f sf (nth x0 s i) = false.

Lemma filter_app:
   l1 l2, filter f (l1 ++ l2) = filter f l1 ++ filter f l2.

Lemma filter_snoc : s x,
  filter f (snoc s x) = if f x then snoc (filter f s) x else filter f s.

Lemma count_app : s1 s2, count f (s1 ++ s2) = count f s1 + count f s2.

Lemma has_app : s1 s2, has f (s1 ++ s2) = has f s1 || has f s2.

Lemma has_snoc : s x, has f (snoc s x) = f x || has f s.

Lemma all_app : s1 s2, all f (s1 ++ s2) = all f s1 && all f s2.

Lemma all_snoc : s x, all f (snoc s x) = f x && all f s.

Lemma filter_pred0 : s, filter pred0 s = nil.

Lemma filter_predT : s, filter predT s = s.

Lemma filter_predI : a1 a2 s,
  filter (predI a1 a2) s = filter a1 (filter a2 s).

Lemma count_pred0 : s, count pred0 s = 0.

Lemma count_predT : s, count predT s = length s.

Lemma count_predUI : a1 a2 l,
 count (predU a1 a2) l + count (predI a1 a2) l = count a1 l + count a2 l.

Lemma count_predC : a l, count a l + count (predC a) l = length l.

Lemma has_pred0 : s, has pred0 s = false.

Lemma has_predT : s, has predT s = (0 < length s).

Lemma has_predC : a l, has (predC a) l = negb (all a l).

Lemma has_predU : a1 a2 l, has (predU a1 a2) l = has a1 l || has a2 l.

Lemma all_pred0 : l, all pred0 l = (length l == 0).

Lemma all_predT : s, all predT s = true.

Lemma all_predC : a s, all (predC a) s = negb (has a s).

Lemma all_predI : a1 a2 s, all (predI a1 a2) s = all a1 s && all a2 s.

Section EqLemmas.

Variables (a1 a2 : pred T).
Variable (EQ : a1 =1 a2).

Lemma eq_find : find a1 =1 find a2.

Lemma eq_filter : filter a1 =1 filter a2.

Lemma eq_count : count a1 =1 count a2.

Lemma eq_has : has a1 =1 has a2.

Lemma eq_all : all a1 =1 all a2.

End EqLemmas.

End SeqFind.

Automation support

Surgery: drop, take, rot, rotr.


Section SequenceSurgery.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Lemma drop_behead : drop n0 =1 iter n0 (@behead T).

Lemma drop0 : s, drop 0 s = s.

Hint Rewrite drop0 : vlib.
Lemma drop1 : l, drop 1 l = behead l.

Lemma drop_overlength : n s, length s ndrop n s = nil.
Implicit Arguments drop_overlength [n s].

Lemma drop_length : s, drop (length s) s = nil.

Lemma drop_cons : x s,
  drop n0 (x :: s) = (match n0 with Ox :: s | S ndrop n s end).

Lemma length_drop : s, length (drop n0 s) = length s - n0.

Lemma drop_app : s1 s2,
 drop n0 (s1 ++ s2) =
   if ltn n0 (length s1) then drop n0 s1 ++ s2 else drop (n0 - length s1) s2.

Lemma drop_length_app : n s1 s2, length s1 = ndrop n (s1 ++ s2) = s2.

Lemma nconsK : n x, cancel (ncons n x) (drop n).

Lemma take0 : s, take 0 s = nil.

Hint Rewrite take0 : vlib.
Lemma take_overlength : n s, length s ntake n s = s.
Implicit Arguments take_overlength [n s].

Lemma take_length : s, take (length s) s = s.

Lemma take_cons : x s,
  take n0 (x :: s) = (match n0 with Onil | S nx :: take n s end).

Lemma drop_snoc : s, n0 length s
   x, drop n0 (snoc s x) = snoc (drop n0 s) x.

Lemma app_take_drop : s, take n0 s ++ drop n0 s = s.

Lemma length_takel : s (H: n0 length s), length (take n0 s) = n0.

Lemma length_take : s,
  length (take n0 s) = if ltn n0 (length s) then n0 else length s.

Lemma take_app : s1 s2,
 take n0 (s1 ++ s2) =
   if ltn n0 (length s1) then take n0 s1 else s1 ++ take (n0 - length s1) s2.

Lemma take_length_app : n s1 s2, length s1 = ntake n (s1 ++ s2) = s1.

Lemma takel_app : s1, n0 length s1
   s2, take n0 (s1 ++ s2) = take n0 s1.

Lemma nth_drop : s i, nth x0 (drop n0 s) i = nth x0 s (n0 + i).

Lemma nth_take : i, i < n0 s, nth x0 (take n0 s) i = nth x0 s i.


Lemma drop_nth : n s, n < length sdrop n s = nth x0 s n :: drop (S n) s.

Lemma take_nth : n s, n < length s
  take (S n) s = snoc (take n s) (nth x0 s n).

Lemma rot0 : s, rot 0 s = s.

Lemma length_rot : s, length (rot n0 s) = length s.

Lemma rot_overlength : n s (H: length s n), rot n s = s.

Lemma rot_length : s, rot (length s) s = s.

Lemma has_rot : l f, has f (rot n0 l) = has f l.

Lemma all_rot : l f, all f (rot n0 l) = all f l.

Lemma rot_length_app : s1 s2, rot (length s1) (s1 ++ s2) = s2 ++ s1.

Lemma rotK : l, rotr n0 (rot n0 l) = l.

Lemma rot_inj : injective (@rot T n0).

Lemma rot1_cons : x s, rot 1 (x :: s) = snoc s x.

End SequenceSurgery.

Automation support


Hint Rewrite drop0 drop_length length_drop : vlib.
Hint Rewrite take0 take_length length_take : vlib.
Hint Rewrite nth_drop : vlib.
Hint Rewrite rot0 length_rot rot_length has_rot all_rot rot_length_app rotK rot1_cons : vlib.

Section Rev.

Variable T : Type.
Implicit Type s : list T.

Lemma rev_nil : rev nil = (@nil T).

Lemma rev_snoc : s x, rev (snoc s x) = x :: (rev s).

Lemma rev_cons : x s, rev (x :: s) = snoc (rev s) x.

Lemma length_rev : s, length (rev s) = length s.

Lemma rev_app : s1 s2, rev (s1 ++ s2) = rev s2 ++ rev s1.

Lemma rev_rev : s, rev (rev s) = s.

Lemma nth_rev : x0 n s,
  n < length snth x0 (rev s) n = nth x0 s (length s - S n).

End Rev.

Hint Rewrite rev_snoc rev_cons length_rev rev_app rev_rev : vlib.

This page has been generated by coqdoc