Require Import Omega.
Require Import Vbase Relations List Permutation Sorting MMergesort.
Require Import ClassicalDescription.

Set Implicit Arguments.

This file contains a number of basic definitions and lemmas about lists that are missing from the standard library, and a few properties of classical logic.
Very basic lemmas

Definition appA := app_ass.

Lemma in_cons_iff A (a b : A) l : In b (a :: l) a = b In b l.

Lemma In_split2 :
   A (x: A) l (IN: In x l),
   l1 l2, l = l1 ++ x :: l2 ¬ In x l1.

Lemma map_eq_app_inv A B (f : A B) l l1 l2 :
  map f l = l1 ++ l2
   l1' l2', l = l1' ++ l2' map f l1' = l1 map f l2' = l2.

List filtering

Lemma in_filter_iff A l f (x : A) : In x (filter f l) In x l f x.

Lemma filter_app A f (l l' : list A) :
  filter f (l ++ l') = filter f l ++ filter f l'.

List flattening

Fixpoint flatten A (l: list (list A)) :=
  match l with
    | nilnil
    | x :: l'x ++ flatten l'
  end.

Lemma in_flatten_iff A (x: A) ll :
  In x (flatten ll) l, In l ll In x l.

List disjointness

Definition disjoint A (l1 l2 : list A) :=
   a (IN1: In a l1) (IN2: In a l2), False.

Remove duplicate list elements (classical)

Fixpoint undup A (l: list A) :=
  match l with nilnil
    | x :: l
      if excluded_middle_informative (In x l) then undup l else x :: undup l
  end.

Lemmas about NoDup and undup

Lemma nodup_one A (x: A) : NoDup (x :: nil).

Hint Resolve NoDup_nil nodup_one.

Lemma nodup_map:
   (A B: Type) (f: A B) (l: list A),
  NoDup l
  ( x y, In x l In y l x y f x f y)
  NoDup (map f l).

Lemma nodup_append_commut:
   (A: Type) (a b: list A),
  NoDup (a ++ b) NoDup (b ++ a).

Lemma nodup_cons A (x: A) l:
  NoDup (x :: l) ¬ In x l NoDup l.

Lemma nodup_app:
   (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2)
  NoDup l1 NoDup l2 disjoint l1 l2.

Lemma nodup_append:
   (A: Type) (l1 l2: list A),
  NoDup l1 NoDup l2 disjoint l1 l2
  NoDup (l1 ++ l2).

Lemma nodup_append_right:
   (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) NoDup l2.

Lemma nodup_append_left:
   (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) NoDup l1.

Lemma nodup_filter A (l: list A) (ND: NoDup l) f : NoDup (filter f l).

Hint Resolve nodup_filter.

Lemma Permutation_nodup A ( l l' : list A) :
  Permutation l l' NoDup l NoDup l'.

Lemma nodup_eq_one A (x : A) l :
   NoDup l In x l ( y (IN: In y l), y = x) l = x :: nil.

Lemma nodup_consD A (x : A) l : NoDup (x :: l) NoDup l.

Lemma nodup_mapD A B (f : A B) l : NoDup (map f l) NoDup l.

Lemma In_NoDup_Permutation A (a : A) l (IN: In a l) (ND : NoDup l) :
   l', Permutation l (a :: l') ¬ In a l'.

Lemma in_undup_iff A (x : A) (l : list A) : In x (undup l) In x l.

Lemma nodup_undup A (l : list A) : NoDup (undup l).

Hint Resolve nodup_undup.

Lemma undup_nodup A (l : list A) : NoDup l undup l = l.

Lemma Sorted_undup A p (l : list A) :
  StronglySorted p l StronglySorted p (undup l).

Lemma undup_nonnil A (l : list A) : l nil undup l nil.

Lemma Permutation_undup A (l l' : list A) :
  Permutation l l' Permutation (undup l) (undup l').

Function update

Definition upd A B (f : A B) a b x :=
  if excluded_middle_informative (x = a) then b else f x.

Lemma upds A B (f: A B) a b : upd f a b a = b.

Lemma updo A B (f: A B) a b c (NEQ: c a) : upd f a b c = f c.

Ltac rupd := repeat first [rewrite upds | rewrite updo ; try done].

Lemma updss A B (f : A B) l x y : upd (upd f l x) l y = upd f l y.

Lemma updC A l l' (NEQ: l l') B (f : A B) x y :
  upd (upd f l x) l' y = upd (upd f l' y) l x.

Lemma updI A B (f : A B) a : upd f a (f a) = f.

Lemma map_upd_irr A (a: A) l (NIN: ¬ In a l) B f (b : B) :
  map (upd f a b) l = map f l.

Decidable function update

Definition mupd (A: eqType) B (h : A B) y z :=
  fun xif x == y then z else h x.

Lemma mupds (A: eqType) B (f: A B) x y : mupd f x y x = y.

Lemma mupdo (A: eqType) B (f: A B) x y z : x z mupd f x y z = f z.

Lemmas about sorting

Lemma sorted_perm_eq : A (cmp: A A Prop)
  (TRANS: transitive _ cmp)
  (ANTIS: antisymmetric _ cmp)
  l l' (P: Permutation l l')
  (S : StronglySorted cmp l) (S' : StronglySorted cmp l'), l = l'.

Lemma perm_sort_eq A (l l': list A) (P: Permutation l l') cmp
    (TOTAL: x y, In x l In y l cmp x y = true cmp y x = true)
    (TRANS: transitive _ cmp)
    (ANTIS: antisymmetric _ cmp) :
  sort cmp l = sort cmp l'.

Lemma In_sort A (x: A) cmp l : In x (sort cmp l) In x l.

Lemma NoDup_sort A cmp (l : list A) : NoDup (sort cmp l) NoDup l.

Lemma NoDup_sort1 A cmp (l : list A) : NoDup l NoDup (sort cmp l).

Hint Resolve NoDup_sort1.

Lemma Sorted_total :
   A cmp (R: reflexive _ cmp) (l: list A), StronglySorted cmp l
     x y, In x l In y l
      cmp x y cmp y x.

Lemma Sorted_app_end_inv A (cmp : A A Prop) l x :
  StronglySorted cmp (l ++ x :: nil)
   y, In y l cmp y x.


Fixpoint dprod A B al (f : A list B) :=
  match al with
    | nilnil
    | a :: almap (fun b(a, b)) (f a) ++ dprod al f
  end.

Lemma in_dprod_iff A B x al (f : A list B) :
  In x (dprod al f) In (fst x) al In (snd x) (f (fst x)).

Miscellaneous

Lemma perm_from_subset :
   A (l : list A) l',
    NoDup l'
    ( x, In x l' In x l)
     l'', Permutation l (l' ++ l'').

Lemma seq_split_gen :
   l n a,
  n a < n + l
  seq n l = seq n (a - n) ++ a :: seq (S a) (l + n - a - 1).

Lemma seq_split0 :
   l a,
  a < l
  seq 0 l = seq 0 a ++ a :: seq (S a) (l - a - 1).

Lemma list_prod_app A (l l' : list A) B (m : list B) :
  list_prod (l ++ l') m = list_prod l m ++ list_prod l' m.

Lemma list_prod_nil_r A (l : list A) B :
  list_prod l (@nil B) = nil.

Lemma list_prod_cons_r A (l : list A) B a (m : list B) :
  Permutation (list_prod l (a :: m)) (map (fun x(x,a)) l ++ list_prod l m).

Lemma list_prod_app_r A (l : list A) B (m m' : list B) :
  Permutation (list_prod l (m ++ m')) (list_prod l m ++ list_prod l m').

Lemma in_seq_iff a n l : In a (seq n l) n a < n + l.

Lemma in_seq0_iff x a : In x (seq 0 a) x < a.

Lemma nodup_seq n l : NoDup (seq n l).

Lemma seq_split :
   l a,
  a < l
   l', Permutation (seq 0 l) (a :: l') ¬ In a l'.

Lemma Permutation_listprod_r A (l : list A) B (m m' : list B) :
  Permutation m m'
  Permutation (list_prod l m) (list_prod l m').

Ltac in_simp :=
  try match goal with |- ¬ _intro end;
  repeat first [
    rewrite in_flatten_iff in *; desc; clarify |
    rewrite in_map_iff in *; desc; clarify |
    rewrite in_seq0_iff in *; desc; clarify ].

Global Opaque seq.

This page has been generated by coqdoc