From 42fe87d7cc3ae4138cd717c09396e12d596d7a8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Mar 2015 03:18:02 -0700 Subject: [PATCH] feat(library/data/list/basic): add sublist predicate --- library/data/list/basic.lean | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 13e47c0735..b2b097f3a2 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -237,6 +237,36 @@ list.rec_on l iff.elim_right (not_iff_not_of_iff !mem_cons_iff) H1, decidable.inr H2))) +theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l := +or.elim H₂ (λe, absurd e H₁) (λr, r) + +definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ l₂ + +infix `⊆`:50 := sublist + +lemma nil_sub (l : list T) : [] ⊆ l := +λ b i, false.elim (iff.mp (mem_nil b) i) + +lemma sub.refl (l : list T) : l ⊆ l := +λ b i, i + +lemma sub.trans {l₁ l₂ l₃ : list T} (H₁ : l₁ ⊆ l₂) (H₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ := +λ b i, H₂ (H₁ i) + +lemma sub_cons (a : T) (l : list T) : l ⊆ a::l := +λ b i, or.inr i + +lemma cons_sub_cons {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l₁) ⊆ (a::l₂) := +λ b Hin, or.elim Hin + (λ e : b = a, or.inl e) + (λ i : b ∈ l₁, or.inr (s i)) + +lemma sub_append_left (l₁ l₂ : list T) : l₁ ⊆ l₁++l₂ := +λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inl i) + +lemma sub_append_right (l₁ l₂ : list T) : l₂ ⊆ l₁++l₂ := +λ b i, iff.mp' (mem_append_iff b l₁ l₂) (or.inr i) + /- find -/ section