From a065c7bf96fb95a6426ed123cf0ef0d6fa45107d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Nov 2014 17:57:17 -0800
Subject: [PATCH] test(tests/lean/run/tree_height): experiment with wf relation
 based on the height

This is easier to generate than the subterm relation
---
 tests/lean/run/tree_height.lean | 36 +++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/lean/run/tree_height.lean

diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean
new file mode 100644
index 000000000..950330d05
--- /dev/null
+++ b/tests/lean/run/tree_height.lean
@@ -0,0 +1,36 @@
+import logic data.nat
+open eq.ops nat
+
+inductive tree (A : Type) :=
+leaf : A → tree A,
+node : tree A → tree A → tree A
+
+namespace tree
+
+definition height {A : Type} (t : tree A) : nat :=
+rec_on t
+  (λ a, zero)
+  (λ t₁ t₂ h₁ h₂, succ (max h₁ h₂))
+
+definition height_lt {A : Type} : tree A → tree A → Prop :=
+inv_image lt (@height A)
+
+definition height_lt.wf (A : Type) : well_founded (@height_lt A) :=
+inv_image.wf height lt.wf
+
+theorem height_lt.node_left {A : Type} (t₁ t₂ : tree A) : height_lt t₁ (node t₁ t₂) :=
+le_imp_lt_succ (left_le_max (height t₁) (height t₂))
+
+theorem height_lt.node_right {A : Type} (t₁ t₂ : tree A) : height_lt t₂ (node t₁ t₂) :=
+le_imp_lt_succ (right_le_max (height t₁) (height t₂))
+
+theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
+inv_image.trans lt height @lt_trans
+
+example : height_lt (leaf 2) (node (leaf 1) (leaf 2)) :=
+!height_lt.node_right
+
+example : height_lt  (leaf 2) (node (node (leaf 1) (leaf 2)) (leaf 3)) :=
+height_lt.trans !height_lt.node_right !height_lt.node_left
+
+end tree