refactor(library/data/list): avoid placeholders '_', make first argument of false_elim implicit

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/data/list/basic.lean

@@ -11,15 +11,15 @@
 
 import tools.tactic
 import data.nat
-import logic
+import logic tools.helper_tactics
 -- import if -- for find
 
 using nat
 using eq_ops
+using helper_tactics
 
 namespace list
 
-
 -- Type
 -- ----
 
@@ -52,24 +52,23 @@ list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
 infixl `++` : 65 := concat
 
-theorem nil_concat (t : list T) : nil ++ t = t := refl _
+theorem nil_concat {t : list T} : nil ++ t = t
 
-theorem cons_concat (x : T) (s t : list T) : (x :: s) ++ t = x :: (s ++ t) := refl _
+theorem cons_concat {x : T} {s t : list T} : (x :: s) ++ t = x :: (s ++ t)
 
-theorem concat_nil (t : list T) : t ++ nil = t :=
+theorem concat_nil {t : list T} : t ++ nil = t :=
-list_induction_on t (refl _)
+list_induction_on t rfl
   (take (x : T) (l : list T) (H : concat l nil = l),
-    show concat (cons x l) nil = cons x l, from H ▸ refl _)
+    show concat (cons x l) nil = cons x l, from H ▸ rfl)
 
-theorem concat_assoc (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
+theorem concat_assoc {s t u : list T} : s ++ t ++ u = s ++ (t ++ u) :=
-list_induction_on s (refl _)
+list_induction_on s rfl
   (take x l,
     assume H : concat (concat l t) u = concat l (concat t u),
     calc
-      concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : refl _
+      concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : rfl
-        ... = cons x (concat l (concat t u)) : { H }
+        ... = cons x (concat l (concat t u))                          : {H}
-        ... = concat (cons x l) (concat t u) : refl _)
+        ... = concat (cons x l) (concat t u)                          : rfl)
-
 
 -- Length
 -- ------
@@ -78,9 +77,9 @@ definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
 
 theorem length_nil : length (@nil T) = 0 := rfl
 
-theorem length_cons (x : T) (t : list T) : length (x :: t) = succ (length t) := rfl
+theorem length_cons {x : T} {t : list T} : length (x :: t) = succ (length t)
 
-theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
+theorem length_concat {s t : list T} : length (s ++ t) = length s + length t :=
 list_induction_on s
   (calc
     length (concat nil t) = length t   : rfl
@@ -90,99 +89,95 @@ list_induction_on s
     assume H : length (concat s t) = length s + length t,
     calc
       length (concat (cons x s) t ) = succ (length (concat s t))  : rfl
-        ... = succ (length s + length t)   : { H }
+        ... = succ (length s + length t)   : {H}
         ... = succ (length s) + length t   : {add_succ_left⁻¹}
         ... = length (cons x s) + length t : rfl)
 
 -- add_rewrite length_nil length_cons
 
-
 -- Append
 -- ------
 
 definition append (x : T) : list T → list T := list_rec [x] (fun y l l', y :: l')
 
-theorem append_nil (x : T) : append x nil = [x] := refl _
+theorem append_nil {x : T} : append x nil = [x]
 
-theorem append_cons (x : T) (y : T) (l : list T) : append x (y :: l)  = y :: (append x l) := refl _
+theorem append_cons {x y : T} {l : list T} : append x (y :: l)  = y :: (append x l)
 
-theorem append_eq_concat  (x : T) (l : list T) : append x l = l ++ [x] := refl _
+theorem append_eq_concat  {x : T} {l : list T} : append x l = l ++ [x]
 
 -- add_rewrite append_nil append_cons
 
-
 -- Reverse
 -- -------
 
 definition reverse : list T → list T := list_rec nil (fun x l r, r ++ [x])
 
-theorem reverse_nil : reverse (@nil T) = nil := refl _
+theorem reverse_nil : reverse (@nil T) = nil
 
-theorem reverse_cons (x : T) (l : list T) : reverse (x :: l) = append x (reverse l) := refl _
+theorem reverse_cons {x : T} {l : list T} : reverse (x :: l) = append x (reverse l)
 
-theorem reverse_singleton (x : T) : reverse [x] = [x] := refl _
+theorem reverse_singleton {x : T} : reverse [x] = [x]
 
-theorem reverse_concat (s t : list T) : reverse (s ++ t) = (reverse t) ++ (reverse s) :=
+theorem reverse_concat {s t : list T} : reverse (s ++ t) = (reverse t) ++ (reverse s) :=
-list_induction_on s (symm (concat_nil _))
+list_induction_on s (concat_nil⁻¹)
   (take x s,
     assume IH : reverse (s ++ t) = concat (reverse t) (reverse s),
     calc
-      reverse ((x :: s) ++ t) = reverse (s ++ t) ++ [x] : refl _
+      reverse ((x :: s) ++ t) = reverse (s ++ t) ++ [x] : rfl
-        ... = reverse t ++ reverse s ++ [x] : {IH}
+        ... = reverse t ++ reverse s ++ [x]             : {IH}
-        ... = reverse t ++ (reverse s ++ [x]) : concat_assoc _ _ _
+        ... = reverse t ++ (reverse s ++ [x])           : concat_assoc
-        ... = reverse t ++ (reverse (x :: s)) : refl _)
+        ... = reverse t ++ (reverse (x :: s))           : rfl)
 
-theorem reverse_reverse (l : list T) : reverse (reverse l) = l :=
+theorem reverse_reverse {l : list T} : reverse (reverse l) = l :=
-list_induction_on l (refl _)
+list_induction_on l rfl
   (take x l',
     assume H: reverse (reverse l') = l',
     show reverse (reverse (x :: l')) = x :: l', from
       calc
-        reverse (reverse (x :: l')) = reverse (reverse l' ++ [x]) : refl _
+        reverse (reverse (x :: l')) = reverse (reverse l' ++ [x]) : rfl
-          ... = reverse [x] ++ reverse (reverse l') : reverse_concat _ _
+          ... = reverse [x] ++ reverse (reverse l')               : reverse_concat
-          ... = [x] ++ l' : { H }
+          ... = [x] ++ l'                                         : {H}
-          ... = x :: l' : refl _)
+          ... = x :: l'                                           : rfl)
 
-theorem append_eq_reverse_cons  (x : T) (l : list T) : append x l = reverse (x :: reverse l) :=
+theorem append_eq_reverse_cons  {x : T} {l : list T} : append x l = reverse (x :: reverse l) :=
-list_induction_on l (refl _)
+list_induction_on l rfl
   (take y l',
     assume H : append x l' = reverse (x :: reverse l'),
     calc
-      append x (y :: l') = (y :: l') ++ [ x ] : append_eq_concat _ _
+      append x (y :: l') = (y :: l') ++ [ x ]            : append_eq_concat
-        ... = concat (reverse (reverse (y :: l'))) [ x ] : {symm (reverse_reverse _)}
+        ... = concat (reverse (reverse (y :: l'))) [ x ] : {reverse_reverse⁻¹}
-        ... = reverse (x :: (reverse (y :: l'))) : refl _)
+        ... = reverse (x :: (reverse (y :: l')))         : rfl)
 
 
 -- Head and tail
 -- -------------
 
-definition head (x0 : T) : list T → T := list_rec x0 (fun x l h, x)
+definition head (x : T) : list T → T := list_rec x (fun x l h, x)
 
-theorem head_nil (x0 : T) : head x0 (@nil T) = x0 := refl _
+theorem head_nil {x : T} : head x (@nil T) = x
 
-theorem head_cons (x : T) (x0 : T) (t : list T) : head x0 (x :: t) = x := refl _
+theorem head_cons {x x' : T} {t : list T} : head x' (x :: t) = x
 
-theorem head_concat (s t : list T) (x0 : T) : s ≠ nil → (head x0 (s ++ t) = head x0 s) :=
+theorem head_concat {s t : list T} {x : T} : s ≠ nil → (head x (s ++ t) = head x s) :=
 list_cases_on s
-  (take H : nil ≠ nil, absurd (refl nil) H)
+  (take H : nil ≠ nil, absurd rfl H)
-  (take x s,
+  (take x s, take H : cons x s ≠ nil,
-    take H : cons x s ≠ nil,
     calc
-      head x0 (concat (cons x s) t) = head x0 (cons x (concat s t)) : {cons_concat _ _ _}
+      head x (concat (cons x s) t) = head x (cons x (concat s t)) : {cons_concat}
-        ... = x : {head_cons _ _ _}
+        ... = x                                                   : {head_cons}
-        ... = head x0 (cons x s) : {symm ( head_cons x x0 s)})
+        ... = head x (cons x s)                                   : {head_cons⁻¹})
 
 definition tail : list T → list T := list_rec nil (fun x l b, l)
 
-theorem tail_nil : tail (@nil T) = nil := refl _
+theorem tail_nil : tail (@nil T) = nil
 
-theorem tail_cons (x : T) (l : list T) : tail (cons x l) = l := refl _
+theorem tail_cons {x : T} {l : list T} : tail (cons x l) = l
 
-theorem cons_head_tail (x0 : T) (l : list T) : l ≠ nil → (head x0 l) :: (tail l) = l :=
+theorem cons_head_tail {x : T} {l : list T} : l ≠ nil → (head x l) :: (tail l) = l :=
 list_cases_on l
-  (assume H : nil ≠ nil, absurd (refl _) H)
+  (assume H : nil ≠ nil, absurd rfl H)
-  (take x l, assume H : cons x l ≠ nil, refl _)
+  (take x l, assume H : cons x l ≠ nil, rfl)
-
 
 -- List membership
 -- ---------------
@@ -192,11 +187,11 @@ definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨
 infix `∈` := mem
 
 -- TODO: constructively, equality is stronger. Use that?
-theorem mem_nil (x : T) : x ∈ nil ↔ false := iff_refl _
+theorem mem_nil {x : T} : x ∈ nil ↔ false := iff_rfl
 
-theorem mem_cons (x : T) (y : T) (l : list T) : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff_refl _
+theorem mem_cons {x y : T} {l : list T} : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff_rfl
 
-theorem mem_concat_imp_or (x : T) (s t : list T) : x ∈ s ++ t → x ∈ s ∨ x ∈ t :=
+theorem mem_concat_imp_or {x : T} {s t : list T} : x ∈ s ++ t → x ∈ s ∨ x ∈ t :=
 list_induction_on s or_inr
   (take y s,
     assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t,
@@ -205,9 +200,9 @@ list_induction_on s or_inr
     have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or_imp_or_right H2 IH,
     iff_elim_right or_assoc H3)
 
-theorem mem_or_imp_concat (x : T) (s t : list T) : x ∈ s ∨ x ∈ t → x ∈ s ++ t :=
+theorem mem_or_imp_concat {x : T} {s t : list T} : x ∈ s ∨ x ∈ t → x ∈ s ++ t :=
 list_induction_on s
-  (take H, or_elim H (false_elim _) (assume H, H))
+  (take H, or_elim H false_elim (assume H, H))
   (take y s,
     assume IH : x ∈ s ∨ x ∈ t → x ∈ s ++ t,
     assume H : x ∈ y :: s ∨ x ∈ t,
@@ -218,24 +213,24 @@ list_induction_on s
             (take H2 : x ∈ s, or_inr (IH (or_inl H2))))
         (assume H1 : x ∈ t, or_inr (IH (or_inr H1))))
 
-theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t
+theorem mem_concat {x : T} {s t : list T} : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t
-:= iff_intro (mem_concat_imp_or _ _ _) (mem_or_imp_concat _ _ _)
+:= iff_intro mem_concat_imp_or mem_or_imp_concat
 
-theorem mem_split (x : T) (l : list T) : x ∈ l → ∃s t : list T, l = s ++ (x :: t) :=
+theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x :: t) :=
 list_induction_on l
-  (take H : x ∈ nil, false_elim _ (iff_elim_left (mem_nil x) H))
+  (take H : x ∈ nil, false_elim (iff_elim_left mem_nil H))
   (take y l,
     assume IH : x ∈ l → ∃s t : list T, l = s ++ (x :: t),
     assume H : x ∈ y :: l,
     or_elim H
       (assume H1 : x = y,
         exists_intro nil
-          (exists_intro l (subst H1 (refl _))))
+          (exists_intro l (subst H1 rfl)))
       (assume H1 : x ∈ l,
         obtain s (H2 : ∃t : list T, l = s ++ (x :: t)), from IH H1,
         obtain t (H3 : l = s ++ (x :: t)), from H2,
         have H4 : y :: l = (y :: s) ++ (x :: t),
-          from subst H3 (refl (y :: l)),
+          from subst H3 rfl,
         exists_intro _ (exists_intro _ H4)))
 
 -- Find
@@ -276,12 +271,12 @@ list_induction_on l
 -- nth element
 -- -----------
 
-definition nth (x0 : T) (l : list T) (n : ℕ) : T :=
+definition nth (x : T) (l : list T) (n : ℕ) : T :=
-nat_rec (λl, head x0 l) (λm f l, f (tail l)) n l
+nat_rec (λl, head x l) (λm f l, f (tail l)) n l
 
-theorem nth_zero (x0 : T) (l : list T) : nth x0 l 0 = head x0 l := refl _
+theorem nth_zero {x : T} {l : list T} : nth x l 0 = head x l
 
-theorem nth_succ (x0 : T) (l : list T) (n : ℕ) : nth x0 l (succ n) = nth x0 (tail l) n := refl _
+theorem nth_succ {x : T} {l : list T} {n : ℕ} : nth x l (succ n) = nth x (tail l) n
 
 end
 

library/data/sigma.lean

@@ -28,7 +28,7 @@ section
   sigma_rec H p
 
   theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
-  sigma_destruct p (take a b, refl _)
+  sigma_destruct p (take a b, rfl)
 
   -- Note that we give the general statment explicitly, to help the unifier
   theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2) :

library/data/sum.lean

@@ -71,13 +71,13 @@ rec_on s1
       (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
       (take b2,
         have H3 : (inl B a1 = inr A b2) ↔ false,
-          from iff_intro inl_neq_inr (assume H4, false_elim _ H4),
+          from iff_intro inl_neq_inr (assume H4, false_elim H4),
         show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3)))
   (take b1, show decidable (inr A b1 = s2), from
     rec_on s2
       (take a2,
         have H3 : (inr A b1 = inl B a2) ↔ false,
-          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4),
+          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim H4),
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 

library/data/unit.lean

@@ -16,6 +16,9 @@ notation `⋆`:max := star
 theorem unit_eq (a b : unit) : a = b :=
 unit_rec (unit_rec (refl ⋆) b) a
 
+theorem unit_eq_star (a : unit) : a = star :=
+unit_eq a star
+
 theorem unit_inhabited [instance] : inhabited unit :=
 inhabited_mk ⋆
 

library/logic/axioms/classical.lean

@@ -35,9 +35,9 @@ theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
 or_elim (prop_complete a)
   (assume Hat,  or_elim (prop_complete b)
     (assume Hbt,  Hat ⬝ Hbt⁻¹)
-    (assume Hbf, false_elim (a = b) (Hbf ▸ (Hab (eq_true_elim Hat)))))
+    (assume Hbf, false_elim (Hbf ▸ (Hab (eq_true_elim Hat)))))
   (assume Haf, or_elim (prop_complete b)
-    (assume Hbt,  false_elim (a = b) (Haf ▸ (Hba (eq_true_elim Hbt))))
+    (assume Hbt,  false_elim (Haf ▸ (Hba (eq_true_elim Hbt))))
     (assume Hbf, Haf ⬝ Hbf⁻¹))
 
 theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=

library/logic/classes/decidable.lean

@@ -44,7 +44,7 @@ or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
 theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
 or_elim (em p)
   (assume H1 : p, H1)
-  (assume H1 : ¬p, false_elim p (H H1))
+  (assume H1 : ¬p, false_elim (H H1))
 
 theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ∧ b) :=

library/logic/core/identities.lean

@@ -47,7 +47,7 @@ theorem not_not_elim {a : Prop} {D : decidable a} (H : ¬¬a) : a :=
 iff_mp not_not_iff H
 
 theorem not_true : (¬true) ↔ false :=
-iff_intro (assume H, H trivial) (false_elim _)
+iff_intro (assume H, H trivial) false_elim
 
 theorem not_false : (¬false) ↔ true :=
 iff_intro (assume H, trivial) (assume H H', H')
@@ -117,12 +117,12 @@ iff_intro
 theorem iff_false_intro {a : Prop} (H : ¬a) : a ↔ false :=
 iff_intro
   (assume H1 : a,     absurd H1 H)
-  (assume H2 : false, false_elim a H2)
+  (assume H2 : false, false_elim H2)
 
 theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false :=
 iff_intro
   (assume H, a_neq_a_elim H)
-  (assume H, false_elim (a ≠ a) H)
+  (assume H, false_elim H)
 
 theorem eq_id {A : Type} (a : A) : (a = a) ↔ true :=
 iff_true_intro (refl a)
@@ -135,7 +135,7 @@ iff_intro
   (assume H,
     have H' : ¬a, from assume Ha, (H ▸ Ha) Ha,
     H' (H⁻¹ ▸ H'))
-  (assume H, false_elim (a ↔ ¬a) H)
+  (assume H, false_elim H)
 
 theorem true_eq_false : (true ↔ false) ↔ false :=
 not_true ▸ (a_iff_not_a true)

library/logic/core/prop.lean

@@ -18,7 +18,7 @@ abbreviation imp (a b : Prop) : Prop := a → b
 
 inductive false : Prop
 
-theorem false_elim (c : Prop) (H : false) : c :=
+theorem false_elim {c : Prop} (H : false) : c :=
 false_rec c H
 
 inductive true : Prop :=
@@ -36,7 +36,7 @@ theorem not_intro {a : Prop} (H : a → false) : ¬a := H
 theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
 
 theorem absurd {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
-false_elim b (H2 H1)
+false_elim (H2 H1)
 
 theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna

tests/lean/run/sum_bug.lean

@@ -57,13 +57,13 @@ rec_on s1
       (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
       (take b2,
         have H3 : (inl B a1 = inr A b2) ↔ false,
-          from iff_intro inl_neq_inr (assume H4, false_elim _ H4),
+          from iff_intro inl_neq_inr (assume H4, false_elim H4),
         show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3)))
   (take b1, show decidable (inr A b1 = s2), from
     rec_on s2
       (take a2,
         have H3 : (inr A b1 = inl B a2) ↔ false,
-          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4),
+          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim H4),
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))