How to "extract" Z from subset type {z : Z | z > 0}

Link:: https://stackoverflow.com/q/26493911

Display all goals and responses

Question

If a function take Z as arguments, it should also be possible to take any subset of Z, right? For example, Zmod takes two Z and return Z. Can I improve on this method with subset types without reimplementing it?

I want this:

Require Import ZArith.
Open Scope Z_scope.

Definition Z_gt0 := {z | z > 0}.

Definition mymod (n1 n2 : Z_gt0) := Zmod n1 n2.In environment
n1 : Z_gt0
n2 : Z_gt0
The term "n1" has type "Z_gt0"
while it is expected to have type "Z".

But Coq complains that n1 is expected to have type Z, of course. How can I make it work with Z_gt0? Coerce?

This question is related to my other one here: Random nat stream and subset types in Coq

Edit: proj1_sig might do the trick, thanks Coq IRC channel!

Answer

proj1_sig is the usual way to go. Another solution is to pattern match:

match z1 with
  exist _ z hz => ...
end

z will be your projection, and hz will be a proof that z > 0. I usually leave the first parameter anonymous since I know that z : Z.

I recent version of Coq, there is another way to do it, using let (because sig is an inductive with only one constructor):

Definition Zmod_gt0 (z1 z2 : Z_gt0) : Z :=
  let (a, _) := z1 in
  let (b, _) := z2 in
  Zmod a b.