From 7a06912427792cf39eecefc16a9d64f27a203ffd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Dec 2016 18:38:35 -0800
Subject: [PATCH] test(tests/lean/run): add test for destruct tactic

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

diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean
new file mode 100644
index 0000000000..23eef38b99
--- /dev/null
+++ b/tests/lean/run/destruct.lean
@@ -0,0 +1,30 @@
+universe variables u
+
+inductive Vec (α : Type u) : nat → Type (max 1 u)
+| nil  : Vec 0
+| cons : ∀ {n}, α → Vec n → Vec (nat.succ n)
+
+lemma split {α : Type u} {n : nat} (v : Vec α n) : (v == (Vec.nil α) ∧ n = 0) ∨ ∃ m h (t : Vec α m), v == Vec.cons h t ∧ n = nat.succ m :=
+Vec.cases_on v
+    (or.inl ⟨heq.refl _, rfl⟩)
+    (λ n h t, or.inr ⟨n, h, t, heq.refl _, rfl⟩)
+
+constant f {α : Type u} {n : nat} : Vec α n → nat
+axiom fax1 (α : Type u) : f (Vec.nil α) = 0
+axiom fax2 {α : Type u} {n : nat} (v : Vec α (nat.succ n)) : f v = 1
+
+example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 :=
+begin
+  destruct v,
+  intros, intro, note h := fax1 α, cc,
+  intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc
+end
+
+open nat
+example : ∀ n, 0 < n → succ (pred n) = n :=
+begin
+  intro n,
+  destruct n,
+   dsimp, intros, note h := lt_irrefl 0, cc,
+   dsimp, intros, subst n, reflexivity
+end