From f737a140c176bd60127f97919ed267da9996d7cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Nov 2014 16:22:11 -0800
Subject: [PATCH] test(tests/lean/run): direct subterm for non-reflexive
 datatype

---
 tests/lean/run/inf_tree.lean | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 tests/lean/run/inf_tree.lean

diff --git a/tests/lean/run/inf_tree.lean b/tests/lean/run/inf_tree.lean
new file mode 100644
index 000000000..2f5d341cb
--- /dev/null
+++ b/tests/lean/run/inf_tree.lean
@@ -0,0 +1,31 @@
+import logic data.nat.basic
+open nat
+
+inductive inftree (A : Type) :=
+leaf : A → inftree A,
+node : (nat → inftree A) → inftree A
+
+namespace inftree
+  inductive dsub {A : Type} : inftree A → inftree A → Prop :=
+  intro : Π (f : nat → inftree A) (a : nat), dsub (f a) (node f)
+
+  definition dsub.node.acc {A : Type} (f : nat → inftree A) (H : ∀a, acc dsub (f a)) : acc dsub (node f) :=
+  acc.intro (node f) (λ (y : inftree A) (hlt : dsub y (node f)),
+    have aux : ∀ z, dsub y z → node f = z → acc dsub y, from
+      λ z hlt, dsub.rec_on hlt (λ (f₁ : nat → inftree A) (a : nat) (eq₁ : node f = node f₁),
+        inftree.no_confusion eq₁ (λe, eq.rec_on e (H a))),
+    aux (node f) hlt rfl)
+
+  definition dsub.leaf.acc {A : Type} (a : A) : acc dsub (leaf a) :=
+  acc.intro (leaf a) (λ (y : inftree A) (hlt : dsub y (leaf a)),
+    have aux : ∀ z, dsub y z → leaf a = z → acc dsub y, from
+      λz hlt, dsub.rec_on hlt (λ f n (heq : leaf a = node f), inftree.no_confusion heq),
+    aux (leaf a) hlt rfl)
+
+  definition dsub.wf (A : Type) : well_founded (@dsub A) :=
+  well_founded.intro (λ (t : inftree A),
+    rec_on t
+      (λ a, dsub.leaf.acc a)
+      (λ f (ih :∀a, acc dsub (f a)), dsub.node.acc f ih))
+
+end inftree