From 862492778a6dcd5cd78922a5d310e697dc57d11c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 15:50:40 -0700
Subject: [PATCH] test: add `deq_correct` test from Zulip

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

diff --git a/tests/lean/run/deq.lean b/tests/lean/run/deq.lean
new file mode 100644
index 0000000000..65f61fe2d6
--- /dev/null
+++ b/tests/lean/run/deq.lean
@@ -0,0 +1,36 @@
+inductive LazyList (α : Type u)
+| nil : LazyList α
+| cons (hd : α) (tl : LazyList α) : LazyList α
+| delayed (t : Thunk (LazyList α)) : LazyList α
+
+namespace LazyList
+
+def force : LazyList α → Option (α × LazyList α)
+| delayed as => force as.get
+| nil        => none
+| cons a as  => some (a,as)
+
+end LazyList
+
+def deq (Q : LazyList τ) : Option (τ × LazyList τ) :=
+  match h:Q.force with
+  | some (x, F') => some (x, F')
+  | none => none
+
+theorem deq_correct_1 (Q : LazyList τ)
+  : deq Q = none ↔ Q.force = none
+  := by
+    unfold deq
+    cases h' : Q.force <;> simp
+
+theorem deq_correct_2 (Q : LazyList τ)
+  : deq Q = none ↔ Q.force = none
+  := by
+    cases h' : Q.force with
+    | none => unfold deq; rw [h']; simp
+    | some => unfold deq; rw [h']; simp
+
+theorem deq_correct_3 (Q : LazyList τ)
+  : deq Q = none ↔ Q.force = none
+  := by
+    cases h' : Q.force <;> unfold deq <;> rw [h'] <;> simp