时间戳

首页 > 解决方案 > Coq：有什么方法可以避免对 sort Set 进行案例分析？

coq - Coq：有什么方法可以避免对 sort Set 进行案例分析？

问题描述

我试图通过使用有理数的柯西序列来构造实数。

(* Some Definitions:
   <Q, >Q, <=Q, >=Q: the order in rational
   Q0: the zero as a rational number
   -Q: the subtractions b/w rationals
   Q_abs: the abs value of a rational *)

Definition Cauchy (a: nat -> rational): Prop :=
forall (epsilon: rational), epsilon >Q Q0 ->
  exists (N: nat), forall (n m: nat), n > N -> m > N -> Q_abs (a n -Q a m) <Q epsilon.

Definition real: Set := {r: nat -> rational | Cauchy r}.

Definition R_ne_0 (a: nat -> rational): Prop :=
  exists epsilon: rational, (
    epsilon >Q Q0 /\
    forall N: nat, exists n: nat, (n > N /\ Q_abs (a n) >=Q epsilon)
  ).

Definition R_nonzero: Set := {a : real | R_ne_0 (proj1_sig a)}.

但是，我不能destruct存在陈述，R_ne_0因为它需要对以下情况进行案例分析Set：

Definition R_recip (a: R_nonzero): R_nonzero. (* r |-> 1/r *)
  destruct a as [[a c] n].
  unfold R_ne_0 in n. 
  destruct n.   (* !!!ERROR!!! *)

有没有办法使用R_nonzero（在建设性数学中）的适当定义来定义这样的倒数？或者，有什么方法可以避免（或忽略）通常数学中的这种错误？

我知道在 mathcomp 中，实数被构造为阿基米德场，我想知道是否有可能的方法来定义柯西序列。

标签： coq

解决方案

推荐阅读