From 23a1f5fa4b990bb9fab5e4489614851bc02a1073 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Apr 2015 15:44:07 -0700 Subject: [PATCH] feat(library/data/list/basic): define nodup and disjoint --- library/data/list/basic.lean | 110 ++++++++++++++++++++++++++++++++++- 1 file changed, 108 insertions(+), 2 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index eacfae222..6bb95dd55 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -7,7 +7,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura Basic properties of lists. -/ -import logic tools.helper_tactics data.nat.basic +import logic tools.helper_tactics data.nat.basic algebra.function open eq.ops helper_tactics nat prod function @@ -206,6 +206,12 @@ list.induction_on s theorem mem_append_iff (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t := iff.intro mem_or_mem_of_mem_append mem_append_of_mem_or_mem +theorem not_mem_of_not_mem_append_left {x : T} {s t : list T} : x ∉ s++t → x ∉ s := +λ nxinst xins, absurd (mem_append_of_mem_or_mem (or.inl xins)) nxinst + +theorem not_mem_of_not_mem_append_right {x : T} {s t : list T} : x ∉ s++t → x ∉ t := +λ nxinst xint, absurd (mem_append_of_mem_or_mem (or.inr xint)) nxinst + local attribute mem [reducible] local attribute append [reducible] theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) := @@ -381,7 +387,11 @@ theorem map_nil (f : A → B) : map f [] = [] theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l -theorem map_map (g : B → C) (f : A → B) : ∀ l : list A, map g (map f l) = map (g ∘ f) l +theorem map_id : ∀ l : list A, map id l = l +| [] := rfl +| (x::xs) := begin rewrite [map_cons, map_id] end + +theorem map_map (g : B → C) (f : A → B) : ∀ l, map g (map f l) = map (g ∘ f) l | [] := rfl | (a :: l) := show (g ∘ f) a :: map g (map f l) = map (g ∘ f) (a :: l), @@ -393,6 +403,12 @@ theorem len_map (f : A → B) : ∀ l : list A, length (map f l) = length l show length (map f l) + 1 = length l + 1, by rewrite (len_map l) +theorem mem_map {A B : Type} (f : A → B) : ∀ {a l}, a ∈ l → f a ∈ map f l +| a [] i := absurd i !not_mem_nil +| a (x::xs) i := or.elim i + (λ aeqx : a = x, by rewrite [aeqx, map_cons]; apply mem_cons) + (λ ainxs : a ∈ xs, or.inr (mem_map ainxs)) + definition map₂ (f : A → B → C) : list A → list B → list C | [] _ := [] | _ [] := [] @@ -659,6 +675,96 @@ lemma erase_sub (a : A) : ∀ l, erase a l ⊆ l or.inr yinxs)) end erase + +/- disjoint -/ +section disjoint +variable {A : Type} + +definition disjoint (l₁ l₂ : list A) : Prop := ∀ a, (a ∈ l₁ → a ∉ l₂) ∧ (a ∈ l₂ → a ∉ l₁) + +lemma disjoint_left {l₁ l₂ : list A} : disjoint l₁ l₂ → ∀ a, a ∈ l₁ → a ∉ l₂ := +λ d a, and.elim_left (d a) + +lemma disjoint_right {l₁ l₂ : list A} : disjoint l₁ l₂ → ∀ a, a ∈ l₂ → a ∉ l₁ := +λ d a, and.elim_right (d a) + +lemma disjoint.comm {l₁ l₂ : list A} : disjoint l₁ l₂ → disjoint l₂ l₁ := +λ d a, and.intro + (λ ainl₂ : a ∈ l₂, disjoint_right d a ainl₂) + (λ ainl₁ : a ∈ l₁, disjoint_left d a ainl₁) + +lemma disjoint_of_disjoint_cons_left {a : A} {l₁ l₂} : disjoint (a::l₁) l₂ → disjoint l₁ l₂ := +λ d x, and.intro + (λ xinl₁ : x ∈ l₁, disjoint_left d x (or.inr xinl₁)) + (λ xinl₂ : x ∈ l₂, + have nxinal₁ : x ∉ a::l₁, from disjoint_right d x xinl₂, + not_mem_of_not_mem nxinal₁) + +lemma disjoint_of_disjoint_cons_right {a : A} {l₁ l₂} : disjoint l₁ (a::l₂) → disjoint l₁ l₂ := +λ d, disjoint.comm (disjoint_of_disjoint_cons_left (disjoint.comm d)) + +lemma disjoint_nil_left (l : list A) : disjoint [] l := +λ a, and.intro + (λ ab : a ∈ nil, absurd ab !not_mem_nil) + (λ ainl : a ∈ l, !not_mem_nil) + +lemma disjoint_nil_right (l : list A) : disjoint l [] := +disjoint.comm (disjoint_nil_left l) +end disjoint + +/- no duplicates predicate -/ + +inductive nodup {A : Type} : list A → Prop := +| ndnil : nodup [] +| ndcons : ∀ {a l}, a ∉ l → nodup l → nodup (a::l) + +section nodup +open nodup +variables {A B : Type} + +lemma nodup_nil : @nodup A [] := +ndnil + +lemma nodup_cons {a : A} {l : list A} : a ∉ l → nodup l → nodup (a::l) := +λ i n, ndcons i n + +lemma nodup_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → nodup l +| a xs (ndcons i n) := n + +lemma not_mem_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → a ∉ l +| a xs (ndcons i n) := i + +lemma nodup_of_nodup_append_left : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₁ +| [] l₂ n := nodup_nil +| (x::xs) l₂ n := + have ndxs : nodup xs, from nodup_of_nodup_append_left (nodup_of_nodup_cons n), + have nxinxsl₂ : x ∉ xs++l₂, from not_mem_of_nodup_cons n, + have nxinxs : x ∉ xs, from not_mem_of_not_mem_append_left nxinxsl₂, + nodup_cons nxinxs ndxs + +lemma nodup_of_nodup_append_right : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₂ +| [] l₂ n := n +| (x::xs) l₂ n := nodup_of_nodup_append_right (nodup_of_nodup_cons n) + +lemma nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l → nodup (map f l) +| [] n := begin rewrite [map_nil], apply nodup_nil end +| (x::xs) n := + assert nxinxs : x ∉ xs, from not_mem_of_nodup_cons n, + assert ndxs : nodup xs, from nodup_of_nodup_cons n, + assert ndmfxs : nodup (map f xs), from nodup_map ndxs, + assert nfxinm : f x ∉ map f xs, from + λ ab : f x ∈ map f xs, + obtain (finv : B → A) (isinv : finv ∘ f = id), from inj, + assert finvfxin : finv (f x) ∈ map finv (map f xs), from mem_map finv ab, + assert xinxs : x ∈ xs, + begin + rewrite [map_map at finvfxin, isinv at finvfxin, left_inv_eq isinv at finvfxin], + rewrite [map_id at finvfxin], + exact finvfxin + end, + absurd xinxs nxinxs, + nodup_cons nfxinm ndmfxs +end nodup end list attribute list.has_decidable_eq [instance]