时间戳

首页 > 解决方案 > 在 Agda 中证明当且仅当的错误情况

agda - 在 Agda 中证明当且仅当的错误情况

问题描述

我试图了解如何在 agda 中创建一个有效的“当且仅当”语句，但在证明它的错误案例以及在证明中使用归纳时遇到问题。例如，我想使用“小于或等于”，我将其定义为：

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data _leq_ : ℕ → ℕ → Set where
  0≤n : ∀ {n : ℕ} → zero leq n
  Sn≤Sm : ∀ {n m : ℕ} → (n leq m) → ((succ n) leq (succ m))

要定义 A 当且仅当 B，我们需要一对函数将 A 的证明与 B 的证明相结合，反之亦然，所以我定义：

record _∧_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _∧_

_iff_ : (A B : Set) → Set
A iff B = (A → B) ∧ (B → A)

现在到我的问题：我想证明(n <= m+1) <=> (n+1 <= m+2)这样制定以下陈述：

prop₂ : ∀ (n m : ℕ) → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop₂ zero zero = (λ x → Sn≤Sm 0≤n) , λ x → 0≤n
prop₂ zero (succ b) = (λ x → Sn≤Sm 0≤n) , (λ x → 0≤n)
prop₂ (succ a) zero = ?
prop₂ (succ a) (succ b) = ?

我的问题是

标签： agdatheorem-proving

解决方案

如果我坚持你的发展，证明如下：

prop₂ : ∀ (n m : ℕ) → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop₂ zero zero = (λ x → Sn≤Sm 0≤n) , λ x → 0≤n
prop₂ zero (succ b) = (λ x → Sn≤Sm 0≤n) , (λ x → 0≤n)
prop₂ (succ a) zero = Sn≤Sm , λ {(Sn≤Sm x) → x}
prop₂ (succ a) (succ b) = Sn≤Sm , λ {(Sn≤Sm x) → x}

但是，有一种更好的方法来证明这种性质。如您所见，代码中存在冗余，因为您对参数进行大小写拆分a，而b不是对包含您需要的所有信息的证明元素进行大小写拆分。这导致了以下证明，它更加优雅和简洁：

prop-better : ∀ {n m : ℕ} → (n leq (succ m)) iff ((succ n) leq (succ (succ m))) 
prop-better = Sn≤Sm , λ {(Sn≤Sm x) → x}

等价的第一个方向只是Sn≤Sm定义上的构造函数，而另一面是通过对证明参数进行大小写拆分来完成的，这必然是形式，Sn≤Sm x因为两个自然数是形式succ y。这为您提供了x正是您所需要的证明。

推荐阅读