Докажите, что m ≤ n - ›k ≤ l -› m + k ≤ n + l в Agda.

Я хочу доказать

{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 + l ≤ n + l с m ≤ n, k ≤ l? Или мне нужно изменить план, чтобы использовать ≤-trans?


theorem-proving agda
person mmsss    schedule 28.07.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это просто

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)
person user3237465    schedule 28.07.2015
comment
Я понял твой ответ! Спасибо! - person mmsss; 28.07.2015
comment
Для всех, кто задается вопросом: это работает, потому что _+_ определяется индукцией по его первому аргументу, а сопоставление с образцом в доказательстве m ≤ n показывает конструктор головы m (и n во втором случае), что позволяет m + k и n + l вычислить. - person gallais; 28.07.2015