feat(library/data/list/*): add theorems from Haitao Zhang and clean up

library/data/list/basic.lean

@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
 
 Basic properties of lists.
 -/
-import logic tools.helper_tactics data.nat.basic algebra.function
+import logic tools.helper_tactics data.nat.order algebra.function
 open eq.ops helper_tactics nat prod function option
 
 inductive list (T : Type) : Type :=
@@ -313,12 +313,18 @@ list.rec_on l
 theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l :=
 or.elim (eq_or_mem_of_mem_cons H₂) (λe, absurd e H₁) (λr, r)
 
-theorem not_eq_of_not_mem {a b : T} {l : list T} : a ∉ b::l → a ≠ b :=
+theorem ne_of_not_mem_cons {a b : T} {l : list T} : a ∉ b::l → a ≠ b :=
 assume nin aeqb, absurd (or.inl aeqb) nin
 
-theorem not_mem_of_not_mem {a b : T} {l : list T} : a ∉ b::l → a ∉ l :=
+theorem not_mem_of_not_mem_cons {a b : T} {l : list T} : a ∉ b::l → a ∉ l :=
 assume nin nainl, absurd (or.inr nainl) nin
 
+lemma not_mem_cons_of_ne_of_not_mem {x y : T} {l : list T} : x ≠ y → x ∉ l → x ∉ y::l :=
+assume P1 P2, not.intro (assume Pxin, absurd (eq_or_mem_of_mem_cons Pxin) (not_or P1 P2))
+
+lemma ne_and_not_mem_of_not_mem_cons {x y : T} {l : list T} : x ∉ y::l → x ≠ y ∧ x ∉ l :=
+assume P, and.intro (ne_of_not_mem_cons P) (not_mem_of_not_mem_cons P)
+
 definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ l₂
 
 infix `⊆` := sublist
@@ -392,7 +398,7 @@ assume e, if_pos e
 theorem find_cons_of_ne {x y : T} (l : list T) : x ≠ y → find x (y::l) = succ (find x l) :=
 assume n, if_neg n
 
-theorem find.not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l :=
+theorem find_of_not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l :=
 list.rec_on l
    (assume P₁ : ¬x ∈ [], _)
    (take y l,
@@ -405,6 +411,36 @@ list.rec_on l
                   ... = succ (find x l)                      : if_neg (and.elim_left P₃)
                   ... = succ (length l)                      : {iH (and.elim_right P₃)}
                   ... = length (y::l)                        : !length_cons⁻¹)
+
+lemma find_le_length : ∀ {a} {l : list T}, find a l ≤ length l
+| a []        := !le.refl
+| a (b::l)    := decidable.rec_on (H a b)
+              (assume Peq, by rewrite [find_cons_of_eq l Peq]; exact !zero_le)
+              (assume Pne,
+                begin
+                  rewrite [find_cons_of_ne l Pne, length_cons],
+                  apply succ_le_succ, apply find_le_length
+                end)
+
+lemma not_mem_of_find_eq_length : ∀ {a} {l : list T}, find a l = length l → a ∉ l
+| a []        := assume Peq, !not_mem_nil
+| a (b::l)    := decidable.rec_on (H a b)
+                (assume Peq, by rewrite [find_cons_of_eq l Peq, length_cons]; contradiction)
+                (assume Pne,
+                  begin
+                    rewrite [find_cons_of_ne l Pne, length_cons, mem_cons_iff],
+                    intro Plen, apply (not_or Pne),
+                    exact not_mem_of_find_eq_length (succ_inj Plen)
+                  end)
+
+lemma find_lt_length {a} {l : list T} (Pin : a ∈ l) : find a l < length l :=
+begin
+  apply nat.lt_of_le_and_ne,
+  apply find_le_length,
+  apply not.intro, intro Peq,
+  exact absurd Pin (not_mem_of_find_eq_length Peq)
+end
+
 end
 
 /- nth element -/

library/data/list/comb.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Leonardo de Moura. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Haitao Zhang
 
 List combinators.
 -/
@@ -364,6 +364,81 @@ theorem length_product : ∀ (l₁ : list A) (l₂ : list B), length (product l
   by rewrite [product_cons, length_append, length_cons,
               length_map, ih, mul.right_distrib, one_mul, add.comm]
 end product
+
+-- new for list/comb dependent map theory
+definition dinj₁ (p : A → Prop) (f : Π a, p a → B) := ∀ ⦃a1 a2⦄ (h1 : p a1) (h2 : p a2), a1 ≠ a2 → (f a1 h1) ≠ (f a2 h2)
+definition dinj (p : A → Prop) (f : Π a, p a → B) := ∀ ⦃a1 a2⦄ (h1 : p a1) (h2 : p a2), (f a1 h1) = (f a2 h2) → a1 = a2
+
+definition dmap (p : A → Prop) [h : decidable_pred p] (f : Π a, p a → B) : list A → list B
+| []       := []
+| (a::l)   := if P : (p a) then cons (f a P) (dmap l) else (dmap l)
+
+-- properties of dmap
+section dmap
+
+variable {p : A → Prop}
+variable [h : decidable_pred p]
+include h
+variable {f : Π a, p a → B}
+
+lemma dmap_nil : dmap p f [] = [] := rfl
+lemma dmap_cons_of_pos {a : A} (P : p a) : ∀ l, dmap p f (a::l) = (f a P) :: dmap p f l :=
+      λ l, dif_pos P
+lemma dmap_cons_of_neg {a : A} (P : ¬ p a) : ∀ l, dmap p f (a::l) = dmap p f l :=
+      λ l, dif_neg P
+
+lemma mem_of_dmap : ∀ {l : list A} {a} (Pa : p a), a ∈ l → (f a Pa) ∈ dmap p f l
+| []     := take a Pa Pinnil, by contradiction
+| (a::l) := take b Pb Pbin, or.elim (eq_or_mem_of_mem_cons Pbin)
+              (assume Pbeqa, begin
+                rewrite [eq.symm Pbeqa, dmap_cons_of_pos Pb],
+                exact !mem_cons
+              end)
+              (assume Pbinl,
+                decidable.rec_on (h a)
+                (assume Pa, begin
+                  rewrite [dmap_cons_of_pos Pa],
+                  apply mem_cons_of_mem,
+                  exact mem_of_dmap Pb Pbinl
+                end)
+                (assume nPa, begin
+                  rewrite [dmap_cons_of_neg nPa],
+                  exact mem_of_dmap Pb Pbinl
+                end))
+
+lemma map_of_dmap_inv_pos {g : B → A} (Pinv : ∀ a (Pa : p a), g (f a Pa) = a) :
+                          ∀ {l : list A}, (∀ ⦃a⦄, a ∈ l → p a) → map g (dmap p f l) = l
+| []     := assume Pl, by rewrite [dmap_nil, map_nil]
+| (a::l) := assume Pal,
+            assert Pa : p a, from Pal a !mem_cons,
+            assert Pl : ∀ a, a ∈ l → p a,
+              from take x Pxin, Pal x (mem_cons_of_mem a Pxin),
+            by rewrite [dmap_cons_of_pos Pa, map_cons, Pinv, map_of_dmap_inv_pos Pl]
+
+lemma dinj_mem_of_mem_of_dmap (Pdi : dinj p f) : ∀ {l : list A} {a} (Pa : p a), (f a Pa) ∈ dmap p f l → a ∈ l
+| []     := take a Pa Pinnil, by contradiction
+| (b::l) := take a Pa Pmap,
+              decidable.rec_on (h b)
+              (λ Pb, begin
+                rewrite (dmap_cons_of_pos Pb) at Pmap,
+                rewrite mem_cons_iff at Pmap,
+                rewrite mem_cons_iff,
+                apply (or_of_or_of_imp_of_imp Pmap),
+                  apply Pdi,
+                  apply dinj_mem_of_mem_of_dmap Pa
+              end)
+              (λ nPb, begin
+                 rewrite (dmap_cons_of_neg nPb) at Pmap,
+                 apply mem_cons_of_mem,
+                 exact dinj_mem_of_mem_of_dmap Pa Pmap
+              end)
+
+lemma dinj_not_mem_of_dmap (Pdi : dinj p f) {l : list A} {a} (Pa : p a) :
+  a ∉ l → (f a Pa) ∉ dmap p f l :=
+not_imp_not_of_imp (dinj_mem_of_mem_of_dmap Pdi Pa)
+
+end dmap
+
 end list
 
 attribute list.decidable_any [instance]

library/data/list/perm.lean

@@ -563,8 +563,8 @@ assume p, perm_induction_on p
               exact skip y r
             end)))
     (λ nxinyt₁ : x ∉ y::t₁,
-      have   xney    : x ≠ y,  from not_eq_of_not_mem nxinyt₁,
+      have   xney    : x ≠ y,  from ne_of_not_mem_cons nxinyt₁,
-      have   nxint₁  : x ∉ t₁, from not_mem_of_not_mem nxinyt₁,
+      have   nxint₁  : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁,
       assert nxint₂  : x ∉ t₂, from
         assume xint₂ : x ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (perm.symm r) (mem_erase_dup xint₂))) nxint₁,
       by_cases

library/data/list/set.lean

@@ -66,7 +66,7 @@ lemma erase_append_right {a : A} : ∀ {l₁} (l₂), a ∉ l₁ → erase a (l
   by_cases
    (λ aeqx : a = x, by rewrite aeqx at h; exact (absurd !mem_cons h))
    (λ anex : a ≠ x,
-    assert nainxs : a ∉ xs, from not_mem_of_not_mem h,
+    assert nainxs : a ∉ xs, from not_mem_of_not_mem_cons h,
     by rewrite [append_cons, *erase_cons_tail _ anex, erase_append_right l₂ nainxs])
 
 lemma erase_sub (a : A) : ∀ l, erase a l ⊆ l
@@ -425,6 +425,26 @@ theorem nodup_filter (p : A → Prop) [h : decidable_pred p] : ∀ {l : list A},
   by_cases
     (λ pa  : p a, by rewrite [filter_cons_of_pos _ pa]; exact (nodup_cons nainf ndf))
     (λ npa : ¬ p a, by rewrite [filter_cons_of_neg _ npa]; exact ndf)
+
+lemma dmap_nodup_of_dinj {p : A → Prop} [h : decidable_pred p] {f : Π a, p a → B} (Pdi : dinj p f):
+    ∀ {l : list A}, nodup l → nodup (dmap p f l)
+| []     := take P, nodup.ndnil
+| (a::l) := take Pnodup,
+              decidable.rec_on (h a)
+                (λ Pa,
+                  begin
+                    rewrite [dmap_cons_of_pos Pa],
+                    apply nodup_cons,
+                    apply (dinj_not_mem_of_dmap Pdi Pa),
+                    exact not_mem_of_nodup_cons Pnodup,
+                    exact dmap_nodup_of_dinj (nodup_of_nodup_cons Pnodup)
+                  end)
+                (λ nPa,
+                  begin
+                    rewrite [dmap_cons_of_neg nPa],
+                    exact dmap_nodup_of_dinj (nodup_of_nodup_cons Pnodup)
+                  end)
+
 end nodup
 
 /- upto -/