プルーフチェッカーcoqでドメインを定義しようとしています。どうすればよいですか?
私はと同等のことをしようとしていますV in [0,10]
。
私はやろうとしましたが、これはCoqに従っていないDefinition V := forall v in R, 0 <= v /\ v <= 10.
などの定数の問題につながります。0
V
プルーフチェッカーcoqでドメインを定義しようとしています。どうすればよいですか?
私はと同等のことをしようとしていますV in [0,10]
。
私はやろうとしましたが、これはCoqに従っていないDefinition V := forall v in R, 0 <= v /\ v <= 10.
などの定数の問題につながります。0
V
簡単なアプローチは次のようになります。
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.
これを行う自然な方法は、Yves もコメントで言及している sig 型を使用することだと思います。
V の要素は R からの数 x であり、それらが実際に集合 V にあるべきであることを示す証明b を伴います。
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.