# [Agda] congruence, Preserves_2

Serge D. Mechveliani mechvel at botik.ru
Mon Sep 10 12:13:23 CEST 2012

On Mon, Sep 10, 2012 at 10:21:40AM +0200, Andreas Abel wrote:
>
>
> On 08.09.12 8:38 PM, Serge D. Mechveliani wrote:
[..]
>>   proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
>>   proo m n p =  ?
>>
>> (for this letter I replace
>>       \bn -> Nat,  _\equiv_ -> ==,  _\~~_ -> ~~,  \. -> op,  \_2 -> _2,
>> ).
[..]
>>   proo m n p =  cong (_+_ m) p
[..]
>> II. In a general situation, one probably needs to apply  op-cong  from
>>      Semigroup. I tried this approach for Nat.
>> [..]
>> proo m n p =  +cong <what to set here ?>
>>    where
>>    isCSemir  = NatProp.isCommutativeSemiring
>>    [..]
>>    +cong : _+_ Preserves_2 == -> == -> ==        -- what must be here?
>>    +cong = IsCommutativeMonoid.op-cong +isComMon
[..]
>> "Could not parse the application _+_ Preserves_2 ==
>>   when scope checking _+_ Preserves_2 ==

> I think you could start trying _==_ instead of ==.

As a wrote above,   ==  stands for  _\equiv_

for this letter, and probably you mean the same.

Improvement for this report:
it is better to put          \equiv -> ==,
and, respectively:

proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
proo 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

"Could not parse the application _+_ Preserves_2 _==_
when scope checking _+_ Preserves_2 _==_

a) What is the type of this  +cong ?
b) For the value    +cong = IsCommutativeMonoid.op-cong  +isComMon'',
can Agda itself show the type of  +cong  ?
c) What to set in the RHS of   proo m n p =  ...   ?

Thanks,

------
Sergei