More test fixing and updating

src/Lean/Elab/LetRec.lean

@@ -60,7 +60,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         pure decl[4]
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
-      let termination := WF.elabTerminationHints ⟨decl[5]⟩
+      -- TODO: Is this right?
+      let termination := WF.elabTerminationHints ⟨attrDeclStx[3]⟩
       pure {
         ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx, termination : LetRecDeclView }
     else

tests/lean/1050.lean.expected.out

@@ -1,4 +1,4 @@
-1050.lean:7:2-18:21: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
+1050.lean:7:2-18:5: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
   Foo as bs → bs : Type (u + 1)
 and for `Foo.bar_aux` is
   bs : Type u

tests/lean/StxQuot.lean.expected.out

@@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
 StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  (Termination.suffix [] [])))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   (Termination.suffix [] [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   (Termination.suffix [] [])))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
 "(«term_+_» (num \"2\") \"+\" (num \"1\"))"
 "(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))"
-"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
-"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))]"
+"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  (Termination.suffix [] [])))"
+"[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   (Termination.suffix [] [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   (Termination.suffix [] [])))]"
 "0"
 0
 1

tests/lean/guessLexFailures.lean

@@ -99,7 +99,7 @@ namespace TrickyCode
 def FinPlus1 n := Fin (n + 1)
 def badCasesOn (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n (.succ m)))
--- termination_by badCasesOn n m => n
+-- termination_by n m => n
 decreasing_by decreasing_tactic
 
 
@@ -109,7 +109,7 @@ decreasing_by decreasing_tactic
 -- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
 def badCasesOn2 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn2 n (.succ m)))
-termination_by badCasesOn2 n m => n
+termination_by n m => n
 decreasing_by decreasing_tactic
 
 -- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
@@ -119,15 +119,15 @@ def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) :=
 def badCasesOn3 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
       (Fin_succ_comp (fun n => badCasesOn3 n (.succ m)))
--- termination_by badCasesOn3 n m => n
+-- termination_by n m => n
 decreasing_by decreasing_tactic
 
 
 -- Same test, explicit termination_by
 def badCasesOn4 (n m : Nat) : Fin (n + 1) :=
    Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
       (Fin_succ_comp (fun n => badCasesOn4 n (.succ m)))
-termination_by badCasesOn4 n m => n
+termination_by n m => n
 decreasing_by decreasing_tactic
 
 end TrickyCode

tests/lean/guessLexTricky.lean

@@ -39,15 +39,32 @@ macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
 mutual
 def prod (x y z : Nat) : Nat :=
   if y % 2 = 0 then eprod x y z else oprod x y z
+decreasing_by
+  -- TODO: Why does it not work to wrap it all in `all_goals`?
+  all_goals simp_wf
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+  · search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
+
 def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
+decreasing_by
+  simp_wf
+  search_lex solve
+    | decreasing_trivial
+    | apply Nat.bitwise_rec_lemma; assumption
+
 def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
-end
--- termination_by
---   prod x y z => (y, 2)
---   oprod x y z => (y, 1)
---   eprod x y z => (y, 0)
 decreasing_by
   simp_wf
   search_lex solve
     | decreasing_trivial
     | apply Nat.bitwise_rec_lemma; assumption
+
+end
+-- termination_by
+--   prod x y z => (y, 2)
+--   oprod x y z => (y, 1)
+--   eprod x y z => (y, 0)

tests/lean/heapSort.lean

@@ -168,9 +168,9 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
       have : a.popMax.size < a.size := by
         simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
+    termination_by _ => a.size
+    decreasing_by assumption
   loop (a.toBinaryHeap gt) #[]
-termination_by _ => a.size
-decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
 #check Array.heapSort.loop._eq_1

tests/lean/interactive/hover.lean

@@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
       --^ textDocument/hover
 
 def g (n : Nat) : Nat := g 0
-termination_by g n => n
+termination_by n => n
 decreasing_by have n' := n; admit
                        --^ textDocument/hover
 

tests/lean/letRecMissingAnnotation.lean

@@ -4,5 +4,6 @@ def sum (as : Array Nat) : Nat :=
       go (i+2) (s + as.get ⟨i, h⟩) -- Error
     else
       s
+    -- TODO: lifted variable not in scope?
+    termination_by go i _ => as.size - i
   go 0 0
-termination_by go i _ => as.size - i

tests/lean/mutwf1.lean

@@ -4,24 +4,24 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g n
+  termination_by n b => (n, if b then 2 else 1)
+  decreasing_by
+  all_goals simp_wf
+  · apply Prod.Lex.right; decide
+  · apply Prod.Lex.right; decide
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
-end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n => (n, 0)
-decreasing_by
-  simp_wf
-  first
-  | apply Prod.Lex.left
-    apply Nat.pred_lt
-  | apply Prod.Lex.right
-    decide
+  termination_by n => (n, 0)
+  decreasing_by
+  all_goals simp_wf
+  apply Prod.Lex.left
+  apply Nat.pred_lt
   done -- should fail
+end
 end Ex1
 
 
@@ -31,14 +31,13 @@ mutual
     | n, true  => 2 * f n false
     | 0, false => 1
     | n, false => n + g (n+1) -- Error
+  termination_by n b => (n, if b then 2 else 1)
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then
       f (n-1) true
     else
       n
+  termination_by n => (n, 0)
 end
-termination_by
-  f n b => (n, if b then 2 else 1)
-  g n   => (n, 0)
 end Ex2

tests/lean/mutwf1.lean.expected.out

@@ -1,4 +1,4 @@
-mutwf1.lean:24:2-24:6: error: unsolved goals
+mutwf1.lean:23:2-23:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0

tests/lean/run/1171.lean

@@ -6,7 +6,7 @@ def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b)
   match h:hasDecEq n m with -- it works without `h:`
   | isTrue heq => isTrue  (heq ▸ rfl)
   | isFalse hne => isFalse (Nat.noConfusion · (λ heq  => absurd heq hne))
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)
 
 set_option pp.proofs true
 #print Nat.hasDecEq

tests/lean/run/1848.lean

@@ -1,11 +1,11 @@
 abbrev f : Nat → Nat
   | 0 => 0
   | n + 1 => f n
-termination_by _ n => n
+termination_by n => n
 
 mutual
 abbrev f1 : Nat → Nat
   | 0 => 0
   | n + 1 => f1 n
+termination_by n => n
 end
-termination_by _ n => n

tests/lean/run/2810.lean

@@ -19,7 +19,7 @@ def f3 (n : Nat) : Nat :=
   match n with
   | 0 => 0
   | n + 1 => (f3) n
-termination_by f3 n => n
+termination_by n => n
 
 -- Same with rewrite
 

tests/lean/run/860.lean

@@ -13,17 +13,19 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
     · apply Nat.zero_lt_succ
 
 def pack (n: Nat) : List Nat :=
-  let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
-    let next (n: Nat) := n / 2;
-    match n with
-    | Nat.zero => List.cons acc accs
-    | n+1 => match evenq n with
-      | true => loop (next n) 0 (List.cons acc accs)
-      | false => loop (next n) (acc+1) accs
+  let rec
+    loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
+      let next (n: Nat) := n / 2;
+      match n with
+      | Nat.zero => List.cons acc accs
+      | n+1 => match evenq n with
+        | true => loop (next n) 0 (List.cons acc accs)
+        | false => loop (next n) (acc+1) accs
+    termination_by n _ _ => n
+    decreasing_by all_goals
+      simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
+      apply pack_loop_terminates
+
   loop n 0 []
-termination_by _ n _ _ => n
-decreasing_by
-  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
-  apply pack_loop_terminates
 
 #eval pack 27

tests/lean/run/879.lean

@@ -5,13 +5,9 @@ termination_by _ => b
 
 def foo2 (b c : Nat) := if h : b = 0 then a + c else foo2 (b - 1) c
 termination_by
-  foo2 x y z => y
-
-def foo3 (b c : Nat) := if h : b = 0 then a + c else foo3 (b - 1) c
-termination_by
-  _ x y z => y
+  x y z => y
 
 def foo4 (b c : Nat) := if h : b = 0 then a + c else foo4 (b - 1) c
 termination_by
   -- We can rename from right to left
-  foo4 y _ => y
+  y _ => y

tests/lean/run/955.lean

@@ -3,11 +3,15 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  termination_by n =>
+    match n with
+    | _ => n
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  termination_by n =>
+    match n with
+    | _ => n
 end
-termination_by _ n =>
-  match n with
-  | _ => n
 end Ex2

tests/lean/run/ack.lean

@@ -2,4 +2,4 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by _ a b => (a, b)
+termination_by a b => (a, b)

tests/lean/run/addDecorationsWithoutPartial.lean

@@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
       let rest := Expr.forallE name newType newBody data
       some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
     | _ => none
-decreasing_by exact Nat.le_trans (by simp_arith) h
+decreasing_by all_goals exact Nat.le_trans (by simp_arith) h

tests/lean/run/binrec.lean

@@ -44,8 +44,8 @@ def Nat.binrec
     bit_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
   else
     bit_div_odd h₂ ▸ ind true  (n / 2) (fun _ => binrec motive base ind (n / 2))
-termination_by _ n => n
-decreasing_by exact Nat.div2_lt h₁
+termination_by n => n
+decreasing_by all_goals exact Nat.div2_lt h₁
 
 theorem Nat.binind
     (motive : Nat → Prop)

tests/lean/run/constProp.lean

@@ -397,7 +397,7 @@ def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.leng
     match σ₂.find? x with
     | some w => if v = w then (x, v) :: join σ₁' σ₂ else join σ₁' σ₂
     | none => join σ₁' σ₂
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 local notation "⊥" => []
 
@@ -468,7 +468,7 @@ theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ :=
       next => apply cons_le_cons; apply le_trans ih (erase_le _)
       next => apply le_trans ih (erase_le_cons (le_refl _))
     next h => apply le_trans ih (erase_le_cons (le_refl _))
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ :=
   le_trans (join_le_left σ₁ σ₃) h
@@ -485,7 +485,7 @@ theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ :
       split <;> simp [*]
       next => apply cons_le_of_eq ih h
     next h => assumption
-termination_by _ σ₁ _ => σ₁.length
+termination_by σ₁ _ => σ₁.length
 
 theorem State.join_le_right_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₃.join σ₁ ≼ σ₂ :=
   le_trans (join_le_right σ₃ σ₁) h

tests/lean/run/decreasingTacticUpdatedEnvIssue.lean

@@ -21,4 +21,4 @@ def f (x : Nat) : Nat :=
     1
   else
     f (g x (x > 0)) + 2
-termination_by f x => x
+termination_by x => x

tests/lean/run/defaultEliminator.lean

@@ -9,16 +9,16 @@
     | x+1, 0   => succ_zero x (go x 0)
     | 0,   y+1 => zero_succ y (go 0 y)
     | x+1, y+1 => succ_succ x y (go x y)
+    termination_by x y => (x, y)
   go x y
-termination_by go x y => (x, y)
 
 def f (x y : Nat) :=
   match x, y with
   | 0,   0   => 1
   | x+1, 0   => f x 0
   | 0,   y+1 => f 0 y
   | x+1, y+1 => f x y
-termination_by f x y => (x, y)
+termination_by x y => (x, y)
 
 example (x y : Nat) : f x y > 0 := by
   induction x, y with

tests/lean/run/eqnsAtSimp.lean

@@ -2,13 +2,17 @@ mutual
   def isEven : Nat → Bool
     | 0 => true
     | n+1 => isOdd n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
+
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
+  decreasing_by
+    simp [measure, invImage, InvImage, Nat.lt_wfRel]
+    apply Nat.lt_succ_self
 end
-decreasing_by
-  simp [measure, invImage, InvImage, Nat.lt_wfRel]
-  apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with