From b7c853692d28ce320e1537753ad7e025fc64c81a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Feb 2022 17:49:03 -0800
Subject: [PATCH] test: add test for `decide` congruence issue

TODO: congruence lemma must be automatically generated.

see #988
---
 tests/lean/run/988.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tests/lean/run/988.lean b/tests/lean/run/988.lean
index e9f9f18621..17f31582c6 100644
--- a/tests/lean/run/988.lean
+++ b/tests/lean/run/988.lean
@@ -24,3 +24,12 @@ example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
 example (as : Array (Nat → Nat)) (h : 0 + x < as.size) :
     as.get ⟨0 + x, h⟩ i = as.get ⟨x, Nat.zero_add x ▸ h⟩ (0+i) := by
   simp -- should also work
+
+-- TODO: generate the following lemma automatically
+@[congr] theorem decide_congr (p q : Prop) (h : p = q) [s₁ : Decidable p] [s₂ : Decidable q] : decide p = decide q := by
+  subst h
+  have : s₁ = s₂ := Subsingleton.elim s₁ s₂
+  subst this
+  rfl
+
+example [Decidable p] : decide (p ∧ True) = decide p := by simp -- should work