如何证明在 agda 中存在一个小于某个有理数的有理数？

Question

我想证明存在一个小于某个有理数的有理数。例如..

v : ℚ
v = + 1 ÷ 2

thm : (Σ[ x ∈ ℚ ] (x Data.Rational.≤ v))
thm = ?

第二行写什么？？

还有x∈ℚ是什么意思，会给出ℚ的元素还是什么。

它在哪里定义在 Set 之上，因为我在 Stream 中找到了它，它在流上定义了它。

Answer 1

您只需要遵循定义即可。

首先我们来看看Σ[ x ∈ ℚ ] x ≤ v的Σ部分是什么。此数据类型在模块 Data.Product 中简单定义为 Σ。 ∈ 的全部内容只是一个 语法糖 ，从以下行可以看出：

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

所以我们真正需要构造的是Σ ℚ λ x → x ≤ v类型的东西。看一下 Σ:

的定义

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

这是一对，使用 _,_ 构建。第一个元素是数字（witness），第二个元素是第一个元素满足给定命题的证明（≤）。所以，thm 应该是这样的：

thm = ? , ?

我们已经知道第一个元素是一个数字（或者更准确地说，是 ℚ 类型的东西）。所以在这里我们选择一个合适的数字 - 我选择了 + 1 ÷ 3，希望它应该小于 + 1 ÷ 2.

thm = + 1 ÷ 3 , ?

这给我们留下了第二个问号。在那里，我们需要 + 1 ÷ 3 ≤ v 类型的东西。同样，我们来看看 ≤:

的定义

data _≤_ : ℚ → ℚ → Set where
  *≤* : ∀ {p q} →
        ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
        ℚ.numerator q ℤ.* ℚ.denominator p →
        p ≤ q

好的，这很简单：唯一的构造函数是 *≤* 所以我们不可能选错：

thm = + 1 ÷ 3 , *≤* ?

? 现在有这种类型：+ 2 ≤ + 3（其中 ≤ 来自 Data.Integer）。同样，让我们看一下 ≤:

的定义

data _≤_ : ℤ → ℤ → Set where
  -≤+ : ∀ {m n} → -[1+ m ] ≤ + n
  -≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ]
  +≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n

这变得更有趣了，因为存在三个可能的构造函数。不过仔细一看，唯一相关的只有+≤+，因为两边的数都是正数

thm = + 1 ÷ 3 , *≤* (+≤+ ?)

唯一剩下的就是写一个2 ≤ 3类型的术语（Data.Nat中的≤）。我将把它留作 reader.

的练习

如果构造函数的选择没有歧义，您可以使用 Agda 的 Emacs 模式为您完成大部分工作 - 您只需按住 C-c C-R（精炼），Agda 就会为您编写证明项。

我不喜欢写那样愚蠢的证明术语，计算机应该能够为我写出 x ≤ v 的证明——毕竟，≤ 是 可判定.

Decidable在标准库中定义：

Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

因此，如果您可以编写一个二元函数（我们称参数为 x 和 y），则二元关系 ~ 是可判定的，即 returns 或者x ~ y 的证明或 x ~ y 的反驳（即 x ~ y → ⊥）。

对我们来说幸运的是，≤ 的可判定性证明在标准库中可用，并且可以在名称 ≤? 下找到 - 我只需要编写相当简单的机制来提取那里的证据（如果存在）：

open import Relation.Nullary

FromDec : ∀ {A : Set} → Dec A → Set
FromDec {A = A} (yes p) = A
FromDec         (no ¬p) = ⊤

fromDec : ∀ {A : Set} (d : Dec A) → FromDec d
fromDec (yes p) = p
fromDec (no ¬p) = _

fromDec 从 Dec A 中提取证明；如果不存在证明（即对于某些 ¬p 的参数是 no ¬p），它只是 returns 空元组。

现在我们可以让计算机判断 + 1 ÷ 3 ≤ v 是否成立。如果是这样 - 太好了，我们只需使用 fromDec 提取计算出的证明就可以了；如果没有，fromDec returns 空元组，我们会得到一个类型错误。

thm : Σ[ x ∈ ℚ ] x ≤ v
thm = , fromDec (+ 1 ÷ 3 ≤? v)

如何证明在 agda 中存在一个小于某个有理数的有理数？

How to prove there exist a rational which is less than some rational in agda?

agda