From 7e875c8d8535176cdd0930a6f22c1e83a4704189 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 May 2015 10:43:28 -0700 Subject: [PATCH] refactor(library): simplify theorems using improved tactics --- library/data/list/basic.lean | 6 +++--- library/data/num.lean | 8 ++++---- library/data/option.lean | 2 +- library/data/prod.lean | 4 ++-- library/data/string.lean | 6 +++--- library/data/subtype.lean | 2 +- library/data/sum.lean | 4 ++-- library/data/vector.lean | 4 ++-- library/init/nat.lean | 2 +- 9 files changed, 19 insertions(+), 19 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 057ba99eb..d9c1dc480 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -418,10 +418,10 @@ definition has_decidable_eq {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : li match H a b with | inl Hab := match has_decidable_eq l₁ l₂ with - | inl He := inl (eq.rec_on Hab (eq.rec_on He rfl)) - | inr Hn := inr (λ H, list.no_confusion H (λ Hab Ht, absurd Ht Hn)) + | inl He := inl (by congruence; repeat assumption) + | inr Hn := inr (by intro H; injection H; contradiction) end - | inr Hnab := inr (λ H, list.no_confusion H (λ Hab Ht, absurd Hab Hnab)) + | inr Hnab := inr (by intro H; injection H; contradiction) end /- quasiequal a l l' means that l' is exactly l, with a added diff --git a/library/data/num.lean b/library/data/num.lean index 758d95c8b..98bb11655 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -64,16 +64,16 @@ namespace pos_num | (bit0 a) one := inr (by contradiction) | (bit0 a) (bit0 b) := match decidable_eq a b with - | inl H₁ := inl (eq.rec_on H₁ rfl) - | inr H₁ := inr (λ H, pos_num.no_confusion H (λ H₂, absurd H₂ H₁)) + | inl H₁ := inl (by rewrite H₁) + | inr H₁ := inr (by intro H; injection H; contradiction) end | (bit0 a) (bit1 b) := inr (by contradiction) | (bit1 a) one := inr (by contradiction) | (bit1 a) (bit0 b) := inr (by contradiction) | (bit1 a) (bit1 b) := match decidable_eq a b with - | inl H₁ := inl (eq.rec_on H₁ rfl) - | inr H₁ := inr (λ H, pos_num.no_confusion H (λ H₂, absurd H₂ H₁)) + | inl H₁ := inl (by rewrite H₁) + | inr H₁ := inr (by intro H; injection H; contradiction) end local notation a < b := (lt a b = tt) diff --git a/library/data/option.lean b/library/data/option.lean index bf15efd78..ada56bb09 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -34,6 +34,6 @@ namespace option | (some v₁) (some v₂) := match H v₁ v₂ with | inl e := by left; congruence; assumption - | inr n := by right; intro h; injection h; refine absurd _ n; assumption + | inr n := by right; intro h; injection h; contradiction end end option diff --git a/library/data/prod.lean b/library/data/prod.lean index 1e0198029..a1369da43 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -24,9 +24,9 @@ namespace prod | inl e₁ := match h₂ b b' with | inl e₂ := by left; congruence; repeat assumption - | inr n₂ := by right; intro h; injection h; refine absurd _ n₂; assumption + | inr n₂ := by right; intro h; injection h; contradiction end - | inr n₁ := by right; intro h; injection h; refine absurd _ n₁; assumption + | inr n₁ := by right; intro h; injection h; contradiction end definition swap {A : Type} : A × A → A × A diff --git a/library/data/string.lean b/library/data/string.lean index 5efce9b5a..c5eed5186 100644 --- a/library/data/string.lean +++ b/library/data/string.lean @@ -28,7 +28,7 @@ begin apply (@by_cases (a₇ = b₇)), intros, apply (@by_cases (a₈ = b₈)), intros, left, congruence, repeat assumption, - repeat (intro n; right; intro h; injection h; refine absurd _ n; assumption) + repeat (intro n; right; intro h; injection h; contradiction) end open string @@ -42,7 +42,7 @@ definition decidable_eq_string [instance] : ∀ s₁ s₂ : string, decidable (s | inl e₁ := match decidable_eq_string r₁ r₂ with | inl e₂ := by left; congruence; repeat assumption - | inr n₂ := by right; intro h; injection h; refine absurd _ n₂; assumption + | inr n₂ := by right; intro h; injection h; contradiction end - | inr n₁ := by right; intro h; injection h; refine absurd _ n₁; assumption + | inr n₁ := by right; intro h; injection h; contradiction end diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 6aa894fb4..39508d099 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -33,6 +33,6 @@ namespace subtype begin apply (@by_cases (v₁ = v₂)), {intro e, revert p₁, rewrite e, intro p₁, left, congruence}, - {intro n, right, intro h, injection h, refine absurd _ n, assumption} + {intro n, right, intro h, injection h, contradiction} end end subtype diff --git a/library/data/sum.lean b/library/data/sum.lean index 10d3d9948..570d428d3 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -41,13 +41,13 @@ namespace sum | has_decidable_eq (inl a₁) (inl a₂) := match h₁ a₁ a₂ with | decidable.inl hp := by left; congruence; assumption - | decidable.inr hn := by right; intro h; injection h; refine absurd _ hn; assumption + | decidable.inr hn := by right; intro h; injection h; contradiction end | has_decidable_eq (inl a₁) (inr b₂) := by right; contradiction | has_decidable_eq (inr b₁) (inl a₂) := by right; contradiction | has_decidable_eq (inr b₁) (inr b₂) := match h₂ b₁ b₂ with | decidable.inl hp := by left; congruence; assumption - | decidable.inr hn := by right; intro h; injection h; refine absurd _ hn; assumption + | decidable.inr hn := by right; intro h; injection h; contradiction end end sum diff --git a/library/data/vector.lean b/library/data/vector.lean index a46e90e0c..04e3f4db0 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -263,8 +263,8 @@ namespace vector | inl Hab := match decidable_eq v₁ v₂ with | inl He := by left; congruence; repeat assumption - | inr Hn := by right; intro h; injection h; refine absurd _ Hn; assumption + | inr Hn := by right; intro h; injection h; contradiction end - | inr Hnab := by right; intro h; injection h; refine absurd _ Hnab; assumption + | inr Hnab := by right; intro h; injection h; contradiction end end vector diff --git a/library/init/nat.lean b/library/init/nat.lean index 7914bf340..53fdee935 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -35,7 +35,7 @@ namespace nat | has_decidable_eq (succ x) (succ y) := match has_decidable_eq x y with | inl xeqy := inl (by rewrite xeqy) - | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney) + | inr xney := inr (by intro h; injection h; contradiction) end -- less-than is well-founded