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

refactor(library/data/list/perm): use anonymous 'suppose' and 'have' expressions

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-19 12:35:12 -07:00
parent 812ddf1ef5
commit 73f665dce3
1 changed files with 29 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -692,35 +692,38 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
have ∃ s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split this, have ∃ s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split this,
obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from this, obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from this,
have dt₂' : nodup (a₁::(s₁++s₂)), from nodup_head (by rewrite [t₂_eq at d₂]; exact d₂), have dt₂' : nodup (a₁::(s₁++s₂)), from nodup_head (by rewrite [t₂_eq at d₂]; exact d₂),
have na₁s₁s₂ : a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
have na₁s₁ : a₁ ∉ s₁, from not_mem_of_not_mem_append_left na₁s₁s₂,
have na₁s₂ : a₁ ∉ s₂, from not_mem_of_not_mem_append_right na₁s₁s₂,
have ds₁s₂ : nodup (s₁++s₂), from nodup_of_nodup_cons dt₂',
have eqv : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from have eqv : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from
take a, iff.intro take a, iff.intro
(λ aint₁ : a ∈ t₁, (suppose a ∈ t₁,
assert aina₂t₂ : a ∈ a₂::t₂, from iff.mp (e a) (mem_cons_of_mem _ aint₁), assert a ∈ a₂::t₂, from iff.mp (e a) (mem_cons_of_mem _ this),
have ains₁a₁s₂ : a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at aina₂t₂]; exact aina₂t₂, have a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at this]; exact this,
or.elim (mem_or_mem_of_mem_append ains₁a₁s₂) or.elim (mem_or_mem_of_mem_append this)
(λ ains₁ : a ∈ s₁, mem_append_left s₂ ains₁) (suppose a ∈ s₁, mem_append_left s₂ this)
(λ aina₁s₂ : a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons aina₁s₂) (suppose a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons this)
(λ aeqa₁ : a = a₁, (suppose a = a₁,
have a₁ ∉ t₁, from not_mem_of_nodup_cons d₁, assert a₁ ∉ t₁, from not_mem_of_nodup_cons d₁,
absurd (aeqa₁ ▸ aint₁) this) by subst a; contradiction)
(λ ains₂ : a ∈ s₂, mem_append_right s₁ ains₂))) (suppose a ∈ s₂, mem_append_right s₁ this)))
(λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂) (suppose a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append this)
(λ ains₁ : a ∈ s₁, (suppose a ∈ s₁,
have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁), have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ this),
have a ∈ a₁::t₁, from iff.mpr (e a) this, have a ∈ a₁::t₁, from iff.mpr (e a) this,
or.elim (eq_or_mem_of_mem_cons this) or.elim (eq_or_mem_of_mem_cons this)
(λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁) (suppose a = a₁,
(λ aint₁ : a ∈ t₁, aint₁)) have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
(λ ains₂ : a ∈ s₂, assert a₁ ∉ s₁, from not_mem_of_not_mem_append_left this,
have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)), by subst a; contradiction)
(suppose a ∈ t₁, this))
(suppose a ∈ s₂,
have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ this)),
have a ∈ a₁::t₁, from iff.mpr (e a) this, have a ∈ a₁::t₁, from iff.mpr (e a) this,
or.elim (eq_or_mem_of_mem_cons this) or.elim (eq_or_mem_of_mem_cons this)
(λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂) (suppose a = a₁,
(λ aint₁ : a ∈ t₁, aint₁))), have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
assert a₁ ∉ s₂, from not_mem_of_not_mem_append_right this,
by subst a; contradiction)
(suppose a ∈ t₁, this))),
have ds₁s₂ : nodup (s₁++s₂), from nodup_of_nodup_cons dt₂',
have nodup t₁, from nodup_of_nodup_cons d₁, have nodup t₁, from nodup_of_nodup_cons d₁,
calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext this ds₁s₂ eqv) calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext this ds₁s₂ eqv)
... ~ s₁++(a₁::s₂) : !perm_middle ... ~ s₁++(a₁::s₂) : !perm_middle
@ -761,8 +764,8 @@ assume u, perm.induction_on u
assume u' : l₁' ~ l₂', assume u' : l₁' ~ l₂',
assume u'' : filter p l₁' ~ filter p l₂', assume u'' : filter p l₁' ~ filter p l₂',
decidable.by_cases decidable.by_cases
(assume H : p x, by rewrite [*filter_cons_of_pos _ H]; apply perm.skip; apply u'') (suppose p x, by rewrite [*filter_cons_of_pos _ this]; apply perm.skip; apply u'')
(assume H : ¬ p x, by rewrite [*filter_cons_of_neg _ H]; apply u'')) (suppose ¬ p x, by rewrite [*filter_cons_of_neg _ this]; apply u''))
(take x y l, (take x y l,
decidable.by_cases decidable.by_cases
(assume H1 : p x, (assume H1 : p x,