What does ∀id1 id2 : id, {id1 = id2} + {id1 ≠ id2} mean?

Question

I'm reading Software Foundations book and in Imp.v file, there is this definition of a theorem eq_id_dec as follows:

Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
   intros id1 id2.
   destruct id1 as [n1]. destruct id2 as [n2].
   destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
   Case "n1 = n2".
     left. rewrite Heq. reflexivity.
   Case "n1 <> n2".
     right. intros contra. inversion contra. apply Hneq. apply H0.
Defined. 

Does this theorem mean that for any id1 and id2 of type id, both id1=id2 and id1!=id2 cannot happen? I'm not sure.

Answer 1

No, it does not preclude the case that both the equality and the inequality are true at the same time (though in practice it is the case here).

The type sumbool A B, of notation {A} + {B}, characterizes a decision procedure that will prove either A or B.

So this eq_id_dec is a term that will take two ids as input, and either return a proof that they are equal, or a proof that they are distinct.

More about sumbool here: https://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Sumbool.html

Answer 2

For all id1 and id2, id1 = id2 or id1 does not equal id2.

Pretty straightforward - either it equals id2 or it does not, which will by definition always be true - so it is true for all id1/id2.