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

refactor(library/data/list) fix theorem name, and do not rely on implementation of mem

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-09 16:27:48 -07:00
parent 4416d9b2c5
commit b209f442f7
2 changed files with 43 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -174,22 +174,22 @@ iff.mp !mem_nil
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
theorem mem_singleton {x a : T} : x ∈ [a] → x = a :=
assume h : x ∈ [a], or.elim h
(λ xeqa : x = a, xeqa)
(λ xinn : x ∈ [], absurd xinn !not_mem_nil)
theorem mem_cons_of_mem (y : T) {x : T} {l : list T} : x ∈ l → x ∈ y :: l := theorem mem_cons_of_mem (y : T) {x : T} {l : list T} : x ∈ l → x ∈ y :: l :=
assume H, or.inr H assume H, or.inr H
theorem mem_cons_iff (x y : T) (l : list T) : x ∈ y::l ↔ (x = y ∨ x ∈ l) := theorem mem_cons_iff (x y : T) (l : list T) : x ∈ y::l ↔ (x = y ∨ x ∈ l) :=
iff.rfl iff.rfl
theorem mem_or_mem_of_mem_cons {x y : T} {l : list T} : x ∈ y::l → x = y ∨ x ∈ l := theorem eq_or_mem_of_mem_cons {x y : T} {l : list T} : x ∈ y::l → x = y ∨ x ∈ l :=
assume h, h assume h, h
theorem mem_singleton {x a : T} : x ∈ [a] → x = a :=
assume h : x ∈ [a], or.elim (eq_or_mem_of_mem_cons h)
(λ xeqa : x = a, xeqa)
(λ xinn : x ∈ [], absurd xinn !not_mem_nil)
theorem mem_of_mem_cons_of_mem {a b : T} {l : list T} : a ∈ b::l → b ∈ l → a ∈ l := theorem mem_of_mem_cons_of_mem {a b : T} {l : list T} : a ∈ b::l → b ∈ l → a ∈ l :=
assume ainbl binl, or.elim (mem_or_mem_of_mem_cons ainbl) assume ainbl binl, or.elim (eq_or_mem_of_mem_cons ainbl)
(λ aeqb : a = b, by rewrite [aeqb]; exact binl) (λ aeqb : a = b, by rewrite [aeqb]; exact binl)
(λ ainl : a ∈ l, ainl) (λ ainl : a ∈ l, ainl)
@ -210,7 +210,7 @@ list.induction_on s
assume H : x ∈ y::s ∨ x ∈ t, assume H : x ∈ y::s ∨ x ∈ t,
or.elim H or.elim H
(assume H1, (assume H1,
or.elim H1 or.elim (eq_or_mem_of_mem_cons H1)
(take H2 : x = y, or.inl H2) (take H2 : x = y, or.inl H2)
(take H2 : x ∈ s, or.inr (IH (or.inl H2)))) (take H2 : x ∈ s, or.inr (IH (or.inl H2))))
(assume H1 : x ∈ t, or.inr (IH (or.inr H1)))) (assume H1 : x ∈ t, or.inr (IH (or.inr H1))))
@ -237,7 +237,7 @@ list.induction_on l
(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,
or.elim H or.elim (eq_or_mem_of_mem_cons H)
(assume H1 : x = y, (assume H1 : x = y,
exists.intro [] (!exists.intro (H1 ▸ rfl))) exists.intro [] (!exists.intro (H1 ▸ rfl)))
(assume H1 : x ∈ l, (assume H1 : x ∈ l,
@ -279,7 +279,7 @@ list.rec_on l
decidable.inr H2))) decidable.inr H2)))
theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l := theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l :=
or.elim H₂ (λe, absurd e H₁) (λr, r) or.elim (eq_or_mem_of_mem_cons H₂) (λe, absurd e H₁) (λr, r)
theorem not_eq_of_not_mem {a b : T} {l : list T} : a ∉ b::l → a ≠ b := theorem not_eq_of_not_mem {a b : T} {l : list T} : a ∉ b::l → a ≠ b :=
assume nin aeqb, absurd (or.inl aeqb) nin assume nin aeqb, absurd (or.inl aeqb) nin
@ -304,7 +304,7 @@ lemma sub_cons (a : T) (l : list T) : l ⊆ a::l :=
λ b i, or.inr i λ b i, or.inr i
lemma cons_sub_cons {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l₁) ⊆ (a::l₂) := lemma cons_sub_cons {l₁ l₂ : list T} (a : T) (s : l₁ ⊆ l₂) : (a::l₁) ⊆ (a::l₂) :=
λ b Hin, or.elim Hin λ b Hin, or.elim (eq_or_mem_of_mem_cons Hin)
(λ e : b = a, or.inl e) (λ e : b = a, or.inl e)
(λ i : b ∈ l₁, or.inr (s i)) (λ i : b ∈ l₁, or.inr (s i))
@ -328,7 +328,7 @@ lemma sub_app_of_sub_right (l l₁ l₂ : list T) : l ⊆ l₂ → l ⊆ l₁++l
mem_append_of_mem_or_mem (or.inr xinl₁) mem_append_of_mem_or_mem (or.inr xinl₁)
lemma cons_sub_of_sub_of_mem {a : T} {l m : list T} : a ∈ m → l ⊆ m → a::l ⊆ m := lemma cons_sub_of_sub_of_mem {a : T} {l m : list T} : a ∈ m → l ⊆ m → a::l ⊆ m :=
λ (ainm : a ∈ m) (lsubm : l ⊆ m) (x : T) (xinal : x ∈ a::l), or.elim xinal λ (ainm : a ∈ m) (lsubm : l ⊆ m) (x : T) (xinal : x ∈ a::l), or.elim (eq_or_mem_of_mem_cons xinal)
(assume xeqa : x = a, eq.rec_on (eq.symm xeqa) ainm) (assume xeqa : x = a, eq.rec_on (eq.symm xeqa) ainm)
(assume xinl : x ∈ l, lsubm xinl) (assume xinl : x ∈ l, lsubm xinl)
@ -422,7 +422,7 @@ theorem len_map (f : A → B) : ∀ l : list A, length (map f l) = length l
theorem mem_map {A B : Type} (f : A → B) : ∀ {a l}, a ∈ l → f a ∈ map f 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 [] i := absurd i !not_mem_nil
| a (x::xs) i := or.elim i | a (x::xs) i := or.elim (eq_or_mem_of_mem_cons i)
(λ aeqx : a = x, by rewrite [aeqx, map_cons]; apply mem_cons) (λ aeqx : a = x, by rewrite [aeqx, map_cons]; apply mem_cons)
(λ ainxs : a ∈ xs, or.inr (mem_map ainxs)) (λ ainxs : a ∈ xs, or.inr (mem_map ainxs))
@ -568,16 +568,16 @@ take q, qeq.induction_on q
lemma mem_tail_of_qeq {a : A} {l₁ l₂ : list A} : l₁≈a|l₂ → ∀ x, x ∈ l₂ → x ∈ l₁ := lemma mem_tail_of_qeq {a : A} {l₁ l₂ : list A} : l₁≈a|l₂ → ∀ x, x ∈ l₂ → x ∈ l₁ :=
take q, qeq.induction_on q take q, qeq.induction_on q
(λ l x i, or.inr i) (λ l x i, or.inr i)
(λ b l l' q r x xinbl, or.elim xinbl (λ b l l' q r x xinbl, or.elim (eq_or_mem_of_mem_cons xinbl)
(λ xeqb : x = b, xeqb ▸ mem_cons x l') (λ xeqb : x = b, xeqb ▸ mem_cons x l')
(λ xinl : x ∈ l, or.inr (r x xinl))) (λ xinl : x ∈ l, or.inr (r x xinl)))
lemma mem_cons_of_qeq {a : A} {l₁ l₂ : list A} : l₁≈a|l₂ → ∀ x, x ∈ l₁ → x ∈ a::l₂ := lemma mem_cons_of_qeq {a : A} {l₁ l₂ : list A} : l₁≈a|l₂ → ∀ x, x ∈ l₁ → x ∈ a::l₂ :=
take q, qeq.induction_on q take q, qeq.induction_on q
(λ l x i, i) (λ l x i, i)
(λ b l l' q r x xinbl', or.elim xinbl' (λ b l l' q r x xinbl', or.elim (eq_or_mem_of_mem_cons xinbl')
(λ xeqb : x = b, xeqb ▸ or.inr (mem_cons x l)) (λ xeqb : x = b, xeqb ▸ or.inr (mem_cons x l))
(λ xinl' : x ∈ l', or.elim (r x xinl') (λ xinl' : x ∈ l', or.elim (eq_or_mem_of_mem_cons (r x xinl'))
(λ xeqa : x = a, xeqa ▸ mem_cons x (b::l)) (λ xeqa : x = a, xeqa ▸ mem_cons x (b::l))
(λ xinl : x ∈ l, or.inr (or.inr xinl)))) (λ xinl : x ∈ l, or.inr (or.inr xinl))))
@ -589,7 +589,7 @@ take q, qeq.induction_on q
lemma qeq_of_mem {a : A} {l : list A} : a ∈ l → (∃l', l≈a|l') := lemma qeq_of_mem {a : A} {l : list A} : a ∈ l → (∃l', l≈a|l') :=
list.induction_on l list.induction_on l
(λ h : a ∈ nil, absurd h (not_mem_nil a)) (λ h : a ∈ nil, absurd h (not_mem_nil a))
(λ x xs r ainxxs, or.elim ainxxs (λ x xs r ainxxs, or.elim (eq_or_mem_of_mem_cons ainxxs)
(λ aeqx : a = x, (λ aeqx : a = x,
assert aux : ∃ l, x::xs≈x|l, from assert aux : ∃ l, x::xs≈x|l, from
exists.intro xs (qhead x xs), exists.intro xs (qhead x xs),
@ -618,7 +618,7 @@ lemma sub_of_mem_of_sub_of_qeq {a : A} {l : list A} {u v : list A} : a ∉ l →
λ (nainl : a ∉ l) (s : a::l ⊆ v) (q : v≈a|u) (x : A) (xinl : x ∈ l), λ (nainl : a ∉ l) (s : a::l ⊆ v) (q : v≈a|u) (x : A) (xinl : x ∈ l),
have xinv : x ∈ v, from s (or.inr xinl), have xinv : x ∈ v, from s (or.inr xinl),
have xinau : x ∈ a::u, from mem_cons_of_qeq q x xinv, have xinau : x ∈ a::u, from mem_cons_of_qeq q x xinv,
or.elim xinau or.elim (eq_or_mem_of_mem_cons xinau)
(λ xeqa : x = a, absurd (xeqa ▸ xinl) nainl) (λ xeqa : x = a, absurd (xeqa ▸ xinl) nainl)
(λ xinu : x ∈ u, xinu) (λ xinu : x ∈ u, xinu)
end qeq end qeq
@ -702,7 +702,7 @@ theorem mem_erase_of_ne_of_mem {a b : A} : ∀ {l : list A}, a ≠ b → a ∈ l
| [] n i := absurd i !not_mem_nil | [] n i := absurd i !not_mem_nil
| (c::l) n i := by_cases | (c::l) n i := by_cases
(λ beqc : b = c, (λ beqc : b = c,
assert ainl : a ∈ l, from or.elim (mem_or_mem_of_mem_cons i) assert ainl : a ∈ l, from or.elim (eq_or_mem_of_mem_cons i)
(λ aeqc : a = c, absurd aeqc (beqc ▸ n)) (λ aeqc : a = c, absurd aeqc (beqc ▸ n))
(λ ainl : a ∈ l, ainl), (λ ainl : a ∈ l, ainl),
by rewrite [beqc, erase_cons_head]; exact ainl) by rewrite [beqc, erase_cons_head]; exact ainl)
@ -722,7 +722,7 @@ theorem mem_of_mem_erase {a b : A} : ∀ {l}, a ∈ erase b l → a ∈ l
(λ beqc : b = c, by rewrite [beqc at i, erase_cons_head at i]; exact (mem_cons_of_mem _ i)) (λ beqc : b = c, by rewrite [beqc at i, erase_cons_head at i]; exact (mem_cons_of_mem _ i))
(λ bnec : b ≠ c, (λ bnec : b ≠ c,
have i₁ : a ∈ c :: erase b l, by rewrite [erase_cons_tail _ bnec at i]; exact i, have i₁ : a ∈ c :: erase b l, by rewrite [erase_cons_tail _ bnec at i]; exact i,
or.elim (mem_or_mem_of_mem_cons i₁) or.elim (eq_or_mem_of_mem_cons i₁)
(λ aeqc : a = c, by rewrite [aeqc]; exact !mem_cons) (λ aeqc : a = c, by rewrite [aeqc]; exact !mem_cons)
(λ ainel : a ∈ erase b l, (λ ainel : a ∈ erase b l,
have ainl : a ∈ l, from mem_of_mem_erase ainel, have ainl : a ∈ l, from mem_of_mem_erase ainel,
@ -766,10 +766,10 @@ disjoint.comm (disjoint_nil_left l)
lemma disjoint_cons_of_not_mem_of_disjoint {a : A} {l₁ l₂} : a ∉ l₂ → disjoint l₁ l₂ → disjoint (a::l₁) l₂ := lemma disjoint_cons_of_not_mem_of_disjoint {a : A} {l₁ l₂} : a ∉ l₂ → disjoint l₁ l₂ → disjoint (a::l₁) l₂ :=
λ nainl₂ d x, and.intro λ nainl₂ d x, and.intro
(λ xinal₁ : x ∈ a::l₁, or.elim xinal₁ (λ xinal₁ : x ∈ a::l₁, or.elim (eq_or_mem_of_mem_cons xinal₁)
(λ xeqa : x = a, xeqa⁻¹ ▸ nainl₂) (λ xeqa : x = a, xeqa⁻¹ ▸ nainl₂)
(λ xinl₁ : x ∈ l₁, disjoint_left d xinl₁)) (λ xinl₁ : x ∈ l₁, disjoint_left d xinl₁))
(λ (xinl₂ : x ∈ l₂) (xinal₁ : x ∈ a::l₁), or.elim xinal₁ (λ (xinl₂ : x ∈ l₂) (xinal₁ : x ∈ a::l₁), or.elim (eq_or_mem_of_mem_cons xinal₁)
(λ xeqa : x = a, absurd (xeqa ▸ xinl₂) nainl₂) (λ xeqa : x = a, absurd (xeqa ▸ xinl₂) nainl₂)
(λ xinl₁ : x ∈ l₁, absurd xinl₁ (disjoint_right d xinl₂))) (λ xinl₁ : x ∈ l₁, absurd xinl₁ (disjoint_right d xinl₂)))
@ -839,13 +839,13 @@ theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂)
have dsj : disjoint xs l₂, from disjoint_of_nodup_append d₂, have dsj : disjoint xs l₂, from disjoint_of_nodup_append d₂,
(λ a, and.intro (λ a, and.intro
(λ ainxxs : a ∈ x::xs, (λ ainxxs : a ∈ x::xs,
or.elim (mem_or_mem_of_mem_cons ainxxs) or.elim (eq_or_mem_of_mem_cons ainxxs)
(λ aeqx : a = x, aeqx⁻¹ ▸ nxinl₂) (λ aeqx : a = x, aeqx⁻¹ ▸ nxinl₂)
(λ ainxs : a ∈ xs, disjoint_left dsj ainxs)) (λ ainxs : a ∈ xs, disjoint_left dsj ainxs))
(λ ainl₂ : a ∈ l₂, (λ ainl₂ : a ∈ l₂,
have nainxs : a ∉ xs, from disjoint_right dsj ainl₂, have nainxs : a ∉ xs, from disjoint_right dsj ainl₂,
assume ain : a ∈ x::xs, or.elim (mem_or_mem_of_mem_cons ain) assume ain : a ∈ x::xs, or.elim (eq_or_mem_of_mem_cons ain)
(λ aeqx : a = x, absurd ainl₂ (aeqx⁻¹ ▸ nxinl₂)) (λ aeqx : a = x, absurd (aeqx ▸ ainl₂) nxinl₂)
(λ ainxs : a ∈ xs, absurd ainxs nainxs))) (λ ainxs : a ∈ xs, absurd ainxs nainxs)))
theorem nodup_append_of_nodup_of_nodup_of_disjoint : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → disjoint l₁ l₂ → nodup (l₁++l₂) theorem nodup_append_of_nodup_of_nodup_of_disjoint : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → disjoint l₁ l₂ → nodup (l₁++l₂)
@ -927,7 +927,7 @@ theorem mem_erase_of_nodup [h : decidable_eq A] (a : A) : ∀ {l}, nodup l → a
(λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact nbinl) (λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact nbinl)
(λ aneb : a ≠ b, (λ aneb : a ≠ b,
assert aux : a ∉ b :: erase a l, from assert aux : a ∉ b :: erase a l, from
assume ainbeal : a ∈ b :: erase a l, or.elim ainbeal assume ainbeal : a ∈ b :: erase a l, or.elim (eq_or_mem_of_mem_cons ainbeal)
(λ aeqb : a = b, absurd aeqb aneb) (λ aeqb : a = b, absurd aeqb aneb)
(λ aineal : a ∈ erase a l, absurd aineal naineal), (λ aineal : a ∈ erase a l, absurd aineal naineal),
by rewrite [erase_cons_tail _ aneb]; exact aux) by rewrite [erase_cons_tail _ aneb]; exact aux)
@ -951,10 +951,10 @@ assume nainl, calc
theorem mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ erase_dup l theorem mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ l → a ∈ erase_dup l
| [] h := absurd h !not_mem_nil | [] h := absurd h !not_mem_nil
| (b::l) h := by_cases | (b::l) h := by_cases
(λ binl : b ∈ l, or.elim h (λ binl : b ∈ l, or.elim (eq_or_mem_of_mem_cons h)
(λ aeqb : a = b, by rewrite [erase_dup_cons_of_mem binl, -aeqb at binl]; exact (mem_erase_dup binl)) (λ aeqb : a = b, by rewrite [erase_dup_cons_of_mem binl, -aeqb at binl]; exact (mem_erase_dup binl))
(λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem binl]; exact (mem_erase_dup ainl))) (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem binl]; exact (mem_erase_dup ainl)))
(λ nbinl : b ∉ l, or.elim h (λ nbinl : b ∉ l, or.elim (eq_or_mem_of_mem_cons h)
(λ aeqb : a = b, by rewrite [erase_dup_cons_of_not_mem nbinl, aeqb]; exact !mem_cons) (λ aeqb : a = b, by rewrite [erase_dup_cons_of_not_mem nbinl, aeqb]; exact !mem_cons)
(λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_not_mem nbinl]; exact (or.inr (mem_erase_dup ainl)))) (λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_not_mem nbinl]; exact (or.inr (mem_erase_dup ainl))))
@ -966,7 +966,7 @@ theorem mem_of_mem_erase_dup [H : decidable_eq A] {a : A} : ∀ {l}, a ∈ erase
or.inr (mem_of_mem_erase_dup h₁)) or.inr (mem_of_mem_erase_dup h₁))
(λ nbinl : b ∉ l, (λ nbinl : b ∉ l,
have h₁ : a ∈ b :: erase_dup l, by rewrite [erase_dup_cons_of_not_mem nbinl at h]; exact h, have h₁ : a ∈ b :: erase_dup l, by rewrite [erase_dup_cons_of_not_mem nbinl at h]; exact h,
or.elim h₁ or.elim (eq_or_mem_of_mem_cons h₁)
(λ aeqb : a = b, by rewrite aeqb; exact !mem_cons) (λ aeqb : a = b, by rewrite aeqb; exact !mem_cons)
(λ ainel : a ∈ erase_dup l, or.inr (mem_of_mem_erase_dup ainel))) (λ ainel : a ∈ erase_dup l, or.inr (mem_of_mem_erase_dup ainel)))
@ -1020,7 +1020,7 @@ theorem mem_or_mem_of_mem_union : ∀ {l₁ l₂} {a : A}, a ∈ union l₁ l₂
(λ ainl₂, or.inr ainl₂)) (λ ainl₂, or.inr ainl₂))
(λ nbinl₂ : b ∉ l₂, (λ nbinl₂ : b ∉ l₂,
have ainb_l₁l₂ : a ∈ b :: union l₁ l₂, by rewrite [union_cons_of_not_mem l₁ nbinl₂ at ainbl₁l₂]; exact ainbl₁l₂, have ainb_l₁l₂ : a ∈ b :: union l₁ l₂, by rewrite [union_cons_of_not_mem l₁ nbinl₂ at ainbl₁l₂]; exact ainbl₁l₂,
or.elim (mem_or_mem_of_mem_cons ainb_l₁l₂) or.elim (eq_or_mem_of_mem_cons ainb_l₁l₂)
(λ aeqb, by rewrite aeqb; exact (or.inl !mem_cons)) (λ aeqb, by rewrite aeqb; exact (or.inl !mem_cons))
(λ ainl₁l₂, (λ ainl₁l₂,
or.elim (mem_or_mem_of_mem_union ainl₁l₂) or.elim (mem_or_mem_of_mem_union ainl₁l₂)
@ -1036,12 +1036,12 @@ theorem mem_union_right {a : A} : ∀ (l₁) {l₂}, a ∈ l₂ → a ∈ union
theorem mem_union_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → a ∈ union l₁ l₂ theorem mem_union_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → a ∈ union l₁ l₂
| [] l₂ h := absurd h !not_mem_nil | [] l₂ h := absurd h !not_mem_nil
| (b::l₁) l₂ h := by_cases | (b::l₁) l₂ h := by_cases
(λ binl₂ : b ∈ l₂, or.elim h (λ binl₂ : b ∈ l₂, or.elim (eq_or_mem_of_mem_cons h)
(λ aeqb : a = b, (λ aeqb : a = b,
by rewrite [union_cons_of_mem l₁ binl₂, -aeqb at binl₂]; exact (mem_union_right _ binl₂)) by rewrite [union_cons_of_mem l₁ binl₂, -aeqb at binl₂]; exact (mem_union_right _ binl₂))
(λ ainl₁ : a ∈ l₁, (λ ainl₁ : a ∈ l₁,
by rewrite [union_cons_of_mem l₁ binl₂]; exact (mem_union_left _ ainl₁))) by rewrite [union_cons_of_mem l₁ binl₂]; exact (mem_union_left _ ainl₁)))
(λ nbinl₂ : b ∉ l₂, or.elim h (λ nbinl₂ : b ∉ l₂, or.elim (eq_or_mem_of_mem_cons h)
(λ aeqb : a = b, (λ aeqb : a = b,
by rewrite [union_cons_of_not_mem l₁ nbinl₂, aeqb]; exact !mem_cons) by rewrite [union_cons_of_not_mem l₁ nbinl₂, aeqb]; exact !mem_cons)
(λ ainl₁ : a ∈ l₁, (λ ainl₁ : a ∈ l₁,

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

@ -67,12 +67,12 @@ calc_trans perm.trans
theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ := theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a ∈ l₂ :=
assume p, perm.induction_on p assume p, perm.induction_on p
(λ h, h) (λ h, h)
(λ x l₁ l₂ p₁ r₁ i, or.elim i (λ x l₁ l₂ p₁ r₁ i, or.elim (eq_or_mem_of_mem_cons i)
(assume aeqx : a = x, by rewrite aeqx; apply !mem_cons) (assume aeqx : a = x, by rewrite aeqx; apply !mem_cons)
(assume ainl₁ : a ∈ l₁, or.inr (r₁ ainl₁))) (assume ainl₁ : a ∈ l₁, or.inr (r₁ ainl₁)))
(λ x y l ainyxl, or.elim ainyxl (λ x y l ainyxl, or.elim (eq_or_mem_of_mem_cons ainyxl)
(assume aeqy : a = y, by rewrite aeqy; exact (or.inr !mem_cons)) (assume aeqy : a = y, by rewrite aeqy; exact (or.inr !mem_cons))
(assume ainxl : a ∈ x::l, or.elim ainxl (assume ainxl : a ∈ x::l, or.elim (eq_or_mem_of_mem_cons ainxl)
(assume aeqx : a = x, or.inl aeqx) (assume aeqx : a = x, or.inl aeqx)
(assume ainl : a ∈ l, or.inr (or.inr ainl)))) (assume ainl : a ∈ l, or.inr (or.inr ainl))))
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ ainl₁, r₂ (r₁ ainl₁)) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ ainl₁, r₂ (r₁ ainl₁))
@ -521,7 +521,7 @@ assume p, perm_induction_on p
(λ yint₁ : y ∈ t₁, (λ yint₁ : y ∈ t₁,
assert yint₂ : y ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁)), assert yint₂ : y ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁)),
assert yinxt₂ : y ∈ x::t₂, from or.inr (yint₂), assert yinxt₂ : y ∈ x::t₂, from or.inr (yint₂),
or.elim xinyt₁ or.elim (eq_or_mem_of_mem_cons xinyt₁)
(λ xeqy : x = y, (λ xeqy : x = y,
assert xint₂ : x ∈ t₂, by rewrite [-xeqy at yint₂]; exact yint₂, assert xint₂ : x ∈ t₂, by rewrite [-xeqy at yint₂]; exact yint₂,
begin begin
@ -552,7 +552,9 @@ assume p, perm_induction_on p
have xint₁ : x ∈ t₁, from or_resolve_right xinyt₁ xney, have xint₁ : x ∈ t₁, from or_resolve_right xinyt₁ xney,
assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)), assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)),
assert nyinxt₂ : y ∉ x::t₂, from assert nyinxt₂ : y ∉ x::t₂, from
assume yinxt₂ : y ∈ x::t₂, or.elim yinxt₂ (λ h, absurd h (ne.symm xney)) (λ h, absurd h nyint₂), assume yinxt₂ : y ∈ x::t₂, or.elim (eq_or_mem_of_mem_cons yinxt₂)
(λ h, absurd h (ne.symm xney))
(λ h, absurd h nyint₂),
begin begin
rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_not_mem nyinxt₂, rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_not_mem nyinxt₂,
erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_mem xint₂], erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_mem xint₂],
@ -573,7 +575,7 @@ assume p, perm_induction_on p
end) end)
(λ nyint₁ : y ∉ t₁, (λ nyint₁ : y ∉ t₁,
assert nyinxt₂ : y ∉ x::t₂, from assert nyinxt₂ : y ∉ x::t₂, from
assume yinxt₂ : y ∈ x::t₂, or.elim yinxt₂ assume yinxt₂ : y ∈ x::t₂, or.elim (eq_or_mem_of_mem_cons yinxt₂)
(λ h, absurd h (ne.symm xney)) (λ h, absurd h (ne.symm xney))
(λ h, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup h))) nyint₁), (λ h, absurd (mem_of_mem_erase_dup (mem_perm (symm r) (mem_erase_dup h))) nyint₁),
begin begin
@ -661,20 +663,20 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
have ains₁a₁s₂ : a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at aina₂t₂]; exact aina₂t₂, have ains₁a₁s₂ : a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at aina₂t₂]; exact aina₂t₂,
or.elim (mem_or_mem_of_mem_append ains₁a₁s₂) or.elim (mem_or_mem_of_mem_append ains₁a₁s₂)
(λ ains₁ : a ∈ s₁, mem_append_left s₂ ains₁) (λ ains₁ : a ∈ s₁, mem_append_left s₂ ains₁)
(λ aina₁s₂ : a ∈ a₁::s₂, or.elim (mem_or_mem_of_mem_cons aina₁s₂) (λ aina₁s₂ : a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons aina₁s₂)
(λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ aint₁) na₁int₁) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ aint₁) na₁int₁)
(λ ains₂ : a ∈ s₂, mem_append_right s₁ ains₂))) (λ ains₂ : a ∈ s₂, mem_append_right s₁ ains₂)))
(λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂) (λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂)
(λ ains₁ : a ∈ s₁, (λ ains₁ : a ∈ s₁,
have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁), have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁),
have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂, have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂,
or.elim (mem_or_mem_of_mem_cons aina₁t₁) or.elim (eq_or_mem_of_mem_cons aina₁t₁)
(λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁)
(λ aint₁ : a ∈ t₁, aint₁)) (λ aint₁ : a ∈ t₁, aint₁))
(λ ains₂ : a ∈ s₂, (λ ains₂ : a ∈ s₂,
have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)), have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)),
have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂, have aina₁t₁ : a ∈ a₁::t₁, from iff.mp' (e a) aina₂t₂,
or.elim (mem_or_mem_of_mem_cons aina₁t₁) or.elim (eq_or_mem_of_mem_cons aina₁t₁)
(λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂)
(λ aint₁ : a ∈ t₁, aint₁))), (λ aint₁ : a ∈ t₁, aint₁))),
calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext dt₁ ds₁s₂ eqv) calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext dt₁ ds₁s₂ eqv)