209 lines
7.7 KiB
Text
209 lines
7.7 KiB
Text
/-
|
||
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Author: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn
|
||
-/
|
||
prelude
|
||
import init.data.list.basic init.function init.meta
|
||
|
||
universe variables u v
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
namespace list
|
||
|
||
lemma nil_append (s : list α) : [] ++ s = s :=
|
||
rfl
|
||
|
||
lemma cons_append (x : α) (s t : list α) : (x::s) ++ t = x::(s ++ t) :=
|
||
rfl
|
||
|
||
lemma map_nil (f : α → β) : map f [] = [] :=
|
||
rfl
|
||
|
||
lemma map_cons (f : α → β) (a : α) (l : list α) : map f (a :: l) = f a :: map f l :=
|
||
rfl
|
||
|
||
lemma length_nil : length (@nil α) = 0 :=
|
||
rfl
|
||
|
||
lemma length_cons (x : α) (t : list α) : length (x::t) = length t + 1 :=
|
||
rfl
|
||
|
||
lemma nth_zero (a : α) (l : list α) : nth (a :: l) 0 = some a :=
|
||
rfl
|
||
|
||
lemma nth_succ (a : α) (l : list α) (n : nat) : nth (a::l) (nat.succ n) = nth l n :=
|
||
rfl
|
||
|
||
/- list membership -/
|
||
lemma mem_nil_iff (a : α) : a ∈ [] ↔ false :=
|
||
iff.rfl
|
||
|
||
@[simp] lemma not_mem_nil (a : α) : a ∉ [] :=
|
||
iff.mp $ mem_nil_iff a
|
||
|
||
@[simp] lemma mem_cons_self (a : α) (l : list α) : a ∈ a :: l :=
|
||
or.inl rfl
|
||
|
||
lemma eq_nil_of_forall_not_mem : ∀ {l : list α}, (∀ a, a ∉ l) → l = nil
|
||
| [] := assume h, rfl
|
||
| (b :: l') := assume h, absurd (mem_cons_self b l') (h b)
|
||
|
||
lemma mem_cons_of_mem (y : α) {a : α} {l : list α} : a ∈ l → a ∈ y :: l :=
|
||
assume H, or.inr H
|
||
|
||
lemma eq_or_mem_of_mem_cons {a y : α} {l : list α} : a ∈ y::l → a = y ∨ a ∈ l :=
|
||
assume h, h
|
||
|
||
lemma mem_singleton {a b : α} : a ∈ [b] → a = b :=
|
||
suppose a ∈ [b], or.elim (eq_or_mem_of_mem_cons this)
|
||
(suppose a = b, this)
|
||
(suppose a ∈ [], absurd this (not_mem_nil a))
|
||
|
||
@[simp] lemma mem_singleton_iff (a b : α) : a ∈ [b] ↔ a = b :=
|
||
iff.intro mem_singleton (begin intro h, simp [h] end)
|
||
|
||
lemma mem_of_mem_cons_of_mem {a b : α} {l : list α} : a ∈ b::l → b ∈ l → a ∈ l :=
|
||
assume ainbl binl, or.elim (eq_or_mem_of_mem_cons ainbl)
|
||
(suppose a = b, begin subst a, exact binl end)
|
||
(suppose a ∈ l, this)
|
||
|
||
lemma mem_or_mem_of_mem_append {a : α} : ∀ {s t : list α}, a ∈ s ++ t → a ∈ s ∨ a ∈ t
|
||
| [] t h := or.inr h
|
||
| (b::s) t h :=
|
||
have a = b ∨ a ∈ s ++ t, from h,
|
||
match this with
|
||
| or.inl h₁ := or.inl (h₁ ▸ mem_cons_self _ _)
|
||
| or.inr h₁ :=
|
||
have a ∈ s ∨ a ∈ t, from mem_or_mem_of_mem_append h₁,
|
||
match this with
|
||
| or.inl h₂ := or.inl (mem_cons_of_mem _ h₂)
|
||
| or.inr h₂ := or.inr h₂
|
||
end
|
||
end
|
||
|
||
lemma mem_append_of_mem_or_mem {a : α} {s t : list α} : a ∈ s ∨ a ∈ t → a ∈ s ++ t :=
|
||
list.induction_on s
|
||
(take h, or.elim h false.elim id)
|
||
(take b s,
|
||
assume ih : a ∈ s ∨ a ∈ t → a ∈ s ++ t,
|
||
suppose a ∈ b::s ∨ a ∈ t,
|
||
or.elim this
|
||
(suppose a ∈ b::s,
|
||
or.elim (eq_or_mem_of_mem_cons this)
|
||
(suppose a = b, or.inl this)
|
||
(suppose a ∈ s, or.inr (ih (or.inl this))))
|
||
(suppose a ∈ t, or.inr (ih (or.inr this))))
|
||
|
||
@[simp] lemma mem_append_iff (a : α) (s t : list α) : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t :=
|
||
iff.intro mem_or_mem_of_mem_append mem_append_of_mem_or_mem
|
||
|
||
lemma not_mem_of_not_mem_append_left {a : α} {s t : list α} : a ∉ s++t → a ∉ s :=
|
||
λ nainst ains, absurd (mem_append_of_mem_or_mem (or.inl ains)) nainst
|
||
|
||
lemma not_mem_of_not_mem_append_right {a : α} {s t : list α} : a ∉ s++t → a ∉ t :=
|
||
λ nainst aint, absurd (mem_append_of_mem_or_mem (or.inr aint)) nainst
|
||
|
||
lemma not_mem_append {a : α} {s t : list α} : a ∉ s → a ∉ t → a ∉ s++t :=
|
||
λ nains naint ainst, or.elim (mem_or_mem_of_mem_append ainst)
|
||
(λ ains, by contradiction)
|
||
(λ aint, by contradiction)
|
||
|
||
lemma length_pos_of_mem {a : α} : ∀ {l : list α}, a ∈ l → 0 < length l
|
||
| [] := suppose a ∈ [], begin simp at this, contradiction end
|
||
| (b::l) := suppose a ∈ b::l, nat.zero_lt_succ _
|
||
|
||
lemma mem_split {a : α} {l : list α} : a ∈ l → ∃ s t : list α, l = s ++ (a::t) :=
|
||
list.induction_on l
|
||
(suppose a ∈ [], begin simp at this, contradiction end)
|
||
(take b l,
|
||
assume ih : a ∈ l → ∃ s t : list α, l = s ++ (a::t),
|
||
suppose a ∈ b::l,
|
||
or.elim (eq_or_mem_of_mem_cons this)
|
||
(suppose a = b, ⟨[], l, begin rw this, reflexivity end⟩)
|
||
(suppose a ∈ l,
|
||
match (ih this) with
|
||
| ⟨s, t, (h : l = s ++ (a::t))⟩ := ⟨b::s, t, begin rw h, reflexivity end⟩
|
||
end))
|
||
|
||
lemma mem_append_left {a : α} {l₁ : list α} (l₂ : list α) : a ∈ l₁ → a ∈ l₁ ++ l₂ :=
|
||
assume ainl₁, mem_append_of_mem_or_mem (or.inl ainl₁)
|
||
|
||
lemma mem_append_right {a : α} (l₁ : list α) {l₂ : list α} : a ∈ l₂ → a ∈ l₁ ++ l₂ :=
|
||
assume ainl₂, mem_append_of_mem_or_mem (or.inr ainl₂)
|
||
|
||
lemma mem_of_ne_of_mem {a y : α} {l : list α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l :=
|
||
or.elim (eq_or_mem_of_mem_cons h₂) (λe, absurd e h₁) (λr, r)
|
||
|
||
lemma ne_of_not_mem_cons {a b : α} {l : list α} : a ∉ b::l → a ≠ b :=
|
||
assume nin aeqb, absurd (or.inl aeqb) nin
|
||
|
||
lemma not_mem_of_not_mem_cons {a b : α} {l : list α} : a ∉ b::l → a ∉ l :=
|
||
assume nin nainl, absurd (or.inr nainl) nin
|
||
|
||
lemma not_mem_cons_of_ne_of_not_mem {a y : α} {l : list α} : a ≠ y → a ∉ l → a ∉ y::l :=
|
||
assume P1 P2, not.intro (assume Pain, absurd (eq_or_mem_of_mem_cons Pain) (not_or P1 P2))
|
||
|
||
lemma ne_and_not_mem_of_not_mem_cons {a y : α} {l : list α} : a ∉ y::l → a ≠ y ∧ a ∉ l :=
|
||
assume P, and.intro (ne_of_not_mem_cons P) (not_mem_of_not_mem_cons P)
|
||
|
||
-- TODO(Jeremy): move this to data/list/set.lean
|
||
|
||
definition sublist (l₁ l₂ : list α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂
|
||
|
||
instance : has_subset (list α) := ⟨sublist⟩
|
||
|
||
@[simp] lemma nil_subset (l : list α) : [] ⊆ l :=
|
||
λ b i, false.elim (iff.mp (mem_nil_iff b) i)
|
||
|
||
@[simp] lemma subset.refl (l : list α) : l ⊆ l :=
|
||
λ b i, i
|
||
|
||
lemma subset.trans {l₁ l₂ l₃ : list α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
|
||
λ b i, h₂ (h₁ i)
|
||
|
||
@[simp] lemma subset_cons (a : α) (l : list α) : l ⊆ a::l :=
|
||
λ b i, or.inr i
|
||
|
||
lemma subset_of_cons_subset {a : α} {l₁ l₂ : list α} : a::l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
|
||
λ s b i, s (mem_cons_of_mem _ i)
|
||
|
||
lemma cons_subset_cons {l₁ l₂ : list α} (a : α) (s : l₁ ⊆ l₂) : (a::l₁) ⊆ (a::l₂) :=
|
||
λ b hin, or.elim (eq_or_mem_of_mem_cons hin)
|
||
(λ e : b = a, or.inl e)
|
||
(λ i : b ∈ l₁, or.inr (s i))
|
||
|
||
@[simp] lemma subset_append_left (l₁ l₂ : list α) : l₁ ⊆ l₁++l₂ :=
|
||
λ b i, iff.mpr (mem_append_iff b l₁ l₂) (or.inl i)
|
||
|
||
@[simp] lemma subset_append_right (l₁ l₂ : list α) : l₂ ⊆ l₁++l₂ :=
|
||
λ b i, iff.mpr (mem_append_iff b l₁ l₂) (or.inr i)
|
||
|
||
lemma subset_cons_of_subset (a : α) {l₁ l₂ : list α} : l₁ ⊆ l₂ → l₁ ⊆ (a::l₂) :=
|
||
λ (s : l₁ ⊆ l₂) (a : α) (i : a ∈ l₁), or.inr (s i)
|
||
|
||
lemma subset_app_of_subset_left (l l₁ l₂ : list α) : l ⊆ l₁ → l ⊆ l₁++l₂ :=
|
||
λ (s : l ⊆ l₁) (a : α) (ainl : a ∈ l),
|
||
have a ∈ l₁, from s ainl,
|
||
mem_append_of_mem_or_mem (or.inl this)
|
||
|
||
lemma subset_app_of_subset_right (l l₁ l₂ : list α) : l ⊆ l₂ → l ⊆ l₁++l₂ :=
|
||
λ (s : l ⊆ l₂) (a : α) (ainl : a ∈ l),
|
||
have a ∈ l₂, from s ainl,
|
||
mem_append_of_mem_or_mem (or.inr this)
|
||
|
||
lemma cons_subset_of_subset_of_mem {a : α} {l m : list α} (ainm : a ∈ m) (lsubm : l ⊆ m) :
|
||
a::l ⊆ m :=
|
||
take b, suppose b ∈ a::l,
|
||
or.elim (eq_or_mem_of_mem_cons this)
|
||
(suppose b = a, begin subst b, exact ainm end)
|
||
(suppose b ∈ l, lsubm this)
|
||
|
||
lemma app_subset_of_subset_of_subset {l₁ l₂ l : list α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) :
|
||
l₁ ++ l₂ ⊆ l :=
|
||
take a, suppose a ∈ l₁ ++ l₂,
|
||
or.elim (mem_or_mem_of_mem_append this)
|
||
(suppose a ∈ l₁, l₁subl this)
|
||
(suppose a ∈ l₂, l₂subl this)
|
||
|
||
end list
|