如何“提取”来自子集类型{z：Z | & 0} [英] How to "extract" Z from subset type {z : Z | z > 0}

问题描述

如果函数使用 Z 作为参数，那么也应该可以使用 Z 的任何子集，对？例如， Zmod 取两个 Z 并返回 Z 。我可以在不重新实现子集类型的情况下改进此方法吗？

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?

我想要这样做：

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

Definition mymod (n1 n2 : Z_gt0) :=
  Zmod n1 n2.

但是Coq抱怨 n1的类型应该是Z ，当然。如何使其与 Z_gt0 一起使用？强制吗？

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

这个问题与我的另一个问题有关： Coq中的随机nat流和子集类型

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

编辑： proj1_sig 可能可以解决问题，谢谢Coq IRC频道！

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

推荐答案

proj1_sig 是常用的方法。另一种解决方案是模式匹配：

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

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

z 是您的投影， hz 将证明 z> 0 。我通常将第一个参数保留为匿名，因为我知道 z：Z 。

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.

我是最新版的Coq，另一种方法是使用 let （因为 sig 是仅具有一个构造函数的归纳法）：

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.

这篇关于如何“提取”来自子集类型{z：Z | & 0}的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！