feat(init/meta/tactic): by_contradiction tweaks (#491)

This adds support for classical `by_contradiction`, as well as always using
`intro` instead of `intro1` (which picks up the binder variable of `not`,
which is never meaningful), instead using `h` as default name.

library/init/meta/interactive.lean

@@ -1577,15 +1577,17 @@ meta def funext : parse ident_* → tactic unit
 | hs := funext_lst hs >> skip
 
 /--
-If the target of the main goal is a proposition `p`, `by_contradiction h` reduces the goal to proving `false` using the additional hypothesis `h : ¬ p`. If `h` is omitted, a name is generated automatically.
+If the target of the main goal is a proposition `p`, `by_contradiction` reduces the goal to proving `false` using the additional hypothesis `h : ¬ p`. `by_contradiction h` can be used to name the hypothesis `h : ¬ p`.
 
-This tactic requires that `p` is decidable. To ensure that all propositions are decidable via classical reasoning, use  `local attribute [instance] classical.prop_decidable`.
+This tactic will attempt to use decidability of `p` if available, and will otherwise fall back on classical reasoning.
 -/
 meta def by_contradiction (n : parse ident?) : tactic unit :=
-tactic.by_contradiction n >> return ()
+tactic.by_contradiction (n.get_or_else `h) $> ()
 
 /--
-An abbreviation for `by_contradiction`.
+If the target of the main goal is a proposition `p`, `by_contra` reduces the goal to proving `false` using the additional hypothesis `h : ¬ p`. `by_contra h` can be used to name the hypothesis `h : ¬ p`.
+
+This tactic will attempt to use decidability of `p` if available, and will otherwise fall back on classical reasoning.
 -/
 meta def by_contra (n : parse ident?) : tactic unit :=
 by_contradiction n

library/init/meta/tactic.lean

@@ -302,7 +302,7 @@ end
 /--
 `resume r` continues execution from a result previously obtained using `capture`.
 
-This is like `unwrap`, but the `tactic_state` is rolled back to point of capture even upon success. 
+This is like `unwrap`, but the `tactic_state` is rolled back to point of capture even upon success.
 -/
 meta def resume {α : Type*} (t : tactic_result α) : tactic α :=
 λ s, t
@@ -1474,17 +1474,13 @@ meta def triv : tactic unit := mk_const `trivial >>= exact
 
 notation `dec_trivial` := of_as_true (by tactic.triv)
 
-meta def by_contradiction (H : option name := none) : tactic expr :=
-do tgt : expr ← target,
-   (match_not tgt >> return ())
-   <|>
-   (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip)
-   <|>
-   fail "tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute [instance] classical.prop_decidable' is used, all propositions are decidable)",
-   match H with
-   | some n := intro n
-   | none   := intro1
-   end
+meta def by_contradiction (H : name) : tactic expr :=
+do tgt ← target,
+  (match_not tgt $> ()) <|>
+  (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip) <|>
+  applyc ``classical.by_contradiction <|>
+  fail "tactic by_contradiction failed, target is not a proposition",
+  intro H
 
 private meta def generalizes_aux (md : transparency) : list expr → tactic unit
 | []      := skip

tests/lean/by_contradiction.lean

@@ -19,16 +19,6 @@ by do
 #print "-------"
 
 example (p q : Prop) : ¬¬ p → p :=
-by do
-  intros,
-  by_contradiction `H, -- should fail
-  trace_state
-
-#print "-------"
-
-local attribute [instance] classical.prop_decidable -- Now all propositions are decidable
-
-example (p q : Prop) : ¬¬p → p :=
 by do
   intros,
   by_contradiction `H,

tests/lean/by_contradiction.lean.expected.out

@@ -8,12 +8,6 @@ a_1 : ¬¬a = b,
 H : ¬a = b
 ⊢ false
 -------
-by_contradiction.lean:22:3: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute [instance] classical.prop_decidable' is used, all propositions are decidable)
-state:
-p q : Prop,
-a : ¬¬p
-⊢ p
--------
 p q : Prop,
 a : ¬¬p,
 H : ¬p