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

refactor(library/data): use "suppose"-expressions to cleanup proofs

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-20 19:44:29 -07:00
parent fa7a527590
commit 10e5b182b5
3 changed files with 90 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -199,8 +199,8 @@ theorem tail_cons [rewrite] (a : T) (l : list T) : tail (a::l) = l
theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ [] → (head l)::(tail l) = l := theorem cons_head_tail [h : inhabited T] {l : list T} : l ≠ [] → (head l)::(tail l) = l :=
list.cases_on l list.cases_on l
(assume H : [] ≠ [], absurd rfl H) (suppose [] ≠ [], absurd rfl this)
(take x l, assume H : x::l ≠ [], rfl) (take x l, suppose x::l ≠ [], rfl)
/- list membership -/ /- list membership -/
@ -230,36 +230,36 @@ theorem eq_or_mem_of_mem_cons {x y : T} {l : list T} : x ∈ y::l → x = y ∨
assume h, h assume h, h
theorem mem_singleton {x a : T} : x ∈ [a] → x = a := theorem mem_singleton {x a : T} : x ∈ [a] → x = a :=
assume h : x ∈ [a], or.elim (eq_or_mem_of_mem_cons h) suppose x ∈ [a], or.elim (eq_or_mem_of_mem_cons this)
(λ xeqa : x = a, xeqa) (suppose x = a, this)
(λ xinn : x ∈ [], absurd xinn !not_mem_nil) (suppose x ∈ [], absurd this !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 (eq_or_mem_of_mem_cons ainbl) assume ainbl binl, or.elim (eq_or_mem_of_mem_cons ainbl)
(λ aeqb : a = b, by substvars; exact binl) (suppose a = b, by substvars; exact binl)
(λ ainl : a ∈ l, ainl) (suppose a ∈ l, this)
theorem mem_or_mem_of_mem_append {x : T} {s t : list T} : x ∈ s ++ t → x ∈ s ∨ x ∈ t := theorem mem_or_mem_of_mem_append {x : T} {s t : list T} : x ∈ s ++ t → x ∈ s ∨ x ∈ t :=
list.induction_on s or.inr list.induction_on s or.inr
(take y s, (take y s,
assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t, assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t,
assume H1 : x ∈ y::s ++ t, suppose x ∈ y::s ++ t,
have H2 : x = y ∨ x ∈ s ++ t, from H1, have x = y ∨ x ∈ s ++ t, from this,
have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or_of_or_of_imp_right H2 IH, have x = y ∨ x ∈ s ∨ x ∈ t, from or_of_or_of_imp_right this IH,
iff.elim_right or.assoc H3) iff.elim_right or.assoc this)
theorem mem_append_of_mem_or_mem {x : T} {s t : list T} : x ∈ s ∨ x ∈ t → x ∈ s ++ t := theorem mem_append_of_mem_or_mem {x : T} {s t : list T} : x ∈ s ∨ x ∈ t → x ∈ s ++ t :=
list.induction_on s list.induction_on s
(take H, or.elim H false.elim (assume H, H)) (take H, or.elim H false.elim (assume H, H))
(take y s, (take y s,
assume IH : x ∈ s ∨ x ∈ t → x ∈ s ++ t, assume IH : x ∈ s ∨ x ∈ t → x ∈ s ++ t,
assume H : x ∈ y::s ∨ x ∈ t, suppose x ∈ y::s ∨ x ∈ t,
or.elim H or.elim this
(assume H1, (suppose x ∈ y::s,
or.elim (eq_or_mem_of_mem_cons H1) or.elim (eq_or_mem_of_mem_cons this)
(take H2 : x = y, or.inl H2) (suppose x = y, or.inl this)
(take H2 : x ∈ s, or.inr (IH (or.inl H2)))) (suppose x ∈ s, or.inr (IH (or.inl this))))
(assume H1 : x ∈ t, or.inr (IH (or.inr H1)))) (suppose x ∈ t, or.inr (IH (or.inr this))))
theorem mem_append_iff (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t := theorem mem_append_iff (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t :=
iff.intro mem_or_mem_of_mem_append mem_append_of_mem_or_mem iff.intro mem_or_mem_of_mem_append mem_append_of_mem_or_mem
@ -283,19 +283,19 @@ 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_iff H)) (suppose x ∈ [], false.elim (iff.elim_left !mem_nil_iff this))
(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, suppose x ∈ y::l,
or.elim (eq_or_mem_of_mem_cons H) or.elim (eq_or_mem_of_mem_cons this)
(assume H1 : x = y, (suppose x = y,
exists.intro [] (!exists.intro (H1 ▸ rfl))) exists.intro [] (!exists.intro (this ▸ rfl)))
(assume H1 : x ∈ l, (suppose x ∈ l,
obtain s (H2 : ∃t : list T, l = s ++ (x::t)), from IH H1, obtain s (H2 : ∃t : list T, l = s ++ (x::t)), from IH this,
obtain t (H3 : l = s ++ (x::t)), from H2, obtain t (H3 : l = s ++ (x::t)), from H2,
have H4 : y :: l = (y::s) ++ (x::t), have y :: l = (y::s) ++ (x::t),
from H3 ▸ rfl, from H3 ▸ rfl,
!exists.intro (!exists.intro H4))) !exists.intro (!exists.intro this)))
theorem mem_append_left {a : T} {l₁ : list T} (l₂ : list T) : a ∈ l₁ → a ∈ l₁ ++ l₂ := theorem mem_append_left {a : T} {l₁ : list T} (l₂ : list T) : a ∈ l₁ → a ∈ l₁ ++ l₂ :=
assume ainl₁, mem_append_of_mem_or_mem (or.inl ainl₁) assume ainl₁, mem_append_of_mem_or_mem (or.inl ainl₁)
@ -417,7 +417,7 @@ assume n, if_neg n
theorem find_of_not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l := theorem find_of_not_mem {l : list T} {x : T} : ¬x ∈ l → find x l = length l :=
list.rec_on l list.rec_on l
(assume P₁ : ¬x ∈ [], _) (suppose ¬x ∈ [], _)
(take y l, (take y l,
assume iH : ¬x ∈ l → find x l = length l, assume iH : ¬x ∈ l → find x l = length l,
suppose ¬x ∈ y::l, suppose ¬x ∈ y::l,

84
library/data/list/comb.lean
View file

@ -55,18 +55,18 @@ theorem exists_of_mem_map {A B : Type} {f : A → B} {b : B} :
∀{l}, b ∈ map f l → ∃a, a ∈ l ∧ f a = b ∀{l}, b ∈ map f l → ∃a, a ∈ l ∧ f a = b
| [] H := false.elim H | [] H := false.elim H
| (c::l) H := or.elim (iff.mp !mem_cons_iff H) | (c::l) H := or.elim (iff.mp !mem_cons_iff H)
(assume H1 : b = f c, (suppose b = f c,
exists.intro c (and.intro !mem_cons (eq.symm H1))) exists.intro c (and.intro !mem_cons (eq.symm this)))
(assume H1 : b ∈ map f l, (suppose b ∈ map f l,
obtain a (Hl : a ∈ l) (Hr : f a = b), from exists_of_mem_map H1, obtain a (Hl : a ∈ l) (Hr : f a = b), from exists_of_mem_map this,
exists.intro a (and.intro (mem_cons_of_mem _ Hl) Hr)) exists.intro a (and.intro (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₂ 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 | [] h := absurd h !not_mem_nil
| (a::l) h := | (a::l) h :=
or.elim (eq_or_mem_of_mem_cons h) or.elim (eq_or_mem_of_mem_cons h)
(λ b₁eqb₂ : b₁ = b₂, b₁eqb₂) (suppose b₁ = b₂, this)
(λ b₁inl : b₁ ∈ map (const A b₂) l, eq_of_map_const b₁inl) (suppose b₁ ∈ map (const A b₂) l, eq_of_map_const this)
definition map₂ (f : A → B → C) : list A → list B → list C definition map₂ (f : A → B → C) : list A → list B → list C
| [] _ := [] | [] _ := []
@ -89,22 +89,22 @@ theorem filter_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} : ∀
theorem of_mem_filter {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ filter p l → p a theorem of_mem_filter {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ filter p l → p a
| [] ain := absurd ain !not_mem_nil | [] ain := absurd ain !not_mem_nil
| (b::l) ain := by_cases | (b::l) ain := by_cases
(λ pb : p b, (assume pb : p b,
have aux : a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain, have aux : a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain,
or.elim (eq_or_mem_of_mem_cons aux) or.elim (eq_or_mem_of_mem_cons aux)
(λ aeqb : a = b, by rewrite [-aeqb at pb]; exact pb) (suppose a = b, by rewrite [-this at pb]; exact pb)
(λ ainl, of_mem_filter ainl)) (suppose a ∈ filter p l, of_mem_filter this))
(λ npb : ¬ p b, by rewrite [filter_cons_of_neg _ npb at ain]; exact (of_mem_filter ain)) (suppose ¬ p b, by rewrite [filter_cons_of_neg _ this at ain]; exact (of_mem_filter ain))
theorem mem_of_mem_filter {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ filter p l → a ∈ l theorem mem_of_mem_filter {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ filter p l → a ∈ l
| [] ain := absurd ain !not_mem_nil | [] ain := absurd ain !not_mem_nil
| (b::l) ain := by_cases | (b::l) ain := by_cases
(λ pb : p b, (λ pb : p b,
have aux : a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain, have a ∈ b :: filter p l, by rewrite [filter_cons_of_pos _ pb at ain]; exact ain,
or.elim (eq_or_mem_of_mem_cons aux) or.elim (eq_or_mem_of_mem_cons this)
(λ aeqb : a = b, by rewrite [aeqb]; exact !mem_cons) (suppose a = b, by rewrite this; exact !mem_cons)
(λ ainl, mem_cons_of_mem _ (mem_of_mem_filter ainl))) (suppose a ∈ filter p l, mem_cons_of_mem _ (mem_of_mem_filter this)))
(λ npb : ¬ p b, by rewrite [filter_cons_of_neg _ npb at ain]; exact (mem_cons_of_mem _ (mem_of_mem_filter ain))) (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 → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ l → p a → a ∈ filter p l theorem mem_filter_of_mem {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ l → p a → a ∈ filter p l
| [] ain pa := absurd ain !not_mem_nil | [] ain pa := absurd ain !not_mem_nil
@ -122,8 +122,8 @@ theorem filter_sub {p : A → Prop} [h : decidable_pred p] (l : list A) : filter
theorem filter_append {p : A → Prop} [h : decidable_pred p] : ∀ (l₁ l₂ : list A), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂ theorem filter_append {p : A → Prop} [h : decidable_pred p] : ∀ (l₁ l₂ : list A), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂
| [] l₂ := rfl | [] l₂ := rfl
| (a::l₁) l₂ := by_cases | (a::l₁) l₂ := by_cases
(λ pa : p a, by rewrite [append_cons, *filter_cons_of_pos _ pa, filter_append]) (suppose p a, by rewrite [append_cons, *filter_cons_of_pos _ this, filter_append])
(λ npa : ¬ p a, by rewrite [append_cons, *filter_cons_of_neg _ npa, filter_append]) (suppose ¬ p a, by rewrite [append_cons, *filter_cons_of_neg _ this, filter_append])
/- foldl & foldr -/ /- foldl & foldr -/
definition foldl (f : A → B → A) : A → list B → A definition foldl (f : A → B → A) : A → list B → A
@ -208,8 +208,8 @@ theorem all_implies {p q : A → Prop} : ∀ {l}, all l p → (∀ x, p x → q
| [] h₁ h₂ := trivial | [] h₁ h₂ := trivial
| (a::l) h₁ h₂ := | (a::l) h₁ h₂ :=
have allq : all l q, from all_implies (all_of_all_cons h₁) h₂, have allq : all l q, from all_implies (all_of_all_cons h₁) h₂,
have qa : q a, from h₂ a (of_all_cons h₁), have q a, from h₂ a (of_all_cons h₁),
all_cons_of_all qa allq all_cons_of_all this allq
theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p → p a theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p → p a
| [] h₁ h₂ := absurd h₁ !not_mem_nil | [] h₁ h₂ := absurd h₁ !not_mem_nil
@ -218,8 +218,8 @@ theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p
(λ aeqb : a = b, (λ aeqb : a = b,
by rewrite [all_cons_eq at h₂, -aeqb at h₂]; exact (and.elim_left h₂)) by rewrite [all_cons_eq at h₂, -aeqb at h₂]; exact (and.elim_left h₂))
(λ ainl : a ∈ l, (λ ainl : a ∈ l,
have allp : all l p, by rewrite [all_cons_eq at h₂]; exact (and.elim_right h₂), have all l p, by rewrite [all_cons_eq at h₂]; exact (and.elim_right h₂),
of_mem_of_all ainl allp) of_mem_of_all ainl this)
theorem all_of_forall {p : A → Prop} : ∀ {l}, (∀a, a ∈ l → p a) → all l p theorem all_of_forall {p : A → Prop} : ∀ {l}, (∀a, a ∈ l → p a) → all l p
| [] H := !all_nil | [] H := !all_nil
@ -328,47 +328,47 @@ eq_of_map_const h₂
theorem mem_of_mem_map_pair₁ {a₁ a : A} {b₁ : B} {l : list B} : (a₁, b₁) ∈ map (λ b, (a, b)) l → b₁ ∈ l := theorem mem_of_mem_map_pair₁ {a₁ a : A} {b₁ : B} {l : list B} : (a₁, b₁) ∈ map (λ b, (a, b)) l → b₁ ∈ l :=
assume ain, assume ain,
assert h₁ : pr2 (a₁, b₁) ∈ map pr2 (map (λ b, (a, b)) l), from mem_map pr2 ain, assert pr2 (a₁, b₁) ∈ map pr2 (map (λ b, (a, b)) l), from mem_map pr2 ain,
assert h₂ : b₁ ∈ map (λx, x) l, by rewrite [map_map at h₁, ↑pr2 at h₁]; exact h₁, assert b₁ ∈ map (λx, x) l, by rewrite [map_map at this, ↑pr2 at this]; exact this,
by rewrite [map_id at h₂]; exact h₂ by rewrite [map_id at this]; exact this
theorem mem_product {a : A} {b : B} : ∀ {l₁ l₂}, a ∈ l₁ → b ∈ l₂ → (a, b) ∈ product l₁ l₂ theorem mem_product {a : A} {b : B} : ∀ {l₁ l₂}, a ∈ l₁ → b ∈ l₂ → (a, b) ∈ product l₁ l₂
| [] l₂ h₁ h₂ := absurd h₁ !not_mem_nil | [] l₂ h₁ h₂ := absurd h₁ !not_mem_nil
| (x::l₁) l₂ h₁ h₂ := | (x::l₁) l₂ h₁ h₂ :=
or.elim (eq_or_mem_of_mem_cons h₁) or.elim (eq_or_mem_of_mem_cons h₁)
(λ aeqx : a = x, (assume aeqx : a = x,
assert aux : (a, b) ∈ map (λ b, (a, b)) l₂, from mem_map _ h₂, assert (a, b) ∈ map (λ b, (a, b)) l₂, from mem_map _ h₂,
begin rewrite [-aeqx, product_cons], exact mem_append_left _ aux end) begin rewrite [-aeqx, product_cons], exact mem_append_left _ this end)
(λ ainl₁ : a ∈ l₁, (assume ainl₁ : a ∈ l₁,
assert inl₁l₂ : (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂, assert (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂,
begin rewrite [product_cons], exact mem_append_right _ inl₁l₂ end) begin rewrite [product_cons], exact mem_append_right _ this end)
theorem mem_of_mem_product_left {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → a ∈ l₁ theorem mem_of_mem_product_left {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → a ∈ l₁
| [] l₂ h := absurd h !not_mem_nil | [] l₂ h := absurd h !not_mem_nil
| (x::l₁) l₂ h := | (x::l₁) l₂ h :=
or.elim (mem_or_mem_of_mem_append h) or.elim (mem_or_mem_of_mem_append h)
(λ ain : (a, b) ∈ map (λ b, (x, b)) l₂, (suppose (a, b) ∈ map (λ b, (x, b)) l₂,
assert aeqx : a = x, from eq_of_mem_map_pair₁ ain, assert a = x, from eq_of_mem_map_pair₁ this,
by rewrite [aeqx]; exact !mem_cons) by rewrite this; exact !mem_cons)
(λ ain : (a, b) ∈ product l₁ l₂, (suppose (a, b) ∈ product l₁ l₂,
have ainl₁ : a ∈ l₁, from mem_of_mem_product_left ain, have a ∈ l₁, from mem_of_mem_product_left this,
mem_cons_of_mem _ ainl₁) mem_cons_of_mem _ this)
theorem mem_of_mem_product_right {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → b ∈ l₂ theorem mem_of_mem_product_right {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → b ∈ l₂
| [] l₂ h := absurd h !not_mem_nil | [] l₂ h := absurd h !not_mem_nil
| (x::l₁) l₂ h := | (x::l₁) l₂ h :=
or.elim (mem_or_mem_of_mem_append h) or.elim (mem_or_mem_of_mem_append h)
(λ abin : (a, b) ∈ map (λ b, (x, b)) l₂, (suppose (a, b) ∈ map (λ b, (x, b)) l₂,
mem_of_mem_map_pair₁ abin) mem_of_mem_map_pair₁ this)
(λ abin : (a, b) ∈ product l₁ l₂, (suppose (a, b) ∈ product l₁ l₂,
mem_of_mem_product_right abin) mem_of_mem_product_right this)
theorem length_product : ∀ (l₁ : list A) (l₂ : list B), length (product l₁ l₂) = length l₁ * length l₂ theorem length_product : ∀ (l₁ : list A) (l₂ : list B), length (product l₁ l₂) = length l₁ * length l₂
| [] l₂ := by rewrite [length_nil, zero_mul] | [] l₂ := by rewrite [length_nil, zero_mul]
| (x::l₁) l₂ := | (x::l₁) l₂ :=
assert ih : length (product l₁ l₂) = length l₁ * length l₂, from length_product l₁ l₂, assert length (product l₁ l₂) = length l₁ * length l₂, from length_product l₁ l₂,
by rewrite [product_cons, length_append, length_cons, by rewrite [product_cons, length_append, length_cons,
length_map, ih, mul.right_distrib, one_mul, add.comm] length_map, this, mul.right_distrib, one_mul, add.comm]
end product end product
-- new for list/comb dependent map theory -- new for list/comb dependent map theory

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

@ -39,10 +39,10 @@ lemma length_erase_of_mem {a : A} : ∀ {l}, a ∈ l → length (erase a l) = pr
| [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 :=
by_cases by_cases
(λ aeqx : a = x, by rewrite [aeqx, erase_cons_head]) (suppose a = x, by rewrite [this, erase_cons_head])
(λ anex : a ≠ x, (suppose a ≠ x,
assert ainyxs : a ∈ y::xs, from or_resolve_right h anex, assert ainyxs : a ∈ y::xs, from or_resolve_right h this,
by rewrite [erase_cons_tail _ anex, *length_cons, length_erase_of_mem ainyxs]) by rewrite [erase_cons_tail _ this, *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
@ -227,26 +227,28 @@ theorem nodup_of_nodup_append_right : ∀ {l₁ l₂ : list A}, nodup (l₁++l
theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → disjoint l₁ l₂ theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list A}, nodup (l₁++l₂) → disjoint l₁ l₂
| [] l₂ d := disjoint_nil_left l₂ | [] l₂ d := disjoint_nil_left l₂
| (x::xs) l₂ d := | (x::xs) l₂ d :=
have d₁ : nodup (x::(xs++l₂)), from d, have nodup (x::(xs++l₂)), from d,
have d₂ : nodup (xs++l₂), from nodup_of_nodup_cons d₁, have x ∉ xs++l₂, from not_mem_of_nodup_cons this,
have nxin : x ∉ xs++l₂, from not_mem_of_nodup_cons d₁, have nxinl₂ : x ∉ l₂, from not_mem_of_not_mem_append_right this,
have nxinl₂ : x ∉ l₂, from not_mem_of_not_mem_append_right nxin, take a, suppose a ∈ x::xs,
have dsj : disjoint xs l₂, from disjoint_of_nodup_append d₂, or.elim (eq_or_mem_of_mem_cons this)
λ a (ainxxs : a ∈ x::xs), (suppose a = x, this⁻¹ ▸ nxinl₂)
or.elim (eq_or_mem_of_mem_cons ainxxs) (suppose ainxs : a ∈ xs,
(λ aeqx : a = x, aeqx⁻¹ ▸ nxinl₂) have nodup (x::(xs++l₂)), from d,
(λ ainxs : a ∈ xs, disjoint_left dsj ainxs) have nodup (xs++l₂), from nodup_of_nodup_cons this,
have disjoint xs l₂, from disjoint_of_nodup_append this,
disjoint_left this ainxs)
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₂)
| [] l₂ d₁ d₂ dsj := by rewrite [append_nil_left]; exact d₂ | [] l₂ d₁ d₂ dsj := by rewrite [append_nil_left]; exact d₂
| (x::xs) l₂ d₁ d₂ dsj := | (x::xs) l₂ d₁ d₂ dsj :=
have dsj₁ : disjoint xs l₂, from disjoint_of_disjoint_cons_left dsj,
have ndxs : nodup xs, from nodup_of_nodup_cons d₁, have ndxs : nodup xs, from nodup_of_nodup_cons d₁,
have ndxsl₂ : nodup (xs++l₂), from nodup_append_of_nodup_of_nodup_of_disjoint ndxs d₂ dsj₁, have disjoint xs l₂, from disjoint_of_disjoint_cons_left dsj,
have ndxsl₂ : nodup (xs++l₂), from nodup_append_of_nodup_of_nodup_of_disjoint ndxs d₂ this,
have nxinxs : x ∉ xs, from not_mem_of_nodup_cons d₁, have nxinxs : x ∉ xs, from not_mem_of_nodup_cons d₁,
have nxinl₂ : x ∉ l₂, from disjoint_left dsj !mem_cons, have x ∉ l₂, from disjoint_left dsj !mem_cons,
have nxinxsl₂ : x ∉ xs++l₂, from not_mem_append nxinxs nxinl₂, have x ∉ xs++l₂, from not_mem_append nxinxs this,
nodup_cons nxinxsl₂ ndxsl₂ nodup_cons this ndxsl₂
theorem nodup_app_comm {l₁ l₂ : list A} (d : nodup (l₁++l₂)) : nodup (l₂++l₁) := theorem nodup_app_comm {l₁ l₂ : list A} (d : nodup (l₁++l₂)) : nodup (l₂++l₁) :=
have d₁ : nodup l₁, from nodup_of_nodup_append_left d, have d₁ : nodup l₁, from nodup_of_nodup_append_left d,