[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