Lists -- part II

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. The map2 definition and its properties are new.

Require Import Omega.
Require Import Vbase Vlistbase Varith.

Set Implicit Arguments.

Open Scope bool_scope.
Open Scope list_scope.

Lemma has_psplit (A : Type) (p : pred A) (s : list A) (x : A) :
  has p s
  s = take (find p s) s ++ nth x s (find p s) :: drop (S (find p s)) s.

Equality and eqType for list

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Notation Local nth := (nth x0).
Implicit Type s : list T.
Implicit Types x y z : T.

Fixpoint eqlist s1 s2 {struct s2} :=
  match s1, s2 with
  | nil, niltrue
  | x1 :: s1', x2 :: s2'(x1 == x2) && eqlist s1' s2'
  | _, _false
  end.

Lemma eqlistP : Equality.axiom eqlist.

Canonical Structure list_eqMixin := EqMixin eqlistP.
Canonical Structure list_eqType := Eval hnf in EqType _ list_eqMixin.

Lemma eqlistE : eqlist = eq_op.

Lemma eqlist_cons : x1 x2 s1 s2,
  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).

Lemma eqlist_app : s1 s2 s3 s4,
  length s1 = length s2 (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).

Lemma eqlist_rev2 : l1 l2,
  (rev l1 == rev l2) = (l1 == l2).

Lemma eqlist_snoc : s1 s2 x1 x2,
  (snoc s1 x1 == snoc s2 x2) = (s1 == s2) && (x1 == x2).

Lemma has_filter : a s, has a s = (filter a s != nil).

Lemma length_eq0 : l, (length l == 0) = (l == nil).


Fixpoint mem_list (s : list T) :=
  match s with
    | nil ⇒ (fun _false)
    | y :: s' ⇒ (fun x(x == y) || mem_list s' x)
  end.

Definition eqlist_class := list T.
Identity Coercion list_of_eqlist : eqlist_class >-> list.

Coercion pred_of_eq_list (s : eqlist_class) : pred_class := (fun xmem_list s x).

Canonical Structure list_predType := @mkPredType T (list T) pred_of_eq_list.
Canonical Structure mem_list_predType := mkPredType mem_list.

Lemma in_cons : y s x, (x \in y :: s) = (x == y) || (x \in s).

Hint Rewrite in_cons: vlib.
Lemma in_nil : x, (x \in nil) = false.

Lemma mem_list1 : x y, (x \in y :: nil) = (x == y).



Lemma mem_app : x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).

Lemma mem_snoc : s y, snoc s y =i y :: s.

Lemma mem_head : x s, x \in x :: s.

Lemma mem_last : x s, last x s \in x :: s.

Lemma mem_behead : s, {subset behead s s}.

Lemma mem_belast : s y, {subset belast y s y :: s}.

Lemma mem_nth : s n, n < length s nth s n \in s.

Lemma mem_take : s x, x \in take n0 s x \in s.

Lemma mem_drop : s x, x \in drop n0 s x \in s.

Lemma mem_rev : s, rev s =i s.

Lemma in_head : x l, x \in x :: l.

Lemma in_behead : x y l, x \in l x \in y :: l.

Lemma in_consE : {x y l}, x \in y :: l {x = y} + {x \in l}.

Lemma in_split : x l, x \in l l1 l2, l = l1 ++ x :: l2.

Ltac clarify2 :=
  vlib__clarify1;
  repeat match goal with
    | H1: ?x = Some _, H2: ?x = None |- _rewrite H2 in H1; discriminate
    | H1: ?x = Some _, H2: ?x = Some _ |- _rewrite H2 in H1; vlib__clarify1
  end; try done.

Lemma inP :
   x l , reflect (In x l) (x \in l).

Section Filters.

Variable a : pred T.

Lemma hasP : l, reflect (exists2 x, x \in l & a x) (has a l).

Lemma hasPn : l, reflect ( x, x \in l negb (a x)) (negb (has a l)).

Lemma allP : l, reflect ( x, x \in l a x) (all a l).

Lemma allPn : l, reflect (exists2 x, x \in l & negb (a x)) (negb (all a l)).

Lemma mem_filter : x l, (x \in filter a l) = a x && (x \in l).

End Filters.

Lemma eq_in_filter : (a1 a2 : pred T) s,
  {in s, a1 =1 a2} filter a1 s = filter a2 s.

Lemma eq_has_r : s1 s2 (EQ: s1 =i s2) f, has f s1 = has f s2.

Lemma eq_all_r : s1 s2 (EQ: s1 =i s2) f, all f s1 = all f s2.

Lemma has_sym : s1 s2, has (mem s1) s2 = has (mem s2) s1.

Lemma has_pred1 : x l, has (fun yy == x) l = (x \in l).

Constant sequences, i.e., the image of nlist.

Definition constant s :=
  match s with
    | niltrue
    | x :: s'all (fun yy == x) s'
  end.

Lemma all_pred1P x s :
  reflect (s = nlist (length s) x) (all (fun yy == x) s).

Lemma all_pred1_constant x s : all (fun yy == x) s constant s.

Implicit Arguments all_pred1_constant [].

Lemma all_pred1_nlist : x y n,
  all (fun yy == x) (nlist n y) = ((n == 0) || (x == y)).

Lemma constant_nlist : n x, constant (nlist n x).

Lemma constantP : s,
  reflect ( x, s = nlist (length s) x) (constant s).


Fixpoint uniq s :=
  match s with
    | niltrue
    | x :: s'(x \notin s') && uniq s'
  end.

Lemma cons_uniq : x s, uniq (x :: s) = (x \notin s) && uniq s.

Lemma app_uniq : s1 s2,
  uniq (s1 ++ s2) = uniq s1 && negb (has (mem s1) s2) && uniq s2.

Lemma uniq_appC : s1 s2, uniq (s1 ++ s2) = uniq (s2 ++ s1).

Lemma uniq_appCA : s1 s2 s3,
  uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).

Lemma snoc_uniq : s x, uniq (snoc s x) = (x \notin s) && uniq s.

Lemma filter_uniq : s a, uniq s uniq (filter a s).

Lemma rot_uniq : s, uniq (rot n0 s) = uniq s.

Lemma rev_uniq : s, uniq (rev s) = uniq s.

Lemma count_uniq_mem :
   s x, uniq s count (fun yy == x) s = if (x \in s) then 1 else 0.

Lemma in_split_uniq :
   x l,
    x \in l uniq l
     l1 l2, l = l1 ++ x :: l2
      uniq (l1 ++ l2) x \notin (l1 ++ l2).


Fixpoint undup s :=
  match s with
    | nilnil
    | x :: s'if x \in s' then undup s' else x :: undup s'
  end.

Lemma length_undup : s, length (undup s) length s.

Lemma mem_undup : s, undup s =i s.

Hint Rewrite mem_undup : vlib.

Lemma undup_uniq : s, uniq (undup s).

Lemma undup_id : s, uniq s undup s = s.

Lemma ltn_length_undup : s, (length (undup s) < length s) = negb (uniq s).


Definition index x := find (fun yy == x).

Lemma index_length : x s, index x s length s.

Lemma index_mem : x s, (index x s < length s) = (x \in s).

Lemma nth_index : x s, x \in s nth s (index x s) = x.

Lemma index_app : x s1 s2,
 index x (s1 ++ s2) = if x \in s1 then index x s1 else length s1 + index x s2.

Lemma index_uniq : i s, i < length s uniq s index (nth s i) s = i.

Lemma index_head : x s, index x (x :: s) = 0.

Lemma index_last : x s,
  uniq (x :: s) index (last x s) (x :: s) = length s.

Lemma nth_uniq : s i j,
   i < length s j < length s uniq s (nth s i == nth s j) = (i == j).

Lemma mem_rot : s, rot n0 s =i s.

Lemma eqlist_rot : s1 s2, (rot n0 s1 == rot n0 s2) = (s1 == s2).

Inductive rot_to_spec (s : list T) (x : T) : Type :=
  RotToSpec i s' (_ : rot i s = x :: s').

Lemma rot_to : s x, x \in s rot_to_spec s x.

End EqSeq.



Implicit Arguments eqlistP [T x y].
Implicit Arguments all_filterP [T f s].
Implicit Arguments hasP [T a l].
Implicit Arguments hasPn [T a l].
Implicit Arguments allP [T a l].
Implicit Arguments allPn [T a l].
Implicit Arguments index [T].
Implicit Arguments uniq [T].

Hint Rewrite in_cons in_cons mem_app mem_filter mem_rot : vlib.
Hint Resolve in_head in_behead : vlib.
Hint Resolve undup_uniq : vlib.

Section NlistthTheory.

Lemma nthP : (T : eqType) (s : list T) x x0,
  reflect (exists2 i, i < length s & nth x0 s i = x) (x \in s).

Variable T : Type.

Lemma has_nthP : (a : pred T) s x0,
  reflect (exists2 i, i < length s & a (nth x0 s i)) (has a s).

Lemma all_nthP : (a : pred T) s x0,
  reflect ( i, i < length s a (nth x0 s i)) (all a s).

End NlistthTheory.

Lemma set_nth_default : T s (y0 x0 : T) n,
  n < length s nth x0 s n = nth y0 s n.

Lemma headI : T s (x : T),
  snoc s x = head x s :: behead (snoc s x).

Implicit Arguments nthP [T s x].
Implicit Arguments has_nthP [T a s].
Implicit Arguments all_nthP [T a s].



Fixpoint incr_nth (v : list nat) (i : nat) {struct i} : list nat :=
  match v, i with
    | n :: v', 0 ⇒ S n :: v'
    | n :: v', S i'n :: incr_nth v' i'
    | nil, _ncons i 0 (1 :: nil)
  end.

Lemma nth_incr_nth : v i j,
  nth 0 (incr_nth v i) j = (if i == j then 1 else 0) + nth 0 v j.

Lemma length_incr_nth : v i,
  length (incr_nth v i) = if i < length v then length v else S i.


Section PermSeq.

Variable T : eqType.

Notation cou1 := (fun xcount (fun yy == x)).

Definition same_count1 (s1 s2 : list T) x :=
   count (fun yy == x) s1 == count (fun yy == x) s2.

Definition perm_eq (s1 s2 : list T) := all (same_count1 s1 s2) (s1 ++ s2).

Lemma perm_eqP_weak : s1 s2,
  reflect (cou1 ^~ s1 =1 cou1 ^~ s2) (perm_eq s1 s2).

Lemma perm_eq_refl : s, perm_eq s s.
Hint Resolve perm_eq_refl.

Lemma perm_eq_sym : symmetric perm_eq.

Lemma perm_eq_trans : transitive perm_eq.

Notation perm_eql := (fun s1 s2perm_eq s1 =1 perm_eq s2).
Notation perm_eqr := (fun s1 s2perm_eq^~ s1 =1 perm_eq^~ s2).

Lemma perm_eqlP : s1 s2, reflect (perm_eql s1 s2) (perm_eq s1 s2).

Lemma perm_eqrP : s1 s2, reflect (perm_eqr s1 s2) (perm_eq s1 s2).

Lemma perm_appC : s1 s2, perm_eql (s1 ++ s2) (s2 ++ s1).

Lemma perm_app2l : s1 s2 s3,
  perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.

Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.

Lemma perm_app2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.

Lemma perm_appAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).

Lemma perm_appCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).

Lemma perm_snoc : x s, perm_eql (snoc s x) (x :: s).

Lemma perm_rot : n s, perm_eql (rot n s) s.

Lemma perm_rotr : n s, perm_eql (rotr n s) s.

Lemma perm_eq_mem : s1 s2, perm_eq s1 s2 s1 =i s2.

Lemma perm_eq_nilD : s, perm_eq nil s s = nil.

Lemma perm_eq_consD : x s1 s2,
  perm_eq (x :: s1) s2 sa sb, s2 = sa ++ x :: sb perm_eq s1 (sa ++ sb).

Lemma perm_eqD : s1 s2 (EQ: perm_eq s1 s2) f, count f s1 = count f s2.

Lemma perm_eq_length : s1 s2, perm_eq s1 s2 length s1 = length s2.

Lemma perm_eqP s1 s2 :
  reflect ((@count _) ^~ s1 =1 (@count _) ^~ s2) (perm_eq s1 s2).

Lemma uniq_leq_length : s1 s2 : list T,
  uniq s1 {subset s1 s2} length s1 length s2.

Lemma leq_length_uniq : s1 s2 : list T,
  uniq s1 {subset s1 s2} length s2 length s1 uniq s2.

Lemma uniq_length_uniq : s1 s2 : list T,
  uniq s1 s1 =i s2 uniq s2 = (length s2 == length s1).

Lemma leq_length_perm : s1 s2 : list T,
  uniq s1 {subset s1 s2}
  length s2 length s1
  s1 =i s2 length s1 = length s2.

Lemma perm_uniq : s1 s2 : list T,
  s1 =i s2 length s1 = length s2 uniq s1 = uniq s2.

Lemma perm_eq_uniq : s1 s2, perm_eq s1 s2 uniq s1 = uniq s2.

Lemma uniq_perm_eq : s1 s2,
  uniq s1 uniq s2 s1 =i s2 perm_eq s1 s2.

Lemma count_mem_uniq : s : list T,
  ( x, count (fun yy == x) s = if (x \in s) then 1 else 0) uniq s.

End PermSeq.

Section RotrLemmas.

Variables (n0 : nat) (T : Type) (T' : eqType).

Lemma length_rotr : s : list T, length (rotr n0 s) = length s.

Lemma mem_rotr : s : list T', rotr n0 s =i s.

Lemma rotr_size_app : s1 s2 : list T,
  rotr (length s2) (s1 ++ s2) = s2 ++ s1.

Lemma rotr1_snoc : x (s : list T), rotr 1 (snoc s x) = x :: s.

Lemma has_rotr : f (s : list T), has f (rotr n0 s) = has f s.

Lemma rotr_uniq : s : list T', uniq (rotr n0 s) = uniq s.

Lemma rotrK : cancel (rotr n0) (@rot T n0).

Lemma rotr_inj : injective (@rotr T n0).

Lemma rev_rot : s : list T, rev (rot n0 s) = rotr n0 (rev s).

Lemma rev_rotr : s : list T, rev (rotr n0 s) = rot n0 (rev s).

End RotrLemmas.

Hint Rewrite length_rotr rotr_size_app rotr1_snoc has_rotr : vlib.


Section Sieve.

Variables (n0 : nat) (T : Type).

Implicit Types l s : list T.

Lemma sieve_false : s n, sieve (nlist n false) s = nil.

Lemma sieve_true : s n, length s n sieve (nlist n true) s = s.

Lemma sieve0 : m, sieve m nil = (@nil T).


Lemma sieve_cons : b m x s,
  sieve (b :: m) (x :: s) = (if b then (x :: nil) else nil) ++ sieve m s.

Lemma length_sieve : m s,
  length m = length s length (sieve m s) = count id m.

Lemma sieve_app : m1 s1, length m1 = length s1
   m2 s2, sieve (m1 ++ m2) (s1 ++ s2) = sieve m1 s1 ++ sieve m2 s2.

Lemma has_sieve_cons : a b m x s,
  has a (sieve (b :: m) (x :: s)) = b && a x || has a (sieve m s).

Lemma sieve_rot : m s, length m = length s
 sieve (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (sieve m s).

End Sieve.

Section EqSieve.

Variables (n0 : nat) (T : eqType).

Lemma mem_sieve_cons x b m y (s : list T) :
  (x \in sieve (b :: m) (y :: s)) = b && (x == y) || (x \in sieve m s).

Lemma mem_sieve : x m (s : list T), (x \in sieve m s) (x \in s).

Lemma sieve_uniq : s : list T, uniq s m, uniq (sieve m s).

Lemma mem_sieve_rot : m (s : list T), length m = length s
  sieve (rot n0 m) (rot n0 s) =i sieve m s.

End EqSieve.

Section Map.

Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 T2).

Fixpoint map (l : list T1) : list T2 :=
  match l with
    | nilnil
    | x :: lf x :: map l
  end.

Lemma map_cons : x s, map (x :: s) = f x :: map s.

Lemma map_nlist : x, map (nlist n0 x) = nlist n0 (f x).

Lemma map_app : s1 s2, map (s1 ++ s2) = map s1 ++ map s2.

Lemma map_snoc : s x, map (snoc s x) = snoc (map s) (f x).

Lemma length_map : l, length (map l) = length l.

Lemma behead_map : l, behead (map l) = map (behead l).

Lemma nth_map : n l, n < length l nth x2 (map l) n = f (nth x1 l n).

Lemma last_map : s x, last (f x) (map s) = f (last x s).

Lemma belast_map : s x, belast (f x) (map s) = map (belast x s).

Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).

Lemma find_map a s : find a (map s) = find (preim f a) s.

Lemma has_map a s : has a (map s) = has (preim f a) s.

Lemma count_map a s : count a (map s) = count (preim f a) s.

Lemma map_take s : map (take n0 s) = take n0 (map s).

Lemma map_drop s : map (drop n0 s) = drop n0 (map s).

Lemma map_rot s : map (rot n0 s) = rot n0 (map s).

Lemma map_rotr s : map (rotr n0 s) = rotr n0 (map s).

Lemma map_rev s : map (rev s) = rev (map s).

Lemma map_sieve m s : map (sieve m s) = sieve m (map s).

Lemma inj_map (Hf : injective f) : injective map.

End Map.

Hint Rewrite map_nlist map_app map_snoc length_map
  behead_map last_map belast_map map_take map_drop
  map_rot map_rev map_sieve map_rotr : vlib.

map2 and its properties


Section Map2.

Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2).
Variables (T3 : Type) (f : T1 T2 T3).

Fixpoint map2 (l1 : list T1) (l2 : list T2) {struct l1}: list T3 :=
  match l1, l2 with
    | nil, _nil
    | x1 :: l1, nilnil
    | x1 :: l1, x2 :: l2f x1 x2 :: map2 l1 l2
  end.

Lemma map2_0l : l, map2 nil l = nil.
Lemma map2_l0 : l, map2 l nil = nil.

Lemma map2_cons : x1 l1 x2 l2, map2 (x1 :: l1) (x2 :: l2) = f x1 x2 :: map2 l1 l2.

Lemma map2_nlist : x y, map2 (nlist n0 x) (nlist n0 y) = nlist n0 (f x y).

Lemma map2_app : s1 s2 t1 t2 (Leq: length s1 = length t1),
  map2 (s1 ++ s2) (t1 ++ t2) = map2 s1 t1 ++ map2 s2 t2.

Lemma length_map2_eq : l1 l2, length l1 = length l2
  length (map2 l1 l2) = (length l1).

Lemma map2_take :
   l1 l2, map2 (take n0 l1) (take n0 l2) = take n0 (map2 l1 l2).

Lemma map2_drop :
   l1 l2, map2 (drop n0 l1) (drop n0 l2) = drop n0 (map2 l1 l2).

Lemma map2_rot l1 l2 (Leq: length l1 = length l2) :
    map2 (rot n0 l1) (rot n0 l2) = rot n0 (map2 l1 l2).

End Map2.

Lemma map2I :
   {T1} {f: T1 T1 T1} (Cf: x, f x x = x) x,
    map2 f x x = x.

Lemma map2C :
   {T1 T2} {f: T1 T1 T2} (Cf: x y, f x y = f y x) x y,
    map2 f x y = map2 f y x.

Lemma map2A :
   {T1} {f: T1 T1 T1} (Cf: x y z, f x (f y z) = f (f x y) z) x y z,
    map2 f x (map2 f y z) = map2 f (map2 f x y) z.

Lemma map2K :
   {T1 T2} {f: T1 T1 T2} {v} (Cf: x, f x x = v) x,
    map2 f x x = nlist (length x) v.

Lemma map2Kl :
   {T1 T2 T3} {f: T1 T2 T3} {v1 v2} (Cf: x, f v1 x = v2)
    n x (Leq: length x = n),
    map2 f (nlist n v1) x = nlist n v2.

Lemma map2Il :
   {T1 T2} {f: T1 T2 T2} {v1} (Cf: x, f v1 x = x)
    n x (Leq: length x = n),
    map2 f (nlist n v1) x = x.

Lemma map2Sl :
   {T1 T2} {f: T1 T1 T2} {v g} (Cf: x, f v x = g x)
    n x (Leq: length x = n),
    map2 f (nlist n v) x = map g x.

Section EqMap.

Variables (n0 : nat) (T1 : eqType) (x1 : T1).
Variables (T2 : eqType) (x2 : T2) (f : T1 T2).

Lemma map_f : (s : list T1) x, x \in s f x \in map f s.

Lemma mapP : (s : list T1) y,
  reflect (exists2 x, x \in s & y = f x) (y \in map f s).

Lemma map_uniq : s, uniq (map f s) uniq s.

Lemma map_inj_in_uniq : s : list T1,
  {in s &, injective f} uniq (map f s) = uniq s.

Hypothesis Hf : injective f.

Lemma mem_map : s x, (f x \in map f s) = (x \in s).

Lemma index_map : s x, index (f x) (map f s) = index x s.

Lemma map_inj_uniq : s, uniq (map f s) = uniq s.

End EqMap.

Implicit Arguments mapP [T1 T2 f s y].

Lemma filter_sieve : T a (s : list T), filter a s = sieve (map a s) s.

Section MapComp.

Variable T1 T2 T3 : Type.

Lemma map_id : s : list T1, map id s = s.

Lemma eq_map : f1 f2 : T1 T2, f1 =1 f2 map f1 =1 map f2.

Lemma map_comp : (f1 : T2 T3) (f2 : T1 T2) s,
  map (f1 \o f2) s = map f1 (map f2 s).

Lemma mapK : (f1 : T1 T2) (f2 : T2 T1),
  cancel f1 f2 cancel (map f1) (map f2).

End MapComp.

Lemma eq_in_map : (T1 : eqType) T2 (f1 f2 : T1 T2) (s : list T1),
  {in s, f1 =1 f2} map f1 s = map f2 s.

Lemma map_id_in : (T : eqType) f (s : list T),
  {in s, f =1 id} map f s = s.


Section Pmap.

Variables (aT rT : Type) (f : aT option rT) (g : rT aT).

Fixpoint pmap s :=
  match s with
    | nilnil
    | x :: s'oapp ((@cons _)^~ (pmap s')) (pmap s') (f x)
  end.

Lemma map_pK : pcancel g f cancel (map g) pmap.

Lemma length_pmap s :
  length (pmap s) = count (fun xmatch f x with Nonefalse | Some _true end) s.

Lemma pmapS_filter s :
  map some (pmap s)
  = map f (filter (fun xmatch f x with Nonefalse | Some _true end) s).

Lemma pmap_filter (fK : ocancel f g) s :
  map g (pmap s) = filter (fun xmatch f x with Nonefalse | Some _true end) s.

End Pmap.


Index sequence


Lemma length_iota : m n, length (iota m n) = n.

Lemma iota_add : m n1 n2,
  iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

Lemma iota_addl : m1 m2 n,
  iota (m1 + m2) n = map (plus m1) (iota m2 n).

Lemma nth_iota : n0 m n i, i < n nth n0 (iota m n) i = m + i.

Lemma mem_iota : m n i, (i \in iota m n) = (m i) && (i < m + n).

Lemma iota_uniq : m n, uniq (iota m n).

Hint Resolve iota_uniq : vlib.
Hint Rewrite length_iota mem_iota iota_uniq : vlib.


Section MakeSeq.

Variables (T : Type) (x0 : T).

Definition mklist f n : list T := map f (iota 0 n).

Lemma length_mklist : f n, length (mklist f n) = n.

Lemma eq_mklist : f g, f =1 g mklist f =1 mklist g.

Lemma nth_mklist : f n i, i < n nth x0 (mklist f n) i = f i.

Lemma mklist_nth : s, mklist (nth x0 s) (length s) = s.

End MakeSeq.

Lemma mklist_uniq : (T : eqType) (f : nat T) n,
  injective f uniq (mklist f n).

Section FoldRight.

Variables (T R : Type) (f : T R R).

Fixpoint foldr (l : list T) (z0: R) : R :=
  match l with
    | nilz0
    | x :: lf x (foldr l z0)
  end.

End FoldRight.

Section FoldRightComp.

Variables (T1 T2 : Type) (h : T1 T2).
Variables (R : Type) (f : T2 R R) (z0 : R).

Lemma foldr_app :
   s1 s2, foldr f (s1 ++ s2) z0 = foldr f s1 (foldr f s2 z0).

Lemma foldr_map :
   s : list T1, foldr f (map h s) z0 = foldr (fun x zf (h x) z) s z0.

End FoldRightComp.

Definition sumn l := foldr plus l 0.

Lemma sumn_nil : sumn nil = 0.

Lemma sumn_cons : n l, sumn (n :: l) = n + sumn l.

Hint Rewrite sumn_nil sumn_cons : vlib.

Lemma sumn_nlist : x n : nat, sumn (nlist n x) = x × n.

Lemma sumn_app : s1 s2, sumn (s1 ++ s2) = sumn s1 + sumn s2.

Lemma natnlist0P : s : list nat,
  reflect (s = nlist (length s) 0) (sumn s == 0).

Section FoldLeft.

Variables (T R : Type) (f : R T R).

Fixpoint foldl z (l : list T) :=
  match l with
    | nilz
    | x :: l ⇒ (foldl (f z x) l)
  end.

Lemma foldl_rev : z s, foldl z (rev s) = foldr (fun x zf z x) s z.

Lemma foldl_app : z s1 s2, foldl z (s1 ++ s2) = foldl (foldl z s1) s2.

End FoldLeft.

Section Scan.

Variables (T1 : Type) (x1 : T1) (T2 : Type) (x2 : T2).
Variables (f : T1 T1 T2) (g : T1 T2 T1).

Fixpoint pairmap x (s : list T1) {struct s} :=
  match s with
    | nilnil
    | y :: s'f x y :: pairmap y s'
  end.

Lemma length_pairmap : x s, length (pairmap x s) = length s.

Lemma nth_pairmap : s n, n < length s
   x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).

Fixpoint scanl x (s : list T2) {struct s} :=
  match s with
    | nilnil
    | y :: s'let x' := g x y in x' :: scanl x' s'
  end.

Lemma length_scanl : x s, length (scanl x s) = length s.

Lemma nth_scanl : s n, n < length s
   x, nth x1 (scanl x s) n = foldl g x (take (S n) s).

Lemma scanlK :
  ( x, cancel (g x) (f x)) x, cancel (scanl x) (pairmap x).

Lemma pairmapK :
  ( x, cancel (f x) (g x)) x, cancel (pairmap x) (scanl x).

End Scan.


Section Zip.

Variables T1 T2 : Type.

Fixpoint zip (s1 : list T1) (s2 : list T2) {struct s2} :=
  match s1, s2 with
  | x1 :: s1', x2 :: s2'(x1,x2) :: zip s1' s2'
  | _, _nil
  end.

Definition unzip1 := map (@fst T1 T2).
Definition unzip2 := map (@snd T1 T2).

Lemma zip_unzip : s, zip (unzip1 s) (unzip2 s) = s.

Lemma unzip1_zip : s1 s2,
  length s1 length s2 unzip1 (zip s1 s2) = s1.

Lemma unzip2_zip : s1 s2,
  length s2 length s1 unzip2 (zip s1 s2) = s2.

Lemma length1_zip : s1 s2,
  length s1 length s2 length (zip s1 s2) = length s1.

Lemma length2_zip : s1 s2,
  length s2 length s1 length (zip s1 s2) = length s2.

End Zip.


Section Flatten.

Variable T : Type.

Definition flatten l := foldr (@app _) l (@nil T).
Definition shape := map (@length T).
Fixpoint reshape (sh : list nat) (s : list T) {struct sh} :=
  match sh with
    | nilnil
    | n :: sh'take n s :: reshape sh' (drop n s)
  end.

Lemma flatten_cons : l ll, flatten (l :: ll) = l ++ flatten ll.

Lemma flatten_app : l l', flatten (l ++ l') = flatten l ++ flatten l'.

Hint Rewrite flatten_cons flatten_app : vlib.

Lemma length_flatten : ss, length (flatten ss) = sumn (shape ss).

Lemma flattenK : ss, reshape (shape ss) (flatten ss) = ss.

Lemma reshapeKr : sh s, length s sumn sh flatten (reshape sh s) = s.

Lemma reshapeKl : sh s, length s sumn sh shape (reshape sh s) = sh.

End Flatten.


Inductive has_spec T (f : T bool) (l : list T) : Prop :=
  HasSpec (l1 l2: list T) (n : T) (EQ: l = l1 ++ n :: l2) (HOLDS : f n) (PREV: has f l1 = false).

Lemma hasD T (f : T bool) l (H: has f l): has_spec f l.

Inductive in_spec {T : eqType} (x : T) (l : list T) : Prop :=
  InSpec (l1 l2: list T) (EQ: l = l1 ++ x :: l2) (PREV: x \notin l1).

Lemma inD {T: eqType} {x: T} {l} (H: x \in l): in_spec x l.

Lemma uniqE (T: eqType) (l : list T) :
  uniq l ( n l1 l2 l3, l = l1 ++ n :: l2 ++ n :: l3 False).

Properties of In

Lemma In_eq : A (a:A) (l:list A), In a (a :: l).

Lemma In_cons : A (a b:A) (l:list A), In b l In b (a :: l).

Lemma In_nil : A (a:A), ¬ In a nil.

Lemma In_split : A x (l:list A), In x l l1 l2, l = l1++x::l2.

Lemma In_dec :
   A (D: x y:A, {x = y} + {x y}) (a: A) l, {In a l} + {¬ In a l}.

Lemma In_appI1 : A (x:A) l (IN: In x l) l', In x (l++l').

Lemma In_appI2 : A (x:A) l' (IN: In x l') l, In x (l++l').

Lemma In_appD : A (x:A) l l' (IN: In x (l++l')), In x l In x l'.

Lemma In_app : A (x:A) l l', In x (l++l') In x l In x l'.

Lemma In_rev : A (x: A) l, In x (rev l) In x l.

Lemma In_revI : A (x: A) l (IN: In x l), In x (rev l).

Lemma In_revD : A (x: A) l (IN: In x (rev l)), In x l.

Lemma In_mapI : A B (f: A B) x l (IN: In x l), In (f x) (map f l).

Lemma In_mapD :
   A B (f: AB) y l, In y (map f l) x, f x = y In x l.

Lemma In_map :
   A B (f: AB) y l, In y (map f l) x, f x = y In x l.

Lemma In_filter :
   A (x:A) f l, In x (filter f l) In x l f x.

Lemma In_filterI :
   A x l (IN: In x l) (f: Abool) (F: f x), In x (filter f l).

Lemma In_filterD :
   A (x:A) f l (D: In x (filter f l)), In x l f x.

Hint Resolve In_eq In_cons In_appI1 In_appI2 In_mapI In_revI In_filterI : vlib.

Lemma uniqP : (T : eqType) (l: list T), reflect (List.NoDup l) (uniq l).

Lemma In_dec_strong :
   {A : Type} (P Q : A Prop)
    (dP: i:A, {P i} + {Q i})
    (l : list A),
      {e | In e l P e} + {( e, In e l Q e)}.

Lemma In_dec_strong_prop :
   {A : Type} (P : A Prop)
    (dP: i:A, P i ¬ P i)
    (l : list A),
      ( e, In e l P e) ( e, ¬ (In e l P e)).

Lemma In_dec_strong_neg :
   {A : Type} (P : A Prop)
    (dP: i:A, {P i} + {¬ P i})
    (l : list A),
      {e | In e l ¬ P e} + {( e, In e l P e)}.

Setoid rewriting for equality up to permutation


Require Import Setoid.

Add Parametric Relation (T: eqType) : (list T) (@perm_eq T)
  reflexivity proved by (@perm_eq_refl T)
  symmetry proved by (pre_from_symmetric (@perm_eq_sym T))
  transitivity proved by (@perm_eq_trans T)
  as perm_rel.

Lemma perm_eq_map (T U : eqType) (f : T U) :
   xs ys (PE : perm_eq xs ys), perm_eq (map f xs) (map f ys).

Lemma perm_eq_flatten (T : eqType) :
   (xs ys: list (list T)) (PE : perm_eq xs ys), perm_eq (flatten xs) (flatten ys).

Lemma perm_eq_map2 (T U : eqType) (f g : T U) :
   xs ys (PE : perm_eq xs ys) (EQ: x (IN: In x xs), f x = g x),
    perm_eq (map f xs) (map g ys).

Add Parametric Morphism A : (@perm_eq A)
  with signature (@perm_eq A) ==> (@perm_eq A) ==> (@eq bool) as perm_morph.

Add Parametric Morphism A a : (cons a)
  with signature (@perm_eq A) ==> (@perm_eq _) as cons_morph.

Add Parametric Morphism A : (@app A)
  with signature (@perm_eq A) ==> (@perm_eq _) ==> (@perm_eq _) as app_morph.

Add Parametric Morphism A B f : (@map A B f)
  with signature (@perm_eq A) ==> (@perm_eq B) as map_morph.

Add Parametric Morphism A : (@flatten A)
  with signature (@perm_eq _) ==> (@perm_eq A) as flatten_morph.

Add Parametric Morphism T : (@uniq T)
  with signature (@perm_eq T) ==> (@eq bool) as uniq_morph.


This page has been generated by coqdoc Imprint | Data protection