1

如果这显然是在某个地方发布的，我深表歉意，但我一直在尝试谷歌搜索和 SO 搜索，但对此一无所获。

A部分。

是否有用于在 Coq 中定义 R^2 和 R^3 中的坐标/向量和点的标准库？我非常想做标准的东西，比如添加向量、叉积、缩放等。

如果没有，这是如何开始的：

Require Import Coq.Reals.Reals.

Inductive Coordinate2 : Type := Point2: R -> R -> Coordinate2.

Definition R2plus (u:Coordinate2) (v:Coordinate2) : Coordinate2 :=
match u, v with
 | (Point2 ux uy),(Point2 vx vy)=>(Point2 ((ux+vx)%R) ((uy+vy)%R))
end.  

(* etc. *)

Notation "x + y" := (R2plus x y).

另外，为什么当我运行时：

Eval compute in ((2%R) < (3%R))%R.

我得到

= (2 < 3)%R
: Prop

而不是

 True

或者其他的东西？

B 部分。

这甚至是个好主意吗？我想构建一个使用实数计算一些东西的算法，并在 Coq 中证明该算法是正确的。Coq.Reals.Reals 是正确的使用方法，还是它真的太抽象了？

4

1 回答 1

2

除了定义Coordinate2，您还可以使用(R * R)%type,list R或t R 2, where t A n, defined inVector是 size 的列表n。

您可能希望为您的符号提供范围和定界键以避免与其他符号发生冲突。

Notation "x + y" := (R2plus x y) : r2_scope.
Delimit Scope r2_scope with R2.
Eval compute in ((Point2 0 1) + (Point2 2 3))%R2.

Prop, Set, 和是排序，这意味着可以归纳定义Type某种类型。Prop

例如，对于nats，le定义为

Inductive le : nat -> nat -> Prop :=
  | le_n : forall n, le n n
  | le_S : forall n m : nat, le n m -> le n (S m).
  • 2 <= 2是真的，因为它居住着le_n 2
  • 2 <= 3是真的，因为它居住着le_S 2 2 (le_n 2)
  • 2 <= 4是真的，因为它居住着le_S 2 3 (le_S 2 2 (le_n 2))
  • 3 <= 2是假的，因为它没有人居住

为了2 <= 3减少到True，le必须定义为，例如，

Fixpoint le (n m : nat) : Prop :=
  match n with
  | 0 => True
  | S n =>
    match m with
    | 0 => False
    | S m => le n m
    end
  end.

Coq 对Rplus和的定义Rlt实际上是公理。要检查某些东西的定义，请使用该Print命令。

要回答 B 部分，我想这取决于您对数学分析的理解程度以及定义实数的各种方法。如果您更熟悉数值方法，则可能希望使用有理数。

于 2013-11-06T14:12:52.303 回答