[Agda] strange `case' requirement
mechvel at botik.ru
Sat Oct 26 21:09:18 CEST 2013
On Sat, 2013-10-26 at 12:22 -0400, Wolfram Kahl wrote:
> On Sat, Oct 26, 2013 at 01:48:55PM +0400, Sergei Meshveliani wrote:
> > People,
> > I write
> > _∙u_ : Op₂ uC
> > (just x) ∙u (just y) = just (x ∙ y)
> > m ∙u nothing = m
> > nothing ∙u m = m
> > for uC = Maybe C, and a semigroup operation _∙u_ : Op₂ C
> > (this is extending a semigroup with unity represented as `nothing').
> > Then I prove
> > goal : (m : uC) → (nothing ∙u m) =u m
> > goal m = IsEquivalence.refl uEquiv
> > where
> > uSetoid = Data.Maybe.setoid setoid
> > uEquiv = Setoid.isEquivalence uSetoid
> > The report is
> > "
> > nothing ∙u .m != .m of type Maybe (Setoid.Carrier ......)
> > when checking that the expression uRefl has type
> > nothing ∙u .m =u .m
> > ".
> > [..]
> > 1) Why is not the first version type-checked by normalization?
> Because the matching case here is the third case
> of your definition of _∙u_, which is only reached
> after matching the first two cases fails --- just like in Haskell.
But let us change the goal to goal : (m : uC) → (m ∙u nothing) =u m
with remaining the implementation.
Normalization is as follows:
(m ∙u nothing) does not match the first rule of _∙u_
(uniformly for all values of m),
and matches the second rule (uniformly for all values of m).
The normalization result is m.
So uRefl proves m =u m, and proves the goal.
But the report is similar, and negative. Why?
More information about the Agda