michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/list): more general theorems for perm foldl and foldr, and other minor improvements

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-09 09:29:58 -07:00
parent 07ff0900aa
commit 8522fbec4b
2 changed files with 74 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
library/data/list/basic.lean
View file

@ -623,7 +623,6 @@ variable {A : Type}
variable [H : decidable_eq A] variable [H : decidable_eq A]
include H include H
definition erase (a : A) : list A → list A definition erase (a : A) : list A → list A
| [] := [] | [] := []
| (b::l) := | (b::l) :=
@ -644,7 +643,7 @@ assume h : a ≠ b,
show match H a b with | inl e := l | inr n₁ := b :: erase a l end = b :: erase a l, show match H a b with | inl e := l | inr n₁ := b :: erase a l end = b :: erase a l,
by rewrite (decidable_eq_inr_neg h) by rewrite (decidable_eq_inr_neg h)
lemma length_erase_of_mem (a : A) : ∀ l, a ∈ l → length (erase a l) = pred (length l) lemma length_erase_of_mem {a : A} : ∀ {l}, a ∈ l → length (erase a l) = pred (length l)
| [] h := rfl | [] h := rfl
| [x] h := by rewrite [mem_singleton h, erase_cons_head] | [x] h := by rewrite [mem_singleton h, erase_cons_head]
| (x::y::xs) h := | (x::y::xs) h :=
@ -652,14 +651,14 @@ lemma length_erase_of_mem (a : A) : ∀ l, a ∈ l → length (erase a l) = pred
(λ aeqx : a = x, by rewrite [aeqx, erase_cons_head]) (λ aeqx : a = x, by rewrite [aeqx, erase_cons_head])
(λ anex : a ≠ x, (λ anex : a ≠ x,
assert ainyxs : a ∈ y::xs, from or_resolve_right h anex, assert ainyxs : a ∈ y::xs, from or_resolve_right h anex,
by rewrite [erase_cons_tail _ anex, *length_cons, length_erase_of_mem (y::xs) ainyxs]) by rewrite [erase_cons_tail _ anex, *length_cons, length_erase_of_mem ainyxs])
lemma length_erase_of_not_mem (a : A) : ∀ l, a ∉ l → length (erase a l) = length l lemma length_erase_of_not_mem {a : A} : ∀ {l}, a ∉ l → length (erase a l) = length l
| [] h := rfl | [] h := rfl
| (x::xs) h := | (x::xs) h :=
assert anex : a ≠ x, from λ aeqx : a = x, absurd (or.inl aeqx) h, assert anex : a ≠ x, from λ aeqx : a = x, absurd (or.inl aeqx) h,
assert aninxs : a ∉ xs, from λ ainxs : a ∈ xs, absurd (or.inr ainxs) h, assert aninxs : a ∉ xs, from λ ainxs : a ∈ xs, absurd (or.inr ainxs) h,
by rewrite [erase_cons_tail _ anex, length_cons, length_erase_of_not_mem xs aninxs] by rewrite [erase_cons_tail _ anex, length_cons, length_erase_of_not_mem aninxs]
lemma erase_append_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → erase a (l₁++l₂) = erase a l₁ ++ l₂ lemma erase_append_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → erase a (l₁++l₂) = erase a l₁ ++ l₂
| [] l₂ h := absurd h !not_mem_nil | [] l₂ h := absurd h !not_mem_nil
@ -772,19 +771,19 @@ section nodup
open nodup open nodup
variables {A B : Type} variables {A B : Type}
lemma nodup_nil : @nodup A [] := theorem nodup_nil : @nodup A [] :=
ndnil ndnil
lemma nodup_cons {a : A} {l : list A} : a ∉ l → nodup l → nodup (a::l) := theorem nodup_cons {a : A} {l : list A} : a ∉ l → nodup l → nodup (a::l) :=
λ i n, ndcons i n λ i n, ndcons i n
lemma nodup_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → nodup l theorem nodup_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → nodup l
| a xs (ndcons i n) := n | a xs (ndcons i n) := n
lemma not_mem_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → a ∉ l theorem not_mem_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → a ∉ l
| a xs (ndcons i n) := i | a xs (ndcons i n) := i
lemma nodup_of_nodup_append_left : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₁ theorem nodup_of_nodup_append_left : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₁
| [] l₂ n := nodup_nil | [] l₂ n := nodup_nil
| (x::xs) l₂ n := | (x::xs) l₂ n :=
have ndxs : nodup xs, from nodup_of_nodup_append_left (nodup_of_nodup_cons n), have ndxs : nodup xs, from nodup_of_nodup_append_left (nodup_of_nodup_cons n),
@ -792,11 +791,11 @@ lemma nodup_of_nodup_append_left : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂)
have nxinxs : x ∉ xs, from not_mem_of_not_mem_append_left nxinxsl₂, have nxinxs : x ∉ xs, from not_mem_of_not_mem_append_left nxinxsl₂,
nodup_cons nxinxs ndxs nodup_cons nxinxs ndxs
lemma nodup_of_nodup_append_right : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₂ theorem nodup_of_nodup_append_right : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₂
| [] l₂ n := n | [] l₂ n := n
| (x::xs) l₂ n := nodup_of_nodup_append_right (nodup_of_nodup_cons 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) theorem 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 | [] n := begin rewrite [map_nil], apply nodup_nil end
| (x::xs) n := | (x::xs) n :=
assert nxinxs : x ∉ xs, from not_mem_of_nodup_cons n, assert nxinxs : x ∉ xs, from not_mem_of_nodup_cons n,
@ -815,6 +814,33 @@ lemma nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l
absurd xinxs nxinxs, absurd xinxs nxinxs,
nodup_cons nfxinm ndmfxs nodup_cons nfxinm ndmfxs
theorem nodup_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → nodup (erase a l)
| [] n := nodup_nil
| (b::l) n := by_cases
(λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact (nodup_of_nodup_cons n))
(λ aneb : a ≠ b,
have nbinl : b ∉ l, from not_mem_of_nodup_cons n,
have ndl : nodup l, from nodup_of_nodup_cons n,
have ndeal : nodup (erase a l), from nodup_erase_of_nodup ndl,
have nbineal : b ∉ erase a l, from λ i, absurd (erase_sub _ _ i) nbinl,
assert aux : nodup (b :: erase a l), from nodup_cons nbineal ndeal,
by rewrite [erase_cons_tail _ aneb]; exact aux)
theorem mem_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → a ∉ erase a l
| [] n := !not_mem_nil
| (b::l) n :=
have ndl : nodup l, from nodup_of_nodup_cons n,
have naineal : a ∉ erase a l, from mem_erase_of_nodup ndl,
assert nbinl : b ∉ l, from not_mem_of_nodup_cons n,
by_cases
(λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact nbinl)
(λ aneb : a ≠ b,
assert aux : a ∉ b :: erase a l, from
assume ainbeal : a ∈ b :: erase a l, or.elim ainbeal
(λ aeqb : a = b, absurd aeqb aneb)
(λ aineal : a ∈ erase a l, absurd aineal naineal),
by rewrite [erase_cons_tail _ aneb]; exact aux)
definition erase_dup [H : decidable_eq A] : list A → list A definition erase_dup [H : decidable_eq A] : list A → list A
| [] := [] | [] := []
| (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs | (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs
@ -952,24 +978,29 @@ if a ∈ l then l else a::l
theorem insert_eq_of_mem {a : A} {l : list A} : a ∈ l → insert a l = l := theorem insert_eq_of_mem {a : A} {l : list A} : a ∈ l → insert a l = l :=
assume ainl, if_pos ainl assume ainl, if_pos ainl
theorem insert_eq_of_non_mem {a : A} {l : list A} : a ∉ l → insert a l = a::l := theorem insert_eq_of_not_mem {a : A} {l : list A} : a ∉ l → insert a l = a::l :=
assume nainl, if_neg nainl assume nainl, if_neg nainl
theorem mem_insert (a : A) (l : list A) : a ∈ insert a l := theorem mem_insert (a : A) (l : list A) : a ∈ insert a l :=
by_cases by_cases
(λ ainl : a ∈ l, by rewrite [insert_eq_of_mem ainl]; exact ainl) (λ ainl : a ∈ l, by rewrite [insert_eq_of_mem ainl]; exact ainl)
(λ nainl : a ∉ l, by rewrite [insert_eq_of_non_mem nainl]; exact !mem_cons) (λ nainl : a ∉ l, by rewrite [insert_eq_of_not_mem nainl]; exact !mem_cons)
theorem mem_insert_of_mem {a : A} (b : A) {l : list A} : a ∈ l → a ∈ insert b l := theorem mem_insert_of_mem {a : A} (b : A) {l : list A} : a ∈ l → a ∈ insert b l :=
assume ainl, by_cases assume ainl, by_cases
(λ binl : b ∈ l, by rewrite [insert_eq_of_mem binl]; exact ainl) (λ binl : b ∈ l, by rewrite [insert_eq_of_mem binl]; exact ainl)
(λ nbinl : b ∉ l, by rewrite [insert_eq_of_non_mem nbinl]; exact (mem_cons_of_mem _ ainl)) (λ nbinl : b ∉ l, by rewrite [insert_eq_of_not_mem nbinl]; exact (mem_cons_of_mem _ ainl))
theorem nodup_insert (a : A) {l : list A} : nodup l → nodup (insert a l) := theorem nodup_insert (a : A) {l : list A} : nodup l → nodup (insert a l) :=
assume n, by_cases assume n, by_cases
(λ ainl : a ∈ l, by rewrite [insert_eq_of_mem ainl]; exact n) (λ ainl : a ∈ l, by rewrite [insert_eq_of_mem ainl]; exact n)
(λ nainl : a ∉ l, by rewrite [insert_eq_of_non_mem nainl]; exact (nodup_cons nainl n)) (λ nainl : a ∉ l, by rewrite [insert_eq_of_not_mem nainl]; exact (nodup_cons nainl n))
theorem length_insert_of_mem {a : A} {l : list A} : a ∈ l → length (insert a l) = length l :=
assume ainl, by rewrite [insert_eq_of_mem ainl]
theorem length_insert_of_not_mem {a : A} {l : list A} : a ∉ l → length (insert a l) = length l + 1 :=
assume nainl, by rewrite [insert_eq_of_not_mem nainl]
end insert end insert
end list end list

40
library/data/list/perm.lean
View file

@ -237,7 +237,7 @@ definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁
(assume xinl₂ : x ∈ l₂, (assume xinl₂ : x ∈ l₂,
let t₂ : list A := erase x l₂ in let t₂ : list A := erase x l₂ in
have len_t₁ : length t₁ = n, from nat.no_confusion H₁ (λ e, e), have len_t₁ : length t₁ = n, from nat.no_confusion H₁ (λ e, e),
assert len_t₂_aux : length t₂ = pred (length l₂), from length_erase_of_mem x l₂ xinl₂, assert len_t₂_aux : length t₂ = pred (length l₂), from length_erase_of_mem xinl₂,
assert len_t₂ : length t₂ = n, by rewrite [len_t₂_aux, H₂], assert len_t₂ : length t₂ = n, by rewrite [len_t₂_aux, H₂],
match decidable_perm_aux n t₁ t₂ len_t₁ len_t₂ with match decidable_perm_aux n t₁ t₂ len_t₁ len_t₂ with
| inl p := inl (calc | inl p := inl (calc
@ -465,10 +465,10 @@ assume p : l₁++(a::l₂) ~ l₃++(a::l₄),
... ~ a::(l₃++l₄) : symm (!perm_middle), ... ~ a::(l₃++l₄) : symm (!perm_middle),
perm_cons_inv p' perm_cons_inv p'
section fold_thms section foldl
variables {f : A → A → A} {l₁ l₂ : list A} (fcomm : commutative f) (fassoc : associative f) variables {f : B → A → B} {l₁ l₂ : list A}
include fcomm variable rcomm : ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
include fassoc include rcomm
theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ a, foldl f a l₁ = foldl f a l₂ := theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ a, foldl f a l₁ = foldl f a l₂ :=
assume p, perm_induction_on p assume p, perm_induction_on p
@ -479,17 +479,31 @@ section fold_thms
... = foldl f a (x::t₂) : foldl_cons) ... = foldl f a (x::t₂) : foldl_cons)
(λ x y t₁ t₂ p r a, calc (λ x y t₁ t₂ p r a, calc
foldl f a (y :: x :: t₁) = foldl f (f (f a y) x) t₁ : by rewrite foldl_cons foldl f a (y :: x :: t₁) = foldl f (f (f a y) x) t₁ : by rewrite foldl_cons
... = foldl f (f (f a x) y) t₁ : by rewrite [right_comm fcomm fassoc] ... = foldl f (f (f a x) y) t₁ : by rewrite rcomm
... = foldl f (f (f a x) y) t₂ : r (f (f a x) y) ... = foldl f (f (f a x) y) t₂ : r (f (f a x) y)
... = foldl f a (x :: y :: t₂) : by rewrite foldl_cons) ... = foldl f a (x :: y :: t₂) : by rewrite foldl_cons)
(λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a)) (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
end foldl
theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ a, foldr f a l₁ = foldr f a l₂ := section foldr
assume p, take a, calc variables {f : A → B → B} {l₁ l₂ : list A}
foldr f a l₁ = foldl f a l₁ : by rewrite [foldl_eq_foldr fcomm fassoc] variable lcomm : ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
... = foldl f a l₂ : foldl_eq_of_perm fcomm fassoc p include lcomm
... = foldr f a l₂ : by rewrite [foldl_eq_foldr fcomm fassoc]
end fold_thms theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ b, foldr f b l₁ = foldr f b l₂ :=
assume p, perm_induction_on p
(λ b, by rewrite *foldl_nil)
(λ x t₁ t₂ p r b, calc
foldr f b (x::t₁) = f x (foldr f b t₁) : foldr_cons
... = f x (foldr f b t₂) : by rewrite [r b]
... = foldr f b (x::t₂) : foldr_cons)
(λ x y t₁ t₂ p r b, calc
foldr f b (y :: x :: t₁) = f y (f x (foldr f b t₁)) : by rewrite foldr_cons
... = f x (f y (foldr f b t₁)) : by rewrite lcomm
... = f x (f y (foldr f b t₂)) : by rewrite [r b]
... = foldr f b (x :: y :: t₂) : by rewrite foldr_cons)
(λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
end foldr
theorem perm_erase_dup_of_perm [H : decidable_eq A] {l₁ l₂ : list A} : l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ := theorem perm_erase_dup_of_perm [H : decidable_eq A] {l₁ l₂ : list A} : l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
assume p, perm_induction_on p assume p, perm_induction_on p
@ -618,6 +632,6 @@ assume p, by_cases
by rewrite [insert_eq_of_mem ainl₁, insert_eq_of_mem ainl₂]; exact p) by rewrite [insert_eq_of_mem ainl₁, insert_eq_of_mem ainl₂]; exact p)
(λ nainl₁ : a ∉ l₁, (λ nainl₁ : a ∉ l₁,
assert nainl₂ : a ∉ l₂, from not_mem_perm p nainl₁, assert nainl₂ : a ∉ l₂, from not_mem_perm p nainl₁,
by rewrite [insert_eq_of_non_mem nainl₁, insert_eq_of_non_mem nainl₂]; exact (skip _ p)) by rewrite [insert_eq_of_not_mem nainl₁, insert_eq_of_not_mem nainl₂]; exact (skip _ p))
end perm_insert end perm_insert
end perm end perm