[Agda] congruence, Preserves_2

[Andreas Abel]

On 08.09.12 8:38 PM, Serge D. Mechveliani wrote:
> 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 ==

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

> "
> 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,


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/