# [Agda] monot-minus for Nat

Serge D. Mechveliani mechvel at botik.ru
Sat Sep 15 18:13:36 CEST 2012

People,
I have a couple of beginner questions about usage of Standard Library
(in Agda-2.3.0.1, lib-0.6).
I need Agda proofs for
(m : Nat) -> (n : Nat) -> m + (suc n) == (suc m) + n,
(k m n : Nat) -> k <= m ->  k .- n <= m .- n

-- with using Standard Library as possible.
For this letter I apply the following denotations:

\bn -> Nat,    \equiv -> ==,   \<=  ->  <=,    \.-  ->  .-
(for writing math symbols under the mutt e-mail program)
,
Relation.Binary.PropositionalEquality as PropEq,
<=trans = let open DecTotalOrder hiding ( _<=_ )
in  IsDecTotalOrder.trans $isDecTotalOrder Nat.decTotalOrder +comm = IsCommutativeMonoid.comm +isComMon where natIsCommSemir = NatProp.isCommutativeSemiring +isComMon = IsCommutativeSemiring.+-isCommutativeMonoid natIsCommSemir I program: ------------------------------------------------------------------------ suc-comm : (m : Nat) -> (n : Nat) -> m + (suc n) == (suc m) + n suc-comm m n = PropEq.trans (PropEq.trans p1 p2) refl where p1 = +comm m (suc n) -- : m + (suc n) == suc (n + m) p2 = cong suc$ +comm n m  -- : suc (n + m) == suc (m + n)

monot.-right : (k m n : Nat) -> k <= m -> k .- n <= m .- n

-- below  "_'"  denotes  suc_
monot.-right 0       m       n       _      = <=trans (n.-m<=n n 0) z<=n
monot.-right _       _       0       k<=m   = k<=m
monot.-right (suc k) (suc m) (suc n) k'<=m' = monot.-right k m n k<=m
-- k'<=m' : suc k <= suc m
where
k<=m = cancel-+-left-<= 1 k'<=m'

monot.-right (suc k) 0       (suc n) k'<=0  =
-- unaccessibe, due to  k' <= 0

<=trans  k'.-n'<=0  z<=n
where
k'.-n'<=k' =  n.-m<=n (suc n) (suc k)
k'.-n'<=0  =  <=trans  k'.-n'<=k'  k'<=0
------------------------------------------------------------------------

(1) Is there possible a simpler expression for  suc-comm, monot.-right ?

(2) The last pattern for  monot.-right  is not accessible, because
suc k <= m  = 0   is not satisfiable.
How to skip this pattern? or at least -- how to reduce its RHS
(for example by setting () in an appropriate place) ?

Thank you in advance for explanation,

------
Sergei

More information about the Agda mailing list