feat(tactic/terminal_goal): determine if other goals depend on the cu…

…rrent one (#984)

* feat(tactics): add "terminal_goal" tactic and relatives

* fix(test/tactics): renaming test functions to avoid a name collision

* fix(tactic): moving terminal_goal to tactic/basic.lean

* fix(test/tactics): open tactics

* touching a file, to prompt travis to try again

* terminal_goal

* fix

* merge

src/tactic/core.lean

@@ -549,6 +549,28 @@ do goals ← get_goals,
    p ← is_proof goals.head,
    guard p
 
+/-- Succeeds only if we can construct an instance showing the
+    current goal is a subsingleton type. -/
+meta def subsingleton_goal : tactic unit :=
+do goals ← get_goals,
+   ty ← infer_type goals.head >>= instantiate_mvars,
+   to_expr ``(subsingleton %%ty) >>= mk_instance >> skip
+
+/-- Succeeds only if the current goal is "terminal", in the sense
+    that no other goals depend on it. -/
+meta def terminal_goal : tactic unit :=
+-- We can't merely test for subsingletons, as sometimes in the presence of metavariables
+-- `propositional_goal` succeeds while `subsingleton_goal` does not.
+propositional_goal <|> subsingleton_goal <|>
+do g₀ :: _ ← get_goals,
+   mvars ← (λ L, list.erase L g₀) <$> metavariables,
+   mvars.mmap' $ λ g, do
+     t ← infer_type g >>= instantiate_mvars,
+     d ← kdepends_on t g₀,
+     monad.whenb d $
+       pp t >>= λ s, fail ("The current goal is not terminal: " ++ s.to_string ++ " depends on it.")
+
+
 meta def triv' : tactic unit := do c ← mk_const `trivial, exact c reducible
 
 variable {α : Type}

test/terminal_goal.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import tactic.core
+
+open tactic
+
+structure C :=
+ ( w : Type )
+ ( x : list w )
+ ( y : Type )
+ ( z : prod w y )
+
+def test_terminal_goal_1 : C :=
+ begin
+    fapply C.mk, -- We don't just split here, as we want the goals in order.
+    success_if_fail { tactic.terminal_goal },
+    exact ℕ,
+    terminal_goal,
+    exact [],
+    success_if_fail { terminal_goal },
+    exact bool,
+    terminal_goal,
+    exact (0, tt)
+ end
+
+ -- verifying that terminal_goal correctly considers all propositional goals as terminal
+structure terminal_goal_struct :=
+(x : ℕ)
+(p : x = 0)
+
+lemma test_terminal_goal_2 : ∃ F : terminal_goal_struct, F = ⟨ 0, by refl ⟩ :=
+begin
+  split,
+  swap,
+  split,
+  terminal_goal,
+  swap,
+  success_if_fail { terminal_goal },
+  exact 0,
+  refl,
+  refl,
+end
+
+structure terminal_goal_struct' :=
+ ( w : ℕ → Type )
+ ( x : list (w 0) )
+
+def test_terminal_goal_3 : terminal_goal_struct' :=
+begin
+  split,
+  swap,
+  success_if_fail { terminal_goal },
+  intros,
+  success_if_fail { terminal_goal },
+  exact ℕ,
+  exact []
+end
+
+def f : unit → Type := λ _, ℕ
+
+def test_terminal_goal_4 : Σ x : unit, f x :=
+begin
+  split,
+  terminal_goal,
+  swap,
+  terminal_goal,
+  exact (),
+  dsimp [f],
+  exact 0
+end
+
+def test_subsingleton_goal_1 : 0 = 0 :=
+begin
+ subsingleton_goal,
+ refl
+end
+
+def test_subsingleton_goal_2 : list ℕ :=
+begin
+ success_if_fail { subsingleton_goal },
+ exact []
+end