Eval computing is incomplete when native solvability is used in Coq

Question

The team Eval computedoes not always appreciate a simple expression. Consider the code:

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Qed.

And if I executed the following command:

Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2).

Coq tells me the result 2. However, when I execute the following expression:

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

I get a long expression in which an In-predicate seems to unfold, but the result is not specified.

What do I need to change to get the answer 1in the last line Eval compute?

Answer 1

Coq : Qed Defined. , , , Eval compute. , , . , Defined Qed.:

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Defined.

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

sumbool {A} + {B} , , ; , . Ssreflect , :

Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT of P : reflect P true
  | ReflectF of ~ P : reflect P false.

, true, - . Ssreflect .

Answer 2

, . , Defined. Qed , , .