diff --git a/library/data/list/permutations.lean b/library/data/list/permutations.lean new file mode 100644 index 0000000000..8157b3f083 --- /dev/null +++ b/library/data/list/permutations.lean @@ -0,0 +1,43 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Mario Carneiro +-/ +universes u v + +namespace list +variables {α : Type u} {β : Type v} +open nat prod well_founded + +def permutations_aux2 (t : α) (ts : list α) : list α → (list α → β) → list β → list α × list β +| [] f r := (ts, r) +| (y::ys) f r := let (us, zs) := permutations_aux2 ys (λx : list α, f (y::x)) r in + (y :: us, f (t :: y :: us) :: zs) + +private def meas : list α × list α → ℕ × ℕ | (l, i) := (length l + length i, length l) + +local infix ` ≺ `:50 := inv_image (lex (<) (<)) meas + +def permutations_aux.F : Π (x : list α × list α), (Π (y : list α × list α), y ≺ x → list (list α)) → list (list α) +| ([], is) IH := [] +| (t::ts, is) IH := +have h1 : (ts, t :: is) ≺ (t :: ts, is), from + show lex _ _ (succ (length ts + length is), length ts) (succ (length ts) + length is, length (t :: ts)), + by rw nat.succ_add; exact lex.right _ _ (lt_succ_self _), +have h2 : (is, []) ≺ (t :: ts, is), from lex.left _ _ _ (lt_add_of_pos_left _ (succ_pos _)), +foldr (λy r, (permutations_aux2 t ts y id r).2) (IH (ts, t::is) h1) (is :: IH (is, []) h2) + +def permutations_aux : list α × list α → list (list α) := +fix (inv_image.wf meas (prod.lex_wf lt_wf lt_wf)) permutations_aux.F + +def permutations (l : list α) : list (list α) := +l :: permutations_aux (l, []) + +def permutations_aux.eqn_1 (is : list α) : permutations_aux ([], is) = [] := +fix_eq _ _ _ + +def permutations_aux.eqn_2 (t : α) (ts is) : permutations_aux (t::ts, is) = + foldr (λy r, (permutations_aux2 t ts y id r).2) (permutations_aux (ts, t::is)) (permutations is) := +fix_eq _ _ _ + +end list diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index a87cafca60..36b44d167a 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -134,27 +134,63 @@ def filter (p : α → Prop) [decidable_pred p] : list α → list α | [] := [] | (a::l) := if p a then a :: filter l else filter l -def find [decidable_eq α] : α → list α → nat -| a [] := 0 -| a (b :: l) := if a = b then 0 else succ (find a l) +def partition (p : α → Prop) [decidable_pred p] : list α → list α × list α +| [] := ([], []) +| (a::l) := let (l₁, l₂) := partition l in if p a then (a :: l₁, l₂) else (l₁, a :: l₂) + +def take_while (p : α → Prop) [decidable_pred p] : list α → list α +| [] := [] +| (a::l) := if p a then a :: take_while l else [] + +def drop_while (p : α → Prop) [decidable_pred p] : list α → list α +| [] := [] +| (a::l) := if p a then drop_while l else a::l + +def span (p : α → Prop) [decidable_pred p] : list α → list α × list α +| [] := ([], []) +| (a::xs) := if p a then let (l, r) := span xs in (a :: l, r) else ([], a::xs) + +def find (p : α → Prop) [decidable_pred p] : list α → option α +| [] := none +| (a::l) := if p a then some a else find l + +def find_index (p : α → Prop) [decidable_pred p] : list α → nat +| [] := 0 +| (a::l) := if p a then 0 else succ (find_index l) + +def find_indexes_aux (p : α → Prop) [decidable_pred p] : list α → nat → list nat +| [] n := [] +| (a::l) n := let t := find_indexes_aux l (succ n) in if p a then n :: t else t + +def find_indexes (p : α → Prop) [decidable_pred p] (l : list α) : list nat := +find_indexes_aux p l 0 + +def index_of [decidable_eq α] (a : α) : list α → nat := find_index (eq a) + +def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a) def dropn : ℕ → list α → list α -| 0 a := a -| (succ n) [] := [] +| 0 a := a +| (succ n) [] := [] | (succ n) (x::r) := dropn n r def taken : ℕ → list α → list α -| 0 a := [] -| (succ n) [] := [] +| 0 a := [] +| (succ n) [] := [] | (succ n) (x :: r) := x :: taken n r +def split_at : ℕ → list α → list α × list α +| 0 a := ([], a) +| (succ n) [] := ([], []) +| (succ n) (x :: xs) := let (l, r) := split_at n xs in (x :: l, r) + def foldl (f : α → β → α) : α → list β → α | a [] := a | a (b :: l) := foldl (f a b) l -def foldr (f : α → β → β) : β → list α → β -| b [] := b -| b (a :: l) := f a (foldr b l) +def foldr (f : α → β → β) (b : β) : list α → β +| [] := b +| (a :: l) := f a (foldr l) def any (l : list α) (p : α → bool) : bool := foldr (λ a r, p a || r) ff l @@ -188,12 +224,9 @@ def range_core : ℕ → list ℕ → list ℕ def range (n : ℕ) : list ℕ := range_core n [] -def iota_core : ℕ → list ℕ → list ℕ -| 0 l := reverse l -| (succ n) l := iota_core n (succ n :: l) - -def iota : ℕ → list ℕ := -λ n, iota_core n [] +def iota : ℕ → list ℕ +| 0 := [] +| (succ n) := succ n :: iota n def enum_from : ℕ → list α → list (ℕ × α) | n [] := nil @@ -228,4 +261,48 @@ join (map b a) @[inline] def ret {α : Type u} (a : α) : list α := [a] + +def transpose_aux : list α → list (list α) → list (list α) +| [] ls := ls +| (a::i) [] := [a] :: transpose_aux i [] +| (a::i) (l::ls) := (a::l) :: transpose_aux i ls + +def transpose : list (list α) → list (list α) +| [] := [] +| (l::ls) := transpose_aux l (transpose ls) + +def sublists_aux : list α → (list α → list β → list β) → list β +| [] f := [] +| (a::l) f := f [a] (sublists_aux l (λys r, f ys (f (a :: ys) r))) + +def sublists (l : list α) : list (list α) := +[] :: sublists_aux l cons + +def scanl (f : α → β → α) : α → list β → list α +| a [] := [a] +| a (b::l) := a :: scanl (f a b) l + +def scanr_aux (f : α → β → β) (b : β) : list α → β × list β +| [] := (b, []) +| (a::l) := let (b', l') := scanr_aux l in (f a b', b' :: l') + +def scanr (f : α → β → β) (b : β) (l : list α) : list β := +let (b', l') := scanr_aux f b l in b' :: l' + +def inits : list α → list (list α) +| [] := [[]] +| (a::l) := [] :: map (λt, a::t) (inits l) + +def tails : list α → list (list α) +| [] := [[]] +| (a::l) := (a::l) :: tails l + +def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂ +def is_suffix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, t ++ l₁ = l₂ +def is_infix (l₁ : list α) (l₂ : list α) : Prop := ∃ s t, s ++ l₁ ++ t = l₂ + +infix ` <+: `:50 := is_prefix +infix ` <:+ `:50 := is_suffix +infix ` <:+: `:50 := is_infix + end list diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index 0d61d88896..f97f445596 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -84,4 +84,54 @@ if h : ∃ x ∈ l, ¬ p x then else is_true $ λ x hx, if h' : p x then h' else false.elim $ h ⟨x, hx, h'⟩ +instance decidable_prefix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidable (l₁ <+: l₂) +| [] l₂ := is_true ⟨l₂, rfl⟩ +| (a::l₁) [] := is_false $ λ⟨t, te⟩, list.no_confusion te +| (a::l₁) (b::l₂) := + if h : a = b then + decidable_of_decidable_of_iff (decidable_prefix l₁ l₂) $ by rw -h; exact + ⟨λ⟨t, te⟩, ⟨t, by rw -te; refl⟩, + λ⟨t, te⟩, list.no_confusion te (λ_ te, ⟨t, te⟩)⟩ + else + is_false $ λ⟨t, te⟩, list.no_confusion te $ λh', absurd h' h + +-- Alternatively, use mem_tails +instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidable (l₁ <:+ l₂) +| [] l₂ := is_true ⟨l₂, append_nil _⟩ +| (a::l₁) [] := is_false $ λ⟨t, te⟩, absurd te $ + append_ne_nil_of_ne_nil_right _ _ $ λh, list.no_confusion h +| l₁ l₂ := let len1 := length l₁, len2 := length l₂ in + if hl : len1 ≤ len2 then + if he : dropn (len2 - len1) l₂ = l₁ then is_true $ + ⟨taken (len2 - len1) l₂, by rw [-he, taken_append_dropn]⟩ + else is_false $ + suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → dropn (length l₂ - length l₁) l₂ = l₁, + from λsuf, he (this hl suf), + λ hl ⟨t, te⟩, and.right $ + append_right_inj (eq.trans (taken_append_dropn (length l₂ - length l₁) l₂) te.symm) $ + by simp; exact nat.sub_sub_self hl + else is_false $ λ⟨t, te⟩, hl $ + show length l₁ ≤ length l₂, by rw [-te, length_append]; apply nat.le_add_left + +instance decidable_infix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidable (l₁ <:+: l₂) +| [] l₂ := is_true ⟨[], l₂, rfl⟩ +| (a::l₁) [] := is_false $ λ⟨s, t, te⟩, absurd te $ append_ne_nil_of_ne_nil_left _ _ $ + append_ne_nil_of_ne_nil_right _ _ $ λh, list.no_confusion h +| l₁ l₂ := decidable_of_decidable_of_iff (list.decidable_bex (λt, l₁ <+: t) (tails l₂)) $ + by refine (exists_congr (λt, _)).trans (infix_iff_prefix_suffix _ _).symm; + exact ⟨λ⟨h1, h2⟩, ⟨h2, (mem_tails _ _).1 h1⟩, λ⟨h2, h1⟩, ⟨(mem_tails _ _).2 h1, h2⟩⟩ + +instance decidable_sublist [decidable_eq α] : ∀ (l₁ l₂ : list α), decidable (l₁ <+ l₂) +| [] l₂ := is_true $ nil_sublist _ +| (a::l₁) [] := is_false $ λh, list.no_confusion $ eq_nil_of_sublist_nil h +| (a::l₁) (b::l₂) := + if h : a = b then + decidable_of_decidable_of_iff (decidable_sublist l₁ l₂) $ + by rw -h; exact ⟨cons_sublist_cons _, sublist_of_cons_sublist_cons⟩ + else decidable_of_decidable_of_iff (decidable_sublist (a::l₁) l₂) + ⟨sublist_cons_of_sublist _, λs, match a, l₁, s, h with + | a, l₁, sublist.cons ._ ._ ._ s', h := s' + | ._, ._, sublist.cons2 t ._ ._ s', h := absurd rfl h + end⟩ + end list diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index 7021b52fc5..d761caab18 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -34,10 +34,10 @@ lemma append_ne_nil_of_ne_nil_right (s t : list α) : t ≠ [] → s ++ t ≠ [] by induction s; intros; contradiction lemma append_foldl (f : α → β → α) (a : α) (s t : list β) : foldl f a (s ++ t) = foldl f (foldl f a s) t := -by {revert a, induction s with b s H, exact λ_, rfl, intros, simp[foldl], rw H _} +by {revert a, induction s with b s H, exact λ_, rfl, intros, simp [foldl], rw H _} lemma append_foldr (f : α → β → β) (a : β) (s t : list α) : foldr f a (s ++ t) = foldr f (foldr f a t) s := -by {revert a, induction s with b s H, exact λ_, rfl, intros, simp[foldr], rw H _} +by {revert a, induction s with b s H, exact λ_, rfl, intros, simp [foldr], rw H _} /- concat -/ @@ -61,6 +61,16 @@ by cases l; refl attribute [simp] repeat taken dropn +@[simp] lemma split_at_eq_taken_dropn : ∀ (n : ℕ) (l : list α), split_at n l = (taken n l, dropn n l) +| 0 a := rfl +| (succ n) [] := rfl +| (succ n) (x :: xs) := by simp [split_at, split_at_eq_taken_dropn n xs] + +@[simp] lemma taken_append_dropn : ∀ (n : ℕ) (l : list α), taken n l ++ dropn n l = l +| 0 a := rfl +| (succ n) [] := rfl +| (succ n) (x :: xs) := by simp [taken_append_dropn n xs] + /- length -/ attribute [simp] length @@ -104,6 +114,24 @@ lemma length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length ( | (x::xs) (i+1) h := have i < length xs, from lt_of_succ_lt_succ h, by dsimp [remove_nth]; rw [length_remove_nth xs i this, nat.sub_add_cancel (lt_of_le_of_lt (nat.zero_le _) this)]; refl +lemma append_inj : ∀ {s₁ s₂ t₁ t₂ : list α}, s₁ ++ t₁ = s₂ ++ t₂ → length s₁ = length s₂ → s₁ = s₂ ∧ t₁ = t₂ +| [] [] t₁ t₂ h hl := ⟨rfl, h⟩ +| (a::s₁) [] t₁ t₂ h hl := list.no_confusion $ eq_nil_of_length_eq_zero hl +| [] (b::s₂) t₁ t₂ h hl := list.no_confusion $ eq_nil_of_length_eq_zero hl.symm +| (a::s₁) (b::s₂) t₁ t₂ h hl := list.no_confusion h $ λab hap, + let ⟨e1, e2⟩ := @append_inj s₁ s₂ t₁ t₂ hap (succ.inj hl) in + by rw [ab, e1, e2]; exact ⟨rfl, rfl⟩ + +lemma append_inj_left {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = length s₂) : s₁ = s₂ := +(append_inj h hl).left + +lemma append_inj_right {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = length s₂) : t₁ = t₂ := +(append_inj h hl).right + +lemma append_right_inj {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ ∧ t₁ = t₂ := +append_inj h $ @nat.add_right_cancel _ (length t₁) _ $ +let hap := congr_arg length h in by simp at hap; rwa -hl at hap + /- nth -/ theorem nth_le_nth : Π (l : list α) (n h), nth l n = some (nth_le l n h) @@ -398,6 +426,25 @@ iff_true_intro $ λx, false.elim ⟨λal, ⟨al a (mem_cons_self _ _), λx h, al x (mem_cons_of_mem _ h)⟩, λ⟨pa, al⟩ x o, o.elim (λe, e.symm ▸ pa) (al x)⟩ +lemma mem_map (f : α → β) {a : α} {l : list α} (h : a ∈ l) : f a ∈ map f l := +begin + induction l with b l' ih, + {simp at h, contradiction }, + {simp, simp at h, cases h with h h, + {simph}, + {exact or.inr (ih h)}} +end + +lemma exists_of_mem_map {f : α → β} {b : β} {l : list α} (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := +begin + induction l with c l' ih, + {simp at h, contradiction}, + {cases (eq_or_mem_of_mem_cons h) with h h, + {existsi c, simp [h]}, + {cases ih h with a ha, cases ha with ha₁ ha₂, + existsi a, simph }} +end + /- list subset -/ protected def subset (l₁ l₂ : list α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ @@ -457,6 +504,10 @@ or.elim (mem_or_mem_of_mem_append this) (suppose a ∈ l₁, l₁subl this) (suppose a ∈ l₂, l₂subl this) +lemma eq_nil_of_subset_nil : ∀ {l : list α}, l ⊆ [] → l = [] +| [] s := rfl +| (a::l) s := absurd (s $ mem_cons_self a l) (not_mem_nil a) + /- sublists -/ inductive sublist : list α → list α → Prop @@ -489,7 +540,7 @@ sublist.cons _ _ _ (sublist.refl l) lemma sublist_of_cons_sublist {a : α} {l₁ l₂ : list α} : a::l₁ <+ l₂ → l₁ <+ l₂ := sublist.trans (sublist_cons a l₁) -lemma cons_sublist_cons {l₁ l₂ : list α} (a : α) (s : l₁ <+ l₂) : (a::l₁) <+ (a::l₂) := +lemma cons_sublist_cons {l₁ l₂ : list α} (a : α) (s : l₁ <+ l₂) : a::l₁ <+ a::l₂ := sublist.cons2 _ _ _ s @[simp] lemma sublist_append_left : Π (l₁ l₂ : list α), l₁ <+ l₁++l₂ @@ -500,7 +551,7 @@ sublist.cons2 _ _ _ s | [] l₂ := sublist.refl _ | (a::l₁) l₂ := sublist.cons _ _ _ (sublist_append_right l₁ l₂) -lemma sublist_cons_of_sublist (a : α) {l₁ l₂ : list α} : l₁ <+ l₂ → l₁ <+ (a::l₂) := +lemma sublist_cons_of_sublist (a : α) {l₁ l₂ : list α} : l₁ <+ l₂ → l₁ <+ a::l₂ := sublist.cons _ _ _ lemma sublist_app_of_sublist_left (l l₁ l₂ : list α) (s : l <+ l₁) : l <+ l₁++l₂ := @@ -509,42 +560,178 @@ sublist.trans s (sublist_append_left _ _) lemma sublist_app_of_sublist_right (l l₁ l₂ : list α) (s : l <+ l₂) : l <+ l₁++l₂ := sublist.trans s (sublist_append_right _ _) -lemma subset_of_sublist : Π {l₁ l₂ : list α} (s : l₁ <+ l₂) ⦃b⦄ (h : b ∈ l₁), b ∈ l₂ -| ._ ._ sublist.slnil b h := h -| ._ ._ (sublist.cons l₁ l₂ a s) b h := mem_cons_of_mem _ (subset_of_sublist s h) +lemma sublist_of_cons_sublist_cons {l₁ l₂ : list α} : ∀ {a : α}, a::l₁ <+ a::l₂ → l₁ <+ l₂ +| ._ (sublist.cons ._ ._ a s) := sublist_of_cons_sublist s +| ._ (sublist.cons2 ._ ._ a s) := s + +lemma subset_of_sublist : Π {l₁ l₂ : list α}, l₁ <+ l₂ → l₁ ⊆ l₂ +| ._ ._ sublist.slnil b h := h +| ._ ._ (sublist.cons l₁ l₂ a s) b h := mem_cons_of_mem _ (subset_of_sublist s h) | ._ ._ (sublist.cons2 l₁ l₂ a s) b h := match eq_or_mem_of_mem_cons h with | or.inl h := by rw h; exact mem_cons_self _ _ | or.inr h := mem_cons_of_mem _ (subset_of_sublist s h) end +lemma length_le_of_sublist : ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → length l₁ ≤ length l₂ +| ._ ._ sublist.slnil := le_refl 0 +| ._ ._ (sublist.cons l₁ l₂ a s) := le_succ_of_le (length_le_of_sublist s) +| ._ ._ (sublist.cons2 l₁ l₂ a s) := succ_le_succ (length_le_of_sublist s) + +lemma eq_nil_of_sublist_nil {l : list α} (s : l <+ []) : l = [] := +eq_nil_of_subset_nil $ subset_of_sublist s + lemma eq_nil_of_map_eq_nil {f : α → β} {l :list α} (h : map f l = nil) : l = nil := eq_nil_of_length_eq_zero (begin rw -(length_map f l), simp [h] end) -lemma mem_map (f : α → β) {a : α} {l : list α} (h : a ∈ l) : f a ∈ map f l := -begin - induction l with b l' ih, - {simp at h, contradiction }, - {simp, simp at h, cases h with h h, - {simph}, - {exact or.inr (ih h)}} -end +lemma eq_of_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) : b₁ = b₂ := +let ⟨a, _, e⟩ := exists_of_mem_map h in e.symm -lemma exists_of_mem_map {f : α → β} {b : β} {l : list α} (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := -begin - induction l with c l' ih, - {simp at h, contradiction}, - {cases (eq_or_mem_of_mem_cons h) with h h, - {existsi c, simp [h]}, - {cases ih h with a ha, cases ha with ha₁ ha₂, - existsi a, simph }} -end +/- foldl, foldr, scanl, scanr -/ -lemma eq_of_map_const {b₁ b₂ : β} : ∀ {l : list α}, b₁ ∈ map (function.const α b₂) l → b₁ = b₂ -| [] h := absurd h (not_mem_nil b₁) -| (a::l) h := - or.elim (eq_or_mem_of_mem_cons h) - (suppose b₁ = b₂, this) - (suppose b₁ ∈ map (function.const α b₂) l, eq_of_map_const this) +attribute [simp] foldl foldr + +@[simp] lemma foldr_eta : ∀ (l : list α), foldr cons [] l = l +| [] := rfl +| (x::l) := by simp [foldr_eta l] + +@[simp] lemma scanr_nil (f : α → β → β) (b : β) : scanr f b [] = [b] := rfl + +@[simp] lemma scanr_aux_cons (f : α → β → β) (b : β) : ∀ (a : α) (l : list α), + scanr_aux f b (a::l) = (foldr f b (a::l), scanr f b l) +| a [] := rfl +| a (x::l) := let t := scanr_aux_cons x l in + by simp [scanr, scanr_aux] at t; simp [scanr, scanr_aux, t] + +@[simp] lemma scanr_cons (f : α → β → β) (b : β) (a : α) (l : list α) : + scanr f b (a::l) = foldr f b (a::l) :: scanr f b l := +by simp [scanr] + +/- filter, partition, take_while, drop_while, span -/ + +attribute [simp] repeat taken dropn + +@[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l) +| [] := rfl +| (a::l) := by { by_cases p a; intro pa; simp [partition, filter, pa, partition_eq_filter_filter l], + rw [if_neg (not_not_intro pa)], rw [if_pos pa] } + +@[simp] lemma span_eq_take_drop (p : α → Prop) [decidable_pred p] : ∀ (l : list α), span p l = (take_while p l, drop_while p l) +| [] := rfl +| (a::l) := by by_cases p a; intro pa; simp [span, take_while, drop_while, pa, span_eq_take_drop l] + +@[simp] lemma take_while_append_drop (p : α → Prop) [decidable_pred p] : ∀ (l : list α), take_while p l ++ drop_while p l = l +| [] := rfl +| (a::l) := by by_cases p a; intro pa; simp [take_while, drop_while, pa, take_while_append_drop l] + +/- inits, tails -/ + +attribute [simp] inits tails + +/- prefix, suffix, infix -/ + +lemma prefix_append (l₁ l₂ : list α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩ + +lemma suffix_append (l₁ l₂ : list α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩ + +lemma infix_append (l₁ l₂ l₃ : list α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩ + +lemma prefix_refl (l : list α) : l <+: l := ⟨[], append_nil _⟩ + +lemma suffix_refl (l : list α) : l <:+ l := ⟨[], rfl⟩ + +lemma infix_of_prefix {l₁ l₂ : list α} : l₁ <+: l₂ → l₁ <:+: l₂ := +λ⟨t, h⟩, ⟨[], t, h⟩ + +lemma infix_of_suffix {l₁ l₂ : list α} : l₁ <:+ l₂ → l₁ <:+: l₂ := +λ⟨t, h⟩, ⟨t, [], by simp [h]⟩ + +lemma infix_refl (l : list α) : l <:+: l := infix_of_prefix $ prefix_refl l + +lemma sublist_of_infix {l₁ l₂ : list α} : l₁ <:+: l₂ → l₁ <+ l₂ := +λ⟨s, t, h⟩, by rw -h; exact (sublist_append_right _ _).trans (sublist_append_left _ _) + +lemma length_le_of_infix {l₁ l₂ : list α} (s : l₁ <:+: l₂) : length l₁ ≤ length l₂ := +length_le_of_sublist $ sublist_of_infix s + +lemma eq_nil_of_infix_nil {l : list α} (s : l <:+: []) : l = [] := +eq_nil_of_sublist_nil $ sublist_of_infix s + +lemma eq_nil_of_prefix_nil {l : list α} (s : l <+: []) : l = [] := +eq_nil_of_infix_nil $ infix_of_prefix s + +lemma eq_nil_of_suffix_nil {l : list α} (s : l <:+ []) : l = [] := +eq_nil_of_infix_nil $ infix_of_suffix s + +lemma infix_iff_prefix_suffix (l₁ l₂ : list α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ := +⟨λ⟨s, t, e⟩, ⟨l₁ ++ t, ⟨_, rfl⟩, by rw [-e, append_assoc]; exact ⟨_, rfl⟩⟩, +λ⟨._, ⟨t, rfl⟩, ⟨s, e⟩⟩, ⟨s, t, by rw append_assoc; exact e⟩⟩ + +@[simp] lemma mem_inits : ∀ (s t : list α), s ∈ inits t ↔ s <+: t +| s [] := by simp; exact ⟨λh, by rw h; exact prefix_refl [], eq_nil_of_prefix_nil⟩ +| s (a::t) := by simp; exact ⟨λo, match s, o with + | ._, or.inl rfl := ⟨_, rfl⟩ + | s, or.inr mm := let ⟨r, hr, hs⟩ := exists_of_mem_map mm, ⟨s, ht⟩ := (mem_inits _ _).1 hr in + by rw [-hs, -ht]; exact ⟨s, rfl⟩ + end, λmi, match s, mi with + | [], ⟨._, rfl⟩ := or.inl rfl + | (b::s), ⟨r, hr⟩ := list.no_confusion hr $ λba st, or.inr $ + by rw ba; exact mem_map _ ((mem_inits _ _).2 ⟨_, st⟩) + end⟩ + +@[simp] lemma mem_tails : ∀ (s t : list α), s ∈ tails t ↔ s <:+ t +| s [] := by simp; exact ⟨λh, by rw h; exact suffix_refl [], eq_nil_of_suffix_nil⟩ +| s (a::t) := by simp [mem_tails s t]; exact show s <:+ t ∨ s = a :: t ↔ s <:+ a :: t, from + ⟨λo, match s, t, o with + | s, ._, or.inl ⟨l, rfl⟩ := ⟨a::l, rfl⟩ + | ._, t, or.inr rfl := suffix_refl _ + end, λe, match s, t, e with + | ._, t, ⟨[], rfl⟩ := or.inr rfl + | s, t, ⟨b::l, he⟩ := list.no_confusion he (λab lt, or.inl ⟨l, lt⟩) + end⟩ + +lemma sublists_aux_eq_foldl : ∀ (l : list α) {β : Type u} (f : list α → list β → list β), + sublists_aux l f = foldr f [] (sublists_aux l cons) +| [] β f := rfl +| (a::l) β f := suffices ∀ t, foldr (λ ys r, f ys (f (a :: ys) r)) [] t = + foldr f [] (foldr (λ ys r, ys :: (a :: ys) :: r) nil t), +by simp [sublists_aux]; rw [sublists_aux_eq_foldl l, sublists_aux_eq_foldl l (λ ys r, ys :: (a :: ys) :: r), this], +λt, by induction t; simp; simp [ih_1] + +lemma sublists_aux_cons_cons (l : list α) (a : α) : + sublists_aux (a::l) cons = [a] :: foldr (λys r, ys :: (a :: ys) :: r) [] (sublists_aux l cons) := +by rw -sublists_aux_eq_foldl; refl + +@[simp] lemma mem_sublists (s t : list α) : s ∈ sublists t ↔ s <+ t := +by simp [sublists]; exact +⟨λm, let good := λ (l : list (list α)), ∀ s ∈ l, s <+ t in + suffices ∀ l (f : list α → list (list α) → list (list α)), + (∀ {x y}, x <+ l → good y → good (f x y)) → l <+ t → good (sublists_aux l f), from + or.elim m (λe, by rw e; apply nil_sublist) + (this t cons (λ x y hx hy s m, by exact or.elim m (λe, by rw e; exact hx) (hy s)) (sublist.refl _) s), + begin + intro l; induction l with a l IH; intros f al sl x m, + exact false.elim m, + refine al (cons_sublist_cons a (nil_sublist _)) _ _ m, + exact λs hs, IH _ (λx y hx hy, al (sublist_cons_of_sublist _ hx) (al (cons_sublist_cons _ hx) hy)) + (sublist_of_cons_sublist sl) _ hs + end, +λsl, begin + assert this : ∀ {a : α} {y t}, y ∈ t → y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t + ∧ a :: y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t, + { intros a y t yt, induction t with x t IH, exact absurd yt (not_mem_nil _), + simp, simp at yt, cases yt with yx yt, + { rw yx, exact ⟨or.inl rfl, or.inr $ or.inl rfl⟩ }, + { cases IH yt with h1 h2, + exact ⟨or.inr $ or.inr h1, or.inr $ or.inr h2⟩ } }, + induction sl with l₁ l₂ a sl IH l₁ l₂ a sl IH, exact or.inl rfl, + { refine or.imp_right (λh, _) IH, + rw sublists_aux_cons_cons, + exact mem_cons_of_mem _ (this h).left }, + { refine or.inr _, + rw sublists_aux_cons_cons, simp, + refine or.imp (λ(h : l₁ = []), by rw h) (λh, _) IH, + exact (this h).right }, +end⟩ end list diff --git a/library/init/data/list/qsort.lean b/library/init/data/list/qsort.lean index 7e434fd7a9..c2f3a5432a 100644 --- a/library/init/data/list/qsort.lean +++ b/library/init/data/list/qsort.lean @@ -16,8 +16,7 @@ namespace list meta def qsort {α} (lt : α → α → bool) : list α → list α | [] := [] | (h::t) := - let small := filter (λ x, lt h x = ff) t, - large := filter (λ x, lt h x = tt) t + let (large, small) := partition (λ x, lt h x = tt) t in qsort small ++ h :: qsort large end list diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 8bbbe99103..aa10f21095 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -408,7 +408,7 @@ do r ← result, <|> fail ("'" ++ to_string ctor ++ "' is not a constructor"), let ctors := env.constructors_of ty, let idx := env.inductive_num_params ty + /- motive -/ 1 + - list.find ctor ctors, + list.index_of ctor ctors, gs ← get_goals, (case, g) ← (find_case gs ty idx (env.inductive_num_indices ty) none r ).to_monad <|> fail "could not find open goal of given case",