在 Agda 中证明 m ≤ n -> k ≤ l -> m + k ≤ n + l答案

【问题标题】：Prove m ≤ n -> k ≤ l -> m + k ≤ n + l in Agda在 Agda 中证明 m ≤ n -> k ≤ l -> m + k ≤ n + l
【发布时间】：2015-07-28 01:08:56
【问题描述】：

我要证明

{m n k l : ℕ} -> m ≤ n -> k ≤ l -> m + k ≤ n + l

在阿格达。我可以通过以下代码证明m + k ≤ m + l

add≤ : {m n : ℕ} -> (k : ℕ) -> m ≤ n -> k + m ≤ k + n
add≤ zero exp = exp
add≤ (suc k) exp = s≤s (add≤ k exp)

既然我可以证明m + k ≤ m + l，我想证明m + l ≤ n + l。如果可以，我将使用我已经定义的≤-trans : Transitive _≤_。

我可以用m ≤ n, k ≤ l 证明m + l ≤ n + l 吗？或者，我是否必须更改计划以使用≤-trans？

【问题讨论】：

标签： agda theorem-proving

【解决方案1】：

很简单

open import Data.Nat
open import Data.Nat.Properties

le : {m n k l : ℕ} -> m ≤ n -> k ≤ l -> m + k ≤ n + l
le {n = n}  z≤n    q = ≤-steps n q
le         (s≤s p) q = s≤s (le p q)

【讨论】：

我能理解你的回答！谢谢！
对于任何想知道的人来说：它之所以有效，是因为_+_ 是由其第一个参数的归纳定义的，m ≤ n 证明上的模式匹配揭示了m 的头构造函数（和n 在第二种情况）因此允许m + k 和n + l 进行计算。