From f475408f4ced3e09d9b0537ad3ab33007132e5e6 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 5 Jun 2015 18:18:59 +1000 Subject: [PATCH] feat(library/data/list/*): add theorems from Haitao Zhang and clean up --- library/data/list/basic.lean | 44 +++++++++++++++++++-- library/data/list/comb.lean | 77 +++++++++++++++++++++++++++++++++++- library/data/list/perm.lean | 4 +- library/data/list/set.lean | 22 ++++++++++- 4 files changed, 139 insertions(+), 8 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index a66107157..2ae6527e2 100644 --- a/library/data/list/basic.lean +++ b/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 -/ diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index dc4df3090..b8a66ad80 100644 --- a/library/data/list/comb.lean +++ b/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] diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index a36344c31..1ab4fb88d 100644 --- a/library/data/list/perm.lean +++ b/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 nxint₁ : x ∉ t₁, from not_mem_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_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 diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 5527ae934..f8e54516a 100644 --- a/library/data/list/set.lean +++ b/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 -/