证明if且仅当在Agda中时为假情况

Question

我试图理解如何在agda中创建一个有效的“ if and only if”语句，但是在证明虚假情况以及在证明中使用归纳法时遇到问题。例如，我想使用“小于或等于”，它定义为：

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) = ?

我的问题是

• 证明的第三行，我需要给一个从空集到空集的函数，但不知道如何表达它

• 在最后一行中，我希望使用归纳法，即prop2 (succ a) (succ b) = prop2 a b，但是agda不接受这种类型正确的输入吗？

Answer 1

如果我坚持您的开发，请按照以下步骤进行证明：

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正是您所需要的。