Coq: easiest way to construct members of a decidable sigma type?

Question

Consider the following toy development:

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

I'd like to create a function that, given a number that I personally know to be even, returns the corresponding value of type EvenNat with minimum fuss.

Example fortyTwo : EvenNat := mkEven 42.

Answer 1

The question, as originally stated, has an obvious answer.

Question A: If you have in your context a number n of type nat and a proof knowledge with statement IsEven n, how do you construct an object of type EvenNat?

you can simply construct an object of type EvenNat by writing the following expression

exist _ n knowledge

Or, if you really want to be explicit:

exist IsEven n knowledge

This is embodied in the following script

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

Definition mkEven (n : nat) (knowledge : IsEven n) : EvenNat :=
  exist IsEven n knowledge.

Another reading of the question is as follows:

Question B: how do you construct an object of type EvenNat from a known constant (like 42) which is obviously even to the naked eye?

Here is my elaboration of a solution sketched by Theo Winterhalter, using the device of type classes in full.

Require Import Coq.Init.Specif.

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

Definition makeEvenNat (n : nat) (knowledge : IsEven n) : EvenNat :=
  exist IsEven n knowledge.

Class EvenClass n : Prop :=
  is_even : IsEven n.

#[export] Instance evenClass0 : EvenClass 0.
Proof.
apply is_even_z.
Qed.

#[export] Instance evenClassS n {h : EvenClass n}  : EvenClass (S (S n)).
Proof.
apply is_even_S; exact h.
Qed.

(* Using curly braces for the second argument h here deserves an
  explanation. *)
Definition mkEven (n : nat) {h : EvenClass n} : EvenNat :=
  exist IsEven n h.

Definition ev42 := mkEven 42.

Lemma ev42P : proj1_sig ev42 = 42.
Proof. easy. Qed.

Lemma IsEven42 : IsEven 42.
Proof. exact (proj2_sig ev42). Qed.

The explanation for using curly braces in the definition of mkEven is that mkEven actually requires 2 arguments, but the second one is not written by the user: it must be automatically constructed using the type class inference mechanism. This proof must succeed for the object to be actually defined.

The definition of ev42 is the answer of question B. Note that a definition relying on mkEven 3 will fail, because no proof that 3 is even can be found.

Fail Definition ev3 := mkEven 3.

This code was tested with coq.8.15.0.