[stdlib] [PeanoNat] Add EvenT and OddT (Even and Odd in Type)

[olaure01]

Versions of Nat.Even and Nat.Odd with type Type.
Decision and induction principles in Type are defined: EvenT_OddT_dec and EvenT_OddT_rect.

• Added changelog.

[SkySkimmer]

Why not define the principles for the Prop predicates instead?

[olaure01]

Mostly to be able to extract the k such that n = 2 * k or n = 2 * k + 1 when the goal is in Type:

Lemma parity_Type (P : nat -> Type) n : P n.
Proof.
Fail destruct (Nat.Even_Odd_dec n) as [[k ->]|[k ->]].
destruct (Nat.EvenT_OddT_dec n) as [[k ->]|[k ->]].
Admitted.

[Alizter]

Do you think it's a good idea to make these all Qed proofs? I feel like we could refactor them so that only the equality is Qed using abstract or something. That way projecting IsEvenT actually computes something?

[olaure01]

Maybe. I do not have a clear view on that, including where to put the cursor between Defined and Qed.
If we consider EvenT_OddT_dec for example, Defined could be a good thing but the proof should be refactored.
@Alizter Do you think targeting EvenT_OddT_dec (with adapted proof), EvenT_OddT_rect and OddT_EvenT_rect to be Defined (and thus all intermediary results leading to them as well) would be the natural thing to do?

[Alizter]

Perhaps this is something to do in the future then, since I am also a bit unsure about how to do it. For now, maybe leave a comment at the top of the T versions stating that they are useful for eliminating into Type but are still opaque.

[olaure01]

Done.
By the way when the exact (computed) value of some k such that n = 2 * k or n = 2 * k + 1 is needed (not just its existence), it might be easier to access it directly with Nat.div2 and associated lemmas.

[ppedrot]

My 2cts: we should probably design a generic way to do this instead of duplicating everything in the stdlib on a per-need basis. Regarding the Qed vs. Defined debate, the use of SProp would probably solve this kind of issues when the predicate is decidable.

[olaure01]

My 2cts: we should probably design a generic way to do this instead of duplicating everything in the stdlib on a per-need basis.

Absolutely! I am facing the situation again and again. What about the following suggestion (from #11966 (comment)):

More generally, I think most of the predicates about types in Set like lists, should be primarily defined with output in Type to get maximal expressive power. It is then possible to get back Prop versions through inhabited if I am right.

[olaure01]

Regarding the Qed vs. Defined debate, the use of SProp would probably solve this kind of issues when the predicate is decidable.

Could you elaborate on that? I know almost nothing about how to use SProp.

[ppedrot]

It is then possible to get back Prop versions through inhabited if I am right.

This is not true for recursive predicates. There is a bit of choice axiom hidden in that in general. This will work when the Prop and Type predicates are logically equivalent, though.

Could you elaborate on that? I know almost nothing about how to use SProp.

With SProp, it just does not matter whether a proof is Qed or Defined, because all proofs are convertible. The price to pay is that some predicates that satisfy singleton elimination in Prop do not anymore in SProp, notably Acc and eq. Said otherwise, the only thing you can eliminate from SProp to Type are proofs of False.

For decidable predicates it does not matter though because you can always obtain a canonical proof in Type or Prop from a proof in SProp. In some sense, SProp is a statically-typed way to enforce the Coq design pattern that "the only things that can be safely wrapped in Qed are statements used to prove a contradiction".

The problem is that SProp is still badly supported in the current Coq versions. Many tactics do not handle it correctly, and unification is completely broken when you use it. So it's not yet usable at a large scale, but hopefully there will be progress on the matter.

[Alizter]

merging soon

[Alizter]

@coqbot merge now