refactor(library): rename 'intersection' to 'inter' in list and finset, add finset abbreviation at top level
This commit is contained in:
Leonardo de Moura
parent
2405ce34de
commit
11f74363e2
4 changed files with 95 additions and 94 deletions
|
|
@ -238,54 +238,54 @@ calc ∅ ∪ s = s ∪ ∅ : union.comm
|
|||
... = s : union_empty
|
||||
end union
|
||||
|
||||
/- intersection -/
|
||||
section intersection
|
||||
/- inter -/
|
||||
section inter
|
||||
variable [h : decidable_eq A]
|
||||
include h
|
||||
|
||||
definition intersection (s₁ s₂ : finset A) : finset A :=
|
||||
definition inter (s₁ s₂ : finset A) : finset A :=
|
||||
quot.lift_on₂ s₁ s₂
|
||||
(λ l₁ l₂,
|
||||
to_finset_of_nodup (list.intersection (elt_of l₁) (elt_of l₂))
|
||||
(nodup_intersection_of_nodup _ (has_property l₁)))
|
||||
(λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_intersection p₁ p₂))
|
||||
to_finset_of_nodup (list.inter (elt_of l₁) (elt_of l₂))
|
||||
(nodup_inter_of_nodup _ (has_property l₁)))
|
||||
(λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_inter p₁ p₂))
|
||||
|
||||
notation s₁ ∩ s₂ := intersection s₁ s₂
|
||||
notation s₁ ∩ s₂ := inter s₁ s₂
|
||||
|
||||
theorem mem_of_mem_intersection_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_left ainl₁l₂)
|
||||
theorem mem_of_mem_inter_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_left ainl₁l₂)
|
||||
|
||||
theorem mem_of_mem_intersection_right {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₂ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_right ainl₁l₂)
|
||||
theorem mem_of_mem_inter_right {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₂ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_right ainl₁l₂)
|
||||
|
||||
theorem mem_intersection_of_mem_of_mem {a : A} {s₁ s₂ : finset A} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_intersection_of_mem_of_mem ainl₁ ainl₂)
|
||||
theorem mem_inter_of_mem_of_mem {a : A} {s₁ s₂ : finset A} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_inter_of_mem_of_mem ainl₁ ainl₂)
|
||||
|
||||
theorem mem_intersection_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
|
||||
theorem mem_inter_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
|
||||
propext (iff.intro
|
||||
(λ h, and.intro (mem_of_mem_intersection_left h) (mem_of_mem_intersection_right h))
|
||||
(λ h, mem_intersection_of_mem_of_mem (and.elim_left h) (and.elim_right h)))
|
||||
(λ h, and.intro (mem_of_mem_inter_left h) (mem_of_mem_inter_right h))
|
||||
(λ h, mem_inter_of_mem_of_mem (and.elim_left h) (and.elim_right h)))
|
||||
|
||||
theorem intersection.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
|
||||
ext (λ a, by rewrite [*mem_intersection_eq]; exact and.comm)
|
||||
theorem inter.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
|
||||
ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm)
|
||||
|
||||
theorem intersection.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
|
||||
ext (λ a, by rewrite [*mem_intersection_eq]; exact and.assoc)
|
||||
theorem inter.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
|
||||
ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc)
|
||||
|
||||
theorem intersection_self (s : finset A) : s ∩ s = s :=
|
||||
theorem inter_self (s : finset A) : s ∩ s = s :=
|
||||
ext (λ a, iff.intro
|
||||
(λ h, mem_of_mem_intersection_right h)
|
||||
(λ h, mem_intersection_of_mem_of_mem h h))
|
||||
(λ h, mem_of_mem_inter_right h)
|
||||
(λ h, mem_inter_of_mem_of_mem h h))
|
||||
|
||||
theorem intersection_empty (s : finset A) : s ∩ ∅ = ∅ :=
|
||||
theorem inter_empty (s : finset A) : s ∩ ∅ = ∅ :=
|
||||
ext (λ a, iff.intro
|
||||
(λ h : a ∈ s ∩ ∅, absurd (mem_of_mem_intersection_right h) !not_mem_empty)
|
||||
(λ h : a ∈ s ∩ ∅, absurd (mem_of_mem_inter_right h) !not_mem_empty)
|
||||
(λ h : a ∈ ∅, absurd h !not_mem_empty))
|
||||
|
||||
theorem empty_intersection (s : finset A) : ∅ ∩ s = ∅ :=
|
||||
calc ∅ ∩ s = s ∩ ∅ : intersection.comm
|
||||
... = ∅ : intersection_empty
|
||||
end intersection
|
||||
theorem empty_inter (s : finset A) : ∅ ∩ s = ∅ :=
|
||||
calc ∅ ∩ s = s ∩ ∅ : inter.comm
|
||||
... = ∅ : inter_empty
|
||||
end inter
|
||||
|
||||
/- subset -/
|
||||
definition subset (s₁ s₂ : finset A) : Prop :=
|
||||
|
|
@ -330,3 +330,4 @@ theorem mem_upto_of_lt {n a : nat} : a < n → a ∈ upto n :=
|
|||
list.mem_upto_of_lt
|
||||
end upto
|
||||
end finset
|
||||
abbreviation finset := finset.finset
|
||||
|
|
|
|||
|
|
@ -59,11 +59,11 @@ quot.induction_on s (λ l h₁ h₂, list.all_insert_of_all h₁ h₂)
|
|||
theorem all_erase_of_all {p : A → Prop} (a : A) {s : finset A}: all s p → all (erase a s) p :=
|
||||
quot.induction_on s (λ l h, list.all_erase_of_all a h)
|
||||
|
||||
theorem all_intersection_of_all_left {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₁ p → all (s₁ ∩ s₂) p :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_left _ h)
|
||||
theorem all_inter_of_all_left {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₁ p → all (s₁ ∩ s₂) p :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_left _ h)
|
||||
|
||||
theorem all_intersection_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_right _ h)
|
||||
theorem all_inter_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p :=
|
||||
quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_right _ h)
|
||||
end all
|
||||
|
||||
section cross_product
|
||||
|
|
|
|||
|
|
@ -641,48 +641,48 @@ assume p, by_cases
|
|||
by rewrite [insert_eq_of_not_mem nainl₁, insert_eq_of_not_mem nainl₂]; exact (skip _ p))
|
||||
end perm_insert
|
||||
|
||||
section perm_intersection
|
||||
section perm_inter
|
||||
variable [H : decidable_eq A]
|
||||
include H
|
||||
|
||||
theorem perm_intersection_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (intersection l₁ t₁) ~ (intersection l₂ t₁) :=
|
||||
theorem perm_inter_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (inter l₁ t₁) ~ (inter l₂ t₁) :=
|
||||
assume p, perm.induction_on p
|
||||
!refl
|
||||
(λ x l₁ l₂ p₁ r₁, by_cases
|
||||
(λ xint₁ : x ∈ t₁, by rewrite [*intersection_cons_of_mem _ xint₁]; exact (skip x r₁))
|
||||
(λ nxint₁ : x ∉ t₁, by rewrite [*intersection_cons_of_not_mem _ nxint₁]; exact r₁))
|
||||
(λ xint₁ : x ∈ t₁, by rewrite [*inter_cons_of_mem _ xint₁]; exact (skip x r₁))
|
||||
(λ nxint₁ : x ∉ t₁, by rewrite [*inter_cons_of_not_mem _ nxint₁]; exact r₁))
|
||||
(λ x y l, by_cases
|
||||
(λ yint : y ∈ t₁, by_cases
|
||||
(λ xint : x ∈ t₁,
|
||||
by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_mem _ yint, *intersection_cons_of_mem _ xint];
|
||||
by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_mem _ yint, *inter_cons_of_mem _ xint];
|
||||
exact !swap)
|
||||
(λ nxint : x ∉ t₁,
|
||||
by rewrite [*intersection_cons_of_mem _ yint, *intersection_cons_of_not_mem _ nxint, intersection_cons_of_mem _ yint];
|
||||
by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint];
|
||||
exact !refl))
|
||||
(λ nyint : y ∉ t₁, by_cases
|
||||
(λ xint : x ∈ t₁,
|
||||
by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_not_mem _ nyint, intersection_cons_of_mem _ xint];
|
||||
by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint];
|
||||
exact !refl)
|
||||
(λ nxint : x ∉ t₁,
|
||||
by rewrite [*intersection_cons_of_not_mem _ nxint, *intersection_cons_of_not_mem _ nyint,
|
||||
intersection_cons_of_not_mem _ nxint];
|
||||
by rewrite [*inter_cons_of_not_mem _ nxint, *inter_cons_of_not_mem _ nyint,
|
||||
inter_cons_of_not_mem _ nxint];
|
||||
exact !refl)))
|
||||
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
|
||||
|
||||
theorem perm_intersection_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (intersection l t₁) ~ (intersection l t₂) :=
|
||||
theorem perm_inter_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (inter l t₁) ~ (inter l t₂) :=
|
||||
list.induction_on l
|
||||
(λ p, by rewrite [*intersection_nil]; exact !refl)
|
||||
(λ p, by rewrite [*inter_nil]; exact !refl)
|
||||
(λ x xs r p, by_cases
|
||||
(λ xint₁ : x ∈ t₁,
|
||||
assert xint₂ : x ∈ t₂, from mem_perm p xint₁,
|
||||
by rewrite [intersection_cons_of_mem _ xint₁, intersection_cons_of_mem _ xint₂]; exact (skip _ (r p)))
|
||||
by rewrite [inter_cons_of_mem _ xint₁, inter_cons_of_mem _ xint₂]; exact (skip _ (r p)))
|
||||
(λ nxint₁ : x ∉ t₁,
|
||||
assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
|
||||
by rewrite [intersection_cons_of_not_mem _ nxint₁, intersection_cons_of_not_mem _ nxint₂]; exact (r p)))
|
||||
by rewrite [inter_cons_of_not_mem _ nxint₁, inter_cons_of_not_mem _ nxint₂]; exact (r p)))
|
||||
|
||||
theorem perm_intersection {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (intersection l₁ t₁) ~ (intersection l₂ t₂) :=
|
||||
assume p₁ p₂, trans (perm_intersection_left t₁ p₁) (perm_intersection_right l₂ p₂)
|
||||
end perm_intersection
|
||||
theorem perm_inter {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (inter l₁ t₁) ~ (inter l₂ t₂) :=
|
||||
assume p₁ p₂, trans (perm_inter_left t₁ p₁) (perm_inter_right l₂ p₂)
|
||||
end perm_inter
|
||||
|
||||
/- extensionality -/
|
||||
section ext
|
||||
|
|
|
|||
|
|
@ -652,103 +652,103 @@ assume h₁ h₂, by_cases
|
|||
(λ nainl : a ∉ l, by rewrite [insert_eq_of_not_mem nainl]; exact (all_cons_of_all h₁ h₂))
|
||||
end insert
|
||||
|
||||
/- intersection -/
|
||||
section intersection
|
||||
/- inter -/
|
||||
section inter
|
||||
variable {A : Type}
|
||||
variable [H : decidable_eq A]
|
||||
include H
|
||||
|
||||
definition intersection : list A → list A → list A
|
||||
definition inter : list A → list A → list A
|
||||
| [] l₂ := []
|
||||
| (a::l₁) l₂ := if a ∈ l₂ then a :: intersection l₁ l₂ else intersection l₁ l₂
|
||||
| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
|
||||
|
||||
theorem intersection_nil (l : list A) : intersection [] l = []
|
||||
theorem inter_nil (l : list A) : inter [] l = []
|
||||
|
||||
theorem intersection_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → intersection (a::l₁) l₂ = a :: intersection l₁ l₂ :=
|
||||
theorem inter_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → inter (a::l₁) l₂ = a :: inter l₁ l₂ :=
|
||||
assume i, if_pos i
|
||||
|
||||
theorem intersection_cons_of_not_mem {a : A} (l₁ : list A) {l₂} : a ∉ l₂ → intersection (a::l₁) l₂ = intersection l₁ l₂ :=
|
||||
theorem inter_cons_of_not_mem {a : A} (l₁ : list A) {l₂} : a ∉ l₂ → inter (a::l₁) l₂ = inter l₁ l₂ :=
|
||||
assume i, if_neg i
|
||||
|
||||
theorem mem_of_mem_intersection_left : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₁
|
||||
theorem mem_of_mem_inter_left : ∀ {l₁ l₂} {a : A}, a ∈ inter l₁ l₂ → a ∈ l₁
|
||||
| [] l₂ a i := absurd i !not_mem_nil
|
||||
| (b::l₁) l₂ a i := by_cases
|
||||
(λ binl₂ : b ∈ l₂,
|
||||
have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i,
|
||||
have aux : a ∈ b :: inter l₁ l₂, by rewrite [inter_cons_of_mem _ binl₂ at i]; exact i,
|
||||
or.elim (eq_or_mem_of_mem_cons aux)
|
||||
(λ aeqb : a = b, by rewrite [aeqb]; exact !mem_cons)
|
||||
(λ aini, mem_cons_of_mem _ (mem_of_mem_intersection_left aini)))
|
||||
(λ aini, mem_cons_of_mem _ (mem_of_mem_inter_left aini)))
|
||||
(λ nbinl₂ : b ∉ l₂,
|
||||
have ainl₁ : a ∈ l₁, by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_left i),
|
||||
have ainl₁ : a ∈ l₁, by rewrite [inter_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_inter_left i),
|
||||
mem_cons_of_mem _ ainl₁)
|
||||
|
||||
theorem mem_of_mem_intersection_right : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₂
|
||||
theorem mem_of_mem_inter_right : ∀ {l₁ l₂} {a : A}, a ∈ inter l₁ l₂ → a ∈ l₂
|
||||
| [] l₂ a i := absurd i !not_mem_nil
|
||||
| (b::l₁) l₂ a i := by_cases
|
||||
(λ binl₂ : b ∈ l₂,
|
||||
have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i,
|
||||
have aux : a ∈ b :: inter l₁ l₂, by rewrite [inter_cons_of_mem _ binl₂ at i]; exact i,
|
||||
or.elim (eq_or_mem_of_mem_cons aux)
|
||||
(λ aeqb : a = b, by rewrite [aeqb]; exact binl₂)
|
||||
(λ aini : a ∈ intersection l₁ l₂, mem_of_mem_intersection_right aini))
|
||||
(λ aini : a ∈ inter l₁ l₂, mem_of_mem_inter_right aini))
|
||||
(λ nbinl₂ : b ∉ l₂,
|
||||
by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_right i))
|
||||
by rewrite [inter_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_inter_right i))
|
||||
|
||||
theorem mem_intersection_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ intersection l₁ l₂
|
||||
theorem mem_inter_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ inter l₁ l₂
|
||||
| [] l₂ a i₁ i₂ := absurd i₁ !not_mem_nil
|
||||
| (b::l₁) l₂ a i₁ i₂ := by_cases
|
||||
(λ binl₂ : b ∈ l₂,
|
||||
or.elim (eq_or_mem_of_mem_cons i₁)
|
||||
(λ aeqb : a = b,
|
||||
by rewrite [intersection_cons_of_mem _ binl₂, aeqb]; exact !mem_cons)
|
||||
by rewrite [inter_cons_of_mem _ binl₂, aeqb]; exact !mem_cons)
|
||||
(λ ainl₁ : a ∈ l₁,
|
||||
by rewrite [intersection_cons_of_mem _ binl₂];
|
||||
by rewrite [inter_cons_of_mem _ binl₂];
|
||||
apply mem_cons_of_mem;
|
||||
exact (mem_intersection_of_mem_of_mem ainl₁ i₂)))
|
||||
exact (mem_inter_of_mem_of_mem ainl₁ i₂)))
|
||||
(λ nbinl₂ : b ∉ l₂,
|
||||
or.elim (eq_or_mem_of_mem_cons i₁)
|
||||
(λ aeqb : a = b, absurd (aeqb ▸ i₂) nbinl₂)
|
||||
(λ ainl₁ : a ∈ l₁,
|
||||
by rewrite [intersection_cons_of_not_mem _ nbinl₂]; exact (mem_intersection_of_mem_of_mem ainl₁ i₂)))
|
||||
by rewrite [inter_cons_of_not_mem _ nbinl₂]; exact (mem_inter_of_mem_of_mem ainl₁ i₂)))
|
||||
|
||||
theorem nodup_intersection_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (intersection l₁ l₂)
|
||||
theorem nodup_inter_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (inter l₁ l₂)
|
||||
| [] l₂ d := nodup_nil
|
||||
| (a::l₁) l₂ d :=
|
||||
have d₁ : nodup l₁, from nodup_of_nodup_cons d,
|
||||
assert d₂ : nodup (intersection l₁ l₂), from nodup_intersection_of_nodup _ d₁,
|
||||
have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d,
|
||||
assert naini : a ∉ intersection l₁ l₂, from λ i, absurd (mem_of_mem_intersection_left i) nainl₁,
|
||||
have d₁ : nodup l₁, from nodup_of_nodup_cons d,
|
||||
assert d₂ : nodup (inter l₁ l₂), from nodup_inter_of_nodup _ d₁,
|
||||
have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d,
|
||||
assert naini : a ∉ inter l₁ l₂, from λ i, absurd (mem_of_mem_inter_left i) nainl₁,
|
||||
by_cases
|
||||
(λ ainl₂ : a ∈ l₂, by rewrite [intersection_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂))
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact d₂)
|
||||
(λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂))
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact d₂)
|
||||
|
||||
theorem intersection_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → intersection l₁ l₂ = []
|
||||
theorem inter_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → inter l₁ l₂ = []
|
||||
| [] l₂ d := rfl
|
||||
| (a::l₁) l₂ d :=
|
||||
assert aux_eq : intersection l₁ l₂ = [], from intersection_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d),
|
||||
assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
|
||||
by rewrite [intersection_cons_of_not_mem _ nainl₂, aux_eq]
|
||||
assert aux_eq : inter l₁ l₂ = [], from inter_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d),
|
||||
assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
|
||||
by rewrite [inter_cons_of_not_mem _ nainl₂, aux_eq]
|
||||
|
||||
theorem all_intersection_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p → all (intersection l₁ l₂) p
|
||||
theorem all_inter_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p → all (inter l₁ l₂) p
|
||||
| [] l₂ h := trivial
|
||||
| (a::l₁) l₂ h :=
|
||||
have h₁ : all l₁ p, from all_of_all_cons h,
|
||||
assert h₂ : all (intersection l₁ l₂) p, from all_intersection_of_all_left _ h₁,
|
||||
have pa : p a, from of_all_cons h,
|
||||
assert h₃ : all (a :: intersection l₁ l₂) p, from all_cons_of_all pa h₂,
|
||||
have h₁ : all l₁ p, from all_of_all_cons h,
|
||||
assert h₂ : all (inter l₁ l₂) p, from all_inter_of_all_left _ h₁,
|
||||
have pa : p a, from of_all_cons h,
|
||||
assert h₃ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₂,
|
||||
by_cases
|
||||
(λ ainl₂ : a ∈ l₂, by rewrite [intersection_cons_of_mem _ ainl₂]; exact h₃)
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact h₂)
|
||||
(λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact h₃)
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₂)
|
||||
|
||||
theorem all_intersection_of_all_right {p : A → Prop} : ∀ (l₁) {l₂}, all l₂ p → all (intersection l₁ l₂) p
|
||||
theorem all_inter_of_all_right {p : A → Prop} : ∀ (l₁) {l₂}, all l₂ p → all (inter l₁ l₂) p
|
||||
| [] l₂ h := trivial
|
||||
| (a::l₁) l₂ h :=
|
||||
assert h₁ : all (intersection l₁ l₂) p, from all_intersection_of_all_right _ h,
|
||||
assert h₁ : all (inter l₁ l₂) p, from all_inter_of_all_right _ h,
|
||||
by_cases
|
||||
(λ ainl₂ : a ∈ l₂,
|
||||
have pa : p a, from of_mem_of_all ainl₂ h,
|
||||
assert h₂ : all (a :: intersection l₁ l₂) p, from all_cons_of_all pa h₁,
|
||||
by rewrite [intersection_cons_of_mem _ ainl₂]; exact h₂)
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact h₁)
|
||||
have pa : p a, from of_mem_of_all ainl₂ h,
|
||||
assert h₂ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₁,
|
||||
by rewrite [inter_cons_of_mem _ ainl₂]; exact h₂)
|
||||
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₁)
|
||||
|
||||
end intersection
|
||||
end inter
|
||||
end list
|
||||
|
|
|
|||
Loading…
Reference in a new issue