fix: add missing [reducible] annotations Init/WF.lean

src/Init/WF.lean

@@ -128,7 +128,7 @@ def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
-def invImage (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α where
+@[reducible] def invImage (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α where
   rel := InvImage h.rel f
   wf  := InvImage.wf f h.wf
 
@@ -171,13 +171,13 @@ def Nat.lt_wfRel : WellFoundedRelation Nat where
 def Measure {α : Sort u} : (α → Nat) → α → α → Prop :=
   InvImage (fun a b => a < b)
 
-def measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
+abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
   invImage f Nat.lt_wfRel
 
 def SizeOfRef (α : Sort u) [SizeOf α] : α → α → Prop :=
   Measure sizeOf
 
-def sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
+abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
   measure sizeOf
 
 instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
@@ -218,7 +218,7 @@ def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a
       | right _ h   => apply ihb _ h
 
 -- The lexicographical order of well founded relations is well-founded
-def lex (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
+@[reducible] def lex (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
   rel := Lex ha.rel hb.rel
   wf  := ⟨fun (a, b) => lexAccessible (WellFounded.apply ha.wf) (WellFounded.apply hb.wf) a b⟩
 
@@ -270,7 +270,7 @@ def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b
       | right => apply ihb; assumption
 
 -- The lexicographical order of well founded relations is well-founded
-def lex (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) : WellFoundedRelation (PSigma β) where
+@[reducible] def lex (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) : WellFoundedRelation (PSigma β) where
   rel := Lex ha.rel (fun a => hb a |>.rel)
   wf  := WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha.wf a) (fun a => hb a |>.wf) b
 

src/Init/WFTactics.lean

@@ -8,7 +8,7 @@ import Init.SizeOf
 import Init.WF
 
 macro "decreasing_tactic" : tactic =>
- `((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel];
+ `((simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, sizeOf, WellFoundedRelation.rel];
     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     first

tests/lean/run/879.lean

@@ -1,3 +1,17 @@
 variable (a : Nat)
-def foo (b c : Nat) := if h : b = 0 then a + c else foo (b - 1) c
+
+def foo1 (b c : Nat) := if h : b = 0 then a + c else foo1 (b - 1) c
 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
+
+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