如何在Coq中以sigma类型为例？

Question

对于该类型：

Record Version := mkVersion { 
  major  : nat; 
  minor  : nat; 
  branch : {b:nat| b > 0 /\ b <= 9};
  hotfix : {h:nat| h > 0 /\ h < 8} 
}.

我正在尝试举一个例子：

Example ex1 := mkVersion 3 2 (exist _ 5) (exist _ 5).

它失败了：

术语“存在？P 5”的类型为“？P 5-> {x：nat |？P x}”，而术语为“ {b：nat | b> 0 / \ b <= 9}”。 。

我想念什么？

Answer 1

失败的原因是，不仅需要提供证人（b和h在这种情况下），而且也使相应的条件成立的提供证人证明。

我将改用布尔值来简化生活，因为这允许通过计算进行证明，这基本上是eq_refl下面的代码片段所做的事情：

From Coq Require Import Bool Arith.

Coercion is_true : bool >-> Sortclass.

Record Version := mkVersion {
  major  : nat;
  minor  : nat;
  branch : {b:nat| (0 <? b) && (b <=? 9)};
  hotfix : {h:nat| (0 <? h) && (h <? 8)}
}.

Example ex1 := mkVersion 3 2 (exist _ 5 eq_refl) (exist _ 5 eq_refl).

我们可以引入一种表示法，以更好地表示文字：

Notation "<| M ',' m ',' b '~' h |>" :=
  (mkVersion M m (exist _ b eq_refl) (exist _ h eq_refl)).

Example ex2 := <| 3,2,5~5 |>.

如果需要添加手动证明，那么我建议使用Program机制：

From Coq Require Import Program.

Program Definition ex3 b h (condb : b =? 5) (condh : h =? 1) :=
  mkVersion 3 2 (exist _ b _) (exist _ h _).
Next Obligation.
  now unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst. Qed.
Next Obligation.
  now unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst. Qed.

或refine战术：

Definition ex3' b h (condb : b =? 5) (condh : h =? 1) : Version.
Proof.
  now refine (mkVersion 3 2 (exist _ b _) (exist _ h _));
  unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst.
Qed.