refactor(library/data/bitvec,library/data/tuple): use automation

library/data/bitvec.lean

@@ -35,26 +35,13 @@ section shift
   variable {n : ℕ}
 
   def shl (x : bitvec n) (i : ℕ) : bitvec n :=
-  let r := dropn i x ++ₜ repeat ff (min n i) in
-  have length r = n, begin dsimp, rewrite [nat.sub_add_min_cancel] end,
-  bitvec.cong this r
+  bitvec.cong (by simp) $
+    dropn i x ++ₜ repeat ff (min n i)
 
+  local attribute [ematch] nat.add_sub_assoc sub_le le_of_not_ge sub_eq_zero_of_le
   def fill_shr (x : bitvec n) (i : ℕ) (fill : bool) : bitvec n :=
-  let y := repeat fill (min n i) ++ₜ firstn (n-i) x in
-  have length y = n, from if h : i ≤ n then
-    begin
-      dsimp,
-      rw [min_eq_right h, min_eq_left (sub_le _ _), -nat.add_sub_assoc h,
-        nat.add_sub_cancel_left]
-    end
-  else
-    have h : i ≥ n, from le_of_not_ge h,
-    begin
-      dsimp,
-      rw [min_eq_left h, sub_eq_zero_of_le h, min_eq_left (zero_le _)],
-      apply rfl
-    end,
-  bitvec.cong this y
+  bitvec.cong (begin [smt] by_cases (i ≤ n), eblast end) $
+    repeat fill (min n i) ++ₜ firstn (n-i) x
 
   -- unsigned shift right
   def ushr (x : bitvec n) (i : ℕ) : bitvec n :=
@@ -84,7 +71,7 @@ section arith
   protected def carry (x y c : bool) :=
   x && y || x && c || y && c
 
-  def neg (x : bitvec n) : bitvec n :=
+  protected def neg (x : bitvec n) : bitvec n :=
   let f := λ y c, (y || c, bxor y c) in
   prod.snd (map_accumr f x ff)
 
@@ -94,7 +81,7 @@ section arith
   let ⟨c, z⟩ := tuple.map_accumr₂ f x y c in
   c :: z
 
-  def add (x y : bitvec n) : bitvec n := tail (adc x y ff)
+  protected def add (x y : bitvec n) : bitvec n := tail (adc x y ff)
 
   protected def borrow (x y b : bool) :=
   bnot x && y || bnot x && b || y && b
@@ -104,19 +91,19 @@ section arith
   let f := λ x y c, (bitvec.borrow x y c, bitvec.xor3 x y c) in
   tuple.map_accumr₂ f x y b
 
-  def sub (x y : bitvec n) : bitvec n := prod.snd (sbb x y ff)
+  protected def sub (x y : bitvec n) : bitvec n := prod.snd (sbb x y ff)
 
   instance : has_zero (bitvec n) := ⟨bitvec.zero n⟩
   instance : has_one (bitvec n)  := ⟨bitvec.one n⟩
-  instance : has_add (bitvec n)  := ⟨add⟩
-  instance : has_sub (bitvec n)  := ⟨sub⟩
-  instance : has_neg (bitvec n)  := ⟨neg⟩
+  instance : has_add (bitvec n)  := ⟨bitvec.add⟩
+  instance : has_sub (bitvec n)  := ⟨bitvec.sub⟩
+  instance : has_neg (bitvec n)  := ⟨bitvec.neg⟩
 
-  def mul (x y : bitvec n) : bitvec n :=
+  protected def mul (x y : bitvec n) : bitvec n :=
   let f := λ r b, cond b (r + r + y) (r + r) in
   list.foldl f 0 (to_list x)
 
-  instance : has_mul (bitvec n)  := ⟨mul⟩
+  instance : has_mul (bitvec n)  := ⟨bitvec.mul⟩
 end arith
 
 section comparison
@@ -133,10 +120,11 @@ section comparison
   def sborrow : Π {n : ℕ}, bitvec n → bitvec n → bool
   | 0        _ _ := ff
   | (succ n) x y :=
-     bool.cases_on
-       (head x)
-       (bool.cases_on (head y) (uborrow (tail x) (tail y)) tt)
-       (bool.cases_on (head y) ff (uborrow (tail x) (tail y)))
+    match (head x, head y) with
+    | (tt, ff) := tt
+    | (ff, tt) := ff
+    | _        := uborrow (tail x) (tail y)
+    end
 
   def slt (x y : bitvec n) : Prop := sborrow x y
   def sgt (x y : bitvec n) : Prop := slt y x

library/data/list/basic.lean

@@ -17,6 +17,7 @@ variables {α : Type u} {β : Type v} {φ : Type w}
 
 /- length theorems -/
 
+@[simp]
 theorem length_append : ∀ (x y : list α), length (x ++ y) = length x + length y
   | [] l := eq.symm (nat.zero_add (length l))
   | (a::s) l :=
@@ -28,6 +29,7 @@ theorem length_concat (a : α) : ∀ (l : list α), length (concat l a) = succ (
   | nil := rfl
   | (cons b l) := congr_arg succ (length_concat l)
 
+@[simp]
 theorem length_dropn
 : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i
 | 0 l := rfl
@@ -37,10 +39,12 @@ theorem length_dropn
           = length l - i             : length_dropn i l
       ... = succ (length l) - succ i : nat.sub_eq_succ_sub_succ (length l) i
 
+@[simp]
 theorem length_map (f : α → β) : ∀ (a : list α), length (map f a) = length a
 | [] := rfl
 | (a :: l) := congr_arg succ (length_map l)
 
+@[simp]
 theorem length_repeat (a : α) : ∀ (n : ℕ), length (repeat a n) = n
   | 0 := eq.refl 0
   | (succ i) := congr_arg succ (length_repeat i)
@@ -52,6 +56,7 @@ def firstn : ℕ → list α → list α
 | (succ n) []     := []
 | (succ n) (a::l) := a :: firstn n l
 
+@[simp]
 theorem length_firstn
 : ∀ (i : ℕ) (l : list α), length (firstn i l) = min i (length l)
 | 0        l      := eq.symm (nat.zero_min (length l))

library/data/list/comb.lean

@@ -22,16 +22,19 @@ definition map₂ {α : Type u} {β : Type v} {φ : Type w} (f : α → β →
 | l [] := []
 | (a::s) (b::t) := f a b :: map₂ s t
 
+@[simp]
 theorem map₂_nil_1 {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ)
    : Π y, map₂ f nil y = nil
 | [] := eq.refl nil
 | (b::t) := eq.refl nil
 
+@[simp]
 theorem map₂_nil_2 {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ)
    : Π (x : list α), map₂ f x nil = nil
 | [] := eq.refl nil
 | (b::t) := eq.refl nil
 
+@[simp]
 theorem length_map₂ {α : Type u} {β : Type v} {φ : Type w} (f : α → β → φ)
   : Π x y, length (map₂ f x y) = min (length x) (length y)
 | [] y :=
@@ -59,6 +62,7 @@ definition map_accumr (f : α → σ → σ × β) : list α → σ → (σ × l
   let z := f y (prod.fst r) in
   (prod.fst z, prod.snd z :: prod.snd r)
 
+@[simp]
 theorem length_map_accumr
 : ∀ (f : α → σ → σ × β) (x : list α) (s : σ),
   length (prod.snd (map_accumr f x s)) = length x
@@ -80,6 +84,7 @@ definition map_accumr₂ {α β σ φ : Type} (f : α → β → σ → σ × φ
   let q := f x y (prod.fst r) in
   (prod.fst q, prod.snd q :: (prod.snd r))
 
+@[simp]
 theorem length_map_accumr₂ {α β σ φ : Type}
 : ∀ (f : α → β → σ → σ × φ) x y c,
   length (prod.snd (map_accumr₂ f x y c)) = min (length x) (length y)

library/data/tuple.lean

@@ -10,7 +10,7 @@ import data.list
 
 universe variables u v w
 
-def tuple (α : Type u) (n : ℕ) := {l : list α // list.length l = n}
+def tuple (α : Type u) (n : ℕ) := { l : list α // l^.length = n }
 
 namespace tuple
 variables {α : Type u} {β : Type v} {φ : Type w}
@@ -32,92 +32,60 @@ notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
 open nat
 
 def head : tuple α (nat.succ n) → α
-| ⟨list.nil,      h ⟩ := let q : 0 = succ n := h in by contradiction
-| ⟨list.cons a v, h ⟩ := a
+| ⟨ [],     h ⟩ := by contradiction
+| ⟨ a :: v, h ⟩ := a
 
 theorem head_cons (a : α) : Π (v : tuple α n), head (a :: v) = a
 | ⟨ l, h ⟩ := rfl
 
 def tail : tuple α (succ n) → tuple α n
-| ⟨ list.nil,   h ⟩ := let q : 0 = succ n := h in by contradiction
-| ⟨ list.cons a v, h ⟩ := ⟨ v,  congr_arg pred h ⟩
+| ⟨ [],     h ⟩ := by contradiction
+| ⟨ a :: v, h ⟩ := ⟨ v, congr_arg pred h ⟩
 
 theorem tail_cons (a : α) : Π (v : tuple α n), tail (a :: v) = v
 | ⟨ l, h ⟩ := rfl
 
 def to_list : tuple α n → list α | ⟨ l, h ⟩ := l
 
-/- append -/
-
 def append {n m : nat} : tuple α n → tuple α m → tuple α (n + m)
-| ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ :=
-  let p := calc
-     list.length (l₁ ++ l₂)
-           = list.length l₁ + list.length l₂ : list.length_append l₁ l₂
-       ... = n + list.length l₂ : congr_arg (λi, i + list.length l₂) h₁
-       ... = n + m              : congr_arg (λi, n + i) h₂ in
-  ⟨ list.append l₁ l₂, p ⟩
+| ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ := ⟨ l₁ ++ l₂, by simp_using_hs ⟩
 
 /- map -/
 
 def map (f : α → β) : tuple α n → tuple β n
-| ⟨ l, h ⟩  :=
-  let q := calc list.length (list.map f l) = list.length l : list.length_map f l
-                                       ... = n             : h in
-  ⟨ list.map f l, q ⟩
+| ⟨ l, h ⟩  := ⟨ list.map f l, by simp_using_hs ⟩
 
-theorem map_nil (f : α → β) : map f nil = nil := rfl
+@[simp] lemma map_nil (f : α → β) : map f nil = nil := rfl
 
-theorem map_cons (f : α → β) (a : α)
-      : Π (v : tuple α n), map f (a::v) = f a :: map f v
-| ⟨ l, h ⟩ := rfl
+lemma map_cons (f : α → β) (a : α) : Π (v : tuple α n), map f (a::v) = f a :: map f v
+| ⟨l,h⟩ := rfl
 
 def map₂ (f : α → β → φ) : tuple α n → tuple β n → tuple φ n
-| ⟨ x, px ⟩ ⟨ y, py ⟩ :=
-  let z : list φ := list.map₂ f x y in
-  let pxx : list.length x = n := px in
-  let pyy : list.length y = n := py in
-  let p : list.length z = n := calc
-       list.length z = min (list.length x) (list.length y) : list.length_map₂ f x y
-                 ... = min n n                             : by rewrite [pxx, pyy]
-                 ... = n                                   : min_self n in
-  ⟨ z, p ⟩
+| ⟨ x, _ ⟩ ⟨ y, _ ⟩ := ⟨ list.map₂ f x y, by simp_using_hs ⟩
 
 def repeat (a : α) (n : ℕ) : tuple α n :=
-⟨list.repeat a n, list.length_repeat a n⟩
+⟨ list.repeat a n, list.length_repeat a n ⟩
 
 def dropn (i : ℕ) : tuple α n → tuple α (n - i)
-| ⟨l, p⟩ := ⟨list.dropn i l, p ▸ list.length_dropn i l⟩
+| ⟨l, p⟩ := ⟨ list.dropn i l, by simp_using_hs ⟩
 
 def firstn (i : ℕ) : tuple α n → tuple α (min i n)
-| ⟨l, p⟩ :=
-  let q := calc list.length (list.firstn i l)
-                   = min i (list.length l)  : list.length_firstn i l
-               ... = min i n                : congr_arg (min i) p in
-  ⟨list.firstn i l, q⟩
+| ⟨l, p⟩ := ⟨ list.firstn i l, by simp_using_hs ⟩
 
 section accum
   open prod
   variable {σ : Type}
 
-  def map_accumr
-  : (α → σ → σ × β) → tuple α n → σ → σ × tuple β n
-  | f ⟨ x, px ⟩ c :=
-    let z := list.map_accumr f x c in
-    let p := eq.trans (list.length_map_accumr f x c) px in
-    (prod.fst z, ⟨ prod.snd z, p ⟩)
+  def map_accumr (f : α → σ → σ × β) : tuple α n → σ → σ × tuple β n
+  | ⟨ x, px ⟩ c :=
+    let res := list.map_accumr f x c in
+    ⟨ res.1, res.2, by simp_using_hs ⟩
 
   def map_accumr₂ {α β σ φ : Type} (f : α → β → σ → σ × φ)
    : tuple α n → tuple β n → σ → σ × tuple φ n
   | ⟨ x, px ⟩ ⟨ y, py ⟩ c :=
-    let z := list.map_accumr₂ f x y c in
-    let pxx : list.length x = n := px in
-    let pyy : list.length y = n := py in
-    let p := calc
-          list.length (prod.snd (list.map_accumr₂ f x y c))
-                  = min (list.length x) (list.length y)  : list.length_map_accumr₂ f x y c
-              ... = n                                    : by rewrite [ pxx, pyy, min_self ] in
-    (prod.fst z, ⟨prod.snd z, p ⟩)
+    let res := list.map_accumr₂ f x y c in
+    ⟨ res.1, res.2, by simp_using_hs ⟩
 
 end accum
 end tuple

library/init/algebra/field.lean

@@ -32,14 +32,20 @@ instance division_ring_has_div [division_ring α] : has_div α :=
 lemma division_def (a b : α) : a / b = a * b⁻¹ :=
 rfl
 
+@[simp]
 lemma mul_inv_cancel {a : α} (h : a ≠ 0) : a * a⁻¹ = 1 :=
 division_ring.mul_inv_cancel h
 
+@[simp]
 lemma inv_mul_cancel {a : α} (h : a ≠ 0) : a⁻¹ * a = 1 :=
 division_ring.inv_mul_cancel h
 
+@[simp]
+lemma one_div_eq_inv (a : α) : 1 / a = a⁻¹ :=
+one_mul a⁻¹
+
 lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a :=
-eq.symm $ one_mul (a⁻¹)
+by simp
 
 local attribute [simp]
 division_def mul_comm mul_assoc

library/init/algebra/functions.lean

@@ -62,12 +62,15 @@ end
 lemma min_left_comm : ∀ (a b c : α), min a (min b c) = min b (min a c) :=
 left_comm (@min α _) (@min_comm α _) (@min_assoc α _)
 
+@[simp]
 lemma min_self (a : α) : min a a = a :=
 by min_tac a a
 
+@[ematch]
 lemma min_eq_left {a b : α} (h : a ≤ b) : min a b = a :=
 begin apply eq.symm, apply eq_min (le_refl _) h, intros, assumption end
 
+@[ematch]
 lemma min_eq_right {a b : α} (h : b ≤ a) : min a b = b :=
 eq.subst (min_comm b a) (min_eq_left h)
 
@@ -89,6 +92,7 @@ end
 lemma max_left_comm : ∀ (a b c : α), max a (max b c) = max b (max a c) :=
 left_comm (@max α _) (@max_comm α _) (@max_assoc α _)
 
+@[simp]
 lemma max_self (a : α) : max a a = a :=
 by min_tac a a
 

library/init/data/list/lemmas.lean

@@ -11,31 +11,38 @@ variables {α : Type u} {β : Type v}
 
 namespace list
 
+@[simp]
 lemma nil_append (s : list α) : [] ++ s = s :=
 rfl
 
 lemma cons_append (x : α) (s t : list α) : (x::s) ++ t = x::(s ++ t) :=
 rfl
 
+@[simp]
 lemma map_nil (f : α → β) : map f [] = [] :=
 rfl
 
 lemma map_cons (f : α → β) (a : α) (l : list α) : map f (a :: l) = f a :: map f l :=
 rfl
 
+@[simp]
 lemma length_nil : length (@nil α) = 0 :=
 rfl
 
+@[simp]
 lemma length_cons (x : α) (t : list α) : length (x::t) = length t + 1 :=
 rfl
 
+@[simp]
 lemma nth_zero (a : α) (l : list α) : nth (a :: l) 0 = some a :=
 rfl
 
+@[simp]
 lemma nth_succ (a : α) (l : list α) (n : nat) : nth (a::l) (nat.succ n) = nth l n :=
 rfl
 
 /- list membership -/
+@[simp]
 lemma mem_nil_iff (a : α) : a ∈ [] ↔ false :=
 iff.rfl
 

library/init/data/nat/lemmas.lean

@@ -75,9 +75,11 @@ lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
 lemma eq_zero_of_add_eq_zero_left {n m : ℕ} (h : n + m = 0) : m = 0 :=
 @eq_zero_of_add_eq_zero_right m n (nat.add_comm n m ▸ h)
 
+@[simp]
 lemma pred_zero : pred 0 = 0 :=
 rfl
 
+@[simp]
 lemma pred_succ (n : ℕ) : pred (succ n) = n :=
 rfl
 
@@ -577,6 +579,7 @@ instance : semiring nat           := by apply_instance
 instance : ordered_semiring nat   := by apply_instance
 
 /- subtraction -/
+@[simp]
 protected theorem sub_zero (n : ℕ) : n - 0 = n :=
 rfl
 
@@ -594,18 +597,22 @@ protected theorem sub_self : ∀ (n : ℕ), n - n = 0
 | 0        := by rw nat.sub_zero
 | (succ n) := by rw [succ_sub_succ, sub_self n]
 
+@[ematch]
 protected theorem add_sub_add_right : ∀ (n k m : ℕ), (n + k) - (m + k) = n - m
 | n 0        m := by rw [add_zero, add_zero]
 | n (succ k) m := by rw [add_succ, add_succ, succ_sub_succ, add_sub_add_right n k m]
 
+@[ematch]
 protected theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
 by rw [add_comm k n, add_comm k m, nat.add_sub_add_right]
 
+@[ematch]
 protected theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
 suffices n + m - (0 + m) = n, from
   by rwa [zero_add] at this,
 by rw [nat.add_sub_add_right, nat.sub_zero]
 
+@[ematch]
 protected theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m :=
 show n + m - (n + 0) = m, from
 by rw [nat.add_sub_add_left, nat.sub_zero]
@@ -709,6 +716,7 @@ lemma sub_eq_sub_min (n m : ℕ) : n - m = n - min n m :=
 if h : n ≥ m then by rewrite [min_eq_right h]
 else by rewrite [sub_eq_zero_of_le (le_of_not_ge h), min_eq_left (le_of_not_ge h), nat.sub_self]
 
+@[simp]
 lemma sub_add_min_cancel (n m : ℕ) : n - m + min n m = n :=
 by rewrite [sub_eq_sub_min, nat.sub_add_cancel (min_le_left n m)]