From 92b0a538c59ac332ddc23c1907c9653b2021d162 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Nov 2014 10:18:24 -0800
Subject: [PATCH] refactor(library/logic/wf): add well_founded class, and
 cleanup file

---
 library/logic/wf.lean | 61 +++++++++++++++++++++++--------------------
 1 file changed, 33 insertions(+), 28 deletions(-)

diff --git a/library/logic/wf.lean b/library/logic/wf.lean
index 4063bdb42..53e5641de 100644
--- a/library/logic/wf.lean
+++ b/library/logic/wf.lean
@@ -6,27 +6,31 @@ import logic.eq
 inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
 intro : ∀x, (∀ y, R y x → acc R y) → acc R x
 
-definition well_founded {A : Type} (R : A → A → Prop) :=
-∀a, acc R a
+namespace acc
+  variables {A : Type} {R : A → A → Prop}
+
+  definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y :=
+  acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂
+end acc
+
+inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop :=
+intro : (∀ a, acc R a) → well_founded R
 
 namespace well_founded
+  definition apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
+  take a, well_founded.rec_on wf (λp, p) a
 
-context
+  context
   parameters {A : Type} {R : A → A → Prop}
   infix `≺`:50    := R
 
-  definition acc_inv {x y : A} (H₁ : acc R x) (H₂ : y ≺ x) : acc R y :=
-  have gen : y ≺ x → acc R y, from
-    acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂),
-  gen H₂
+  hypothesis [Hwf : well_founded R]
 
-  hypothesis Hwf : well_founded R
-
-  theorem well_founded_rec {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
+  theorem recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
   acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH)
 
-  theorem well_founded_ind {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
-  well_founded_rec a H
+  theorem indunction {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
+  recursion a H
 
   variable {C : A → Type}
   variable F : Πx, (Πy, y ≺ x → C y) → C x
@@ -35,29 +39,30 @@ context
   acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)
 
   theorem fix_F_eq (x : A) (r : acc R x) :
-    fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc_inv r p)) :=
-  have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc_inv r p)), from
+    fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
+  have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)), from
   acc.rec_on r
     (λ x₁ ac iH (r₁ : acc R x₁),
       -- The proof is straightforward after we replace r₁ with acc.intro (to "unblock" evaluation).
       calc fix_F F x₁ r₁
            = fix_F F x₁ (acc.intro x₁ ac)             : proof_irrel r₁
-       ... = F x₁ (λ y ay, fix_F F y (acc_inv r₁ ay)) : rfl),
+       ... = F x₁ (λ y ay, fix_F F y (acc.inv r₁ ay)) : rfl),
   gen r
-end
+  end
 
-variables {A : Type} {C : A → Type} {R : A → A → Prop}
--- Well-founded fixpoint
-definition fix (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
-fix_F F x (Hwf x)
+  variables {A : Type} {C : A → Type} {R : A → A → Prop}
 
--- Well-founded fixpoint satisfies fixpoint equation
-theorem fix_eq (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
-  fix Hwf F x = F x (λy h, fix Hwf F y) :=
-calc
-  -- The proof is straightforward, it just uses fix_F_eq and proof irrelevance
-  fix Hwf F x
-      = F x (λy h, fix_F F y (acc_inv (Hwf x) h)) : fix_F_eq F x (Hwf x)
-  ... = F x (λy h, fix Hwf F y) : rfl  -- proof irrelevance is used here
+  -- Well-founded fixpoint
+  definition fix [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
+  fix_F F x (Hwf x)
+
+  -- Well-founded fixpoint satisfies fixpoint equation
+  theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
+    fix F x = F x (λy h, fix F y) :=
+  calc
+    -- The proof is straightforward, it just uses fix_F_eq and proof irrelevance
+    fix F x
+        = F x (λy h, fix_F F y (acc.inv (Hwf x) h)) : fix_F_eq F x (Hwf x)
+    ... = F x (λy h, fix F y)                       : rfl  -- proof irrelevance is used here
 
 end well_founded