# [Agda] congruence, Preserves_2

Serge D. Mechveliani mechvel at botik.ru
Sat Sep 8 20:38:26 CEST 2012

People,
I have several beginner questions on the  \.-cong  field  in
Standard library  (Agda-2.3.0.1 + lib-0.6).

For  m n : Nat,  p : n == 1,  build a proof for  (m + n) == (m + 1).

p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
p m n p =  ?

(for this letter I replace
\bn -> Nat,  _\equiv_ -> ==,  _\~~_ -> ~~,  \. -> op,  \_2 -> _2,
).

I.  The first successful expression I found was

p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
p m n p =  cong (_+_ m) p

But initially I tried the following.

II. In a general situation, one probably needs to apply  op-cong  from
Semigroup. I tried this approach for Nat.
IsCommutativeMonoid  has a field
op-cong : op Preserves_2 ~~ -> ~~ -> ~~
And I write
-------------------------------------------------
open import Data.Nat as Nat
open import Data.Nat.Properties as NatProp
...
p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
p m n p =  +cong <what to set here ?>
where
isCSemir  = NatProp.isCommutativeSemiring
+isComMon = IsCommutativeSemiring.+-isCommutativeMonoid isCSemir
+comm = IsCommutativeMonoid.comm  +isComMon  -- Commutative == _+_

+cong : _+_ Preserves_2 == -> == -> ==        -- what must be here?
+cong = IsCommutativeMonoid.op-cong +isComMon
-------------------------------------------------

because I think that it is needed the instance of
op Preserves_2 ~~ -> ~~ -> ~~
for  op -> Nat._+_,  ~~ -> ==.

The compiler reports
"Could not parse the application _+_ Preserves_2 ==
when scope checking _+_ Preserves_2 ==
"
a) Please, how to fix this?
b) What is the type of this  +cong ?
c) For the value    +cong = IsCommutativeMonoid.op-cong  +isComMon'',
can Agda itself show the type of  +cong  ?
(such an info often occurs helpful).

d) What to set in the RHS of   p m n p =  ...   ?

Thank you in advance for explanation,

------
Sergei


More information about the Agda mailing list