From cff7b7474a9de5950b799d7ddcbb503a2ffb303f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Jun 2015 16:17:29 -0700
Subject: [PATCH] test(tests/lean/run): add examples showing how to prove
 (using tactics) that direct_subterm relation is well-founded

see issue #347
---
 tests/lean/run/541b.lean                | 16 +++++++++++
 tests/lean/run/inf_tree.lean            |  7 +++++
 tests/lean/run/tree_subterm_pred.lean   |  6 ++++
 tests/lean/run/type_equations.lean      | 38 +++++++++++++++++++++++++
 tests/lean/run/vector_subterm_pred.lean |  7 ++++-
 5 files changed, 73 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/type_equations.lean

diff --git a/tests/lean/run/541b.lean b/tests/lean/run/541b.lean
index 57280908f7..7aeb0c9275 100644
--- a/tests/lean/run/541b.lean
+++ b/tests/lean/run/541b.lean
@@ -15,6 +15,22 @@ inductive exp : Type :=
 
 open exp
 
+inductive direct_subterm : exp → exp → Prop :=
+| lam    : ∀ n t e, direct_subterm e (lam n t e)
+| ap_fn  : ∀ f a, direct_subterm f (ap f a)
+| ap_arg : ∀ f a, direct_subterm a (ap f a)
+
+theorem direct_subterm_wf : well_founded direct_subterm :=
+begin
+  constructor, intro e, induction e,
+  repeat (constructor; intro y hlt; cases hlt; repeat assumption)
+end
+
+definition subterm := tc direct_subterm
+
+theorem subterm_wf : well_founded subterm :=
+tc.wf direct_subterm_wf
+
 inductive is_val : exp → Prop :=
 | vcnst    : Π c,     is_val (cnst c)
 | vlam     : Π x t e, is_val (lam x t e)
diff --git a/tests/lean/run/inf_tree.lean b/tests/lean/run/inf_tree.lean
index b53a73136c..29f5605601 100644
--- a/tests/lean/run/inf_tree.lean
+++ b/tests/lean/run/inf_tree.lean
@@ -28,4 +28,11 @@ namespace inftree
       (λ a, dsub.leaf.acc a)
       (λ f (ih :∀a, acc dsub (f a)), dsub.node.acc f ih))
 
+  theorem dsub.wf₂ (A : Type) : well_founded (@dsub A) :=
+  begin
+    constructor, intro t, induction t with a f ih ,
+     {constructor, intro y hlt, cases hlt},
+     {constructor, intro y hlt, cases hlt, exact ih a}
+  end
+
 end inftree
diff --git a/tests/lean/run/tree_subterm_pred.lean b/tests/lean/run/tree_subterm_pred.lean
index 7b4c2cb586..3c8d7df955 100644
--- a/tests/lean/run/tree_subterm_pred.lean
+++ b/tests/lean/run/tree_subterm_pred.lean
@@ -26,6 +26,12 @@ well_founded.intro (λ t : tree A,
            (λ (l' r' : tree A) (Heq : node l r = node l' r'), tree.no_confusion Heq (λ leq req, eq.rec_on req ihr)),
         gen (node l r) H rfl)))
 
+definition direct_subterm.wf₂ {A : Type} : well_founded (@direct_subterm A) :=
+begin
+  constructor, intro t, induction t,
+  repeat (constructor; intro y hlt; cases hlt; repeat assumption)
+end
+
 definition subterm {A : Type} : tree A → tree A → Prop := tc (@direct_subterm A)
 
 definition subterm.wf {A : Type} : well_founded (@subterm A) :=
diff --git a/tests/lean/run/type_equations.lean b/tests/lean/run/type_equations.lean
new file mode 100644
index 0000000000..d8f28c008d
--- /dev/null
+++ b/tests/lean/run/type_equations.lean
@@ -0,0 +1,38 @@
+open nat
+
+inductive expr :=
+| zero : expr
+| one  : expr
+| add  : expr → expr → expr
+
+namespace expr
+
+inductive direct_subterm : expr → expr → Prop :=
+| add_1 : ∀ e₁ e₂ : expr, direct_subterm e₁ (add e₁ e₂)
+| add_2 : ∀ e₁ e₂ : expr, direct_subterm e₂ (add e₁ e₂)
+
+theorem direct_subterm_wf : well_founded direct_subterm :=
+begin
+  constructor, intro e, induction e,
+  repeat (constructor; intro y hlt; cases hlt; repeat assumption)
+end
+
+definition subterm := tc direct_subterm
+
+theorem subterm_wf [instance] : well_founded subterm :=
+tc.wf direct_subterm_wf
+
+infix `+` := expr.add
+
+set_option pp.notation false
+
+definition ev : expr → nat
+| zero             := 0
+| one              := 1
+| ((a : expr) + b) := ev a + ev b
+
+definition foo : expr := add zero (add one one)
+
+example : ev foo = 2 :=
+rfl
+end expr
diff --git a/tests/lean/run/vector_subterm_pred.lean b/tests/lean/run/vector_subterm_pred.lean
index 85c305118e..869047e7a3 100644
--- a/tests/lean/run/vector_subterm_pred.lean
+++ b/tests/lean/run/vector_subterm_pred.lean
@@ -39,9 +39,14 @@ well_founded.intro (λ (bv : vec A),
                 gen₂ n₁ e₃ v₁ ih e₂))),
             gen (to_vec (cons a₁ v₁)) lt₁ rfl))))
 
+definition direct_subterm.wf₂ (A : Type) : well_founded (direct_subterm A) :=
+begin
+  constructor, intro V, cases V with n v, induction v,
+  repeat (constructor; intro y hlt; cases hlt; repeat assumption)
+end
+
 definition subterm (A : Type) := tc (direct_subterm A)
 
 definition subterm.wf (A : Type) : well_founded (subterm A) :=
 tc.wf (direct_subterm.wf A)
-
 end vector