From e71d0abc7ddb2c9da37e91b88fd2be2a903601c7 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 24 Oct 2025 16:54:36 +0200 Subject: [PATCH] test: test case for #10775 (#10943) --- tests/lean/run/issue10775.lean | 132 +++++++++++++++++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 tests/lean/run/issue10775.lean diff --git a/tests/lean/run/issue10775.lean b/tests/lean/run/issue10775.lean new file mode 100644 index 0000000000..7f03aa63e1 --- /dev/null +++ b/tests/lean/run/issue10775.lean @@ -0,0 +1,132 @@ +set_option linter.unusedVariables false + +opaque R : (n m : Int) → Type + +axiom mkR : Nat → R n m + +noncomputable def d : ∀ (n m : Int), R n m + | .ofNat n, .ofNat m => mkR 0 + | .negSucc n, .negSucc m => mkR 0 + | .negSucc 0, .ofNat 0 => mkR 0 + | .ofNat _, .negSucc _ => mkR 0 + | .negSucc _, .ofNat _ => mkR 0 + +/-- +error: unsolved goals +case refine_1 +⊢ ∀ (n m : Nat), ¬↑n + 1 = ↑m → mkR 0 = mkR 0 + +case refine_2 +⊢ ∀ (n m : Nat), ¬Int.negSucc n + 1 = Int.negSucc m → mkR 0 = mkR 0 + +case refine_3 +⊢ ¬0 = 0 → mkR 0 = mkR 0 + +case refine_4 +⊢ ∀ (a a_1 : Nat), ¬↑a + 1 = Int.negSucc a_1 → mkR 0 = mkR 0 + +case refine_5 +⊢ ∀ (a a_1 : Nat), (a = 0 → a_1 = 0 → False) → ¬Int.negSucc a + 1 = ↑a_1 → mkR 0 = mkR 0 +-/ +#guard_msgs in +example : (n m : Int) → (hnm : n + 1 ≠ m) → d n m = mkR 0 := by + refine d.fun_cases_unfolding (motive := fun n m r => (n + 1 ≠ m) → r = mkR 0) + ?_ ?_ ?_ ?_ ?_ <;> dsimp + +/-- +error: unsolved goals +case case1 +n✝ m✝ : Nat +hnm : Int.ofNat n✝ + 1 ≠ Int.ofNat m✝ +⊢ d (Int.ofNat n✝) (Int.ofNat m✝) = mkR 0 + +case case2 +n✝ m✝ : Nat +hnm : Int.negSucc n✝ + 1 ≠ Int.negSucc m✝ +⊢ d (Int.negSucc n✝) (Int.negSucc m✝) = mkR 0 + +case case3 +hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0 +⊢ d (Int.negSucc 0) (Int.ofNat 0) = mkR 0 + +case case4 +a✝¹ a✝ : Nat +hnm : Int.ofNat a✝¹ + 1 ≠ Int.negSucc a✝ +⊢ d (Int.ofNat a✝¹) (Int.negSucc a✝) = mkR 0 + +case case5 +a✝¹ a✝ : Nat +x✝ : a✝¹ = 0 → a✝ = 0 → False +hnm : Int.negSucc a✝¹ + 1 ≠ Int.ofNat a✝ +⊢ d (Int.negSucc a✝¹) (Int.ofNat a✝) = mkR 0 +-/ +#guard_msgs in +example : (n m : Int) → (hnm : n + 1 ≠ m) → d n m = mkR 0 := by + intros n m hnm + fun_cases d + +-- set_option trace.Elab.induction true in + +/-- +error: unsolved goals +case case1 +n✝ m✝ : Nat +hnm : Int.ofNat n✝ + 1 ≠ Int.ofNat m✝ +⊢ d (Int.ofNat n✝) (Int.ofNat m✝) = mkR 0 + +case case2 +n✝ m✝ : Nat +hnm : Int.negSucc n✝ + 1 ≠ Int.negSucc m✝ +⊢ d (Int.negSucc n✝) (Int.negSucc m✝) = mkR 0 + +case case3 +hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0 +⊢ d (Int.negSucc 0) (Int.ofNat 0) = mkR 0 + +case case4 +a✝¹ a✝ : Nat +hnm : Int.ofNat a✝¹ + 1 ≠ Int.negSucc a✝ +⊢ d (Int.ofNat a✝¹) (Int.negSucc a✝) = mkR 0 + +case case5 +a✝¹ a✝ : Nat +x✝ : a✝¹ = 0 → a✝ = 0 → False +hnm : Int.negSucc a✝¹ + 1 ≠ Int.ofNat a✝ +⊢ d (Int.negSucc a✝¹) (Int.ofNat a✝) = mkR 0 +-/ +#guard_msgs(pass trace, all) in +example : (n m : Int) → (hnm : n + 1 ≠ m) → d n m = mkR 0 := by + intros n m hnm + cases n, m using d.fun_cases_unfolding + +/-- +error: unsolved goals +case case1 +n✝ m✝ : Nat +hnm : Int.ofNat n✝ + 1 ≠ Int.ofNat m✝ +⊢ mkR 0 = mkR 0 + +case case2 +n✝ m✝ : Nat +hnm : Int.negSucc n✝ + 1 ≠ Int.negSucc m✝ +⊢ mkR 0 = mkR 0 + +case case3 +hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0 +⊢ mkR 0 = mkR 0 + +case case4 +a✝¹ a✝ : Nat +hnm : Int.ofNat a✝¹ + 1 ≠ Int.negSucc a✝ +⊢ mkR 0 = mkR 0 + +case case5 +a✝¹ a✝ : Nat +x✝ : a✝¹ = 0 → a✝ = 0 → False +hnm : Int.negSucc a✝¹ + 1 ≠ Int.ofNat a✝ +⊢ mkR 0 = mkR 0 +-/ +#guard_msgs(pass trace, all) in +example : (n m : Int) → (hnm : n + 1 ≠ m) → d n m = mkR 0 := by + intros n m hnm + induction n, m using d.fun_cases_unfolding