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

@@ -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)

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

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) :=

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

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