How to “extract” Z from a type of a subset {z: Z | z> 0}

Question

If a function takes Z as arguments, it is also possible to take any subset of Z , right? For example, Zmod takes two Z and returns Z Can I improve this method with subset types without overriding it?

I want it:

 Definition Z_gt0 := {z | z > 0}. Definition mymod (n1 n2 : Z_gt0) := Zmod n1 n2. 

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

This question is related to my other here: Random stream types and subsets in Coq

Edit : proj1_sig can do the trick thanks to the IRC Coq channel!

Answer 1

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

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

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

In the latest version of Coq, there is another way to do this using let (because sig is inductive with only one constructor):

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