From 4ebd3e2c279b90fa94586cfbe31671578cd490f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Nov 2014 21:06:15 -0800
Subject: [PATCH] feat(library/logic/wf): transitive closure of a well-founded
 relation is well-founded

---
 library/logic/wf.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/library/logic/wf.lean b/library/logic/wf.lean
index ccd79f8f02..c62f5d9848 100644
--- a/library/logic/wf.lean
+++ b/library/logic/wf.lean
@@ -115,3 +115,35 @@ context
   well_founded.intro (λ a, accessible (H (f a)))
 end
 end inv_image
+
+-- Transitive closure
+inductive tc {A : Type} (R : A → A → Prop) : A → A → Prop :=
+base  : ∀a b, R a b → tc R a b,
+trans : ∀a b c, tc R a b → tc R b c → tc R a c
+
+-- The transitive closure of a well-founded relation is well-founded
+namespace tc
+context
+  parameters {A : Type} {R : A → A → Prop}
+  notation `R⁺` := tc R
+
+  definition accessible {z} (ac: acc R z) : acc R⁺ z :=
+  acc.rec_on ac
+    (λ (x : A) (ax : _) (iH : ∀y, R y x → acc (tc R) y),
+      acc.intro x (λ (y : A) (lt : R⁺ y x),
+        have gen : x = x → acc (tc R) y, from
+          tc.rec_on lt
+            (λa b (H : R a b) (Heq : b = x),
+               iH a (eq.rec_on Heq H))
+            (λa b c (H₁ : R⁺ a b) (H₂ : R⁺ b c)
+                (iH₁ : b = x → acc (tc R) a)
+                (iH₂ : c = x → acc (tc R) b)
+                (Heq : c = x),
+              acc.inv (iH₂ Heq) H₁),
+        gen rfl))
+
+  definition wf (H : well_founded R) : well_founded R⁺ :=
+  well_founded.intro (λ a, accessible (H a))
+
+end
+end tc