From 3fbf5acbee93c567a166150c710702fedc59a3da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Jan 2022 17:12:55 -0800
Subject: [PATCH] fix: add missing `[reducible]` annotations `Init/WF.lean`

---
 src/Init/WF.lean        | 10 +++++-----
 src/Init/WFTactics.lean |  2 +-
 tests/lean/run/879.lean | 16 +++++++++++++++-
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index dfce2ae3fc..81b48fa3a2 100644
--- a/src/Init/WF.lean
+++ b/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
 
diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index a6bd3344ee..b2738abb84 100644
--- a/src/Init/WFTactics.lean
+++ 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
diff --git a/tests/lean/run/879.lean b/tests/lean/run/879.lean
index 9c30e349e4..c7fbf89a02 100644
--- a/tests/lean/run/879.lean
+++ b/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