feat(tactic/tauto): add an option for tauto to work in classical logic

tactic/basic.lean

@@ -461,7 +461,7 @@ meta def apply_assumption
   (asms : tactic (list expr) := local_context)
   (tac : tactic unit := skip) : tactic unit :=
 do { ctx ← asms,
-     ctx.any_of (λ H, symm_apply H >> tac) } <|> 
+     ctx.any_of (λ H, symm_apply H >> tac) } <|>
 do { exfalso,
      ctx ← asms,
      ctx.any_of (λ H, symm_apply H >> tac) }
@@ -633,4 +633,9 @@ instance : monad id :=
      let out := format.to_string format!"{{ {format.join fs} }",
      return [(out,"")] }
 
+meta def classical : tactic unit :=
+do h ← get_unused_name `_inst,
+   mk_const `classical.prop_decidable >>= note h none,
+   reset_instance_cache
+
 end tactic

tactic/interactive.lean

@@ -269,10 +269,13 @@ do asms ← mk_assumption_set no_dflt hs attr_names,
 and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
 using `reflexivity` or `solve_by_elim`
 -/
-meta def tautology := tactic.tautology
+meta def tautology (c : parse $ (tk "!")?) := tactic.tautology c.is_some
 
 /-- Shorter name for the tactic `tautology`. -/
-meta def tauto := tautology
+meta def tauto (c : parse $ (tk "!")?) := tautology c
+
+/-- Make every propositions in the context decidable -/
+meta def classical := tactic.classical
 
 private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
 | (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x)

tactic/tauto.lean

@@ -176,26 +176,27 @@ do { ctx ← local_context,
 meta def assumption_symm :=
 using_new_ref (native.rb_map.mk _ _) assumption_with
 
-meta def tautology : tactic unit :=
-using_new_ref (expr_map.mk _) $ λ r,
-do try (contradiction_with r);
-   try (assumption_with r);
-   repeat (do
-     gs ← get_goals,
-     () <$ tactic.intros;
-     distrib_not;
-     casesm (some ()) [``(_ ∧ _),``(_ ∨ _),``(Exists _),``(false)];
-     try (contradiction_with r);
-     try (target >>= match_or >> refine ``( or_iff_not_imp_left.mpr _));
-     try (target >>= match_or >> refine ``( or_iff_not_imp_right.mpr _));
-     () <$ tactic.intros;
-     constructor_matching (some ()) [``(_ ∧ _),``(_ ↔ _),``(true)];
-     try (assumption_with r),
-     gs' ← get_goals,
-     guard (gs ≠ gs') ) ;
-   repeat
-   (reflexivity <|> solve_by_elim <|>
-    constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _),``(true)] ) ;
-   done
+meta def tautology (c : bool) : tactic unit :=
+do classical,
+   using_new_ref (expr_map.mk _) $ λ r,
+   do try (contradiction_with r);
+      try (assumption_with r);
+      repeat (do
+        gs ← get_goals,
+        () <$ tactic.intros;
+        distrib_not;
+        casesm (some ()) [``(_ ∧ _),``(_ ∨ _),``(Exists _),``(false)];
+        try (contradiction_with r);
+        try (target >>= match_or >> refine ``( or_iff_not_imp_left.mpr _));
+        try (target >>= match_or >> refine ``( or_iff_not_imp_right.mpr _));
+        () <$ tactic.intros;
+        constructor_matching (some ()) [``(_ ∧ _),``(_ ↔ _),``(true)];
+        try (assumption_with r),
+        gs' ← get_goals,
+        guard (gs ≠ gs') ) ;
+      repeat
+      (reflexivity <|> solve_by_elim <|>
+       constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _),``(true)] ) ;
+      done
 
 end tactic