From f631bd8df91d48c03a4e9674a3afa21cc0e2f608 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Apr 2021 16:21:06 -0700
Subject: [PATCH] test: inductive predicate example

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

diff --git a/tests/lean/run/inductive_pred.lean b/tests/lean/run/inductive_pred.lean
new file mode 100644
index 0000000000..4928af43c4
--- /dev/null
+++ b/tests/lean/run/inductive_pred.lean
@@ -0,0 +1,46 @@
+inductive LE : Nat → Nat → Prop
+  | refl : LE n n
+  | succ : LE n m → LE n m.succ
+
+theorem LE.trans : LE m n → LE n o → LE m o := by
+  intro h1 h2
+  induction h2 with
+  | refl => assumption
+  | succ h2 ih => exact succ (ih h1)
+
+theorem LE.trans' : LE m n → LE n o → LE m o
+  | h1, refl    => h1
+  | h1, succ h2 => succ (trans' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
+
+inductive Even : Nat → Prop
+  | zero : Even 0
+  | ss   : Even n → Even n.succ.succ
+
+theorem Even.add : Even n → Even m → Even (n+m) := by
+  intro h1 h2
+  induction h2 with
+  | zero => exact h1
+  | ss h2 ih => exact ss ih
+
+theorem Even.add' : Even n → Even m → Even (n+m)
+  | h1, zero  => h1
+  | h1, ss h2 => ss (add' h1 h2)  -- the structural recursion in being performed on the implicit `Nat` parameter
+
+theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
+  rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
+
+inductive Power2 : Nat → Prop
+  | base : Power2 1
+  | ind  : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
+
+theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
+  intro h1 h2
+  induction h2 with
+  | base      => simp_all
+  | ind h2 ih => exact mul_left_comm .. ▸ ind ih
+
+/- The following example fails because the structural recursion cannot be performed on the `Nat`s and
+   the `brecOn` construction doesn't work for inductive predicates -/
+-- theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
+--  | h1, base => by simp_all
+--  | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)