From 499fc355df8f6bf42e90413b714d96fc42dd2bd2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 May 2017 14:34:52 -0700
Subject: [PATCH] feat(library/init): add has_well_founded type class

---
 library/init/data/sigma/lex.lean |  4 ++++
 library/init/wf.lean             | 17 ++++++++++++++++-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean
index 5f8225223d..cdd4617365 100644
--- a/library/init/data/sigma/lex.lean
+++ b/library/init/data/sigma/lex.lean
@@ -114,4 +114,8 @@ section
                    (a₁ a₂ : α) (h : s b₁ b₂) : skip_left α s (sigma.mk a₁ b₁) (sigma.mk a₂ b₂) :=
   rev_lex.right _ _ _ h
 end
+
+instance has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : ∀ a, has_well_founded (β a)] : has_well_founded (sigma β) :=
+{r := lex s₁.r (λ a, (s₂ a).r), wf := lex_wf s₁.wf (λ a, (s₂ a).wf)}
+
 end sigma
diff --git a/library/init/wf.lean b/library/init/wf.lean
index c9b69edb5b..0e288cab61 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -22,6 +22,9 @@ end acc
 inductive well_founded {α : Type u} (r : α → α → Prop) : Prop
 | intro : (∀ a, acc r a) → well_founded
 
+class has_well_founded (α : Type u) : Type u :=
+(r : α → α → Prop) (wf : well_founded r)
+
 namespace well_founded
 def apply {α : Type u} {r : α → α → Prop} (wf : well_founded r) : ∀ a, acc r a :=
 take a, well_founded.rec_on wf (λ p, p) a
@@ -136,6 +139,15 @@ inv_image (<)
 def measure_wf {α : Type u} (f : α → ℕ) : well_founded (measure f) :=
 inv_image.wf f nat.lt_wf
 
+def sizeof_measure (α : Type u) [has_sizeof α] : α → α → Prop :=
+measure sizeof
+
+def sizeof_measure_wf (α : Type u) [has_sizeof α] : well_founded (sizeof_measure α) :=
+measure_wf sizeof
+
+instance has_well_founded_of_has_sizeof (α : Type u) [has_sizeof α] : has_well_founded α :=
+{r := sizeof_measure α, wf := sizeof_measure_wf α}
+
 namespace prod
 open well_founded
 
@@ -181,6 +193,9 @@ section
   -- The relational product of well founded relations is well-founded
   def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) :=
   subrelation.wf (rprod_sub_lex) (lex_wf ha hb)
-
 end
+
+instance has_well_founded {α : Type u} {β : Type v} [s₁ : has_well_founded α] [s₂ : has_well_founded β] : has_well_founded (α × β) :=
+{r := lex s₁.r s₂.r, wf := lex_wf s₁.wf s₂.wf}
+
 end prod