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

refactor(library/data/list/basic.lean): make minor renaming

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-08 20:25:28 +10:00
parent 75e50fd371
commit 624b664950
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -162,11 +162,11 @@ definition mem : T → list T → Prop
notation e ∈ s := mem e s notation e ∈ s := mem e s
notation e ∉ s := ¬ e ∈ s notation e ∉ s := ¬ e ∈ s
theorem mem_nil (x : T) : x ∈ [] ↔ false := theorem mem_nil_iff (x : T) : x ∈ [] ↔ false :=
iff.rfl iff.rfl
theorem not_mem_nil (x : T) : x ∉ [] := theorem not_mem_nil (x : T) : x ∉ [] :=
iff.mp !mem_nil iff.mp !mem_nil_iff
theorem mem_cons (x : T) (l : list T) : x ∈ x :: l := theorem mem_cons (x : T) (l : list T) : x ∈ x :: l :=
or.inl rfl or.inl rfl
@ -230,7 +230,7 @@ local attribute mem [reducible]
local attribute append [reducible] local attribute append [reducible]
theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) := theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
list.induction_on l list.induction_on l
(take H : x ∈ [], false.elim (iff.elim_left !mem_nil H)) (take H : x ∈ [], false.elim (iff.elim_left !mem_nil_iff H))
(take y l, (take y l,
assume IH : x ∈ l → ∃s t : list T, l = s ++ (x::t), assume IH : x ∈ l → ∃s t : list T, l = s ++ (x::t),
assume H : x ∈ y::l, assume H : x ∈ y::l,
@ -252,7 +252,7 @@ assume ainl₂, mem_append_of_mem_or_mem (or.inr ainl₂)
definition decidable_mem [instance] [H : decidable_eq T] (x : T) (l : list T) : decidable (x ∈ l) := definition decidable_mem [instance] [H : decidable_eq T] (x : T) (l : list T) : decidable (x ∈ l) :=
list.rec_on l list.rec_on l
(decidable.inr (not_of_iff_false !mem_nil)) (decidable.inr (not_of_iff_false !mem_nil_iff))
(take (h : T) (l : list T) (iH : decidable (x ∈ l)), (take (h : T) (l : list T) (iH : decidable (x ∈ l)),
show decidable (x ∈ h::l), from show decidable (x ∈ h::l), from
decidable.rec_on iH decidable.rec_on iH
@ -289,7 +289,7 @@ definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈
infix `⊆`:50 := sublist infix `⊆`:50 := sublist
theorem nil_sub (l : list T) : [] ⊆ l := theorem nil_sub (l : list T) : [] ⊆ l :=
λ b i, false.elim (iff.mp (mem_nil b) i) λ b i, false.elim (iff.mp (mem_nil_iff b) i)
theorem sub.refl (l : list T) : l ⊆ l := theorem sub.refl (l : list T) : l ⊆ l :=
λ b i, i λ b i, i