时间戳

首页 > 解决方案 > 我如何在 Coq 中为 sigma 类型做例子？

coq - 我如何在 Coq 中为 sigma 类型做例子？

问题描述

对于该类型：

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).

它失败了：

术语“exist ?P 5”的类型为“?P 5 -> {x : nat | ?P x}”，而预期的类型为“{b : nat | b > 0 /\ b <= 9}” .

我错过了什么？

标签： coq

解决方案

它失败的原因是您不仅需要提供证人（在这种情况下），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.

推荐阅读