From 6056a4cbfa806735dcc9a395f10fd0895c8698e1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Mar 2022 12:38:05 -0700
Subject: [PATCH] test: stars_and_bars

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

diff --git a/tests/lean/run/starsAndBars.lean b/tests/lean/run/starsAndBars.lean
new file mode 100644
index 0000000000..e42d433a7b
--- /dev/null
+++ b/tests/lean/run/starsAndBars.lean
@@ -0,0 +1,49 @@
+@[simp] def List.count [DecidableEq α] : List α → α → Nat
+  | [], _    => 0
+  | a::as, b => if a = b then as.count b + 1 else as.count b
+
+inductive StarsAndBars : Nat → Nat → Type where
+  | nil  : StarsAndBars 0 0
+  | star : StarsAndBars s b → StarsAndBars (s+1) b
+  | bar  : StarsAndBars s b → StarsAndBars s (b+1)
+
+namespace StarsAndBars
+
+namespace Ex1
+
+def toList : StarsAndBars s b → { bs : List Bool // bs.count false = s ∧ bs.count true = b }
+  | nil    => ⟨[], by simp⟩
+  | star h => ⟨false :: toList h, by simp [(toList h).2]⟩
+  | bar  h => ⟨true :: toList h, by simp [(toList h).2]⟩
+
+theorem toList_star (h : StarsAndBars s b) (h') : toList (star h) = ⟨false :: toList h, h'⟩ := by
+  simp [toList]
+
+theorem toList_bar (h : StarsAndBars s b) (h') : toList (bar h) = ⟨true :: toList h, h'⟩ := by
+  simp [toList]
+
+end Ex1
+
+/- Same example with explicit proofs -/
+namespace Ex2
+
+theorem toList_star_proof (h : bs.count false = s ∧ bs.count true = b) : (false :: bs).count false = s.succ ∧ (false :: bs).count true = b := by
+  simp [*]
+
+theorem toList_bar_proof (h : bs.count false = s ∧ bs.count true = b) : (true :: bs).count false = s ∧ (true :: bs).count true = b.succ := by
+  simp [*]
+
+def toList : StarsAndBars s b → { bs : List Bool // bs.count false = s ∧ bs.count true = b }
+  | nil    => ⟨[], by simp⟩
+  | star h => ⟨false :: toList h, toList_star_proof (toList h).property⟩
+  | bar  h => ⟨true :: toList h,  toList_bar_proof (toList h).property⟩
+
+theorem toList_star (h : StarsAndBars s b) : toList (star h) = ⟨false :: toList h, toList_star_proof (toList h).property⟩ := by
+  simp [toList]
+
+theorem toList_bar (h : StarsAndBars s b) : toList (bar h) = ⟨true :: toList h, toList_bar_proof (toList h).property⟩ := by
+  simp [toList]
+
+end Ex2
+
+end StarsAndBars