coq - 如何在coq中定义一个有限域

Question

我正在尝试在证明检查器 coq 中定义一个域。我该怎么做呢？

我正在尝试做相当于 V in [0,10] .

我试过做Definition V := forall v in R, 0 <= v /\ v <= 10. , 但这会导致像 0 这样的常量出现问题不在V根据 Coq。

Answer 1

一个简单的方法可能是这样的，

Require Import Omega.

Inductive V : Set :=
  mkV : forall (v:nat), 0 <= v /\ v <= 10 -> V.

Lemma member0 : V.
Proof. apply (mkV 0). omega. Qed.

Definition inc (v:V) : nat := match v with mkV n _ => n + 1 end.

Lemma inc_bounds : forall v, 0 <= inc v <= 11.
Proof. intros v; destruct v; simpl. omega. Qed.

当然是 member0 的类型可能不像您希望的那样提供信息。在这种情况下，您可能需要索引 V由 nat对应集合中的每个元素。

Require Import Omega.

Inductive V : nat -> Set :=
  mkV : forall (v:nat), 0 <= v /\ v <= 10 -> V v.

Lemma member0 : V 0.
Proof. apply (mkV 0). omega. Qed.

Definition inc {n} (v:V n) : nat := n + 1.

Lemma inc_bounds : forall {n:nat} (v:V n), 0 <= inc v <= 11.
Proof. intros n v. unfold inc. destruct v. omega. Qed.

我没有和 Reals 合作过之前，但以上可以在 R 上实现也是。

Require Import Reals.
Require Import Fourier.
Open Scope R_scope.

Inductive V : R -> Set :=
  mkV : forall (v:R), 0 <= v /\ v <= 10 -> V v.

Lemma member0 : V 0.
Proof. apply (mkV 0). split. right; auto. left; fourier. Qed.

Definition inc {r} (v:V r) : R := r + 1.

Lemma inc_bounds : forall {r:R} (v:V r), 0 <= inc v <= 11.
Proof. intros r v; unfold inc. 
  destruct v as (r,pf). destruct pf. split; fourier. 
Qed.