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

feat(library/data/list/set): add decidable_nodup

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-11 09:39:26 -07:00
parent dff05557a3
commit 1b34f40f36
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/data/list/set.lean
View file

@ -219,6 +219,12 @@ theorem nodup_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → nodup l
theorem not_mem_of_nodup_cons : ∀ {a : A} {l : list A}, nodup (a::l) → a ∉ l
| a xs (ndcons i n) := i
theorem not_nodup_cons_of_mem {a : A} {l : list A} : a ∈ l → ¬ nodup (a :: l) :=
λ ainl d, absurd ainl (not_mem_of_nodup_cons d)
theorem not_nodup_cons_of_not_nodup {a : A} {l : list A} : ¬ nodup l → ¬ nodup (a :: l) :=
λ nd d, absurd (nodup_of_nodup_cons d) nd
theorem nodup_of_nodup_append_left : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → nodup l₁
| [] l₂ n := nodup_nil
| (x::xs) l₂ n :=
@ -388,6 +394,18 @@ theorem erase_dup_eq_of_nodup [H : decidable_eq A] : ∀ {l : list A}, nodup l
assert nainl : a ∉ l, from not_mem_of_nodup_cons d,
assert dl : nodup l, from nodup_of_nodup_cons d,
by rewrite [erase_dup_cons_of_not_mem nainl, erase_dup_eq_of_nodup dl]
definition decidable_nodup [instance] [h : decidable_eq A] : ∀ (l : list A), decidable (nodup l)
| [] := inl nodup_nil
| (a::l) :=
match decidable_mem a l with
| inl p := inr (not_nodup_cons_of_mem p)
| inr n :=
match decidable_nodup l with
| inl nd := inl (nodup_cons n nd)
| inr d := inr (not_nodup_cons_of_not_nodup d)
end
end
end nodup
/- upto -/