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

refactor(library/data/list/perm): remove unnessary lambda abstractions

Browse source 
The contradiction tactic takes care of it.
This commit is contained in:
Leonardo de Moura 2015-04-30 14:02:19 -07:00
parent 9760968b45
commit 59b11c815c
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/perm.lean
View file

@ -24,17 +24,17 @@ theorem eq_nil_of_perm_nil {l₁ : list A} (p : [] ~ l₁) : l₁ = [] :=
have gen : ∀ (l₂ : list A) (p : l₂ ~ l₁), l₂ = [] → l₁ = [], from
take l₂ p, perm.induction_on p
(λ h, h)
(λ x y l₁ l₂ p₁ r₁, by contradiction)
(λ x y l e, by contradiction)
(by contradiction)
(by contradiction)
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ e, r₂ (r₁ e)),
gen [] p rfl
theorem not_perm_nil_cons (x : A) (l : list A) : ¬ [] ~ (x::l) :=
have gen : ∀ (l₁ l₂ : list A) (p : l₁ ~ l₂), l₁ = [] → l₂ = (x::l) → false, from
take l₁ l₂ p, perm.induction_on p
(λ e₁ e₂, by contradiction)
(λ x l₁ l₂ p₁ r₁ e₁ e₂, by contradiction)
(λ x y l e₁ e₂, by contradiction)
(by contradiction)
(by contradiction)
(by contradiction)
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ e₁ e₂,
begin
rewrite [e₂ at *, e₁ at *],