如何在coq中定義一個有限的域

Question

我想在證明檢查器coq中定義一個域。我該怎麼做呢？

我正在嘗試做相當於V in [0,10]。

我試過做Definition V := forall v in R, 0 <= v /\ v <= 10.，但這會導致常見問題，如0根據Coq不在V。

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. 

Answer 2

我相信這樣做的自然方法是使用sig類型，這也是伊夫斯在評論中提到的。

的V元素將來自R數x，連同其showsb他們真的應該在集五

Require Import Reals Fourier. 
Open Scope R_scope. 

Definition V_prop (x : R) : Prop := 0 <= x /\ x <= 10. 

Definition V : Set := { x : R | V_prop x }. 

Lemma V_prop0: V_prop 0. 
Proof. 
    unfold V_prop; split; 
    [right; auto | left; fourier]. 
Qed. 

Definition V0 : V := exist _ 0 V_prop0.