refactor(library/data): test new tactics in the standard library

library/data/bool.lean

@@ -51,9 +51,7 @@ namespace bool
   bool.cases_on a rfl rfl
 
   theorem bor.comm (a b : bool) : a || b = b || a :=
-  bool.cases_on a
+  by cases a; repeat (cases b | reflexivity)
-    (bool.cases_on b rfl rfl)
-    (bool.cases_on b rfl rfl)
 
   theorem bor.assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
   match a with

library/data/option.lean

@@ -10,8 +10,9 @@ import logic.eq
 open eq.ops decidable
 
 namespace option
-  definition is_none {A : Type} (o : option A) : Prop :=
+  definition is_none {A : Type} : option A →  Prop
-  option.rec true (λ a, false) o
+  | none     := true
+  | (some v) := false
 
   theorem is_none_none {A : Type} : is_none (@none A) :=
   trivial
@@ -28,13 +29,13 @@ namespace option
   protected definition is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none
 
-  protected definition has_decidable_eq [instance] {A : Type} [H : decidable_eq A] : decidable_eq (option A) :=
+  protected definition has_decidable_eq [instance] {A : Type} [H : decidable_eq A] : ∀ o₁ o₂ : option A, decidable (o₁ = o₂)
-  take o₁ o₂ : option A,
+  | none      none      := by left;  reflexivity
-    option.rec_on o₁
+  | none      (some v₂) := by right; contradiction
-      (option.rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
+  | (some v₁) none      := by right; contradiction
-      (take a₁ : A, option.rec_on o₂
+  | (some v₁) (some v₂) :=
-        (inr (ne.symm (none_ne_some a₁)))
+    match H v₁ v₂ with
-        (take a₂ : A, decidable.rec_on (H a₁ a₂)
+    | inl e := by left; congruence; assumption
-          (assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
+    | inr n := by right; intro h; injection h; refine absurd _ n; assumption
-          (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some.inj Hn) Hne))))
+    end
 end option

library/data/prod.lean

@@ -20,13 +20,16 @@ namespace prod
   protected definition is_inhabited [instance] [h₁ : inhabited A] [h₂ : inhabited B] : inhabited (prod A B) :=
   inhabited.mk (default A, default B)
 
-  protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : decidable_eq (A × B) :=
+  protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ p₁ p₂ : A × B, decidable (p₁ = p₂)
-  take (u v : A × B),
+  | (a, b) (a', b') :=
-    have H₃ : u = v ↔ (pr₁ u = pr₁ v) ∧ (pr₂ u = pr₂ v), from
+    match h₁ a a' with
-      iff.intro
+    | inl e₁ :=
-        (assume H, H ▸ and.intro rfl rfl)
+      match h₂ b b' with
-        (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)),
+      | inl e₂ := by left; congruence; repeat assumption
-    decidable_of_decidable_of_iff _ (iff.symm H₃)
+      | inr n₂ := by right; intro h; injection h; refine absurd _ n₂; assumption
+      end
+    | inr n₁ := by right; intro h; injection h; refine absurd _ n₁; assumption
+    end
 
   definition swap {A : Type} : A × A → A × A
   | (a, b) := (b, a)

library/data/subtype.lean

@@ -30,9 +30,11 @@ namespace subtype
   protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} :=
   inhabited.mk (tag a H)
 
-  protected definition has_decidable_eq [instance] [H : decidable_eq A] : decidable_eq {x | P x} :=
+  protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂)
-  take a1 a2 : {x | P x},
+  | (tag v₁ p₁) (tag v₂ p₂) :=
-    have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
+    begin
-      iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
+      apply (@by_cases (v₁ = v₂)),
-    decidable_of_decidable_of_iff _ (iff.symm H1)
+        {intro e, revert p₁, rewrite e, intro p₁, left, congruence},
+        {intro n, right, intro h, injection h, refine absurd _ n, assumption}
+    end
 end subtype

library/data/sum.lean

@@ -42,14 +42,14 @@ namespace sum
   protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂)
   | has_decidable_eq (inl a₁) (inl a₂) :=
     match h₁ a₁ a₂ with
-      | decidable.inl hp := decidable.inl (hp ▸ rfl)
+      | decidable.inl hp := by left; congruence; assumption
-      | decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn)
+      | decidable.inr hn := by right; intro h; injection h; refine absurd _ hn; assumption
     end
-  | has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (by contradiction)
+  | has_decidable_eq (inl a₁) (inr b₂) := by right; contradiction
-  | has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (by 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 := decidable.inl (hp ▸ rfl)
+      | decidable.inl hp := by left; congruence; assumption
-      | decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn)
+      | decidable.inr hn := by right; intro h; injection h; refine absurd _ hn; assumption
     end
 end sum

library/data/vector.lean

@@ -259,15 +259,14 @@ namespace vector
    /- decidable equality -/
   open decidable
   definition decidable_eq [H : decidable_eq A] : ∀ {n : nat} (v₁ v₂ : vector A n), decidable (v₁ = v₂)
-  | ⌞0⌟    []      []      := inl rfl
+  | ⌞0⌟    []      []      := by left; reflexivity
   | ⌞n+1⌟  (a::v₁) (b::v₂) :=
     match H a b with
     | inl Hab  :=
       match decidable_eq v₁ v₂ with
-      | inl He := inl (eq.rec_on Hab (eq.rec_on He rfl))
+      | inl He := by left; congruence; repeat assumption
-      | inr Hn := inr (λ H₁, vector.no_confusion H₁ (λ e₁ e₂ e₃, absurd (heq.to_eq e₃) Hn))
+      | inr Hn := by right; intro h; injection h; refine absurd _ Hn; assumption
       end
-    | inr Hnab := inr (λ H₁, vector.no_confusion H₁ (λ e₁ e₂ e₃, absurd e₂ Hnab))
+    | inr Hnab := by right; intro h; injection h; refine absurd _ Hnab; assumption
   end
-
 end vector