From 317492d207c345cabdcb7317ca798a722b86b173 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Apr 2022 16:04:17 -0700
Subject: [PATCH] test: add test for Lean 3 `refine` bug reported on Zulip

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60refine.60.20bug.20.3F/near/278031110
---
 tests/lean/lean3RefineBug.lean              | 28 +++++++++++++++++++++
 tests/lean/lean3RefineBug.lean.expected.out | 16 ++++++++++++
 2 files changed, 44 insertions(+)
 create mode 100644 tests/lean/lean3RefineBug.lean
 create mode 100644 tests/lean/lean3RefineBug.lean.expected.out

diff --git a/tests/lean/lean3RefineBug.lean b/tests/lean/lean3RefineBug.lean
new file mode 100644
index 0000000000..3b4452f4af
--- /dev/null
+++ b/tests/lean/lean3RefineBug.lean
@@ -0,0 +1,28 @@
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun a => ?hp
+  trace_state
+  exact a.1
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => ?hp
+  trace_state
+  exact a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun a => ?hp
+  case hp => exact a.1
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => ?hp
+  case hp => exact a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine λ ⟨a, b⟩ => ?hp
+  trace_state
+  exact a
diff --git a/tests/lean/lean3RefineBug.lean.expected.out b/tests/lean/lean3RefineBug.lean.expected.out
new file mode 100644
index 0000000000..f5d310438d
--- /dev/null
+++ b/tests/lean/lean3RefineBug.lean.expected.out
@@ -0,0 +1,16 @@
+case hp
+p q : Prop
+a : p ∧ q
+⊢ p
+case hp
+p q : Prop
+ : p ∧ q
+a : p
+b : q
+⊢ p
+case hp
+p q : Prop
+ : p ∧ q
+a : p
+b : q
+⊢ p