[Agda] strange mismatch

[MONTIN Mathieu]

Hello Sergei,

Le mercredi 24 mai 2017 à 22:13 +0300, Sergei Meshveliani a écrit :
> Please, what is wrong here?

You are trying to prove something that does not hold.

> test1  is type-checked, and  test2  is not
> (in Agda 2.6.0-207bde6) :

It does not type check because PE.refl has type (x ≡ x) for any x and 
you need to provide an element of type (con zr ≡ con a) while a is not 
necessarily equal to zr.

The way you wrote the function f does not match the expected behaviour. 
Here is, case by case, the actual behaviour of your function :

   f′ : Expression → Expression → Expression
   f′ (con x     ) y         = y
   f′ (zr₁ :+ zr₂) (con x  ) = zr₁ :+ zr₂
   f′ (zr₁ :+ zr₂) (y :+ y₁) = (zr₁ :+ zr₂) :+ (y :+ y₁)

Here is the proof that both functions have the same behaviour :

   f≡f′ : ∀ {x y} → f x y ≡ f′ x y
   f≡f′ {con x  }           = PE.refl
   f≡f′ {x :+ x₁} {con x₂ } = PE.refl
   f≡f′ {x :+ x₁} {y :+ y₁} = PE.refl

In your second test, f (con a) (con zr) reduces to (con zr) because you 
case split on the first argument of f in your definition before case 
splitting on the second.

If f had been defined this way :

   f : Expression → Expression → Expression
   f x        (con zr) =  x
   f (con zr) y        =  y
   f x        y        =  x :+ y

Then test1 would not typecheck while test2 would.

Hope it helped,

MM.

> -------------------------------------------------------------------
> ----
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
>
> module _ {α} (A : Set α) (zr a : A)
>   where
>   data Expression : Set α where
>                           con  : A → Expression
>                           _:+_ : Expression → Expression → Expression
>
>   f : Expression → Expression → Expression
>   f (con zr) y        =  y
>   f x        (con zr) =  x
>   f x        y        =  x :+ y
>
>   test1 :  f (con zr) (con a) ≡ con a
>   test1 =  PE.refl
>
>   test2 :  f (con a) (con zr) ≡ con a
>   test2 =  PE.refl
> -------------------------------------------------------------------
> -----
>
> How to fix?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda