feat(well_founded_tactics): patch default_dec_tac (#1419)

* let simp flip inequalities

* feat(well_founded_tactics):  patch default_dec_tac

* Keeley's suggested syntax, and adding to the docs

* more

* add docs

docs/extras/well_founded_recursion.md

@@ -15,7 +15,12 @@ Because < is a well founded relation on naturals, and because `y % succ x < succ
 
 Whenever you use the equation compiler there will be a default well founded relation on the type being recursed on and the equation compiler will automatically attempt to prove the function is well founded.
 
-If the equation compiler fails, there are two main reasons for this. The first is that it has failed to prove the required inequality. The second is that it is not using the correct well founded relation.
+When the equation compiler fails, there are three main causes.
+
+1. It has failed to prove the required inequality.
+2. It is not using the correct well founded relation.
+3. A bug in the default tactic. (Often indicated by the message `nested exception message:
+tactic failed, there are no goals to be solved`, and solved by appending `using_well_founded wf_tacs`.)
 
 ### Proving required inequality ###
 

docs/tactics.md

@@ -1173,3 +1173,10 @@ Lift an expression to another type.
   specify it again as the third argument to `with`, like this: `lift n to ℕ using h with n rfl h`.
 * More generally, this can lift an expression from `α` to `β` assuming that there is an instance
   of `can_lift α β`. In this case the proof obligation is specified by `can_lift.cond`.
+
+### default_dec_tac'
+
+`default_dec_tac'` is a replacement for the core tactic `default_dec_tac`, fixing a bug. This
+bug is often indicated by a message `nested exception message: tactic failed, there are no goals to be solved`,and solved by appending `using_well_founded wf_tacs` to the recursive definition.
+See also additional documentation of `using_well_founded` in
+[docs/extras/well_founded_recursion.md](extras/well_founded_recursion.md).

src/computability/partrec_code.lean

@@ -558,6 +558,7 @@ def evaln : ∀ k : ℕ, code → ℕ → option ℕ
   x ← evaln (k+1) cf (mkpair a m),
   if x = 0 then pure m else
   evaln k (rfind' cf) (mkpair a (m+1)))
+using_well_founded wf_tacs
 
 theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
 | 0     c n x h := by simp [evaln] at h; cases h

src/data/hash_map.lean

@@ -323,7 +323,7 @@ structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
 /-- Construct an empty hash map with buffer size `nbuckets` (default 8). -/
 def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
 let n := if nbuckets = 0 then 8 else nbuckets in
-let nz : n > 0 := by abstract { cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ} in
+let nz : n > 0 := by abstract { cases nbuckets; simp [if_pos, nat.succ_ne_zero] } in
 { hash_fn  := hash_fn,
   size     := 0,
   nbuckets := ⟨n, nz⟩,

src/data/list/basic.lean

@@ -2984,6 +2984,7 @@ theorem erase_diff_erase_sublist_of_sublist {a : α} : ∀ {l₁ l₂ : list α}
 | (b::l₁) l₂ h := if heq : b = a then by simp only [heq, erase_cons_head, diff_cons]
                   else by simpa only [erase_cons_head, erase_cons_tail _ heq, diff_cons, erase_comm a b l₂]
                   using erase_diff_erase_sublist_of_sublist (erase_sublist_erase b h)
+using_well_founded wf_tacs
 
 end diff
 

src/data/list/sort.lean

@@ -168,6 +168,7 @@ def merge : list α → list α → list α
 | []       l'        := l'
 | l        []        := l
 | (a :: l) (b :: l') := if a ≼ b then a :: merge l (b :: l') else b :: merge (a :: l) l'
+using_well_founded wf_tacs
 
 include r
 /-- Implementation of a merge sort algorithm to sort a list. -/
@@ -206,6 +207,7 @@ theorem perm_merge : ∀ (l l' : list α), merge l l' ~ l ++ l'
   { suffices : b :: merge r (a :: l) l' ~ a :: (l ++ b :: l'), {simpa [merge, h]},
     exact (skip _ (perm_merge _ _)).trans ((swap _ _ _).trans (skip _ perm_middle.symm)) }
 end
+using_well_founded wf_tacs
 
 theorem perm_merge_sort : ∀ l : list α, merge_sort l ~ l
 | []        := perm.refl _
@@ -251,6 +253,7 @@ theorem sorted_merge : ∀ {l l' : list α}, sorted r l → sorted r l' → sort
     { exact trans ba (rel_of_sorted_cons h₁ _ bl) },
     { exact rel_of_sorted_cons h₂ _ bl' } }
 end
+using_well_founded wf_tacs
 
 theorem sorted_merge_sort : ∀ l : list α, sorted r (merge_sort l)
 | []        := sorted_nil

src/data/nat/basic.lean

@@ -21,6 +21,8 @@ variables {m n k : ℕ}
 attribute [simp] nat.add_sub_cancel nat.add_sub_cancel_left
 attribute [simp] nat.sub_self
 
+@[simp] lemma succ_pos' {n : ℕ} : 0 < succ n := succ_pos n
+
 theorem succ_inj' {n m : ℕ} : succ n = succ m ↔ n = m :=
 ⟨succ_inj, congr_arg _⟩
 
@@ -689,7 +691,7 @@ protected theorem pow_mul (a b n : ℕ) : n ^ (a * b) = (n ^ a) ^ b :=
 by induction b; simp [*, nat.succ_eq_add_one, nat.pow_add, mul_add, mul_comm]
 
 theorem pow_pos {p : ℕ} (hp : p > 0) : ∀ n : ℕ, p ^ n > 0
-| 0 := by simpa using zero_lt_one
+| 0 := by simp
 | (k+1) := mul_pos (pow_pos _) hp
 
 lemma pow_eq_mul_pow_sub (p : ℕ) {m n : ℕ} (h : m ≤ n) : p ^ m * p ^ (n - m)  = p ^ n :=

src/data/vector2.lean

@@ -36,7 +36,7 @@ theorem nth_eq_nth_le : ∀ (v : vector α n) (i),
   nth v i = v.to_list.nth_le i.1 (by rw to_list_length; exact i.2)
 | ⟨l, h⟩ i := rfl
 
-@[simp] lemma nth_map {β : Type*} (v : vector α n) (f : α → β) (i : fin n) : 
+@[simp] lemma nth_map {β : Type*} (v : vector α n) (f : α → β) (i : fin n) :
   (v.map f).nth i = f (v.nth i) :=
 by simp [nth_eq_nth_le]
 
@@ -115,6 +115,7 @@ def mmap {m} [monad m] {α} {β : Type u} (f : α → m β) :
   ∀ {n}, vector α n → m (vector β n)
 | _ ⟨[], rfl⟩   := pure nil
 | _ ⟨a::l, rfl⟩ := do h' ← f a, t' ← mmap ⟨l, rfl⟩, pure (h' :: t')
+using_well_founded wf_tacs
 
 @[simp] theorem mmap_nil {m} [monad m] {α β} (f : α → m β) :
   mmap f nil = pure nil := rfl

src/set_theory/lists.lean

@@ -240,7 +240,7 @@ local attribute [-simp] add_comm add_assoc
 open well_founded_tactics
 
 theorem sizeof_pos {b} (l : lists' α b) : 0 < sizeof l :=
-by cases l; {unfold_sizeof, trivial_nat_lt}
+by cases l; unfold_sizeof; trivial_nat_lt
 
 theorem lt_sizeof_cons' {b} (a : lists' α b) (l) :
   sizeof (⟨b, a⟩ : lists α) < sizeof (lists'.cons' a l) :=

src/tactic/basic.lean

@@ -20,4 +20,5 @@ import
   tactic.simpa
   tactic.split_ifs
   tactic.squeeze
+  tactic.well_founded_tactics
   tactic.where

src/tactic/well_founded_tactics.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-!
+Replacement for the definition of `well_founded_tactics.default_dec_tac` in core.
+-/
+
+namespace well_founded_tactics
+open tactic
+
+/--
+The definition of `default_dec_tac` in core is broken, because `unfold_sizeof`
+could actually discharge the goal.
+
+Here we add a test using `done` to detect this.
+-/
+meta def default_dec_tac' : tactic unit :=
+abstract $
+do clear_internals,
+   unfold_wf_rel,
+   process_lex (unfold_sizeof >> (done <|> (cancel_nat_add_lt >> trivial_nat_lt)))
+end well_founded_tactics
+
+/--
+The default `well_founded_tactics` provided in core are broken in some situations, often indicated
+by the message
+```
+The nested exception contains the failure state for the decreasing tactic.
+nested exception message:
+tactic failed, there are no goals to be solved
+state:
+no goals
+```
+
+Use this replacement by adding
+```
+using_well_founded wf_tacs
+```
+at the end of your inductive definition.
+-/
+meta def wf_tacs : well_founded_tactics :=
+{ dec_tac := well_founded_tactics.default_dec_tac' }