I have a code like
Definition even := {n : nat | exists k, n = k + k}.
Definition even_to_nat (e : even) : nat.
Admitted.
Coercion even_to_nat : even >-> nat.
Example Ex : forall n : even, exists k, k + k = n.
Admitted.
Example Ex2 : forall k, exists n : even, k + k = n.
Admitted.
How should I remove Admitted in this case?
Also, why does
Example Ex' : forall n : even, exists k, n = k + k
not work even with coercion? Is there a nice way to remove such errors?
This is a definition for the even_to_nat function written in Gallina:
Definition even := {n : nat | exists k, n = k + k}.
Definition even_to_nat (e : even) : nat :=
match e with
| exist _ n _ => n
end.
Coercion even_to_nat : even >-> nat.
It pattern matches on e to retrieve the wrapped natural number n.
This is an equivalent implementation using tactics:
Definition even_to_nat_tac (e : even) : nat.
destruct e.
auto.
Defined.
The destruct tactic essentially pattern matches on e. Then, auto automatically uses the natural number inside to finish the definition.
Here is a Gallina implementation of your first example:
Example Ex : forall n : even, exists k, k + k = n :=
fun n => match n with
| exist _ n (ex_intro _ k eq) => ex_intro (fun k => k + k = n) k (eq_sym eq)
end.
Essentially, it pattern matches on n, retrieves the k and the proof that n = k + k, then uses eq_sym to flip the equality.
Here is an implementation for Ex2:
Example Ex2 : forall k, exists n : even, k + k = n :=
fun k =>
let n := k + k in
let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
ex_intro (fun n => k + k = even_to_nat n) even_nat eq_refl.
exists_k is the proof contained inside an even number stating exists k, n + n = k. even_nat is an even number fulfilling the condition exists n, k + k = n, where n is obviously k + k. Finally, I inhabit the desired type. It seems that I can't use coercions here, so I explicitly use even_to_nat.
Alternatively, the coercion works if I add a type annotation:
Example Ex2 : forall k, exists n : even, k + k = n :=
fun k =>
let n := k + k in
let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
ex_intro (fun (n : even) => k + k = n) even_nat eq_refl.
For your Ex' example, see the warning in this example from the coercion documentation. Given the coercion Coercion bool_in_nat : bool >-> nat.:
Note that Check (true = O) would fail. This is "normal" behavior of coercions. To validate true=O, the coercion is searched from nat to bool. There is none.
You can only coerce on the right side of the equality type, not the left.