feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof

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

src/builtin/tactic.lua

@@ -25,3 +25,25 @@ tactic_macro("simp", { macro_arg.Ids },
                 return simp_tac(ids)
              end
 )
+
+-- Create a 'bogus' tactic that consume all goals, but it does not create a valid proof.
+-- This tactic is useful for momentarily ignoring/skipping a "hole" in a big proof.
+-- Remark: the kernel will not accept a proof built using this tactic.
+skip_tac = tactic(function (env, ios, s)
+                     local gs      = s:goals()
+                     local pb      = s:proof_builder()
+                     local trivial = mk_constant("trivial")
+                     local new_pb  =
+                        function(m, a)
+                           -- We provide a "fake/incorrect" proof for all goals in gs
+                           local new_m = proof_map(m) -- Copy proof map m
+                           for n, g in gs:pairs() do
+                              new_m:insert(n, trivial)
+                           end
+                           return pb(new_m, a)
+                        end
+                     local new_gs = {}
+                     return  proof_state(s, goals(new_gs), proof_builder(new_pb))
+                  end)
+
+const_tactic("skip", function() return skip_tac end)

tests/lean/j4.lean

@@ -0,0 +1,37 @@
+import macros
+import tactic
+using Nat
+
+definition dvd (a b : Nat) : Bool := ∃ c, a * c = b
+infix 50 | : dvd
+theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b  := H
+theorem dvd_intro {a b : Nat} (c : Nat) (H : a * c = b) : a | b := exists_intro c H
+set_opaque dvd true
+
+
+theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c
+:= obtain (w1 : Nat) (Hw1 : a * w1 = b), from dvd_elim H1,
+   obtain (w2 : Nat) (Hw2 : b * w2 = c), from dvd_elim H2,
+     dvd_intro (w1 * w2)
+       (calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2)
+                       ... = b * w2 : { Hw1 }
+                       ... = c : Hw2)
+
+
+definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p
+
+theorem not_prime_eq (n : Nat) (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n
+:= have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
+     from (not_and _ _ ◂ H2),
+   have H4 : ¬ ¬ n ≥ 2,
+     from by skip, -- Ignore this hole
+   obtain (m : Nat) (H5 :  ¬ (m | n → m = 1 ∨ m = n)),
+     from (not_forall_elim (resolve1 H3 H4)),
+   have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
+     from _,       -- <<< Lean will display the proof state for this hole
+   have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
+     from (not_or (m = 1) (m = n)),
+   have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,
+     from subst H6 H7,
+   show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n,
+     from exists_intro m H8

tests/lean/j4.lean.expected.out

@@ -0,0 +1,27 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'tactic'
+  Using: Nat
+  Defined: dvd
+  Proved: dvd_elim
+  Proved: dvd_intro
+  Proved: dvd_trans
+  Defined: prime
+j4.lean:38:0: error: invalid tactic command, unexpected end of file
+Proof state:
+n :
+    ℕ,
+H1 :
+    n ≥ 2,
+H2 :
+    ¬ prime n,
+H3 :
+    ¬ n ≥ 2 ∨ ¬ (∀ (m : ℕ), m | n → m = 1 ∨ m = n),
+H4 :
+    ¬ ¬ n ≥ 2,
+m :
+    ℕ,
+H5 :
+    ¬ (m | n → m = 1 ∨ m = n)
+⊢ m | n ∧ ¬ (m = 1 ∨ m = n)