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

Question

我要证明

{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？

Answer 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)

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

Prove m ≤ n -> k ≤ l -> m + k ≤ n + l in Agda

theorem-proving

agda