From 93283a4cf8a6dfaaba43661311b7b06d93d8f5d4 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 21 Nov 2015 00:24:08 -0500 Subject: [PATCH] feat(list): also port part of list.comb --- hott/types/list.hlean | 180 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 178 insertions(+), 2 deletions(-) diff --git a/hott/types/list.hlean b/hott/types/list.hlean index a66c62af2..e09ac7cd6 100644 --- a/hott/types/list.hlean +++ b/hott/types/list.hlean @@ -1,10 +1,11 @@ /- Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura Basic properties of lists. -Ported from the standard library +Ported from the standard library (list.basic and list.comb) +Some lemmas are commented out, their proofs need to be repaired when needed -/ import .pointed .nat .pi @@ -732,3 +733,178 @@ end list attribute list.has_decidable_eq [instance] --attribute list.decidable_mem [instance] + +namespace list + +variables {A B C : Type} +/- map -/ +definition map (f : A → B) : list A → list B +| [] := [] +| (a :: l) := f a :: map l + +theorem map_nil (f : A → B) : map f [] = [] := idp + +theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l := idp + +lemma map_append (f : A → B) : Π l₁ l₂, map f (l₁++l₂) = (map f l₁)++(map f l₂) +| nil := take l, rfl +| (a::l) := take l', begin rewrite [append_cons, *map_cons, append_cons, map_append] end + +lemma map_singleton (f : A → B) (a : A) : map f [a] = [f a] := rfl + +theorem map_id : Π l : list A, map id l = l +| [] := rfl +| (x::xs) := begin rewrite [map_cons, map_id] end + +theorem map_id' {f : A → A} (H : Πx, f x = x) : Π l : list A, map f l = l +| [] := rfl +| (x::xs) := begin rewrite [map_cons, H, 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), + by rewrite (map_map l) + +theorem length_map (f : A → B) : Π l : list A, length (map f l) = length l +| [] := by esimp +| (a :: l) := + show length (map f l) + 1 = length l + 1, + by rewrite (length_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 := sum.rec_on (eq_or_mem_of_mem_cons i) + (suppose a = x, by rewrite [this, map_cons]; apply mem_cons) + (suppose a ∈ xs, sum.inr (mem_map this)) + +theorem exists_of_mem_map {A B : Type} {f : A → B} {b : B} : + Π{l}, b ∈ map f l → Σa, a ∈ l × f a = b +| [] H := empty.elim (down H) +| (c::l) H := sum.rec_on (iff.mp !mem_cons_iff H) + (suppose b = f c, + sigma.mk c (pair !mem_cons (inverse this))) + (suppose b ∈ map f l, + obtain a (Hl : a ∈ l) (Hr : f a = b), from exists_of_mem_map this, + sigma.mk a (pair (mem_cons_of_mem _ Hl) Hr)) + +theorem eq_of_map_const {A B : Type} {b₁ b₂ : B} : Π {l : list A}, b₁ ∈ map (const A b₂) l → b₁ = b₂ +| [] h := absurd h !not_mem_nil +| (a::l) h := + sum.rec_on (eq_or_mem_of_mem_cons h) + (suppose b₁ = b₂, this) + (suppose b₁ ∈ map (const A b₂) l, eq_of_map_const this) + +definition map₂ (f : A → B → C) : list A → list B → list C +| [] _ := [] +| _ [] := [] +| (x::xs) (y::ys) := f x y :: map₂ xs ys + +/- filter -/ +definition filter (p : A → Type) [h : decidable_pred p] : list A → list A +| [] := [] +| (a::l) := if p a then a :: filter l else filter l + +theorem filter_nil (p : A → Type) [h : decidable_pred p] : filter p [] = [] := idp + +theorem filter_cons_of_pos {p : A → Type} [h : decidable_pred p] {a : A} : Π l, p a → filter p (a::l) = a :: filter p l := +λ l pa, if_pos pa + +theorem filter_cons_of_neg {p : A → Type} [h : decidable_pred p] {a : A} : Π l, ¬ p a → filter p (a::l) = filter p l := +λ l pa, if_neg pa + +/- +theorem of_mem_filter {p : A → Type} [h : decidable_pred p] {a : A} : Π {l}, a ∈ filter p l → p a +| [] ain := absurd ain !not_mem_nil +| (b::l) ain := by_cases + (assume pb : p b, + have a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain, + sum.rec_on (eq_or_mem_of_mem_cons this) + (suppose a = b, by rewrite [-this at pb]; exact pb) + (suppose a ∈ filter p l, of_mem_filter this)) + (suppose ¬ p b, by rewrite [filter_cons_of_neg _ this at ain]; exact (of_mem_filter ain)) + +theorem mem_of_mem_filter {p : A → Type} [h : decidable_pred p] {a : A} : Π {l}, a ∈ filter p l → a ∈ l +| [] ain := absurd ain !not_mem_nil +| (b::l) ain := by_cases + (λ pb : p b, + have a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain, + sum.rec_on (eq_or_mem_of_mem_cons this) + (suppose a = b, by rewrite this; exact !mem_cons) + (suppose a ∈ filter p l, mem_cons_of_mem _ (mem_of_mem_filter this))) + (suppose ¬ p b, by rewrite [filter_cons_of_neg _ this at ain]; exact (mem_cons_of_mem _ (mem_of_mem_filter ain))) + +theorem mem_filter_of_mem {p : A → Type} [h : decidable_pred p] {a : A} : Π {l}, a ∈ l → p a → a ∈ filter p l +| [] ain pa := absurd ain !not_mem_nil +| (b::l) ain pa := by_cases + (λ pb : p b, sum.rec_on (eq_or_mem_of_mem_cons ain) + (λ aeqb : a = b, by rewrite [filter_cons_of_pos _ pb, aeqb]; exact !mem_cons) + (λ ainl : a ∈ l, by rewrite [filter_cons_of_pos _ pb]; exact (mem_cons_of_mem _ (mem_filter_of_mem ainl pa)))) + (λ npb : ¬ p b, sum.rec_on (eq_or_mem_of_mem_cons ain) + (λ aeqb : a = b, absurd (eq.rec_on aeqb pa) npb) + (λ ainl : a ∈ l, by rewrite [filter_cons_of_neg _ npb]; exact (mem_filter_of_mem ainl pa))) + +theorem filter_sub {p : A → Type} [h : decidable_pred p] (l : list A) : filter p l ⊆ l := +λ a ain, mem_of_mem_filter ain + +theorem filter_append {p : A → Type} [h : decidable_pred p] : Π (l₁ l₂ : list A), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂ +| [] l₂ := rfl +| (a::l₁) l₂ := by_cases + (suppose p a, by rewrite [append_cons, *filter_cons_of_pos _ this, filter_append]) + (suppose ¬ p a, by rewrite [append_cons, *filter_cons_of_neg _ this, filter_append]) +-/ +/- foldl & foldr -/ +definition foldl (f : A → B → A) : A → list B → A +| a [] := a +| a (b :: l) := foldl (f a b) l + +theorem foldl_nil (f : A → B → A) (a : A) : foldl f a [] = a := idp + +theorem foldl_cons (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l := idp + +definition foldr (f : A → B → B) : B → list A → B +| b [] := b +| b (a :: l) := f a (foldr b l) + +theorem foldr_nil (f : A → B → B) (b : B) : foldr f b [] = b := idp + +theorem foldr_cons (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l) := idp + +section foldl_eq_foldr + -- foldl and foldr coincide when f is commutative and associative + parameters {α : Type} {f : α → α → α} + hypothesis (Hcomm : Π a b, f a b = f b a) + hypothesis (Hassoc : Π a b c, f (f a b) c = f a (f b c)) + include Hcomm Hassoc + + theorem foldl_eq_of_comm_of_assoc : Π a b l, foldl f a (b::l) = f b (foldl f a l) + | a b nil := Hcomm a b + | a b (c::l) := + begin + change foldl f (f (f a b) c) l = f b (foldl f (f a c) l), + rewrite -foldl_eq_of_comm_of_assoc, + change foldl f (f (f a b) c) l = foldl f (f (f a c) b) l, + have H₁ : f (f a b) c = f (f a c) b, by rewrite [Hassoc, Hassoc, Hcomm b c], + rewrite H₁ + end + + theorem foldl_eq_foldr : Π a l, foldl f a l = foldr f a l + | a nil := rfl + | a (b :: l) := + begin + rewrite foldl_eq_of_comm_of_assoc, + esimp, + change f b (foldl f a l) = f b (foldr f a l), + rewrite foldl_eq_foldr + end +end foldl_eq_foldr + +theorem foldl_append (f : B → A → B) : Π (b : B) (l₁ l₂ : list A), foldl f b (l₁++l₂) = foldl f (foldl f b l₁) l₂ +| b [] l₂ := rfl +| b (a::l₁) l₂ := by rewrite [append_cons, *foldl_cons, foldl_append] + +theorem foldr_append (f : A → B → B) : Π (b : B) (l₁ l₂ : list A), foldr f b (l₁++l₂) = foldr f (foldr f b l₂) l₁ +| b [] l₂ := rfl +| b (a::l₁) l₂ := by rewrite [append_cons, *foldr_cons, foldr_append] + +end list